Motivation

SAT is the archetypal NP-complete problem and is used as a starting point for hardness reductions in theory, but in practice heuristic SAT solving algorithms can solve large-scale industrial SAT instances very efficiently. One possible explanation for this disparity is that industrial SAT instances have particular properties that make them more easily solvable. One approach to understanding this difference between theory and practice is to study random SAT models whose generated instances share structural properties with real-world SAT instances. This approach has been successfully applied in network problems, where geometric random graph models have been shown to share many properties with real-world networks, be it structural or algorithmic. Two industrial SAT instances (left and middle) and a geometric SAT instance (right). In a recent paper [2] we studied how two properties of random SAT instances affect their tractability. More importantly we showed that when SAT instances are generated with a particular underlying geometry, they can be easily refuted, while this is not the case when the geometry is removed. While in the non-geometric mode each variable is added to each clause independently according to its weight, the geometric model affects the correlation between its clauses as follows. Variables and clauses are dropped uniformly at random as points in a compact space, and then each clause connects to its k closest variables. This way clauses that are geometrically close are likely to contain the same variables. While this is significant progress in explaining the tractability of SAT instances, it does not provide us with a complete answer. The reason is that this geometric random SAT model generates instances that are "too easy" compared to the real-world ones. That is, generated SAT formulae have constant-size unsatisfiable subformulae, while real-world instances have logarithmic-size ones.