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).

# Input parsing

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):

# Unit propagation

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.

## Conflict

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.