- fn run(clauses: &Clauses) {
let mut state = DpllState::Running(Vec::new(), Assignment::new(), clauses.clone()); loop {
- match &state {
- DpllState::Unsat => {
- println!("UNSAT"); break;
} DpllState::Sat(trail) => {
println!("SAT {:?}", trail);
// Generate a complete assignment let max_var = clauses.iter().flat_map(|cl| cl.iter()).map(|&x| x.abs()).max().unwrap_or(0); let mut complete_assignment: Assignment = trail.iter().filter_map(|entry| {
- match entry {
- TrailEntry::Decision(lit) | TrailEntry::Propagated(lit) => Some((lit.abs(), *lit > 0)),
}
}).collect();
// Print all variables up to the max_var for var in 1..=max_var {
let value = complete_assignment.get(&var).cloned().unwrap_or(false); println!("Variable {}: {}", var, value);
}
break;
} _ => {
println!("{:?}", state); state = step(state); println!("⇒");
}
}
}
}
- fn main() {
- let clauses: Clauses = [
- vec![1, 2, 3], vec![-1, 2], vec![-2, 3, 4], vec![-3, -4, 5], vec![1, -5], vec![-1, -3, -5], vec![2, 4, -5], vec![-1, -2, -3, -4, -5],
] .into_iter() .collect();
run(&clauses);
}