Converting (math) problems to SAT instances

Question

What I want to do is turn a math problem I have into a boolean satisfiability problem (SAT) and then solve it using a SAT Solver. I wonder if someone knows a manual, guide or anything that will help me convert my problem to a SAT instance.

Also, I want to solve this in a better than exponential time. I hope a SAT Solver will help me.

Answer 1

Chapter 2 of the SAT Handbook (by Steven Prestwich) covers how to turn discrete decision problems into CNF, in some depth. (Unfortunately, I don't think there is a draft version online -- probably best to consult your local library.) Several of the other references cited in Magnus Björk's quirky overview Successful SAT Encoding Techniques are also useful.

If your problems are continuous, or you are especially interested in systems of inequalities, then other kinds of solvers are more likely to be useful. As Kyle points out, SMT solvers (such as Z3, Yices, or OpenSMT) might be useful, although traditionally SMT theories tend to be focused on verification of computer software, so SMT solvers usually have great support for things like expressions involving intervals of integers, but may perform poorly on injectivity constraints. For problems that are naturally expressed as systems of inequalities, CPLEX is the one to beat (it used to be available for academic use for free, and it might still be). For some combinatorial decision problems (like finding packings of rectangles into a square), constraint solvers such as Minion outperform SAT solvers and are often easier to use.

Answer 2

Unless you're translating mathematical problems to SAT instances as a learning exercise, your time will be much more fruitfully spent learning about satisfiability modulo theories. SMT will allow you to express equations and other constraints much more naturally than as Boolean SAT instances. Some SMT solvers support existential and universal quantifiers, allowing you to move beyond NP and express PSPACE problems.

Besides being more expressive, SMT solvers are faster. Not P=NP faster, but more efficient in that a good SMT solver doesn't discard theory-specific structural information that helps guide the solver through the search space. Doing a Karp reduction directly to a SAT instance forces the SAT solver to relearn all that structure, often at exponential cost. For example, the fact that addition is commutative is lost on both DPLL-based and local search based SAT solvers; the solver isn't aware that it is dealing with numbers at all! To avoid trying all the permutations of x+y+z=10 a SAT solver needs symmetry-breaking code, which requires graph automorphism detection. The best current graph automorphism recognition algorithms require time exponential to the number of vertices in the worst case, so exponential time might be spent relearning a simple rule of arithmetic.

Answer 3

Two tools that convert high level languages to SMT or CNF.

CVC The syntax is close to CAS.

CBMC It convert a C program to CNF, allowing assertions. The assertions are either always true, or if false a counterexample input is found. CBMC unrolls loops, so certain C programs have exponentially large CNF/SMT.