7July_22_2008 Chaff: Engineering an Efficient SAT solver
http://citeseer.ist.psu.edu/moskewicz01chaff.html

1. INTRODUCTION
Boolean Satisfiability (SAT) consists of determining a sat. var assignment, V for a Boolean function f, or that no V exists
(NP-complete)
many practical app domains EDA, and AI
practical sat solvers much research
GRASP, POSIT, SATO, rel_sat, WalkSAT
Two main strategies
1. davis-putname (DP) backtrack search
2. heuristic local search

heuristic local searches not guaranteed to find sat assignment if one exists or prove no existence, so most based on DP

start w/ CNF form,
DP serach :
while (true) {
    if (!decide()) // if no unassigned vars
        return(satisifiable);
    while (!bcp()) {
        if (!resolveConflict())
        return(not satisfiable);
    }
}
bool resolveConflict() {
    d = most recent decision not ‘tried both ways’;
    if (d == NULL) // no such d was found
        return false;
    flip the value of d;
    mark d as tried both ways;
    undo any invalidated implications;
    return true;n
}

decide() --select var not assigned and assign it (decision)
bcp()---identify any var assignments required by curr state to satisfy f. (every clause must be sat, for f to be sat)
  implication-var is set to 1
  conflict--same var both 1 and 0
  decision level (DL) height of decision stack at time of implication


...



2. OPTIMIZED BCP
problem is 90% of time spent in BCP (boolean constraint Propagation)
thus need efficient BCP
...
...