Repository files navigation

Dimple is a simple SAT solver written in Java. This is an attempt at learningabout theBoolean Satisfiability Problem and along the way getting better atJava.

Dimple can be built withgradle. To build Dimple and run its unit tests, rungradle build on the command line. Dimple requires Java 11.

Dimple comes with a command line script to allow easy usage. The tool issurprisingly calleddimple, and receives its input as an s-expression onstdin:

$ cat file.lisp(and  (or A B (not C))  (or B C)  (not B)  (or (not A) C))$ dimple file.lispSATtrue = { A C }false = { B }

Supported s-expression functions arenot,or,and,if, andiff.

What is SAT, and why does it need solving? SAT is short for SATISFIABILITY,which is short for theBoolean Satisfiability Problem. This is the problem ofdetermining if there is a set of assignments for which a given boolean formulais true. That's quite a mouthful, so lets try to clarify it a bit with anexample:

Given the boolean formula(A or B or -C) and (B or C) and -B and (or -A C),are there true or false assignments forA,B andC for which this formulaevaluates to true? Answer in this case is yes, there is only one assignment,A -B C. Another example, in this case not satisfiable isA <=> B and A and -B.

Minor caveat: GitHub does not supportLaTex for its readme files, somathematical notation has been replaced with my own pseudo-notation. Variablenames are capital letters, A dash (-) before a variable name means it islogically negated, the wordsand andor correspond to their booleanlogic counterparts, and the symbols-> and<=> correspond to logicalimplication and a logical biconditional respectively.

SAT is a hard problem, in fact, it has been proven to be NP-Complete. That is,there will never be an algorithm which solves SAT in less than2^N operations,whereN is the number of variables. Most SAT solvers try to achieve a runtimeperformance of2^c*N, wherec is some constant smaller than 1. The fastest(?) known algorithm for SAT is PPSZ, which has a runtime complexity ofO(2^0.386*N).

Dimple's SAT solver is an implementation of Knuth'sSAT0W program. Itis a watch-list based algorithm, which allows for trivial backtracking.

Dimple is capable of solving SAT problems inCNF form. CNF is short forConjunctive Normal Form, or layman's terms, an "and of ors". CNF is a set ofsets of variables connected byors, which in turn are connected byands.This means that in order to solve the SAT, our assignment needs to satisfy atleast one variable in each clause. An example of a formula in CNF form is(A or B) and (A or C), whereasA and (-(A <=> B) or C) is not, because ofthe negation and biconditional.

Before we begin solving the SAT problem, we need to devise a way of encoding it.We need a way to be able to work with our clauses that will allow us to check ifa variable in a clause is negated or not, and a way to traverse the clauseseasily.

For this I chose to use aSet<Integer> for each clause, making the entireproblem aCollection<Set<Integer>>. A variable will be encoded as a numberbetween 1 andN,N being the number of all variables. To remember whichvariable corresponds to which number, aBiMap<String, Integer> is used. Thisallows us to encode the entire problem using these two data structures.

Our set of integers currently does not know whether or not an variable isnegated. For this another trick must be applied. We save the variablev asx = v << 1 | sign(v) in the set.sign(v) returns1 ifv is negated and0 otherwise. This allows us to query the variable easily withx >> 1 andquery its sign withx & 1.

We can look at a SAT as the set of all assignments to a certain formula, and tolist them we can simply iterate through said set, printing them out one by one.For this Dimple implements anAssignmentIterator class whichimplementsIterator<Boolean[]>. Java'sIterator interface will allow us tosimulate this iteration through the set of all assignments.Iterator mustreturn a value for each invocation ofnext(), and we cannot know if anothersolution to the SAT exists without trying to find one. Thus, the last solutionour iterator will return will always be a bogus one. If our iterator returnsonly one solution, the formula is unsatisfiable.

Dimple's algorithm is a backtracking one. Starting from variable0, we assigntrue orfalse to all variables up to variablen-1. The entire search spaceis of courseO(2^N), but hopefully we will terminate the algorithm beforesearching through it all (assuming there is a solution). The assignment is anarray ofBooleans, with valuestrue andfalse for variables which havebeen assigned a value, andnull when they have not. When backtracking, avariable is set tonull to indicate that it has had its assignment removed.

The next construct we need to initialize is the watch-list. The watch-list iswhat enables us to trivially backtrack and I will go into its intricacies later.The watch-list is a list mapping variables to clauses in which they reside. Aclause is consideredwatching a variable, when said variable maps to theclause in the watch-list.

privateList<Deque<Set<Integer>>>createWatchList() {List<Deque<Set<Integer>>>watchList =Stream.generate(() ->newArrayDeque<Set<Integer>>())      .limit(2 *variables.size())      .collect(Collectors.toList());for (varclause :clauses) {varany =clause.iterator().next();// get any variable from the clausewatchList.get(any).add(clause);// make the clause "watch" said variable  }returnwatchList;}AssignmentIterator(/* ... */ ) {// ...this.currentAssignment =Stream.generate(() ->null)      .limit(variables.size())      .toArray(Boolean[]::new);this.watchList =createWatchList();this.currentVariable =0;this.state =Stream.generate(() ->0).limit(variables.size()).toArray(Integer[]::new);}

TheAssignmentIterator will attempt to assign values to all variables inorder, following a set of rules:

1. All watched variables have either been assignedtrue, or have not beenassigned yet.
2. When assigning a variableV totrue, clauses watching-V must now watchanother variable. Conversely, when assigningV tofalse, clauses watchingV are now required to watch another variable.
3. If an alternative variable is not found, we have a contradiction and mustbacktrack.
4. When we have backtracked all the way to the first variable, we know we haveexhausted all possible assignments and can terminate.

privatebooleanfindAlterantive(finalintfalseVariable) {booleanfoundAlternative =false;varclause =watchList.get(falseVariable).getFirst();for (varalternative :clause) {varvariable =alternative >>1;varisFalse = (alternative &1) >0;if (currentAssignment[variable] ==null ||currentAssignment[variable] !=isFalse) {foundAlternative =true;watchList.get(falseVariable).removeFirst();watchList.get(alternative).add(clause);break;    }  }returnfoundAlternative;}privatebooleanupdateWatchList(finalintfalseVariable) {while (!watchList.get(falseVariable).isEmpty())if (!findAlterantive(falseVariable))returnfalse;returntrue;}

The watch-list approach provides us with a very convenient feature: whenbacktracking, assignments go fromtrue orfalse tonull. According torule #1,null is a legal state for the watching clause, which in turn meansthat we do not need to update the watch-list when backtracking, only theassignments.

Finally, all we need to do now is, for each variable, try to assigntrue orfalse to it, and if successful move on to the next. If unsuccessful, assignnull and try to reassign the previous variable. Here I introduce astateproperty which keeps track of which values have been tried for each variable.

privatebooleantryUpdate() {booleantriedUpdate =false;for (varvalue :newint[]{0,1}) {if (((state[currentVariable] >>value) &1) ==0) {triedUpdate =true;state[currentVariable] |=1 <<value;currentAssignment[currentVariable] =value !=0;if (!updateWatchList(currentVariable <<1 |value))currentAssignment[currentVariable] =null;else {currentVariable +=1;break;      }    }  }returntriedUpdate;}

Once we have assigned all of the variables, we can return an assignment, and ifwe have backtracked all the way to the beginning, we can terminate thealgorithm as all assignments have been exhausted. InAssignmentIterator,assignments are saved to a list where they can later be retrieved.

privateBoolean[]nextAssignment() {while (true) {if (currentVariable ==variables.size()) {currentVariable -=1;returncurrentAssignment;    }if (!tryUpdate()) {if (currentVariable ==0) {hasNext =false;returnnull;      }else {state[currentVariable] =0;currentAssignment[currentVariable] =null;currentVariable -=1;      }    }  }}

Now that we have a way to encode and solve a SAT problem, lets make the programdo the encoding for us. Additionally, lets explore the possibilities of solvingproblems not structured as CNF.

To support s-expressions, we need a way to parse them and transform them intoDimple's encoded clauses. Parsing s-expressions is simple, an s-expression is alist of either strings, which we callAtoms, or more s-expressions, forming asort of tree. In Java we can implement an s-expression like so:

classSexpressionextendsLinkedList<Either<String,Sexpression>> {}

Peter Norvig provides asimple s-expression parser on his website,which can easily be adapted to parse strings into our Java s-expression class.All it does is replace( with(, and) with) and split the stringon whitespace. The split string is then recursively parsed into ourSexpression class. SeeSexpressionParser for thefull code.

S-expressions allow us to express problems in a more natural way than CNF. Everynon-CNF boolean logic formula (prepositional formula) can be converted into aCNF equivalent, the only caveat is that the CNF equivalent lead to exponentialexplosion of the formula.

Converting to CNF is done with in following steps:

1. Replace biconditionalsP <=> Q with(P or -Q) and (-P or Q).
2. Replace implicationsP -> Q with(-P or Q).
3. Propagate all negations inward by applying De Morgan's law. Replace-(P and Q) with-P or -Q and-(P or Q) with-P and -Q.
4. Distributeors inwards overands. ReplaceP or (Q and R) with(P or Q) and (P or R).

To do this in Dimple, s-expressions are parsed into an intermediate format Icall aFormula. AFormula is a tree like structure which corresponds to ans-expression but allows easier traversal and transformation using a VisitorPattern:

publicinterfaceFormula {public <T>Taccept(FormulaVisitor<T>visitor);}

The visitor pattern enables separation of algorithms and data. It allows usto implement various transformations on theFormula class without modifyingthe class source code in order to support them. A simple example can be found intheFormulaToStringVisitorclass, returns a string representation of aFormula.

Back to our subject, theCnfConverter class appliesfour visitors, one for each step, which do the conversion:

publicclassCnfConverter {publicstaticFormulaconvert(Formulaformula) {formula =formula.accept(newBiconditionalEliminationVisitor());formula =formula.accept(newImplicationEliminationVisitor());formula =formula.accept(newNotPropagationVisitor());formula =formula.accept(newOrOverAndDistributionVisitor());returnformula;  }}

Clauses can be created using another visitor.ClauseVisitor is applied to eachor clause encountered in the visitation process, which collects variables intoclauses and finally returns a clause.

classClauseVisitorextendsFormulaVisitor<Set<Integer>> {Map<String,Integer>variables;ClauseVisitor(Map<String,Integer>variables) {this.variables =variables;  }@OverridepublicSet<Integer>visit(Atom.Varformula) {Stringvariable =formula.value;variables.computeIfAbsent(variable, (k) -> {returnvariables.size();    });returnSet.of(variables.get(variable) <<1);  }@OverridepublicSet<Integer>visit(UnaryConnective.Notformula) {Atom.Varatom = (Atom.Var)formula.argument;Stringvariable =atom.value;variables.computeIfAbsent(variable, (k) -> {returnvariables.size();    });returnSet.of((variables.get(variable) <<1) |1);  }@OverridepublicSet<Integer>visit(BinaryConnective.Orformula) {varresult =newHashSet<Integer>();result.addAll(formula.left.accept(this));result.addAll(formula.right.accept(this));returnresult;  }}

SAT is an interesting problem and has been extensively studied over the years.SAT solvers have become increasingly better and can scale to millions ofvariables. Many known difficult problems can be reduced to SAT, so having a gooda SAT solver enables us to solve sometimes completely unrelated problems. Thesolver need not know anything about the problem, only how to transform it into aSAT instance and how to transform the solution to something relevant to theproblem. Let's look at a few problems which we can solve with a SAT solver.

The Four Color Theorem states that the regions of any map can be colored in atmost four colors such that no two adjacent regions are colored with the samecolor. We can use Dimple to solve the Four Color problem by reducing it to aSAT.

Let's look at of a map of sizeN=3. We will use4*N variables namedRi,Bi,Gi,Yi, each corresponding to coloring theith map region in theirrespective color or not. This means that for eachi, one and only one colorvariable must be true. Thus we need one(Ri or Bi or Gi or Yi) clause for eachi. This states that we need at least one color for each region. And then foreach pair of colorsC1 andC2 we need a(-C1i or -C2i) clause for eachi, stating that two colors can not be selected for the same region. Finally,for each neighboring region we need a(-Ri or -Rj), indicating that theycannot both be of the same color.

The SAT for a complete 3-vertex graph (N=3) looks like this:

(and; region 1  (or R1 B1 G1 Y1)  (or (not R1) (not B1))  (or (not R1) (not G1))  (or (not R1) (not Y1))  (or (not B1) (not G1))  (or (not B1) (not Y1))  (or (not G1) (not Y1)); region 2  (or R2 B2 G2 Y2)  (or (not R2) (not B2))  (or (not R2) (not G2))  (or (not R2) (not Y2))  (or (not B2) (not G2))  (or (not B2) (not Y2))  (or (not G2) (not Y2)); region 3  (or R3 B3 G3 Y3)  (or (not R3) (not B3))  (or (not R3) (not G3))  (or (not R3) (not Y3))  (or (not B3) (not G3))  (or (not B3) (not Y3))  (or (not G3) (not Y3)); adjacent  (or (not R1) (not R2))  (or (not R1) (not R3))  (or (not B1) (not B2))  (or (not B1) (not B3))  (or (not G1) (not G2))  (or (not G1) (not G3))  (or (not Y1) (not Y2))  (or (not Y1) (not Y3)))

Running this through Dimple gives 24 solutions. In this simple case, we have avalid solution whenever we select three distinct colors, which we can do in4!ways. To automate the reduction of such a problem, we will introduce a newinterface:Reduction.

@FunctionalInterfaceinterfaceReduction<P> {publicFormulareduce(Pproblem);}

Now, given the correct reduction, we can solve any problem simply by reductionto SAT:

classReductionSolver<P> {privatefinalReduction<P>reduction;privateSolvercreateSolver(Pproblem) {returnFormulas.createSolver(reduction.reduce(problem));  }Optional<Map<String,Boolean>>solve(Pproblem) {returncreateSolver(problem).solve();  }}

And finally we can implement the reduction like this:

classFourColorReduction<T>implementsReduction<Graph<T>> {@OverridepublicFormulareduce(Graph<T>graph) {varbuilder =newFourColorSexpressionBuilder(graph);builder.writePrefix();builder.writeAllRegions();builder.writeAllEdges();builder.writeSuffix();returnSexpressions.compile(builder.get());  }privateclassFourColorSexpressionBuilder {// ...  }}

Our automated solver will now allow us to solve the Four Color Problem for muchlarger maps, such as the map of the United States or America. We simply need togenerate a graph which is equivalent to the map and pass it to our solver. Adecode function is used to take the SAT solution and convert it to a mappingfrom a state name to a color. Example code can be found inFourColorReductionTest.

varsolver =ReductionSolver.of(newFourColorReduction<String>());varsolution =solver.solve(mapOfUsa()).get();varcolorMap =FourColorReduction.decodeSolution(solution);

A clique is a fully connected graph within another graph, an N-clique hasNvertices. Finding a clique of sizeN within a graph is one ofKarp's 21 NP-complete problems,and interestingly, is also reducible to SAT. This time, we will go aboutautomatic the reduction immediately, as even the smallest Clique Problem canintroduce hundreds of clauses.

According tothis page,to reduce a Clique Problem to a SAT, we need toN*V variables, whereV isthe number vertices in a graph andN is the size of the clique. For eachrfrom 0 toN,Vi,r is true ifVi is therth node of the clique. Usingthis, we can add the following clauses:

1. (V1,r or V2,r or ... or Vn,r) for allr s.t.0 <= r < N.
2. (-Vi,r or -Vi,s) for alli,r,s,0 <= r < s, s.t.0 <= s < N (Avertex cannot be both therth and thesth vertex in the clique).
3. If there is not edge fromVi toVj, they cannot both be in the clique.Thus, we add-Vi,r or -Vj,s for all s.t.0 <= r, s < N,r != s.

This givesCliqueReduction:

classCliqueReduction<T>implementsReduction<Clique<T>> {@OverridepublicFormulareduce(Clique<T>clique) {varbuilder =newCliqueSexpressionBuilder(clique);builder.writePrefix();builder.writeRthVertex();builder.writeMutualExclusion();builder.writeEdges();builder.writeSuffix();returnSexpressions.compile(builder.get());  }privateclassCliqueSexpressionBuilder {// ...  }}

You can view the test by looking atCliqueReductionTest.The graph being tested is identical to the one in the next figure. The generatedSAT instance has 28 variables and 284 clauses, but Dimple can solve it in undera second.

In the above diagram, a brute force algorithm is applied to search for a cliqueof size 4.

Sudoku is a classic problem for SATsolvers. A reduction from Sudoku to SAT can generate over 1000 clauses andN^3variables, whereN is the size of one side of the Sudoku.

To reduce to SAT we name each variableXi,j=v, for alli,j,v s.t.1 <= i, j, v <= N, if the variable is true, the cell ati,j has the valuev. Then the clauses are simply:

1. ExactlyOneOf(Xi,j=1, Xi,j=2 ... Xi,j=N) for alli,j. This mean we musthave a value for each square.
2. ExactlyOneOf(X1,j=v, X2,j=v ... XN,j=v) for allj,v. This means thatrows cannot contain duplicate values.
3. ExactlyOneOf(Xi,1=v, Xi,2=v ... Xi,N=v) for alli,v. This means thatcolumns cannot contain duplicate values.
4. ExactlyOneOf( (Xi+0,j+0=v, Xi+0,j+1=v ... Xi+0,j+sqrt(N)=v), (Xi+1,j+0=v, Xi+1,j+1=v ... Xi+1,j+sqrt(N)=v) ... (Xi+sqrt(N),j+0=v, Xi+sqrt(N),j+1=v ... Xi+sqrt(N),j+sqrt(N)=v) )for alli,j,v. This is the hardest constraint to read (if only GitHubsupportedLaTeX...), it just means that squares cannot contain duplicatevalues.
5. Finally, the constraints of the puzzle itself are encoded as a clause forevery known value. For example, if we know square 1,2 has the value 5, aconstraintX1,2=5 is added (and hence must be true).

ExactlyOneOf(...) is a helper function, recall from the Four Color examplethat it can be transformed into a "regular" boolean formula by adding thefollowing clauses:

1. (V1 or V2 ... Vn) for all variables in the argument list.
2. (-Vi -Vj) for alli,j s.t.i != j.

Finally, a brief overview of the code looks like this:

classSudokuReductionimplementsReduction<int[][]> {@OverridepublicFormulareduce(int[][]sudoku) {Preconditions.checkArgument(isSudoku(sudoku),"Sudoku is invalid");varbuilder =newSudokuSexpressionBuilder(sudoku);builder.writePrefix();builder.writeValueForEachSquare();builder.writeDedupedRows();builder.writeDedupedCols();builder.writeDedupedSqrts();builder.writePuzzle();builder.writeSuffix();returnSexpressions.compile(builder.get());  }booleanisSudoku(int[][]sudoku) {for (inti =0;i <sudoku.length;i++)if (sudoku[i].length !=sudoku.length)returnfalse;intsqrt =IntMath.sqrt(sudoku.length,RoundingMode.FLOOR);returnsqrt *sqrt ==sudoku.length;  }privateclassSudokuSexpressionBuilder {// ...  }}

Dimple'sSudokuReductioncan make quick work of any 4x4 Sudoku puzzle using this method. When trying tosolve a 9x9 puzzle it chokes because of its recursive parsing of the formula(seeFormulaSolverVisitor).This can be fixed, but for the purpose of this exercise I think solving a 4x4 isenough.

Sudoku puzzles are usually categorized by their difficulty, "easy", "medium","hard", etc. Modern SAT solvers are good enough to be able to solve any of thehardest Sudoku puzzles regardless or their difficulty with ease. In contrast,dedicated naive Sudoku solvers can sometimes choke on harder problems. Check outPeter Norig'sarticle on Sudoku solvers for a more extensivereview of solving Sudoku puzzles using a dedicated solver.

SAT solvers are incredibly powerful programs with many many applications. Somany problems can be reduced to SAT, and using a modern fast SAT solver can besolved in milliseconds.

If you'd like to lean more about SAT solvers, check out Sahand Saba'sUnderstanding SAT by Implementing a Simple SAT Solver in Python which is the blog post thatinspired this write-up, and of course Knuth'sTAOCP section 7.2.2.2which goes into a lot of detail on the subject. Additionally,Modern SAT solvers: fast, neat and underused (part 1 of N) andSudoku solving the easy way using boolean satisfiabilitydiscusssuccessfully solving a Sudoku using a SAT solver in more detail.