Theoretical explanations for practical success of SAT solvers?

Question

What theoretical explanations are there for the practical success of SAT solvers, and can someone give a "wikipedia-style" overview and explanation tying them all together?

By analogy, the smoothed analysis (arXiv version))for the simplex algorithm does a great job explaining why it works so well in practice, despite the fact that it takes exponential time in the worst case and is NP-mighty (arXiv version).

I have heard a little bit about things like backdoors, structure of the clause graph, and phase transitions, but (1) I don't see how these all fit together to give the larger picture (if they do), and (2) I don't know whether these really explain why SAT solvers work so well, for example, on industrial instances. Also, when it comes to things like structure of the clause graph: why is it that current solvers are able to take advantage of certain clause graph structures?

I only find the results about phase transitions partially satisfying in this regard, at least in my currently limited understanding. The phase transition literature is about instances of random k-SAT, but does that really explain anything about real-world instances? I don't expect real-world instances of SAT to look like random instances; should I? Is there a reason to think phase transitions tell us something, even intuitively, about real-world instances even if they don't look like random instances?

Related questions that help, but don't completely answer my question, particularly the request for tying things together into a coherent picture:

• Why is there an enormous difference between SAT solvers?

• Which SAT problems are easy?

• What's the correlation between treewidth and instance hardness from random 3SAT?

Answer 1

I am assuming that you are referring to CDCL SAT solvers on benchmark data sets like those used in the SAT Competition. These programs are based on many heuristics and lots of optimization. There were some very good introductions to how they work at Theoretical Foundations of Applied SAT Solving workshop at Banff in 2014 (videos).

These algorithms are based on DPLL backtracking algorithm which tries to find a satisfying assignment by setting values to variables and backtracks when it finds a conflict. People have looked at how much impact these heuristics have. E.g. see

• Hadi Katebi, Karem A. Sakallah, and Joao P. Marques-Silva, "Empirical Study of the Anatomy of Modern Sat Solvers", 2011

It seems that the efficiency of these SAT solvers on the benchmarks comes mainly from two two heuristics (and their variants):

1. VSIDS heuristic fir selecting which variable to branch on next.
2. CDCL: conflict-driven clause learning heuristic which learns a new clause from a conflict.

It is well-known that DPLL proofs correspond to proofs in resolution. Without CDCL the only resolution proofs we can get are tree resolution proofs which are much weaker than general resolution proofs.

There are results that show with CDCL we can get any general resolution proof. However there are caveats, they need many artificial restarts, artificial branching, and/or particular preprocessing, so it is not clear how close these are to what these programs do in practice. See e.g. the following paper for more details:

• Paul Beame and Ashish Sabharwal, "Non-Restarting SAT Solvers With Simple Preprocessing Can Efficiently Simulate Resolution", 2014

---

CDCL is essentially cutting branches from search space. There are various ways of deriving a new learnt clause from a conflict. Ideally we would add a set of minimal clauses which implied the conflict, but in practice that can be large and can be expensive to compute. Top SAT solvers often delete learned clauses regularly and that helps in practice.

---

The other heuristic VSIDS essentially maintains a score for each variable. Every time there is a conflict, all scores are adjusted by multiplying them with a value $\alpha$<1 and adding a constant to those which were "involved" in the conflict. To see what this means think about the sequence $F(v,i)$ which is 1 if variable v was "involved" in the $i$th conflict. Let $0<\alpha<1$ be a fixed constant. The score of variable $v$ at time $n$ is then: $$\sum_{i<n} F(v,i)\alpha^{(n-i)}$$

Intuitively one can say that this tries to emphasize variables which were consistently involved in recent conflicts. You can also think of it as a simplistic but extremely cheap way of predicting which variables will be involved in the next conflict. So VSIDS branches first on those variables. One can claim that the algorithm is essentially a fail-fast algorithm, find conflicts fast. Fast is related to smaller number of variables set, which means blocking large subtrees of the search tree. But this is mostly intuition, afaik no one has formalized it very careful to test it on SAT data sets. Running a SAT solver on one of these data sets is not cheap, let alone comparing it with the optimal decisions (smallest extension of the current assignment to variables which would violate one of the clauses). VSIDS also depends on which variables we bump as each conflict, there are various ways to define when a variable is involved in a conflict.

---

There are results that show particular implementation of these ideas correspond to a time-weighted centrality of vertices in dynamic graphs.

There are also suggestions that excluding adversarial instances like those based on NP-hard problems and crypto primitives and random instances (which CDCL SAT solvers are not good at) the rest of instances come from very well structured things like software and hardware verification and somehow these structures are exploited by CDCL SAT solvers (lots of ideas have been mentioned like backdoors, frozen variables, etc.) but afaik they are mostly ideas and do not strong theoretical or experimental evidence to back them up. I think one would have to fist rigorously define the properly and show that the instances on which these algorithms work well have the property and then show that these algorithms exploit those properties. What happens in practice is that people are mostly interested in faster algorithms and if someone comes up with an algorithms that is somehow got inspired by one of these ideas and that algorithms beats other algorithms they go with the claim.

---

Some people keep insisting that the clause ratio and thresholds are the only game in the town. That is definitely false as anyone who is slightly familiar with how industrial SAT solvers work or has any knowledge of proof complexity would know. There are lots of things that make a SAT solver work well or not on an instance in practice and the clause ratio is just one of the things that might be involved. I think the following survey is a good starting point to learn about the connections between proof complexity and SAT solvers and perspective:

• Jakob Nordstrom, "On the Interplay Between Proof Complexity and SAT Solving", 2015

Interestingly even the threshold phenomenon is more complicated than most people think, Moshe Vardi stated in his talk "Phase transitions and computational complexity" that the median running time of GRASP remains exponential for random 3SAT formulas after the threshold but that the exponent decreases (afaik, it is not clear how fast it decreases).

---

Why are we studying SAT solvers (as complexity theorists)? I think the answer is the same as for other algorithms: 1. compare them, 2. find their limitations, 3. design better ones, 4. answer fundamental questions of complexity theory.

When modelling a heuristic we often replace heuristic with nondeterminism. The question then becomes is it a "fair" replacement? And here by fair I mean how close is the model in helping us answer the question above.

When we model a SAT solver as a proof system we are partly showing it limitation because the algorithm will be inefficient for statements which have lower bounds in the proof system. But there still is a gap between what the algorithm actually finds and the optimal proof in the proof system. So we need to show that the reverse as well, i.e. the algorithm can find proofs that are as good as those in the proof system. We are not close to answer that question, but the amount of heuristic that is replace by non-determinism defines how close the model is to the proof system. I don't expect that we completely drop the replacement of heuristics with nondeterminism, otherwise we would get automatizability results which have consequences on open problems in crypto, etc. But the more nondeterminism the model has the less convincing it is in explaining the behaviour of the SAT solver.

So the question when looking at a model becomes: how much does the models help explain why SAT solver A is better than SAT solver B? How helpful are they in developing better SAT solvers? Does SAT solver find proofs in practice that are close to optimal proofs in the model? ... We also need to model the practical instances.

Regarding the intuition that CDCL SAT solvers "exploits the structure of practical instances" (whatever that structure is) is generally accepted intuition I think. The real question is to give a convincing explanation of what that means and demonstrate that it is indeed true.

See also Jakob Nordstrom's own answer for more recent developments.

Answer 2

I am typing this quite quickly due to severe time constraints (and didn't even get to responding earlier for the same reason), but I thought I would try to at least chip in with my two cents.

I think this is a truly great question, and have spent a nontrivial amount of time over the last few years looking into this. (Full disclosure: I have received a big part of my current funding precisely in order to try to find answers to questions of this type, and then potentially to convert deeper insights into SAT into more efficient SAT solvers.)

If one would have to give a one-sentence answer, then I think

nobody really knows and this is an active area of research

is pretty much as good as it gets. Except that that there is a lot more room for more activity, especially from the theory side.

Some proposed explanations (not mutually exclusive), which have already been discussed in other answers and comments, are

• (a) backdoors,
• (b) parameterized complexity considerations,
• (c) graph structure of the CNF problem,
• (d) proof complexity considerations, and
• (e) phase transitions.

Starting from the end (e), there seems to be quite some confusion regarding phase transitions. The short answer here is that there is no reason whatsoever to believe that the ratio of clauses to variables is relevant for applied problems or theoretical combinatorial problems (a.k.a. crafted instances). But for some reason it is a not too uncommon misconception in the applied part of the SAT community that the clauses-to-variables ratio should somehow be a generally relevant measure. The clause-to-variable ratio is very relevant for random k-SAT, but not for other models.

My feeling is that backdoors (a) have been a popular explanation, but I personally have not really seen convincing evidence that it explains what goes on in practice.

Parameterized complexity (b) provides a beautiful theory about some aspects of SAT, and a very attractive hypothesis is that SAT instances are easy because they tend to be "close to some island of tractability." I think this hypothesis opens up many exciting directions of research. As noted in some of the answers, there are a lot of connections between (a) and (b). However, so far I don't really see any evidence that parameterized complexity correlates too much with what is going on in practice. In particular, it seems that instances that are tractable can be very, very hard in practice, and instances without any small backdoors can still be very easy.

The explanation that seems most believable to me for industrial instances is (c), namely that the (graph) structure of the CNF formulas in question should be correlated with practical SAT performance. The idea here is that variable and clauses of industrial instances can be clustered into well-connected communities with few connections between, and that SAT solvers somehow exploit this structure. Unfortunately, it seems quite hard to pin this down more rigourously, and equally unfortunately this area suffers from a fair amount of hype. The proposed explanations I have seen so far in papers are quite unsatisfactory and the models seem to be easy to shoot down. The problem would seem to be that if one really wants to do this thoroughly, then the math gets really hard (because it is a hard problem) and it also gets extremely messy (because you need your model to be close enough to reality to get relevant results). In particular, the papers I have seen explaining that the performance of the VSIDS (variable state independent decaying sum) heuristic for variable choices works well because it explores communities in the graph representation of the instances are quite unconvincing, although the hypothesis as such is still very attractive.

One line of research that I have personally pursued is whether practical SAT performance somehow correlates with proof complexity measures of the CNF formulas in question. Unfortunately, the short answer seems to be that there really is no clear and compelling connection. It might still be that there are nontrivial correlations (this is something that we are currently investigating in different ways), but it seems theory is too nice and clean and pretty and reality is too messy for there to be a really good match. (Regarding the paper Relating Proof Complexity Measures and Practical Hardness of SAT by Järvisalo, Matsliah, Nordström, and Živný in CP '12 it has turned out that more detailed experiments provide a much more complex picture with less clear conclusions --- we hope to get to a full journal version reporting on this any decade now, but it is complicated, though still hopefully interesting.)

Another, related, line of work in proof complexity is to model state-of-the-art SAT solvers as proof systems and prove theorems in these models to deduce properties of the corresponding solvers. This is a bit of a minefield, though, in that small and seemingly innocuous design choices on the theoretical model side can lead to the results being pretty much completely irrelevant from a practical point of view. On the other hand, if one wants a theoretical model that is close enough to reality to give relevant results, then this model gets extremely messy. (This is because SAT solver performance depends on the global history of everything that has happened so far in nontrivial ways, and this means the model cannot be modular in the way we usually set up our proof systems --- whether a particular derivation step is "correct" at a certain point in time cannot be locally verified, but depends on the whole proof so far.)

Two papers that really should be mentioned as exceptions to this, though, are [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte and Thurley 2011], where it is shown that conflict-driven clause learning SAT solvers modelled in a natural way have the potential to polynomially simulate full, general resolution. There are a fairly long list of papers preceding [PD11] and [AFT11] that essentially claim the same result, but they all have serious issues with the modelling. (It is true that [PD11] and [AFT11] also need some assumptions to work, but they are pretty much the minimal ones you would expect unless you are asking for papers that would also show that the parameterized complexity hierarchy collapses.)

Again, I am writing all of this very quickly, but if there is substantial interest for anything of the above I could try to elaborate (although it might take a while to return to this again --- please feel free to ping me if there is anything you would want me to comment on). As a quick way of providing references, let me do some shameless self-plugs (although the shame is decreased somewhat when I see that some comments have also cited some of these references):

Tutorial-style talk On the Interplay Between Proof Complexity and SAT Solving given at the International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning in 2016 with lots of full references at the end of the slides: http://www.csc.kth.se/~jakobn/research/TalkInterplaySummerSchool2016.pdf

Slightly more recent, and briefer, survey talk Understanding Conflict-Driven SAT Solving Through the Lens of Proof Complexity from early 2017 (also with full references at the end): http://www.csc.kth.se/~jakobn/research/TalkProofComplexityLensCDCL1702.pdf

Survey of connections between proof complexity and SAT solving: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Bibliographic reference: Jakob Nordström. On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News, volume 2, number 3, pages 19-44, July 2015. (Lightly edited version with some typos fixed.)]

SAT '16 paper with CDCL modelled faithfully as a proof system: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [Bibliographic reference: Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordström, and Marc Vinyals. Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. In Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT '16), Lecture Notes in Computer Science, volume 9710, pages 160-176, July 2016.]

Answer 3

I'm not an expert in this area, but I think the random SAT / phase transition stuff is more or less completely unrelated to the industrial/practical applications stuff.

E.g., the very good solvers for random instances (such as https://www.gableske.net/dimetheus) are based on the statistical physics methods (belief propagation etc.) I believe, whereas the very good 'general' solvers (such as http://fmv.jku.at/lingeling/) are using unrelated techniques (more like what Kaveh was talking about) I believe.

But, as I said, maybe don't take my word for it; this is coming from a definite non-expert.

Answer 4

Let me add my two cents of understanding to this, even though I've never actually worked in the area.

You're asking one of two questions, "what are all the known approaches to proving theoretical efficiency of some SAT solver for some type of instances" and "why are SAT solvers efficient in reality".

For the former question, I'll just direct you to the research of Stefan Szeider. He seems to me to be the currently most active area in the topic of backdoors and FPT parameterizations of SAT (which includes both structural approaches such as treewidth-type measures and so-called backdoor sets, as well as some mixture of the two).

For the latter question, to be honest, that exact question has been debated at every SAT-solving workshop I've attended (including recent years), so it's not a settled matter. But my impression is as follows.

First of all, you need to quantify or restrict what you mean by "in reality". It's not true that SAT solvers are universally good solvers for any problem you throw them at (of course), and between different problems you end up needing different strategies. For example, there are several recent successes where mathematical conjectures have been verified or tightened by an enormous computer search aided by a SAT solvers. In this case, apparently, a lot of the time the clever CDCL-style improvements and heuristics that modern SAT solvers normally employ don't really buy you too much power, and the game boils down to a clever way of splitting your source problem into parts, followed by (essentially) a brute-force branching algorithm with a small constant factor in the running time.

I may be overselling this point slightly, but my point was, when SAT solvers attacked for example the Erdos Discrepancy Conjecture, they were successful for a different reason than when they solve industrial instances derived from circuit testing.

So we're down to asking, why do CDCL-based solvers work so well on industrial instances of, for example, circuit verification (circuit equivalence testing)? I think that the most powerful view (or the consensus view) here is the search strategy of a CDCL solvers gels very well with the structure of these instances. This means, for example, that the circuits consist of relatively complex parts (call them clusters), interconnected by relatively speaking fewer and simpler connections, possibly in a hierarchical manner; and that the CDCL-solvers with all their heuristics are very good at (de facto) exploiting this and "projecting" these clusters onto the shared variables, in whatever way or order is most useful for verifying the circuit at hand. But it also seems to still be the consensus view that this is an insufficient explanations (e.g., we probably cannot theoretically explain the efficiency of CDCL SAT solvers in this domain purely by referring to the graph structure of the instance). So as of yet, I don't think we have a full answer.

So do the tractable parameterizations go some way towards explaining the latter? To be honest, I don't know. I think there is probably a powerful effect in play that the real-world instances are not worst case, nor are they (probably) truly average-case according to any instance distribution we are able to handle. But it's probably still worth asking.

Answer 5

There is a paper "Relating Proof Complexity Measures and Practical Hardness of SAT" by Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný in CP '12 that attempts to link the hardness or easiness of solving certain formulas by CDCL solvers with resolution proof complexity measures, in particular resolution proof space. The results are somewhat mixed, but it is a step in the right direction I think.

Answer 6

Since the original question title asks for theoretical explanations, let me point to a paper that might provide a kind of non-standard theoretical explanation.

The main result of the paper is that one can design a polynomial time errorless heuristic with exponentially small failure rate for all paddable languages (including SAT), if the errors are counted by a modified accounting scheme. This scheme is somewhat different from the usual one (which is the rate of errors among $n$-bit strings), but it is still in a close relationship with it.

See the details in the paper (sorry for self-promotion, I am one of the authors):

"A new algorithm design technique for hard problems," Theoretical Computer Science, Vol. 821, June 2020, pp. 45-56

If it is behind a pay wall, then here is a free version.