21
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ SAT have no efficient methods ... but take a look at these slides $\endgroup$ – Fayez Abdlrazaq Deab May 17 '13 at 20:26
  • $\begingroup$ please also take a look here: cs.stackexchange.com/questions/12135/convert-problem-to-cnf $\endgroup$ – Dchris May 19 '13 at 15:53
  • $\begingroup$ Just a quick and dirty solution before you try anything else, in case you just want to test something: cryptlogver. The tool says that it is focused for crypto, but it will do the trick. Moreover, the syntax of the language that you will use is very c like so you will not have many problems. The installation is not difficult but quartus is big so get a cup of coffee. $\endgroup$ – absinthe_minded Sep 16 '13 at 21:39
  • 1
    $\begingroup$ See also related question cs.stackexchange.com/q/30790 $\endgroup$ – András Salamon May 20 '17 at 8:11
20
$\begingroup$

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.

$\endgroup$
13
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ do you suggest any specific smt solver? $\endgroup$ – Dchris May 18 '13 at 11:43
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ It looks like CBMC doesn't convert an arbitrary C program into a CNF; it creates a CNF based on the C program that performs a static analysis for integer overflows, buffer overflows, and the like. $\endgroup$ – vy32 May 20 '17 at 13:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.