104 lines
3.5 KiB
Markdown
104 lines
3.5 KiB
Markdown
# 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: ![[backjump.png]]
|
|
- 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
|
|
|