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.
Asked By : Dchris
Answered By : András Salamon
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/12087
0 comments:
Post a Comment
Let us know your responses and feedback