Exercise 6: Rebuilding the Cubic Incomplete SAT solver

Overview

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.

Learning Objectives

Getting Started

You will need a few documents to get started.

A short demo:

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       = + 

What to do

  1. Experiment with the linear solver. Work some simple examples from SATExamples. Use the functions
  2. Build some small examples of your own. Try to build examples that
    1. Are satisfiable and linear can solve
    2. Are satisfiable, but linear cannot solve
    3. Are not satisfiable, but linear cannot detect a contradiction
    4. Are not satisfiable and linear can discover they are unsatisfiable.
  3. 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.
  4. 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.
  5. 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.
  6. 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?
  7. 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?
  8. Advanced: Please fix all the bugs! (I've fixed all that I've found; but I suspect there may be more out there)
  9. Advanced: Reimplement the algorithm more naturally as a functional program.

What to turn in.

Back to the class web-page.
Back to the Course Schedule.