SAT solvers

There are so many problems that would be solvable if there were efficient ways of finding satisfying valuations that considerable effort has been spent on finding ways to do this. Programs that find satisfying valuations are known a SAT solvers.

Unfortunately, there is a stumbling block. The problem of finding satisfying valuations is NP-complete.

"NP" refers to the class of problems that are solvable in Non-deterministic Polynomial time. These are problems that if we were able to guess the answer (using the non-determinism, which in this context means that if we have a choice we can try both and keep the one that works) then we could check it in polynomial time.

Satisfiability is in this class: if we guess a valuation v, we can check it quickly by computing 〚P〛v using the steps we saw in Week 1. However, if we can't guess a satisfying valuation there is currently no known general strategy better than trying all of them, which takes an amount of time exponential in the size of the input.

The question of whether or not there is a general strategy that works in polynomial time is known as the P = NP problem, which is a famous major unsolved problem in Computer Science. Finding satisfying valuations is also NP-complete, which means that a polynomial time solution to this problem would give a polynomial time solution to all NP problems.

Despite there being no known general solution that is better than trying every possible valuation, there has been great progress on SAT solvers that do well on problems that arise in the ``real world'' like the ones listed above. Formulas that are generated from real world problems often have a large amount of regularity that it is possible for a SAT solver to exploit to avoid searching every possible valuation.

Video introduction to SAT Solvers

SAT Solvers, introduction

The first video describes how SAT solvers work:

1. They take input in the form of clauses in Conjunctive Normal Form (CNF).

2. They try to find a satisfying valuation by building up partial valuations

   1. Initial guesses are made

   2. If these guesses don't work out, then the solver must backtrack

3. If the solver finds a satisfying valuation, then it returns SAT (and the valuation). If it fails and no more backtracking is available, then it returns UNSAT.

Making SAT Solvers faster with Unit Propagation

The second video describes how to make SAT solvers go faster by using information from the clauses to be solved, in a process called "Unit Propagation". This can considerably speed up a solver:

PDF Notes

Written notes on SAT solvers. These cover the same material as the videos.