Written by Roy van Rijn (royvanrijn.com) on
Nov 11, 2019 21:42:12
: 0 comments
SAT solving: Creating a solver in Java (part 2)
This is the second blogpost in a series about SAT solving. Today we’re going to build a simple solver in Java.
Before continuing, if you don’t know what a SAT solver is, read [part one].
The algorithm we’re going to implement is called DPLL (Davis Putnam Logemann Loveland).
The input we’ll accept is in DIMACS format. For now we can just skip the p-line with all the settings and just parse all the numbers.
Here is an example input:
In Java we can parse this entire file with almost a one liner (don’t do this in production code):
The next step in creating a (slow) SAT solver is to implement the following pseudo code:
Step 1a: Find all the unit variables
Find all the unit variables (-4 0). These are clauses that have just a single (active) variable. If a clause has just a single variable, it has to be true. So in this case we mark 4 as false.
Step 1b: Process all unit variables
Now we go over all the other clauses that contain this variable -4 or the inverse (4).
If the clause has -4 (which we now know is true), we mark this entire clause as ‘satisfied’.
If the clause contains the inverse of the variable, in this case 4, we know that particular variable will never become true, so we remove it from the list.
Lets try step 1 with the following example:
We have a single unit variable, -2, so we mark this variable as true. Next we apply step 1b:
Now we have a new unit variable, 3 0. This again can be processed:
And now we are done with the unit propagation. We are now left with two clauses that both are not a unit clause.
Step 2: Gamble on a variable
First we repeat step 1 until there are no unit clauses left. Now we need to take a gamble. In this case we have unresolved: -1, 1, 4 and -6, 6. We need to pick one of these and try it.
Let’s pick 6.
Again, we process this, if a clause contains 6 we mark it as true. If a clause contains -6 we remove that variable as alive variable.
Now we go back to step 1 and repeat.
There are two possible ways this loop will end.
1) There are no clauses left, everything it true. In this case we have reached SAT.
2) We run into a situation that we have a conflict (!)
A conflict happens when we have a situation that can’t happen. For example when we have the following situation:
In this case we have -1 as a unit clause, we assign this variable. Now we process the following lines and what happens? We are left with:
This is a conflict, we can’t have -2 AND 2. It can’t be true and false at the same time.
In the case of a conflict we backtrack back to the last decision point where we gambled. Reset everything and try a different variable.
Nothing left to gamble? UNSAT
If, at a certain point, you’ve run out of options to gamble on, we are also done. We’ve proven there is no way to assign the variables to satisfy all the clauses. In this case we can return UNSAT.
Put this into code:
If you put the above algorithm into Java code you might end up with something like this:
This is all. This algorithm can solve any problem that can be turned into a SAT problem, which are a lot of mathematical problems.
DPPL isn’t the fastest algorithm, a lot of improvements can be made (part 3?). For example we can learn new clauses during analysis, and instead of backtracking to the last decision moment, sometimes you can backtrack to a much earlier decision moment, making the resolution much faster.
But the basic algorithm to solve SAT, is very simple indeed.