Empirical Impact of Dimensionality on Random Geometric SAT

Abstract

The Boolean Satisfiability Problem is perhaps one of the most well-known problems in theoretical computer science. On the one hand, it is proven to be NP-complete, which means that it is generally considered hard to solve. On the other hand, the SAT problem has found many practical applications, which yield so-called industrial instances, and SAT solvers can often efficiently find solutions to such instances. Closing this gap between theory and practice is a subject of current research. One approach is to identify properties of SAT instances that make them tractable. To aid in this, models for generating SAT instances have been proposed that mimic the properties of industrial instances. So far, attempts at creating such models were mostly unsuccessful, with instances being either too easy or too hard to solve, or missing important properties of industrial SAT instances. In this work, we analyse a promising SAT model introduced by Giráldez-Cru and Levy which is based on an underlying geometry. We empirically analyse the impact of this geometry's dimension on SAT instances with regard to three properties: the location of the satisfiability threshold, solver time, and size of proofs of unsatisfiability. Supplementing theoretical work, we find that low-dimensional geometric instances are throughout very tractable. As dimension increases, instances from the geometric model seem to converge to hard uniform instances, which means that the geometric model is capable of representing the full range of easy to hard instances. We also observe that the satisfiability threshold in low-dimensional geometric instances occurs at lower densities. Additionally, low-dimensional instances behave very unlike uniform instances in that they have no hardness peaks in solver time at the satisfiability threshold. This coincides with proof size, which we show to not correlate to solver time at low dimensions.