In this exercise you will build a cubic (incomplete) SAT solver. You will start with a redacted version of a SAT solver that was built to animate the algorithms for the notes. A few key elements of the program have been replaced with "undefined". Your task is to develop sufficient understanding of the algorithm and the code to replace the undefineds with real values. If you are successful the end result should be a working instance of the "cubic" algorithm from the text.

- Gain mastery of the abstract algorithms in the linear and cubic solvers
- Experiment with a small implementation of the solvers.

You will need a few documents to get started.

- Read HR Section 1.6 about the linear and cubic algorithms
- Read outline.pdf section 6
- Download the files DAG.hs, SATRedacted.hs, and SATExamples.hs

Fire up ghci and load the SATExamples module:

bash-3.2$ ghci GHCi, version 6.10.4: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. Prelude> :l SATExamples.hs [1 of 5] Compiling Prop ( Prop.hs, interpreted ) [2 of 5] Compiling Examples ( Examples.hs, interpreted ) [3 of 5] Compiling DAG ( DAG.hs, interpreted ) [4 of 5] Compiling SATRedacted ( SATRedacted.hs, interpreted ) [5 of 5] Compiling SATExamples ( SATExamples.hs, interpreted ) Ok, modules loaded: SATExamples, SATRedacted, DAG, Examples, Prop.

Set up the state machine to run the linear algorithm on ex1_48:

*SATExamples> setUpLinear ex1_48 Loading package syb ... linking ... done. Loading package array-0.2.0.0 ... linking ... done. Loading package containers-0.2.0.1 ... linking ... done. Loading package pretty-1.0.1.0 ... linking ... done. State = Working Forcing 1 8 0 /\ 7 7 ~ 6 8 6 ~ 5 7 5 2 /\ 4 6 4 ~ 3 5 3 ~ 0 4 2 ~ 1 5 1 q 2 0 p 8,3

This displays a SAT state with an empty history.

Next use the step debugging interface on the previous value (known by ghci as it):

*SATExamples> step it State = Working Forcing 2 8 0 /\ 7 TT 7 ~ 6 8 6 ~ 5 7 5 2 /\ 4 6 4 ~ 3 5 3 ~ 0 4 2 ~ 1 5 1 q 2 0 p 8,3

This has marked the root.

You can blast through multiple steps at a time with the function steps:

*SATExamples> steps 10 it State = Working 8 0 /\ 7 TT 7 ~ 6 8 T T 6 ~ 5 7 F F 5 2 /\ 4 6 T T 4 ~ 3 5 T T 3 ~ 0 4 F F e 2 ~ 1 5 T T 1 q 2 F F 0 p 8,3 T T =

Now we can select different fragments of history for display with the ppSAT command.

Before we do anything else, it is helpful to name this result:

*SATExamples> let foo = it

We can use ppSAT to look at the last 5 steps as follows:

*SATExamples> ppSAT (-5) 0 foo State = Working 8 0 /\ 7 T 7 ~ 6 8 T 6 ~ 5 7 F 5 2 /\ 4 6 T 4 ~ 3 5 T T 3 ~ 0 4 F F e 2 ~ 1 5 T 1 q 2 FF 0 p 8,3 T =

Note that starting with a negative number indexes from the end of the computation.

Alternatively we can look at the first 5 steps of the computation:

*SATExamples> ppSAT 0 5 foo State = Working 8 0 /\ 7 TT 7 ~ 6 8 T T 6 ~ 5 7 F F 5 2 /\ 4 6 T T 4 ~ 3 5 T 3 ~ 0 4 F 2 ~ 1 5 T 1 q 2 F 0 p 8,3 T T

We can even view a segment from the middle:

*SATExamples> ppSAT 3 6 foo State = Working 8 0 /\ 7 T 7 ~ 6 8 T 6 ~ 5 7 FF 5 2 /\ 4 6 T T 4 ~ 3 5 T 3 ~ 0 4 F 2 ~ 1 5 T T 1 q 2 F 0 p 8,3 T

Finally, if we wish to run the algorithm to completion, we can step it forward indefinitely with itStep:

*SATExamples> itStep foo State = Satisfiable 8 0 /\ 7 TT + 7 ~ 6 8 T T + 6 ~ 5 7 F F + 5 2 /\ 4 6 T T + 4 ~ 3 5 T T + 3 ~ 0 4 F F e+ 2 ~ 1 5 T T + 1 q 2 F F + 0 p 8,3 T T = +

- Experiment with the linear solver. Work some simple examples from SATExamples. Use the functions
- setUpLinear
- step
- steps
- ppSAT
- Build some small examples of your own. Try to build examples that
- Are satisfiable and linear can solve
- Are satisfiable, but linear cannot solve
- Are not satisfiable, but linear cannot detect a contradiction
- Are not satisfiable and linear can discover they are unsatisfiable.

- Study the code in SATRedacted.hs. Search for undefined. Using your knowledge of the abstract algorithm from HR and class notes, try to reconstruct the missing bits. As you get some bits replaced, you should be able to explore the consequences with the debugging interface and animations. It is ok to do this step in small groups. Please try to reason out the solution.
- Revisit some of the examples you did for part 2 with the cubic solver. Build some examples that the cubic solver can solve but linear cannot, and some that cannot be solved by cubic.
- Experiment on a few larger examples by connecting this to the Finite Set module. My version of cubic could solve the four queens problem, but failed on the graph coloring problem. It took a long time to not solve the graph coloring problem.
- Advanced: Make the code better ;-) Can you improve the control strategy to make it stop quicker without missing any solutions? Can you find ways to make the code run faster?
- Advanced: Do you have any algorithmic ideas for how to solve problems where the cubic algorithm gives up? Can you develop a strategy that solves ex4?
- Advanced: Please fix all the bugs! (I've fixed all that I've found; but I suspect there may be more out there)
- Advanced: Reimplement the algorithm more naturally as a functional program.

- Create a named subfolder of Ex6 with your examples and reconstituted solver.
- Be prepared to talk about your solution in class.

Back to the Course Schedule.