Logic Project, Part II

The second project revolves around SAT solving. You will encode several problems to SAT, and you will implement your own SAT solver.

This project comes with some code skeleton. The provided OCaml module Dimacs will be useful for all tasks, and the Hex module will be useful to encode the penguins' problem. The documentation of these modules can be generated in html/ by running make doc; it is also available here.

Encoding problems to SAT

We consider here several problems. Each problem will be encoded to SAT, and solved using minisat. More precisely, each instance I of the problem must be encoded to a SAT instance S such that each model of S yields a solution of I and all solutions are obtained in this way.

Latin square

File src/latin.ml shows how to encode latin square to SAT (the input N is the size of the square). It can be tested using, for example, make N=10 test_latin. However, the encoding can be improved: try to modify the file, adding some clauses to help the SAT solver.

Greco-latin square

Adapt src/latin.ml into src/greek.ml to encode the graeco-latin square problem.

Three-color Truchet tiles

Create src/tile.ml which encodes the following tiling problem: given some integer N, tile the a N*N square with quarter-circle Truchet tiles colored with three distinct colors, such that adjacent tiles have matching colors. To avoid too much regularity, you can force a few colors. You can test your encoding using, for example, make N=10 test_tile.

In solution mode, your tile binary should display the tiling by first outputting its size as an integer on one line, then display the tiling as N lines of N characters in [0-2], giving the color of tiling vertices (i.e. points where four tiles meet). An example is given here. This format is expected by the two renderers tile_graphics and tile_cairo (provided, but not necessary to complete the project).

Pingouins

In Hey, That's My Fish! several penguins move on hexagonal ice floats to eat as much fish as possible. We consider the simplified problem where a single penguin has to eat some number of fish, when there is exactly one fish per float. Several instances of this problem are provided in problems/, organized in subdirectories indicating how many floats must be left unvisited.

Write a SAT encoder src/pingouins.ml, using the provided OCaml module Hex to parse input files and handle moves on the hexagonal grid. Your pingouins binary should use the environment variable PENALTY to know how many floats can be left unvisited. This is required to be able to use the provided make targets, e.g. make PROBLEM=problems/1/flake1 PENALTY=1 test_pingouins to test on a given problem and make PENALTY=1 tests_pingouins to test on all problems of problems/1/.

Implementing a SAT solver

The most naive way to solve SAT is to guess the value of all variables, one by one. This is however too inefficient: after guessing, for example, that some variable X is false, there are typically several variables Y whose value is forced by the clauses. This is the main idea behind the DPLL algorithm, which is the core of modern SAT solvers.

A basic implementation of DPLL is provided in src/naive.ml. It alternates between choices and unit propagation — we will not consider pure literal propagations. Backtracking is used to consider alternative choices. When encountering a conflict (i.e. realizing that the current assignment violates a clause) the function simply returns, and it raises SAT m when a model m is found. The partial assignment, containing values resulting from both choices and propagations, is maintained as an association list, of type (literal * bool) list.

Imperative partial assignments

In order to improve our SAT solver, we will first adopt a more efficient data structure for the partial assignment: instead of the association list, we will use two arrays, a first one indicating for each variable whether it is assigned, and a second one giving the actual values of variables. This implementation allows constant-time querying and modification of the partial assignment.

The downside is that the data structure is no more persitent, but mutable. Thanks to its persistent partial assignment, the DPLL function of src/naive.ml simply takes an assignment as argument, and passes its modified versions to its two recursive calls, corresponding to the exploration of the two alternative values for the chosen variable. With the new mutable data structure, something has to be done to cope with backtracking. There are two options:

• We could still take the assignment as argument of dpll, and use Array.copy to keep its initial value, and be able to backtrack. These copies would however be very inefficient, costing time and memory allocations.
• A better approach is to maintain a single partial assignment (two arrays) to be used by all recursive calls of dpll, and maintain a stack of modifications performed on the partial assignment, to be able to undo them. Whenever a variable X is assigned, a new item X should be added to the stack. A special "checkpoint" value, for example 0, can also be pushed to the stack, to be able to undo modifications back to this point: this simply consists in marking as unassigned all variables found on the stack before the checkpoint (changing their value is unnecessary, as the value of unassigned variables is irrelevant).

Modify src/naive.ml into src/arrays.ml to use partial assignments as arrays, using the second approach. You should witness a significant speedup. Correction can be assessed using make PROVER=./arrays test — this will also display the performance ratio between your prover and minisat, which is about 850 in my case.

Two watched literals

Two fundamental ideas have brought impressive performance gains for SAT solvers. The first one is conflict-driven clause learning: it is purely logical, and beautiful, but we will not consider it in this project. The second one is two watched literals: it is an algorithmic improvement of the data structure used to store clauses, allowing more efficient unit propagation.

A DPLL solver spends most of its time propagating literals, it is thus important to optimize this step. Unit propagation requires to iterate over unit clauses wrt. the current assignment. A key observation is that, since a clause becomes a unit clause when all but one of its literals are assigned to false, it suffices to "watch" two of its literals to detect when this happens, maintaining the following invariant:

⊢ In a clause that is not satisfied in the current partial assignment, the two watched literals are unassigned.

Then, propagation takes place as follows when a literal L becomes false:

• There is no need to consider clauses where L is not watched. Indeed, these clauses have at least two other unassigned literals: their watched literals.
• We also do not need to consider clauses that are satisfied, i.e. containing a literal assigned to true. This includes clauses containing the negation of L, watched or not.
• If an unsatisfied clause where L is watched has only one unassigned literal, it must be its other watched literal, and we can propagate it. If two such propagations are contradictory, we have a conflict.
• If a clause where L is watched is not a unit clause, then it must have an unassigned literal L' that is not currently watched. We maintain the invariant by changing the watched literals of the clause, replacing L by L'.

More details, and illustrative examples, may be found in this or that paper.

A key aspect of this technique is that, since the choice of watched literals is arbitrary (as long as the invariant is respected), there is no need to undo the changes of watched literals when backtracking. Thus, we can use an efficient mutable data structure organizing clauses by watched literals, without any cost when backtracking. In practice, we can associate to each literal a doubly-linked list of clauses where the literal is watched, to obtain constant time removal and insertion of clauses.

Adapt src/arrays.ml into src/twl.ml implementing this technique. You should notice a significant speedup, although the resulting prover should still be around 250 times slower than minisat, as indicated by make test.

Literal selection heuristics

To further improve performance, you can explore the impact of different literal selection heuristics. You might consider random literal selection, as well as some of the classic heuristics such as MAXO, MOMS, MAMS, etc. They are defined, for example, here.

Tips

Keep your solvers simple

Do not implement more than what I ask: this means more work but also more opportunities for errors. For your information, I have 124 lines for my arrays solver, and 291 for twl. Both files are self-contained, in particular this line count includes the doubly-linked lists for twl.

Do one thing at a time, then test

It will be easier to debug your code if you change one thing at a time, and test each modification. For instance, avoid changing the variable selection heuristic when changing the naive prover into arrays. This way you can compare the two provers and check that nothing changes besides performance (you may instrument your provers with debug messages to compare the execution traces of two provers on some increasingly complex examples).

Do not debug using make

If you encounter a problem, running for example make PROBLEM=problems/1/flake4hv PENALTY=1 test_pingouins, first identify which program triggers the problem (make runs several program one after the other in such targets). If it's minisat it means that your problem encoder produces an ill-formed output. Otherwise, it's one of your programs: focus on debugging its execution; but don't forget to run make each time you run it again to test modifications (make && ... is your friend).

How to debug when you get an exception

You need a backtrace, it'll help a lot. Run again the OCaml program with OCAMLRUNPARAM=b in the environment. You may also need to recompile with a modified Makefile: change the compiler definition to OCAMLOPT = ocamlopt -I src -g, then make clean and recompile everything.