SC Chapter 3 SAT Solving

1. Decision as enumeration

2. Boolean constraint propagation (BCP)

3. Conflict resolution and backtracking

1. Assign values to all variables as (var, v, false)

2. If all clauses satisfy return SAT // Order of variables and values influences runtime

3. Else change the latest false variable assignment to (var, \neg v, true)

4. If no variable assignment is left return UNSAT

1. Static variable order // x < y < z

2. Static value order // true < false

3. Influences runtime of SAT formulae

4. Does not influence runtime of UNSAT formulae

1. Dynamic largest individual sum (DLIS), 2. Jerosolow-Wang method and 3. Variable state independent decaying sum (VSIDS)

1. Cx is number of unresolved clauses for positive x

2. C\negx is number of unresolved clauses for negative x

3. Choose x as max Cx and y as max C\negy

4. Choose x as true if Cx>C\negy otherwise y as false

5. Requires O(#literals) queries for each decision

6. O(2^n *n*m*k) with n #var, m #clauses and k #litPerClause

1. Compute J(l) = Sum_(l \in c, c \in phi) 2^(-|c|) for all literals l with clause c and |c| number of literals in c // Sum of all clauses where the literal l appears

2. Choose maximizing l

3. Literals in shorter clauses have higher weight

1. Watch variables used in recent clauses used for conflict resolution // Conflict driven decision strategy

2. Static because does not depend on current assignment

3. Dynamic because it gradually changes

4. Count for every variable by increasing increment value

5. Choose unassigned variable with the highest counter for decision // constant time

6. Periodically counters and increment value and counters are divided by constant

7. Chaff stores unassigned variables sorted by counter value

8. Update is only necessary when adding conflict clauses

1. satisfied if at least one literal is satisfied

2. unsatisfied if all literals are assigned but unsatisfied

3. unit if all but one literals are assigned but unsatisfied // imply consequences of decisions

4. unresolved if none of the other statuses