SAT-SOLVING-EXAMPREP/Solvers.md

Davis Putnam Procedure (DP)

while True:
	if [] in formula:
		return UNSAT
	//remove all variables that occur only in one phase
	vars = one_phased(formula)
	for var in vars:
		for clause in formula:
			if var in formula:
				remove(clause)
	
	var = decide(formula)
	
	// Add non trivial resolvants
	formula += resolution(var, formula)
	
	for clause in formula:
			if var in formula:
				remove(clause)

	if formula is []:
		return SAT

• Notice that

  • Adding a resolvant always preservers SAT (resolution rule)

  • Adding any clause always preserves UNSAT

  • Removing any clause always preserves SAT

  • Removing a clause containing a 'one phase variable' preserves UNSAT (reverse of resolution rule)

Davis Putnam Logemann Loveland DPLL

Boolean Constraint Propagation (BCP)

• Given a unit clause l

1. Remove all subsumed clauses, i.e. C where l \in C
2. Remove \lnot l from all C (which contain it) [Unit Prop](SAT_in_general#Special Case Unit Resolution)

def dpll(formula):
	if [] in formula:
		return UNSAT
		vars = one_phased(formula)
	for var in vars:
		for clause in formula:
			if var in formula:
				remove(clause)
	if formula is []:
		return SAT
		
	var = decide()
	if dpll(formula + [var]) == SAT:
		return SAT
	return dpll(formula + [-var])

• Correct because of theorem of Shanon
• f(x) = (x \land f(1)) \lor (\overline x \land f(0))

Backjumping

• If some conflict has been derived without using specific assignments/ decision
• We can skip over that decision when flipping: !
• If conflict stems from for example from (1 2) (1 -2)
• Removes 'bad decisions'/ 'useless' from the trail
• Can reduce search space from exponential to quadratic in number of bad decisions
  • Whatever that means

CDCL

• DPLL with learning
• On conflict, learn a conflict clause which will help in further exploration
  • Usually the first UIP of the [implication graph](SAT_in_general#Implication Graph) is used as conflict clause
• After learning a conflict:
  • Back-jump to the lowest level in the implication graph supporting the UIP
  • Assign negated UIP literal
  • this is why first UIP is good (“pulls in” as few decision levels as possible)

Reduction

• Not all clauses are useful forever
  • Useless via Subsumption, or trivially satisfied by units
• Try to reduce the amount of clauses you need to consider in BCP
• Schedule throwing away clauses
  • geometric, Luby, arithmetic scheme
• Consider various heuristics
  • Size
  • Last Recently Used (LRU),
  • Clause Move To Front (CMTF)
  • Clause Scores similar to VSIDS
  • Glucose/ Literal Block Distance (LBD)
    • LBD = number of distinct decision levels among a (learned) clause's literals
    • Low LBD ("glue clause"): literals tightly related across few levels -> likely useful, keep
    • High LBD: literals span many levels, weakly related -> good deletion candidate
  • Used flag

Restarts

• Schedule restarts every so often can improve performance
• Throw away the trail
• Keep (most) learned clauses, phase saving, other state
• Idea:
  • The solver might have zoomed in on an efficient part of the search space
    • For SAT instances might stuck in a UNSAT part
    • For UNSAT instances might miss a shorter proof
  • Avoid going down the same path by keeping what was learned
    • Clauses, phase saving, variable scoring

Phase saving

• Whenever assigning a variable, save the phase it is assigned
• When deciding on a variable assign the saved phase
• Idea: Go down the right branch of the search tree