From 405e00165cc133456b245b3724c606d3e5caa6a9 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 19 Nov 2024 13:31:24 +1100 Subject: [PATCH] Detect all conflicts on `Engine::check_solution` --- crates/fzn-huub/corpus/jobshop_la02.sol | 2 +- crates/fzn-huub/corpus/jobshop_la03.sol | 2 +- crates/fzn-huub/corpus/jobshop_la04.sol | 2 +- crates/huub/src/solver/engine.rs | 30 +++++++++++++------------ 4 files changed, 19 insertions(+), 17 deletions(-) diff --git a/crates/fzn-huub/corpus/jobshop_la02.sol b/crates/fzn-huub/corpus/jobshop_la02.sol index 020c1ef2..d64be3ab 100644 --- a/crates/fzn-huub/corpus/jobshop_la02.sol +++ b/crates/fzn-huub/corpus/jobshop_la02.sol @@ -1,2 +1,2 @@ objective = 655; -start = [0,20,400,450,572,0,25,57,81,107,0,72,95,123,236,95,229,305,448,510,39,81,188,236,354,162,275,402,483,510,66,305,335,493,589,99,181,275,433,526,25,373,448,498,600,123,195,317,354,573]; +start = [0,20,345,453,573,0,25,57,84,126,0,72,95,136,207,95,232,308,461,510,67,94,306,386,403,165,288,405,483,511,39,72,107,506,590,102,194,288,433,529,25,386,461,511,600,123,195,308,354,586]; diff --git a/crates/fzn-huub/corpus/jobshop_la03.sol b/crates/fzn-huub/corpus/jobshop_la03.sol index 7f25504a..16347d4e 100644 --- a/crates/fzn-huub/corpus/jobshop_la03.sol +++ b/crates/fzn-huub/corpus/jobshop_la03.sol @@ -1,2 +1,2 @@ objective = 597; -start = [0,79,376,458,542,0,23,91,295,397,21,59,336,490,545,0,37,124,228,340,238,295,379,447,548,101,200,290,404,515,0,59,109,352,479,37,61,458,493,580,182,279,286,340,440,61,145,542,578,588]; +start = [0,79,376,458,542,0,23,91,311,397,21,59,295,490,545,0,37,124,228,340,238,295,379,447,548,101,200,290,404,515,0,59,109,352,479,37,61,458,493,580,182,279,286,340,440,61,145,542,578,588]; diff --git a/crates/fzn-huub/corpus/jobshop_la04.sol b/crates/fzn-huub/corpus/jobshop_la04.sol index d998ef08..c7d3eda8 100644 --- a/crates/fzn-huub/corpus/jobshop_la04.sol +++ b/crates/fzn-huub/corpus/jobshop_la04.sol @@ -1,2 +1,2 @@ objective = 590; -start = [0,304,398,490,581,0,19,30,452,473,19,33,113,207,432,135,230,323,384,450,33,107,113,308,398,30,115,170,296,397,230,309,418,490,581,78,166,246,384,482,0,96,108,170,294,61,202,235,294,330]; +start = [0,304,398,490,581,0,19,30,432,476,19,33,113,202,453,61,235,329,384,450,33,107,113,314,398,30,156,176,301,397,230,309,424,490,581,78,166,252,389,487,0,96,108,170,294,176,230,235,294,336]; diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 597204b4..af962294 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -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::(level as usize, false);