CMPS240, Spring 2013, Section 01: SAT stuff

Logic Exercises:

http://www.cl.cam.ac.uk/teaching/1112/DiscMathI/exercises.pdf

 

 

 

Topics to know for final:

       1. SAT Matrix

       2.    0-1 Rule: For a matrix to be unsatisfiable it must have a row with no 0s in it and a row

              (possibly the same)          with no 1s in it.

 

        3. Davis Putnam Algorithm

  

        4. Pure Literal (column with no 0 or no 1)

 

        5. Unit Clause (row with only one variable)

 

        6. Subsumption.      For example:

                         *00*

                         *001    Therefore can eliminate first row!

        7. Solutions killed:

                      for example:   001** kills 4 solutions. Namely: 110**

          8.   Walkthru algorithm (clause by clause greedily winging it LOL)

 

           9.   Subtraction algorithm (see Harrison)

          10.  BOOLEAN SPACE iff  UNSAT    <---- Major result...

             11. RESOLUTION:    deriving an empty clause produces a contradiction (shows Matrix is UNSAT).   EXAMPLES:

                   100*0   and 1**11 generate: 1001*

                        *1***** AND *0***** PROVES unsat!

               (some resulutions are lossy - some are lossless - we will always emply lossless resolution)

                12. Walksub .   A combination of walkthru and subtraction!

                                  (subtract the first clause we fail at - rinse, use the firsta available partial

                                   solution, rinse and repeat).

                     13.  Factoring and BCXF

 

                     14.  Existential Graphs for Propositional Logic

 

                           15. SAT paper:

http://www.louis-coder.com/P_NP_Problem_solved/P_NP_Problem_solved.htm