Understanding SAT
As part of the work done on understanding the satisfiability problem I built some applications to understand some concepts like the DIMACS format, SAT encodings, CNF format and the complexity of a SAT problem.
I used the pigeon hole and the N-Queens problems to understand the complexity of SAT and to evaluate the problems that a computer scientist has when dealing with an NP problem.
First of all I made some encodings of the problems and I built a Java program to encode it in the DIMACS format so I was able to run a SAT solver to understand the complexity of them.
For example, when encoding the N-Queens Problem you have to take care of the restrictions of the problem before attempting to encode it. I found that the N-Queens problem has the following restrictions that can be easily translated into a CNF formula:
- A Queen can be on any place
- A Queen can be only on one place at a time
- A Queen cannot attack another Queen
Another example is the Pigeon Hole problem that can be encoded using the next restrictions:
- Each pigeon can be on any hole
- Each pigeon can be in only one hole at a time
- Each hole have space for only one pigeon (only one pigeon per hole at a time)
The pigeon hole problem is an UNSAT problem. It means there is not an assignment to the variables that makes the formula true. A complete algorithm will have to search the entire space before deciding that it is UNSAT so it can be used to understand the complexity of a SAT problem.
After some
experiments I fixed a graphic to the output of the pigeon hole problem, I
realize that the function that describes better the pigeon hole problem is: 
You
can find the computations done to get the formula and also the experimental
points and a graphic downloading the following Mathematica code: PigeonHole.nb
The following graphic shows the complexity of the problem while the number of holes increases. It is important to remark that the y axis is using a logarithmic scale.
After these experiments were done, the understanding of a NP problem and how do they grow and become impossible to solve in a prudent time by a computer was evident.
Additionally, it was interesting to understand the many ways a problem can be encoded to be solved by a SAT solver. The problems encoded here were small but when we are trying to encode real world problems the task can be very challenging.
Another interesting part of understanding SAT was learning about the different kind of solvers that have been built for the SAT Competition. The experiments done with the encodings were run on zchaff but the learning process made me know more about kcnfs, minisat and WalkSAT.
It was interesting to know that each solver has different strengths and weaknesses, and that those will be important to consider when working with random formulas or structured problems.
Downloads
Pigeon hole formula generator (ZIP)