Lesson Plan 9/18/2008
Conversion to CNF; DPLL; Clause learning

**************************************************************
Conversion to CNF

Why CNF?
- easy to process algorithmically
	- Proof: single rule, resolution
	- Walksat: count # satisfied clauses to get estimate of distance to solution
	- Davis-Putnam-Loveland-Logman DPLL Procedure:
		backtracking search for model finding
		clausal form makes it easy to *simplify* the formula on fly, prune
			the search space by *unit propagation*

****************************************************************
Conversion to CNF:
1. Move in NOT, flipping AND and OR
2. Apply DISTRIBUTIVE LAW 

EXAMPLE

Problem: explosion in size of formula.  Worst case: exponential!

Alternative method: introduce new variables

1. Move in NOT, flipping AND and OR, call result F
	PROCESS( F )

PROCESS( F ):
1. Flatten nested ANDs and nested ORs in F.

2. If top level is AND: F1 & F2 & ...
  Process each conjunct separately.
	RETURN( PROCESS(F1) & PROCESS(F2) & ... )

3. If top level is OR:  F1 v F2 v ...
  3A.  If all the Fi are literals, you have a single clause: 
	RETURN( F1 v F2 v ... )
  3B.  Otherwise: create new propositions G1, G2, ... to 
	represent each disjunct.
	RETURN( (G1 v G2 v ...) & 
		DISTRIBUTE( ~G1, PROCESS(F1) ) &
		DISTRIBUTE( ~G2, PROCESS(F2) ) & ... )

DISTRIBUTE( LITERAL, CNF ):
/* Add LITERAL as an additional disjunct in each clause in
   a formula which is already in CNF form. */
   Where CNF is (C1 & C2 & ...)
     return ((LITERAL v C1) & (LITERAL v C2) & ...)



****************************************************************

DPLL

*** See PDF Slides ***

Go through basic backtrack search over space of partial assignments

Extend to unit propagation

Add clause learning

****************************************************************

Progress

Progress of solvers

SAT competition