|
|
|
|
|
|
145
|
}
|
145
|
}
|
|
146
|
}
|
146
|
}
|
|
147
|
} else if clauses.iter().any(|c| is_clause_unit(&vars, c)) { // a unit clause exists, propagate
|
147
|
} else if clauses.iter().any(|c| is_clause_unit(&vars, c)) { // a unit clause exists, propagate
|
|
148
|
let cs = clauses.clone();
|
|
|
|
149
|
let clause = cs.iter().find(|&c| is_clause_unit(&vars, c)).unwrap();
|
|
|
|
|
|
148
|
let clause = clauses.iter().find(|&c| is_clause_unit(&vars, c)).unwrap();
|
|
150
|
let unknown = *clause.iter().find(|&v| is_unknown(&vars, *v)).unwrap();
|
149
|
let unknown = *clause.iter().find(|&v| is_unknown(&vars, *v)).unwrap();
|
|
151
|
//println!("propagate {} from {:?}", unknown, clause);
|
150
|
//println!("propagate {} from {:?}", unknown, clause);
|
|
152
|
vars.insert(unknown);
|
151
|
vars.insert(unknown);
|
|
153
|
} else { // none of the above, decide (guess) an unknown variable
|
152
|
} else { // none of the above, decide (guess) an unknown variable
|
|
154
|
let mut unknown: Var = 0;
|
153
|
let mut unknown: Var = 0;
|
|
155
|
for c in clauses.clone() {
|
|
|
|
|
|
154
|
for c in &clauses {
|
|
156
|
match c.iter().find(|&v| is_unknown(vars, *v)) {
|
155
|
match c.iter().find(|&v| is_unknown(vars, *v)) {
|
|
157
|
Some(&u) => { unknown = u; break }
|
156
|
Some(&u) => { unknown = u; break }
|
|
158
|
None => continue
|
157
|
None => continue
|