Skip to content

Commit

Permalink
Detect all conflicts on Engine::check_solution
Browse files Browse the repository at this point in the history
  • Loading branch information
Dekker1 committed Nov 19, 2024
1 parent 1669e2b commit 180cf56
Showing 1 changed file with 16 additions and 14 deletions.
30 changes: 16 additions & 14 deletions crates/huub/src/solver/engine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -324,20 +324,22 @@ impl PropagatorExtension for Engine {
}

// Run propgagators to find any conflicts
ctx.run_propagators(&mut self.propagators);
// No propagation can be triggered (all variables are fixed, so only
// conflicts are possible)
debug_assert!(self.state.propagation_queue.is_empty());

// Process propagation results, and accept model if no conflict is detected
let accept = if let Some(conflict) = self.state.conflict.clone() {
// Move conflict to clauses before backtrack
self.state.clauses.push_back(conflict);
false
} else {
true
};

let mut accept = true;
loop {
ctx.run_propagators(&mut self.propagators);
// No propagation can be triggered (all variables are fixed, so only
// conflicts are possible)
debug_assert!(ctx.state.propagation_queue.is_empty());
// Process propagation results, and accept model if no conflict is
// detected
if let Some(conflict) = ctx.state.conflict.take() {
// Move conflict to clauses before backtrack
ctx.state.clauses.push_back(conflict);
accept = false;
} else {
break;
};
}
// Revert to real decision level
self.state.notify_backtrack::<true>(level as usize, false);

Expand Down

0 comments on commit 180cf56

Please sign in to comment.