|
|
@ -133,11 +133,13 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
133
|
133
|
|
|
134
|
134
|
loop {
|
|
135
|
135
|
if clauses.iter().all(|c| is_clause_satisfied(&vars, c.clone())) { // all clauses satisfied, success
|
|
|
136
|
//println!("satisfied");
|
|
136
|
137
|
return Some(vars.clone())
|
|
137
|
138
|
} else if clauses.iter().any(|c| is_clause_conflict(&vars, c.clone())) { // a conflict exists, backtrack
|
|
138
|
139
|
match stack.pop() {
|
|
139
|
140
|
None => return None, // nothing to backtrack, no solution found
|
|
140
|
141
|
Some((v, b)) => {
|
|
|
142
|
//println!("backtrack! {}", v);
|
|
141
|
143
|
vars.clone_from(&b);
|
|
142
|
144
|
vars.insert(v);
|
|
143
|
145
|
}
|
|
|
@ -146,6 +148,7 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
146
|
148
|
let cs = clauses.clone();
|
|
147
|
149
|
let clause = cs.iter().find(|&c| is_clause_unit(&vars, c.clone())).unwrap();
|
|
148
|
150
|
let unknown = *clause.iter().find(|&v| is_unknown(&vars, *v)).unwrap();
|
|
|
151
|
//println!("propagate {} from {:?}", unknown, clause);
|
|
149
|
152
|
vars.insert(unknown);
|
|
150
|
153
|
} else { // none of the above, decide (guess) an unknown variable
|
|
151
|
154
|
let mut unknown: Var = 0;
|
|
|
@ -163,6 +166,7 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
163
|
166
|
}
|
|
164
|
167
|
assert!(unknown != 0);
|
|
165
|
168
|
stack.push((unknown, vars.clone()));
|
|
|
169
|
//println!("decide {}", -unknown);
|
|
166
|
170
|
vars.insert(-unknown);
|
|
167
|
171
|
}
|
|
168
|
172
|
}
|