Theoretical explanations for practical success of SAT solvers? 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?
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): 


VSIDS heuristic fir selecting which variable to branch on next.
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$&lt;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&lt;\alpha&lt;1$ be a fixed constant.
The score of variable $v$ at time $n$ is then: 
$$\sum_{i&lt;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.