SC Chapter 3 SAT Solving

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

A counter for decisions

The unit clause implying the value of l // nil if decision

1. Large effort to watch each literal in each clause of each propagation

2. Instead watch two literals for each clause such that one of them is true or both unassigned

1. If l gets assigned update clause(\neg l, k)

2. If k is true then clause is satisfied

3. Else if k is false then replace k by other literal k’

4. Else if k is unassigned then clause is unit

5. Else clause is unsatisfied

1. labeled directed acyclic with G=(V,E,L)

2. V is set of currently assigned variables and conflict node kappa

3. L is labeling function assigning to each node (var=v@DL) and kappa for node kappa

4. E is set of edges that unit clauses imply other assignments and to node kappa for conflicting clause

1. Asserting clause has one literal from the current DL // considered by modern solvers

2. The clause obtained by applying resolution on the conflicting clauses of the decision level

A node reached by all paths from the decision node // first UIP is closest to the conflict

1. Add asserting clause to clause set // Not necessary for completeness

2. Backtrack to second highest DL (dl) in the asserting clause without erasing

The formula is unsatisfiable

1. Original set of clauses is a core

2. Set of clauses used for resolution in CA // not minimal

3. Small set of clauses via resolution graph

“It is never the case that the solver enters decision level dl again with the same partial assignment.”

1. If BCP not possible return UNSAT

2. Loop { If decision not possible return SAT // satisfiable assignment found

3. While BCP not possible // conflict found

4. If conflict not resolvable return UNSAT } <---

1. Clear trail of all assignments

2. If BCP not possible return UNSAT

3. Loop { If decision not possible return SAT // satisfiable assignment found

4. While BCP not possible // conflict found

5. If backtrack not possible return UNSAT } <---

1. While unit clauses available push assignment to trail

2. If one clause is unsatisfiable return false

3. Else return true

1. If all variables are assigned return false

2. Choose unassigned variable and push assignment to trail

3. return true

1. Loop { If trail is empty return false

2. Pop assignment from trail

3. If assignment unmodified change value and return true }

1. DPLL for search

2. CDCL for backtracking

3. Watching literals to enhance propagation

4. VSIDS as variable ordering heuristics with lexicographic order