I just wanted to try a simple sat solver. So I wrote a short tutorial how to install and use one.

The parallel frontends Plingeling and Treengeling and the SAT solver Lingeling from the JKU Linz are known for speed. They are also quite easy to use.

You can download and install the package like this (should work on Linux & OSX):

wget http://fmv.jku.at/lingeling/lingeling-bal-2293bef-151109.tar.gz
tar -xvf lingeling-bal-2293bef-151109.tar.gz
cd lingeling-bal-2293bef-151109
./configure.sh
make

To run it call the following command in your terminal (you have to be in the right folder):

./plingeling

It uses the DIMACS CNF format, so comments start with c and the input starts with p, which defines the number of variables and clauses. Each variable is a number != 0. A negative one states that the variable is negated.

Example:

c some comment
p cnf 3 3
1 -3 0
2 3 -1 0
2 3 1 0

Submit the input by sending a End of File-sequence (Ctrl + D).

#Links