diff --git a/Cargo.lock b/Cargo.lock index d912b678f..cf31f1139 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -30,7 +30,22 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a" dependencies = [ "anstyle", - "anstyle-parse", + "anstyle-parse 0.2.7", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + +[[package]] +name = "anstream" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" +dependencies = [ + "anstyle", + "anstyle-parse 1.0.0", "anstyle-query", "anstyle-wincon", "colorchoice", @@ -53,6 +68,15 @@ dependencies = [ "utf8parse", ] +[[package]] +name = "anstyle-parse" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e" +dependencies = [ + "utf8parse", +] + [[package]] name = "anstyle-query" version = "1.1.5" @@ -246,7 +270,7 @@ version = "4.5.57" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7b12c8b680195a62a8364d16b8447b01b6c2c8f9aaf68bee653be34d4245e238" dependencies = [ - "anstream", + "anstream 0.6.21", "anstyle", "clap_lex", "strsim", @@ -603,11 +627,11 @@ dependencies = [ [[package]] name = "env_logger" -version = "0.11.9" +version = "0.11.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2daee4ea451f429a58296525ddf28b45a3b64f1acf6587e2067437bb11e218d" +checksum = "0621c04f2196ac3f488dd583365b9c09be011a4ab8b9f37248ffcc8f6198b56a" dependencies = [ - "anstream", + "anstream 1.0.0", "anstyle", "env_filter", "jiff", @@ -1671,9 +1695,9 @@ checksum = "92ecc6618181def0457392ccd0ee51198e065e016d1d527a7ac1b6dc7c1f09d2" [[package]] name = "jiff" -version = "0.2.20" +version = "0.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c867c356cc096b33f4981825ab281ecba3db0acefe60329f044c1789d94c6543" +checksum = "1a3546dc96b6d42c5f24902af9e2538e82e39ad350b0c766eb3fbf2d8f3d8359" dependencies = [ "jiff-static", "jiff-tzdb-platform", @@ -1686,9 +1710,9 @@ dependencies = [ [[package]] name = "jiff-static" -version = "0.2.20" +version = "0.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f7946b4325269738f270bb55b3c19ab5c5040525f83fd625259422a9d25d9be5" +checksum = "2a8c8b344124222efd714b73bb41f8b5120b27a7cc1c75593a6ff768d9d05aa4" dependencies = [ "proc-macro2", "quote", @@ -2133,6 +2157,7 @@ dependencies = [ name = "pumpkin-conflict-resolvers" version = "0.3.0" dependencies = [ + "pumpkin-checking", "pumpkin-core", ] @@ -2192,7 +2217,7 @@ dependencies = [ "clap", "clap-verbosity-flag", "drcp-format", - "env_logger 0.11.9", + "env_logger 0.11.10", "escargot", "flate2", "fzn-rs", diff --git a/clippy.toml b/clippy.toml index db93913b0..b66be827f 100644 --- a/clippy.toml +++ b/clippy.toml @@ -4,4 +4,6 @@ allowed-duplicate-crates = [ "windows-sys", "regex-syntax", "regex-automata", + "anstream", + "anstyle-parse" ] diff --git a/pumpkin-crates/checking/src/variable_state.rs b/pumpkin-crates/checking/src/variable_state.rs index 07cb1d253..9167b0ab9 100644 --- a/pumpkin-crates/checking/src/variable_state.rs +++ b/pumpkin-crates/checking/src/variable_state.rs @@ -31,6 +31,10 @@ impl VariableState where Atomic: AtomicConstraint, { + pub fn reset_domain(&mut self, identified: Atomic::Identifier) { + let _ = self.domains.insert(identified, Domain::all_integers()); + } + /// Create a variable state that applies all the premises and, if present, the negation of the /// consequent. /// @@ -308,9 +312,11 @@ impl Domain { self.upper_bound = IntExt::Int(bound); - // Note the '+ 1' to keep the elements <= the upper bound instead of < - // the upper bound. - let _ = self.holes.split_off(&(bound + 1)); + if bound < i32::MAX { + // Note the '+ 1' to keep the elements <= the upper bound instead of < + // the upper bound. + let _ = self.holes.split_off(&(bound + 1)); + } // Take care of the condition where the new bound is already a hole in the domain. if self.holes.contains(&bound) { diff --git a/pumpkin-crates/conflict-resolvers/Cargo.toml b/pumpkin-crates/conflict-resolvers/Cargo.toml index de3438062..0a8c57cc4 100644 --- a/pumpkin-crates/conflict-resolvers/Cargo.toml +++ b/pumpkin-crates/conflict-resolvers/Cargo.toml @@ -12,3 +12,4 @@ workspace = true [dependencies] pumpkin-core = { version = "0.3.0", path = "../core" } +pumpkin-checking = { version = "0.3.0", path = "../checking" } diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs new file mode 100644 index 000000000..72b8ac617 --- /dev/null +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -0,0 +1,281 @@ +use pumpkin_checking::IntExt; +use pumpkin_checking::VariableState; +use pumpkin_core::conflict_resolving::ConflictAnalysisContext; +use pumpkin_core::containers::KeyedVec; +use pumpkin_core::containers::StorageKey; +use pumpkin_core::predicate; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateType; +use pumpkin_core::propagation::ReadDomains; +use pumpkin_core::variables::DomainId; + +/// A minimiser which iteratively applies rewrite rules based on the semantic meaning of predicates +/// *during* conflict analysis. +/// +/// The implementation is heavily inspired by \[1\]. +/// +/// There are a couple of limitations to note: +/// - Currently, whenever a hole is created at a lower- or upper-bound, the bound is only moved by 1 +/// (even if there are multiple holes which could cause a higher lower-bound). This simplifies a +/// lot of the logic. +/// - Currently, it is unclear how the rules are applied in \[1\]. This means that certain rules are +/// invalid (for, as of yet, unknown reasons), for example, removing all other elements concerning +/// `x` when `[x = v]` is added leads to wrong solutions. +/// - This leads to another slightly nuanced point; which is that when an element is removed from +/// the nogood, it could be that there are other bounds which should be restored. +/// +/// For example, it could be that the nogood contains (among others) the predicates `[x >= v]` +/// and `[x = v + 1]`. In this case, once `[x = v + 1]` gets removed, the lower-bound should be +/// moved back to `v`. +/// +/// ## Developer Notes +/// - The predicates from the previous decision level should also be added to the +/// [`IterativeMinimiser`]; this is due to the fact that they are not guaranteed to be +/// semantically minimised away. +/// +/// Imagine the situation where we have `[x >= v]` from a previous +/// decision level and `[x >= v']` from the current decision level (where `v' > v`). If we then +/// do not process `[x >= v]`, then it would get added to the nogood directly rather than removed +/// due to redundancy. If we now resolve on [`x >= v'`] and the nogood becomes asserting, then +/// there are no other elements over `x` and the predicate from the previous decision level does +/// not get removed. +/// +/// # Bibliography +/// \[1\] T. Feydy, A. Schutt, and P. Stuckey, ‘Semantic learning for lazy clause generation’, in +/// TRICS workshop, held alongside CP, 2013. +#[derive(Debug, Clone, Default)] +pub(crate) struct IterativeMinimiser { + /// Keeps track of the domains induced by the current working nogood. + state: VariableState, + domains: KeyedVec>, +} + +/// The result of processing a predicate, indicating its redundancy. +#[derive(Debug, Clone)] +pub(crate) enum ProcessingResult { + /// The predicate to process was redundant. + Redundant, + /// The predicate to process was not redundant, and it replaced + /// [`ProcessingResult::ReplacedPresent::removed`]. + /// + /// e.g., [x >= 5] can replace [x >= 2]. + ReplacedPresent { removed: Vec }, + /// The predicate to process was replaced with + /// [`ProcessingResult::PossiblyReplacedWithNew::new_predicate`] and it also removed + /// [`ProcessingResult::PossiblyReplacedWithNew::removed`]. + /// + /// Note that it is not always possible to replace with `new_predicate` (since it can lead to + /// infinite loops), so it is not guaranteed that `new_predicate` is added. + /// + /// e.g., if [x >= 5] is in the nogood, and the predicate [x <= 5] is added, then [x >= 5] is + /// removed and replaced with [x == 5] (and [x <= 5] is not added). + PossiblyReplacedWithNew { + removed: Predicate, + new_predicate: Predicate, + }, + /// The predicate was found to be not redundant. + NotRedundant, +} + +impl IterativeMinimiser { + /// Removes the given predicate from the nogood. + pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { + let domain = predicate.get_domain(); + if let Some(to_remove_position) = self.domains[domain] + .iter() + .position(|element| *element == predicate) + { + let _ = self.domains[domain].remove(to_remove_position); + } + } + + /// Applies the given predicate from the nogood. + pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { + let domain = predicate.get_domain(); + self.domains.accomodate(domain, Default::default()); + self.domains[domain].push(predicate) + } + + /// Explains the lower-bound in the proof log. + fn explain_lower_bound_in_proof( + &self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) { + if context.is_proof_logging_inferences() { + let domain = predicate.get_domain(); + + if let IntExt::Int(lower_bound) = self.state.lower_bound(&domain) + && context.get_checkpoint_for_predicate(predicate!(domain >= lower_bound)) + == Some(0) + { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } + + for hole in self.state.holes(&domain) { + if context.get_checkpoint_for_predicate(predicate!(domain != hole)) == Some(0) { + context.explain_root_assignment(predicate!(domain != hole)); + } + } + } + } + + fn explain_upper_bound_in_proof( + &self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) { + if context.is_proof_logging_inferences() { + let domain = predicate.get_domain(); + + if let IntExt::Int(upper_bound) = self.state.upper_bound(&domain) + && context.get_checkpoint_for_predicate(predicate!(domain <= upper_bound)) + == Some(0) + { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } + + for hole in self.state.holes(&domain) { + if context.get_checkpoint_for_predicate(predicate!(domain != hole)) == Some(0) { + context.explain_root_assignment(predicate!(domain != hole)); + } + } + } + } + + /// Processes the predicate, indicating via [`ProcessingResult`] what can happen to it. + pub(crate) fn process_predicate( + &mut self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) -> ProcessingResult { + let domain = predicate.get_domain(); + if domain.index() >= self.domains.len() || self.domains[domain].is_empty() { + return ProcessingResult::NotRedundant; + } + self.domains.accomodate(domain, Default::default()); + + self.state.reset_domain(domain); + for predicate in self.domains[predicate.get_domain()].iter() { + let consistent = self.state.apply(predicate); + assert!(consistent) + } + + let lower_bound = self + .state + .lower_bound(&predicate.get_domain()) + .try_into() + .unwrap_or(i32::MIN); + let upper_bound = self + .state + .upper_bound(&predicate.get_domain()) + .try_into() + .unwrap_or(i32::MAX); + + // If the domain is assigned, then the added predicate is redundant. + // + // Encompasses the rules: + // - [x = v], [x != v'] => [x = v] + // - [x = v], [x <= v'] => [x = v] + // - [x = v], [x >= v'] => [x = v] + if lower_bound == upper_bound { + self.explain_lower_bound_in_proof(predicate, context); + self.explain_upper_bound_in_proof(predicate, context); + return ProcessingResult::Redundant; + } + + match predicate.get_predicate_type() { + PredicateType::LowerBound => { + if predicate.get_right_hand_side() == upper_bound { + self.explain_upper_bound_in_proof(predicate, context); + // [x <= v], [x >= v] => [x = v] + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain <= upper_bound), + new_predicate: predicate!(domain == upper_bound), + } + } else if predicate.get_right_hand_side() > lower_bound { + // [x >= v], [x >= v'] => [x >= v'] if v' > v + let to_remove = self.domains[predicate.get_domain()] + .iter() + .filter(|element| { + element.is_lower_bound_predicate() + || (element.is_not_equal_predicate() + && element.get_right_hand_side() + < predicate.get_right_hand_side()) + }) + .copied() + .collect::>(); + + if !to_remove.is_empty() { + ProcessingResult::ReplacedPresent { removed: to_remove } + } else { + ProcessingResult::NotRedundant + } + } else { + // [x >= v], [x >= v'] => [x >= v] if v > v' + self.explain_lower_bound_in_proof(predicate, context); + ProcessingResult::Redundant + } + } + PredicateType::UpperBound => { + // [x >= v], [x <= v] => [x = v] + if predicate.get_right_hand_side() == lower_bound { + self.explain_lower_bound_in_proof(predicate, context); + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain >= lower_bound), + new_predicate: predicate!(domain == lower_bound), + } + } else if predicate.get_right_hand_side() < upper_bound { + // [x <= v], [x <= v'] => [x <= v'] if v' < v + let to_remove = self.domains[predicate.get_domain()] + .iter() + .filter(|element| { + element.is_upper_bound_predicate() + || (element.is_not_equal_predicate() + && element.get_right_hand_side() + > predicate.get_right_hand_side()) + }) + .copied() + .collect::>(); + if !to_remove.is_empty() { + ProcessingResult::ReplacedPresent { removed: to_remove } + } else { + ProcessingResult::NotRedundant + } + } else { + // [x <= v], [x <= v'] => [x <= v] if v < v' + self.explain_upper_bound_in_proof(predicate, context); + ProcessingResult::Redundant + } + } + PredicateType::NotEqual => { + if predicate.get_right_hand_side() == upper_bound { + // [x <= v], [x != v] => [x <= v - 1] + self.explain_upper_bound_in_proof(predicate, context); + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain <= upper_bound), + new_predicate: predicate!(domain <= upper_bound - 1), + } + } else if predicate.get_right_hand_side() > upper_bound { + // [x <= v], [x != v'] => [x <= v] where v' > v + self.explain_upper_bound_in_proof(predicate, context); + ProcessingResult::Redundant + } else if predicate.get_right_hand_side() == lower_bound { + // [x >= v], [x != v] => [x <= v + 1] + self.explain_lower_bound_in_proof(predicate, context); + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain >= lower_bound), + new_predicate: predicate!(domain >= lower_bound + 1), + } + } else if predicate.get_right_hand_side() < lower_bound { + // [x >= v], [x != v'] => [x >= v] where v' < v + self.explain_lower_bound_in_proof(predicate, context); + ProcessingResult::Redundant + } else { + ProcessingResult::NotRedundant + } + } + PredicateType::Equal => ProcessingResult::NotRedundant, + } + } +} diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs index 99b2efb5d..78c885180 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs @@ -1,8 +1,10 @@ //! Contains the nogood minimisers. +mod iterative_minimiser; mod minimiser; mod recursive_minimiser; mod semantic_minimiser; +pub(crate) use iterative_minimiser::*; pub use minimiser::NogoodMinimiser; pub use recursive_minimiser::RecursiveMinimiser; pub use semantic_minimiser::SemanticMinimisationMode; diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index cd2c763f8..24b961312 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,5 +1,6 @@ +use std::ops::ControlFlow; + use pumpkin_core::asserts::pumpkin_assert_advanced; -use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; use pumpkin_core::conflict_resolving::ConflictResolver; @@ -17,7 +18,9 @@ use pumpkin_core::statistics::StatisticLogger; use pumpkin_core::statistics::moving_averages::CumulativeMovingAverage; use pumpkin_core::statistics::moving_averages::MovingAverage; +use crate::minimisers::IterativeMinimiser; use crate::minimisers::NogoodMinimiser; +use crate::minimisers::ProcessingResult; use crate::minimisers::RecursiveMinimiser; use crate::minimisers::SemanticMinimisationMode; use crate::minimisers::SemanticMinimiser; @@ -65,11 +68,14 @@ pub struct ResolutionResolver { statistics: LearnedNogoodStatistics, should_minimise: bool, + iterative_minimisation: bool, + + iterative_minimiser: IterativeMinimiser, } impl Default for ResolutionResolver { fn default() -> Self { - ResolutionResolver::new(AnalysisMode::OneUIP, true) + ResolutionResolver::new(AnalysisMode::OneUIP, true, false) } } @@ -86,8 +92,11 @@ create_statistics_struct!( average_backtrack_amount: CumulativeMovingAverage, /// The average literal-block distance (LBD) metric for newly added learned nogoods average_lbd: CumulativeMovingAverage, + iterative_minimisation_statistics: IterativeMinimisationStatistics }); +create_statistics_struct!(IterativeMinimisationStatistics { num_removed: usize }); + #[derive(Debug, Clone, Copy, Default)] /// Determines which type of learning is performed by the [`ResolutionResolver`]. pub enum AnalysisMode { @@ -134,7 +143,7 @@ impl ConflictResolver for ResolutionResolver { } impl ResolutionResolver { - pub fn new(mode: AnalysisMode, should_minimise: bool) -> Self { + pub fn new(mode: AnalysisMode, should_minimise: bool, iterative_minimisation: bool) -> Self { Self { mode, to_process_heap: Default::default(), @@ -146,6 +155,8 @@ impl ResolutionResolver { semantic_minimiser: Default::default(), statistics: Default::default(), should_minimise, + iterative_minimisation, + iterative_minimiser: Default::default(), } } @@ -154,6 +165,9 @@ impl ResolutionResolver { let conflict_nogood = context.get_conflict_nogood(); + // println!("======================================================================"); + // println!("C: {conflict_nogood:?}"); + // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { self.add_predicate_to_conflict_nogood(*predicate, self.mode, context); @@ -183,11 +197,27 @@ impl ResolutionResolver { AnalysisMode::AllDecision => self.to_process_heap.num_nonremoved_elements() > 0, } } { + // println!( + // "WORKING NOGOOD: {:?}", + // self.processed_nogood_predicates + // .iter() + // .copied() + // .chain( + // self.to_process_heap + // .keys() + // .map(|id| self.predicate_id_generator.get_predicate(id)) + // ) + // .collect::>() + // ); // Replace the predicate from the nogood that has been assigned last on the trail. // // This is done in two steps: // 1) Pop the predicate last assigned on the trail from the nogood. let next_predicate = self.pop_predicate_from_conflict_nogood(); + if self.iterative_minimisation { + // println!("Removing {next_predicate:?}"); + self.iterative_minimiser.remove_predicate(next_predicate); + } // 2) Get the reason for the predicate and add it to the nogood. self.reason_buffer.clear(); @@ -202,6 +232,8 @@ impl ResolutionResolver { &mut self.reason_buffer, ); + // println!("R: {:?} -> {next_predicate}", self.reason_buffer); + for i in 0..self.reason_buffer.len() { self.add_predicate_to_conflict_nogood(self.reason_buffer[i], self.mode, context); } @@ -215,6 +247,11 @@ impl ResolutionResolver { self.processed_nogood_predicates.clear(); self.predicate_id_generator.clear(); self.to_process_heap.clear(); + + // TODO: make more efficient + if self.iterative_minimisation { + self.iterative_minimiser = IterativeMinimiser::default() + } } /// Add the predicate to the current conflict nogood if we know it needs to be added. @@ -238,6 +275,9 @@ impl ResolutionResolver { }); // Ignore root level predicates. if dec_level == 0 { + // println!("{predicate:?} ROOT LEVEL"); + self.iterative_minimiser.apply_predicate(predicate); + context.explain_root_assignment(predicate); } // 1UIP @@ -247,82 +287,494 @@ impl ResolutionResolver { // All-decision Learning // If the variables are not decisions then we want to potentially add them to the heap, // otherwise we add it to the decision predicates which have been discovered previously - else if match mode { - AnalysisMode::OneUIP => dec_level == context.get_checkpoint(), - AnalysisMode::AllDecision => !context.is_decision_predicate(predicate), - } { + else { let predicate_id = self.predicate_id_generator.get_id(predicate); - // The first time we encounter the predicate, we initialise its value in the - // heap. - // - // Note that if the predicate is already in the heap, no action needs to be - // taken. It can happen that a predicate is returned - // multiple times as a reason for other predicates. - - // TODO: could improve the heap structure to be more user-friendly. + if self.iterative_minimisation + && let ControlFlow::Break(_) = + self.check_for_iterative_redundancy(predicate, context, predicate_id) + { + return; + } + if match mode { + AnalysisMode::OneUIP => dec_level == context.get_checkpoint(), + AnalysisMode::AllDecision => !context.is_decision_predicate(predicate), + } { + // The first time we encounter the predicate, we initialise its value in the + // heap. + // + // Note that if the predicate is already in the heap, no action needs to be + // taken. It can happen that a predicate is returned + // multiple times as a reason for other predicates. + + // TODO: could improve the heap structure to be more user-friendly. + + // Here we manually adjust the size of the heap to accommodate new elements. + while self.to_process_heap.len() <= predicate_id.index() { + let next_id = PredicateId::create_from_index(self.to_process_heap.len()); + self.to_process_heap.grow(next_id, 0); + self.to_process_heap.delete_key(next_id); + } + + if self.iterative_minimisation + || (!self.to_process_heap.is_key_present(predicate_id) + && *self.to_process_heap.get_value(predicate_id) == 0) + { + context.predicate_appeared_in_conflict(predicate); + + // The goal is to traverse predicate in reverse order of the trail. + // + // However some predicates may share the trail position. For example, if a + // predicate that was posted to trail resulted in + // some other predicates being true, then all + // these predicates would have the same trail position. + // + // When considering the predicates in reverse order of the trail, the + // implicitly set predicates are posted after the + // explicitly set one, but they all have the same + // trail position. + // + // To remedy this, we make a tie-breaking scheme to prioritise implied + // predicates over explicit predicates. This is done + // by assigning explicitly set predicates the + // value `2 * trail_position`, whereas implied predicates get `2 * + // trail_position + 1`. + let heap_value = get_heap_value(predicate, context); + + // We restore the key and since we know that the value is 0, we can safely + // increment with `heap_value` + self.to_process_heap.restore_key(predicate_id); + self.to_process_heap.set_value(predicate_id, heap_value); + + pumpkin_assert_simple!( + *self.to_process_heap.get_value(predicate_id) == heap_value, + "The value in the heap should be the same as was added" + ); + } + } else { + // We do not check for duplicate, we simply add the predicate. + // Semantic minimisation will later remove duplicates and do other processing. + self.processed_nogood_predicates.push(predicate); + } + } + } - // Here we manually adjust the size of the heap to accommodate new elements. - while self.to_process_heap.len() <= predicate_id.index() { - let next_id = PredicateId::create_from_index(self.to_process_heap.len()); - self.to_process_heap.grow(next_id, 0); - self.to_process_heap.delete_key(next_id); + fn check_for_iterative_redundancy( + &mut self, + predicate: Predicate, + context: &mut ConflictAnalysisContext<'_>, + predicate_id: PredicateId, + ) -> ControlFlow<()> { + let process_predicate = self + .iterative_minimiser + .process_predicate(predicate, context); + // println!("\tRESULT ({predicate:?}): {process_predicate:?}"); + match process_predicate { + ProcessingResult::Redundant => { + if !self.to_process_heap.is_key_present(predicate_id) { + // println!("\t\tNot present - {predicate:?}"); + if predicate_id.index() < self.to_process_heap.len() { + self.to_process_heap.set_value(predicate_id, 0); + } + self.to_process_heap.delete_key(predicate_id); + } + + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + return ControlFlow::Break(()); + } + ProcessingResult::ReplacedPresent { removed } => { + for removed_predicate in removed { + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + self.iterative_minimiser.remove_predicate(removed_predicate); + let removed_id = self.predicate_id_generator.get_id(removed_predicate); + if self.to_process_heap.is_key_present(removed_id) { + self.to_process_heap.delete_key(removed_id); + } else { + if let Some(position) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == removed_predicate) + { + let _ = self.processed_nogood_predicates.remove(position); + } + } + } + + self.iterative_minimiser.apply_predicate(predicate); + } + ProcessingResult::PossiblyReplacedWithNew { + removed: previous, + new_predicate, + } => { + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + + if context.get_checkpoint_for_predicate(new_predicate).unwrap() + == context.get_checkpoint() + { + if let ControlFlow::Break(_) = + self.replace_if_possible_current_level(context, previous, new_predicate) + { + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); + return ControlFlow::Break(()); + } else { + self.iterative_minimiser.apply_predicate(predicate); + } + } else { + if let ControlFlow::Break(_) = + self.replace_if_possible_previous_level(context, previous, new_predicate) + { + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); + return ControlFlow::Break(()); + } else { + self.iterative_minimiser.apply_predicate(predicate); + } + } } + ProcessingResult::NotRedundant => { + self.iterative_minimiser.apply_predicate(predicate); + } + } + ControlFlow::Continue(()) + } - // Then we check whether the predicate was not already present in the heap, if - // this is not the case then we insert it - if !self.to_process_heap.is_key_present(predicate_id) - && *self.to_process_heap.get_value(predicate_id) == 0 - { - context.predicate_appeared_in_conflict(predicate); + // fn check_redundancy_current_level( + // &mut self, + // predicate: Predicate, + // context: &mut ConflictAnalysisContext<'_>, + // ) -> ControlFlow<()> { + // for element in self + // .to_process_heap + // .keys() + // .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) + // .filter(|element| { + // element.get_domain() == predicate.get_domain() + // && context.get_state().trail_position(*element) + // != context.get_state().trail_position(predicate) + // }) + // .collect::>() + // { + // match (element.get_predicate_type(), predicate.get_predicate_type()) { + // (PredicateType::Equal, PredicateType::NotEqual) + // | (PredicateType::Equal, PredicateType::UpperBound) + // | (PredicateType::Equal, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // return ControlFlow::Break(()); + // } + // (PredicateType::UpperBound, PredicateType::UpperBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // if element.get_right_hand_side() <= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // let element_id = self.predicate_id_generator.get_id(element); + // self.to_process_heap.delete_key(element_id); + // } + // } + // (PredicateType::UpperBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain <= element.get_right_hand_side() - + // 1); self.replace_if_possible_current_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() < + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::LowerBound, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // if element.get_right_hand_side() >= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // let element_id = self.predicate_id_generator.get_id(element); + // self.to_process_heap.delete_key(element_id); + // } + // } + // (PredicateType::LowerBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain >= element.get_right_hand_side() + + // 1); self.replace_if_possible_current_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() > + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::UpperBound, PredicateType::LowerBound) + // if element.get_right_hand_side() == predicate.get_right_hand_side() => + // { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain == element.get_right_hand_side()); + // self.replace_if_possible_current_level(context, element, new_predicate)?; + // } + // + // _ => {} + // } + // } + // ControlFlow::Continue(()) + // } + + fn replace_if_possible_current_level( + &mut self, + context: &mut ConflictAnalysisContext<'_>, + element: Predicate, + new_predicate: Predicate, + ) -> ControlFlow<()> { + let heap_value = get_heap_value(new_predicate, context); + + if heap_value + < self + .to_process_heap + .peek_max() + .map(|(_, value)| *value) + .unwrap_or_default() + { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + + // println!("Removing previous: {element:?}"); + self.iterative_minimiser.remove_predicate(element); + self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); + + return ControlFlow::Break(()); + } + ControlFlow::Continue(()) + } - // The goal is to traverse predicate in reverse order of the trail. - // - // However some predicates may share the trail position. For example, if a - // predicate that was posted to trail resulted in - // some other predicates being true, then all - // these predicates would have the same trail position. - // - // When considering the predicates in reverse order of the trail, the - // implicitly set predicates are posted after the - // explicitly set one, but they all have the same - // trail position. - // - // To remedy this, we make a tie-breaking scheme to prioritise implied - // predicates over explicit predicates. This is done - // by assigning explicitly set predicates the - // value `2 * trail_position`, whereas implied predicates get `2 * - // trail_position + 1`. - let heap_value = if context.get_state().is_on_trail(predicate) { - context - .get_state() - .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") - * 2 - } else { - context - .get_state() - .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") - * 2 - + 1 - }; - - // We restore the key and since we know that the value is 0, we can safely - // increment with `heap_value` - self.to_process_heap.restore_key(predicate_id); - self.to_process_heap - .increment(predicate_id, heap_value as u32); - - pumpkin_assert_moderate!( - *self.to_process_heap.get_value(predicate_id) == heap_value.try_into().unwrap(), - "The value in the heap should be the same as was added" - ) + // fn check_redundancy_previous_level( + // &mut self, + // predicate: Predicate, + // context: &mut ConflictAnalysisContext<'_>, + // ) -> ControlFlow<()> { + // for element in self + // .processed_nogood_predicates + // .iter() + // .filter(|element| { + // element.get_domain() == predicate.get_domain() + // && context.get_state().trail_position(**element) + // != context.get_state().trail_position(predicate) + // }) + // .copied() + // .collect::>() + // { + // match (element.get_predicate_type(), predicate.get_predicate_type()) { + // (PredicateType::Equal, PredicateType::NotEqual) + // | (PredicateType::Equal, PredicateType::UpperBound) + // | (PredicateType::Equal, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // (PredicateType::UpperBound, PredicateType::UpperBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // if element.get_right_hand_side() <= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // if let Some(index) = self + // .processed_nogood_predicates + // .iter() + // .position(|predicate| *predicate == element) + // { + // let _ = self.processed_nogood_predicates.remove(index); + // } + // } + // } + // (PredicateType::UpperBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain <= element.get_right_hand_side() - + // 1); self.replace_if_possible_previous_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() < + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::LowerBound, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // if element.get_right_hand_side() >= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // if let Some(index) = self + // .processed_nogood_predicates + // .iter() + // .position(|predicate| *predicate == element) + // { + // let _ = self.processed_nogood_predicates.remove(index); + // } + // } + // } + // (PredicateType::LowerBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain >= element.get_right_hand_side() + + // 1); self.replace_if_possible_previous_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() > + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::UpperBound, PredicateType::LowerBound) + // if element.get_right_hand_side() == predicate.get_right_hand_side() => + // { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain == element.get_right_hand_side()); + // self.replace_if_possible_previous_level(context, element, new_predicate)?; + // } + // + // _ => {} + // } + // } + // ControlFlow::Continue(()) + // } + + fn replace_if_possible_previous_level( + &mut self, + context: &mut ConflictAnalysisContext<'_>, + element: Predicate, + new_predicate: Predicate, + ) -> ControlFlow<()> { + let heap_value = get_heap_value(new_predicate, context); + + if heap_value + < self + .to_process_heap + .peek_max() + .map(|(_, value)| *value) + .unwrap_or_default() + { + if let Some(index) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == element) + { + let _ = self.processed_nogood_predicates.remove(index); } - } else { - // We do not check for duplicate, we simply add the predicate. - // Semantic minimisation will later remove duplicates and do other processing. - self.processed_nogood_predicates.push(predicate); + + // println!("Removing previous: {element:?}"); + self.iterative_minimiser.remove_predicate(element); + + self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); + + return ControlFlow::Break(()); } + ControlFlow::Continue(()) } fn pop_predicate_from_conflict_nogood(&mut self) -> Predicate { @@ -337,6 +789,18 @@ impl ResolutionResolver { // First we obtain a semantically minimised nogood. // // We reuse the vector with lower decision levels for simplicity. + // println!( + // "FINAL NOGOOD: {:?}", + // self.processed_nogood_predicates + // .iter() + // .copied() + // .chain( + // self.to_process_heap + // .keys() + // .map(|id| self.predicate_id_generator.get_predicate(id)) + // ) + // .collect::>() + // ); if self.to_process_heap.num_nonremoved_elements() > 0 { let last_predicate = self.pop_predicate_from_conflict_nogood(); self.processed_nogood_predicates.push(last_predicate); @@ -393,3 +857,20 @@ impl ResolutionResolver { } } } + +fn get_heap_value(predicate: Predicate, context: &mut ConflictAnalysisContext<'_>) -> u32 { + if context.get_state().is_on_trail(predicate) { + context + .get_state() + .trail_position(predicate) + .expect("Predicate should be true during conflict analysis") as u32 + * 2 + } else { + context + .get_state() + .trail_position(predicate) + .expect("Predicate should be true during conflict analysis") as u32 + * 2 + + 1 + } +} diff --git a/pumpkin-crates/core/src/containers/key_value_heap.rs b/pumpkin-crates/core/src/containers/key_value_heap.rs index 12334728f..490d50c29 100644 --- a/pumpkin-crates/core/src/containers/key_value_heap.rs +++ b/pumpkin-crates/core/src/containers/key_value_heap.rs @@ -62,7 +62,7 @@ where /// Get the keys in the heap. /// /// The order in which the keys are yielded is unspecified. - pub(crate) fn keys(&self) -> impl Iterator + '_ { + pub fn keys(&self) -> impl Iterator + '_ { self.map_position_to_key[..self.end_position] .iter() .copied() @@ -72,7 +72,7 @@ where /// this does not delete the key (see [`KeyValueHeap::pop_max`] to get and delete). /// /// The time-complexity of this operation is O(1) - pub(crate) fn peek_max(&self) -> Option<(&Key, &Value)> { + pub fn peek_max(&self) -> Option<(&Key, &Value)> { if self.has_no_nonremoved_elements() { None } else { @@ -123,6 +123,18 @@ where } } + pub fn set_value(&mut self, key: Key, value: Value) { + if key.index() < self.len() { + let position = self.map_key_to_position[key]; + self.values[position] = value; + // Recall that increment may be applied to keys not present + // So we only apply sift up in case the key is present + if self.is_key_present(key) { + self.sift_up(position); + } + } + } + /// Restores the entry with key 'key' to the heap if the key is not present, otherwise does /// nothing. Its value is the previous value used before 'delete_key' was called. /// diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 68719848f..ae2ae6308 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -171,6 +171,15 @@ struct Args { #[arg(long = "no-learning-minimise", verbatim_doc_comment)] no_learning_clause_minimisation: bool, + /// Decides whether to apply semantic minimisation during conflict analysis; according to the + /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". + /// + /// If this flag is present then the minimisation is turned on. + /// + /// Possible values: bool + #[arg(long = "iterative-minimisation", verbatim_doc_comment)] + iterative_minimisation: bool, + /// Decides the sequence based on which the restarts are performed. /// /// - The "constant" approach uses a constant number of conflicts before another restart is @@ -633,6 +642,7 @@ fn run() -> PumpkinResult<()> { ResolutionResolver::new( AnalysisMode::OneUIP, !args.no_learning_clause_minimisation, + !args.iterative_minimisation, ), )?, }, diff --git a/pumpkin-solver/tests/helpers/mod.rs b/pumpkin-solver/tests/helpers/mod.rs index cff79aa31..3bbe80569 100644 --- a/pumpkin-solver/tests/helpers/mod.rs +++ b/pumpkin-solver/tests/helpers/mod.rs @@ -97,7 +97,10 @@ pub(crate) fn run_solver_with_options( match child.wait_timeout(TEST_TIMEOUT) { Ok(None) => panic!("solver took more than {} seconds", TEST_TIMEOUT.as_secs()), Ok(Some(status)) if status.success() => {} - Ok(Some(e)) => panic!("error solving instance {e}"), + Ok(Some(e)) => panic!( + "error solving instance {e}\n{:?}", + std::fs::read_to_string(err_file_path) + ), Err(e) => panic!("error starting solver: {e}"), }