Tutorial/QuickStart for mini SAT?

[Alex]

Hi,

I am looking for a SAT solver library to deal with simple
satisfiability problems in my work. I am not a researcher, nor do I
have any experience/idea/clue about SAT solvers. I only want to
somehow use them in my own C++ program.

Is there a tutorial or quick start guide about how to do this? I have
downloaded the source files but there is no docs. Which function
should I call? How do I pass in the formulas? Which libraries do I
need? How to interpret output (is it just true or false)?

Thanks in advance.
Alex Loh.

[Nathan Kitchen]

If you don't mind running minisat as an external process you can get started very quickly. You just need to dump your problem to a file in DIMACS format (see Google). Running it once or twice manually should give you a clear idea of how to interpret its output.

If you want to use it through the API, you'll have to do more reading. As far as I know there is no tutorial or quick-start guide, but the main paper linked from the MiniSat page [1] is a good introduction to the interface. You'll still need to look at Solver.h to see the latest version of the interface. You'll need to link to libminisat.a, which you can build by just running "make libminisat.a" in the core subdirectory on Unix-type platforms.

[1] http://minisat.se/MiniSat.html

-- Nathan