Uses of SAT Solvers

There are practical uses of SAT solvers:

• Constraint satisfaction problems, e.g. FPGA routing.

• Circuit checking: two Boolean functions f₁ and f₂ are equal iff (f₁ ∨ f₂) ∧ (¬ f₁ ∨ ¬ f₂) is unsatisfiable.

• Safety checking: show that an instance where two trains are going in opposite directions on the same track is not satisfiable.

• Show that a request will eventually be answered; this may be approximated by unrolling it into k time steps.

• Show that a case where a distributed memory system will give the wrong value for a memory request is unsatisfiable.