|
|
@ -153,15 +153,9 @@ pub fn dpll(clauses: Vec<Clause>) -> Option<BoundVars> {
|
|
153
|
153
|
} else { // none of the above, decide (guess) an unknown variable
|
|
154
|
154
|
let mut unknown: Var = 0;
|
|
155
|
155
|
for c in clauses.clone() {
|
|
156
|
|
for v in c {
|
|
157
|
|
if is_unknown(vars, v) {
|
|
158
|
|
unknown = v;
|
|
159
|
|
break;
|
|
160
|
|
}
|
|
161
|
|
}
|
|
162
|
|
|
|
163
|
|
if unknown != 0 {
|
|
164
|
|
break;
|
|
|
156
|
match c.iter().find(|&v| is_unknown(vars, *v)) {
|
|
|
157
|
Some(&u) => { unknown = u; break }
|
|
|
158
|
None => continue
|
|
165
|
159
|
}
|
|
166
|
160
|
}
|
|
167
|
161
|
assert!(unknown != 0);
|