CMPS240, Spring 2013, Section 01: SAT stuff

Logic Exercises:




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:


                         *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: