diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs new file mode 100644 index 000000000..fb6e8439e --- /dev/null +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -0,0 +1,53 @@ +use crate::containers::HashMap; +use crate::engine::Assignments; +use crate::engine::SolverStatistics; +use crate::engine::conflict_analysis::ConflictAnalysisContext; +#[cfg(doc)] +use crate::engine::propagation::ReadDomains; +use crate::engine::propagation::contexts::HasAssignments; +use crate::predicates::Predicate; +use crate::proof::InferenceCode; +use crate::proof::ProofLog; +use crate::state::CurrentNogood; +use crate::state::State; + +/// The context used for during nogood minimisation. +/// +/// Can be used to get the reason for a [`Predicate`] using +/// [`MinimisationContext::get_propagation_reason`], and information about integer variables and +/// [`Predicate`]s (see [`ReadDomains`]). +pub(crate) struct MinimisationContext<'a> { + pub(crate) state: &'a mut State, + + pub(crate) proof_log: &'a mut ProofLog, + pub(crate) unit_nogood_inference_codes: &'a HashMap, + + pub(crate) counters: &'a mut SolverStatistics, +} +impl<'a> MinimisationContext<'a> { + /// Compute the reason for `predicate` being true. The reason will be stored in + /// `reason_buffer`. + /// + /// If `predicate` is not true, or it is a decision, then this function will panic. + pub(crate) fn get_propagation_reason( + &mut self, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + input_predicate: Predicate, + current_nogood: CurrentNogood<'_>, + ) { + ConflictAnalysisContext::get_propagation_reason( + input_predicate, + current_nogood, + self.proof_log, + self.unit_nogood_inference_codes, + reason_buffer, + self.state, + ); + } +} + +impl<'a> HasAssignments for MinimisationContext<'a> { + fn assignments(&self) -> &Assignments { + &self.state.assignments + } +} diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs new file mode 100644 index 000000000..5752c6bd9 --- /dev/null +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs @@ -0,0 +1,9 @@ +use crate::engine::conflict_analysis::MinimisationContext; +use crate::predicates::Predicate; + +/// A trait for the behaviour of nogood minimisation approaches. +pub(crate) trait NogoodMinimiser: Default { + /// Takes as input a nogood represented by a [`Vec`] of [`Predicate`]s and minimises the + /// nogood. + fn minimise(&mut self, context: MinimisationContext, nogood: &mut Vec); +} diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/mod.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/mod.rs index 451c1e0d5..b6ad2798f 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/mod.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/mod.rs @@ -1,5 +1,9 @@ +mod minimisation_context; +mod minimiser; mod recursive_minimiser; mod semantic_minimiser; +pub(crate) use minimisation_context::*; +pub(crate) use minimiser::*; pub(crate) use recursive_minimiser::*; pub(crate) use semantic_minimiser::*; diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs index c44993c8c..5bc023861 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs @@ -1,15 +1,18 @@ +use super::MinimisationContext; use crate::basic_types::moving_averages::MovingAverage; use crate::containers::HashMap; use crate::containers::HashSet; use crate::engine::Assignments; -use crate::engine::conflict_analysis::ConflictAnalysisContext; -use crate::engine::propagation::CurrentNogood; +use crate::engine::conflict_analysis::NogoodMinimiser; +use crate::engine::propagation::ReadDomains; +use crate::engine::propagation::contexts::HasAssignments; use crate::predicates::Predicate; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; use crate::pumpkin_assert_eq_moderate; use crate::pumpkin_assert_moderate; use crate::pumpkin_assert_simple; +use crate::state::CurrentNogood; #[derive(Debug, Clone, Default)] pub(crate) struct RecursiveMinimiser { @@ -18,7 +21,7 @@ pub(crate) struct RecursiveMinimiser { label_assignments: HashMap>, } -impl RecursiveMinimiser { +impl NogoodMinimiser for RecursiveMinimiser { /// Removes redundant literals from the learned clause. /// Redundancy is detected by looking at the implication graph: /// * a literal is redundant/dominated if a subset of the other literals in the learned clause @@ -34,14 +37,10 @@ impl RecursiveMinimiser { /// to improved propositional proof traces’. SAT'09. /// /// \[2\] N. Sörensson and A. Biere, ‘Minimizing learned clauses’. SAT'09 - pub(crate) fn remove_dominated_predicates( - &mut self, - nogood: &mut Vec, - context: &mut ConflictAnalysisContext, - ) { + fn minimise(&mut self, mut context: MinimisationContext, nogood: &mut Vec) { let num_literals_before_minimisation = nogood.len(); - self.initialise_minimisation_data_structures(nogood, &context.state.assignments); + self.initialise_minimisation_data_structures(nogood, context.assignments()); // Iterate over each predicate and check whether it is a dominated predicate. let mut end_position: usize = 0; @@ -49,7 +48,7 @@ impl RecursiveMinimiser { for i in 0..initial_nogood_size { let learned_predicate = nogood[i]; - self.compute_label(learned_predicate, context, nogood); + self.compute_label(learned_predicate, &mut context, nogood); let label = self.get_predicate_label(learned_predicate); // Keep the predicate in case it was not deemed deemed redundant. @@ -72,11 +71,13 @@ impl RecursiveMinimiser { .average_number_of_removed_atomic_constraints_recursive .add_term(num_predicates_removed as u64); } +} +impl RecursiveMinimiser { fn compute_label( &mut self, input_predicate: Predicate, - context: &mut ConflictAnalysisContext, + context: &mut MinimisationContext, current_nogood: &[Predicate], ) { pumpkin_assert_eq_moderate!(context.state.truth_value(input_predicate), Some(true)); @@ -99,11 +100,7 @@ impl RecursiveMinimiser { // If the predicate is a decision predicate, it cannot be a predicate from the original // learned nogood since those are labelled as part of initialisation. // Therefore the decision literal is labelled as poison and then return. - if context - .state - .assignments - .is_decision_predicate(&input_predicate) - { + if context.is_decision_predicate(&input_predicate) { self.assign_predicate_label(input_predicate, Label::Poison); self.current_depth -= 1; return; @@ -113,8 +110,7 @@ impl RecursiveMinimiser { // (levels from the original learned clause) cannot be removed. if !self.is_decision_level_allowed( context - .state - .get_checkpoint_for_predicate(input_predicate) + .get_checkpoint_for_predicate(&input_predicate) .unwrap(), ) { self.assign_predicate_label(input_predicate, Label::Poison); @@ -125,20 +121,16 @@ impl RecursiveMinimiser { // Due to ownership rules, we have to take ownership of the reason. // TODO: Reuse the allocation if it becomes a bottleneck. let mut reason = vec![]; - ConflictAnalysisContext::get_propagation_reason( + context.get_propagation_reason( + &mut reason, input_predicate, CurrentNogood::from(current_nogood), - context.proof_log, - context.unit_nogood_inference_codes, - &mut reason, - context.state, ); for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context - .state - .get_checkpoint_for_predicate(antecedent_predicate) + .get_checkpoint_for_predicate(&antecedent_predicate) .unwrap() == 0 { diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs index a47c12fa9..225c59544 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs @@ -1,10 +1,12 @@ use std::cmp; +use super::MinimisationContext; use crate::containers::HashSet; use crate::containers::KeyedVec; use crate::containers::SparseSet; -use crate::engine::Assignments; +use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::predicates::predicate::PredicateType; +use crate::engine::propagation::contexts::HasAssignments; use crate::predicate; use crate::predicates::Predicate; use crate::variables::DomainId; @@ -15,6 +17,8 @@ pub(crate) struct SemanticMinimiser { domains: KeyedVec, present_ids: SparseSet, helper: Vec, + + mode: Mode, } impl Default for SemanticMinimiser { @@ -25,6 +29,7 @@ impl Default for SemanticMinimiser { domains: Default::default(), present_ids: SparseSet::new(vec![], mapping), helper: Vec::default(), + mode: Mode::EnableEqualityMerging, } } } @@ -35,14 +40,9 @@ pub(crate) enum Mode { DisableEqualityMerging, } -impl SemanticMinimiser { - pub(crate) fn minimise( - &mut self, - nogood: &Vec, - assignments: &Assignments, - mode: Mode, - ) -> Vec { - self.accommodate(assignments); +impl NogoodMinimiser for SemanticMinimiser { + fn minimise(&mut self, context: MinimisationContext, nogood: &mut Vec) { + self.accommodate(&context); self.clean_up(); self.apply_predicates(nogood); @@ -51,16 +51,23 @@ impl SemanticMinimiser { for domain_id in self.present_ids.iter() { // If at least one domain is inconsistent, we can stop. if self.domains[domain_id].inconsistent { - return vec![Predicate::trivially_false()]; + *nogood = vec![Predicate::trivially_false()]; + return; } self.domains[domain_id].add_domain_description_to_vector( *domain_id, &self.original_domains[domain_id], &mut self.helper, - mode, + self.mode, ); } - self.helper.clone() + *nogood = self.helper.clone(); + } +} + +impl SemanticMinimiser { + pub(crate) fn set_mode(&mut self, mode: Mode) { + self.mode = mode } fn apply_predicates(&mut self, nogood: &Vec) { @@ -95,14 +102,14 @@ impl SemanticMinimiser { } } - fn accommodate(&mut self, assignments: &Assignments) { + fn accommodate(&mut self, context: &MinimisationContext) { assert!(self.domains.len() == self.original_domains.len()); - while (self.domains.len() as u32) < assignments.num_domains() { + while (self.domains.len() as u32) < context.assignments().num_domains() { let domain_id = DomainId::new(self.domains.len() as u32); - let lower_bound = assignments.get_initial_lower_bound(domain_id); - let upper_bound = assignments.get_initial_upper_bound(domain_id); - let holes = assignments.get_initial_holes(domain_id); + let lower_bound = context.assignments().get_initial_lower_bound(domain_id); + let upper_bound = context.assignments().get_initial_upper_bound(domain_id); + let holes = context.assignments().get_initial_holes(domain_id); self.grow(lower_bound, upper_bound, holes); } } @@ -254,98 +261,156 @@ impl SimpleIntegerDomain { #[cfg(test)] mod tests { use crate::conjunction; - use crate::engine::Assignments; + use crate::containers::HashMap; + use crate::engine::SolverStatistics; + use crate::engine::conflict_analysis::MinimisationContext; use crate::engine::conflict_analysis::Mode; + use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::conflict_analysis::SemanticMinimiser; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; + use crate::proof::ProofLog; + use crate::state::State; #[test] fn trivial_nogood() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![predicate!(domain_id >= 0), predicate!(domain_id <= 10)]; - - let p = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + let mut state = State::default(); + let domain_id = state.new_interval_variable(0, 10, None); + let mut nogood: Vec = + vec![predicate!(domain_id >= 0), predicate!(domain_id <= 10)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert!(p.is_empty()); + assert!(nogood.is_empty()); } #[test] fn trivial_conflict_bounds() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![predicate!(domain_id >= 5), predicate!(domain_id <= 4)]; - - let p = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + let mut state = State::default(); + let domain_id = state.new_interval_variable(0, 10, None); + let mut nogood: Vec = + vec![predicate!(domain_id >= 5), predicate!(domain_id <= 4)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(p.len(), 1); - assert_eq!(p[0], Predicate::trivially_false()); + assert_eq!(nogood.len(), 1); + assert_eq!(nogood[0], Predicate::trivially_false()); } #[test] fn trivial_conflict_holes() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![ + let mut state = State::default(); + let domain_id = state.new_interval_variable(0, 10, None); + let mut nogood: Vec = vec![ predicate!(domain_id != 5), predicate!(domain_id >= 5), predicate!(domain_id <= 5), ]; - let p = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(p.len(), 1); - assert_eq!(p[0], Predicate::trivially_false()); + assert_eq!(nogood.len(), 1); + assert_eq!(nogood[0], Predicate::trivially_false()); } #[test] fn trivial_conflict_assignment() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; - - let p = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + let mut state = State::default(); + let domain_id = state.new_interval_variable(0, 10, None); + let mut nogood: Vec = + vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(p.len(), 1); - assert_eq!(p[0], Predicate::trivially_false()); + assert_eq!(nogood.len(), 1); + assert_eq!(nogood[0], Predicate::trivially_false()); } #[test] fn trivial_conflict_bounds_reset() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; - - let _ = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + let mut state = State::default(); + let domain_id = state.new_interval_variable(0, 10, None); + let mut nogood: Vec = + vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - let p = p.minimise(&vec![], &assignments, Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + let mut other = Vec::default(); + p.minimise(context, &mut other); - assert!(p.is_empty()); + assert!(other.is_empty()); } #[test] fn simple_bound1() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); - let domain_1 = assignments.grow(0, 5); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); + let domain_1 = state.new_interval_variable(0, 5, None); - let nogood: Vec = + let mut nogood: Vec = conjunction!([domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] & [domain_1 <= 4]) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 3); + assert_eq!(nogood.len(), 3); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!([domain_0 >= 5] & [domain_0 <= 9] & [domain_1 <= 4]) ); } @@ -353,20 +418,27 @@ mod tests { #[test] fn simple_bound2() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); - let domain_1 = assignments.grow(0, 5); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); + let domain_1 = state.new_interval_variable(0, 5, None); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] & [domain_1 <= 4] & [domain_0 != 7] ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 4); + assert_eq!(nogood.len(), 4); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!([domain_0 >= 5] & [domain_0 <= 9] & [domain_1 <= 4] & [domain_0 != 7]) ); } @@ -374,11 +446,11 @@ mod tests { #[test] fn simple_bound3() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); - let domain_1 = assignments.grow(0, 5); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); + let domain_1 = state.new_interval_variable(0, 5, None); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -390,11 +462,18 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 6); + assert_eq!(nogood.len(), 6); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!( [domain_0 >= 5] & [domain_0 <= 9] @@ -409,11 +488,11 @@ mod tests { #[test] fn simple_assign() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); - let domain_1 = assignments.grow(0, 5); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); + let domain_1 = state.new_interval_variable(0, 5, None); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -426,11 +505,18 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 2); + assert_eq!(nogood.len(), 2); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!([domain_0 == 5] & [domain_1 <= 4]) ); } @@ -438,11 +524,11 @@ mod tests { #[test] fn simple_assign_no_equality() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); - let domain_1 = assignments.grow(0, 5); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); + let domain_1 = state.new_interval_variable(0, 5, None); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -455,11 +541,18 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::DisableEqualityMerging); + p.set_mode(Mode::DisableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 3); + assert_eq!(nogood.len(), 3); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!([domain_0 >= 5] & [domain_0 <= 5] & [domain_1 <= 4]) ); } @@ -467,32 +560,46 @@ mod tests { #[test] fn simple_lb_override1() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); - let nogood = conjunction!([domain_0 >= 2] & [domain_0 >= 1] & [domain_0 >= 5]).into(); + let mut nogood = conjunction!([domain_0 >= 2] & [domain_0 >= 1] & [domain_0 >= 5]).into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 1); - assert_eq!(predicates[0], predicate!(domain_0 >= 5)); + assert_eq!(nogood.len(), 1); + assert_eq!(nogood[0], predicate!(domain_0 >= 5)); } #[test] fn hole_lb_override() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); - let nogood = + let mut nogood = conjunction!([domain_0 != 2] & [domain_0 != 3] & [domain_0 >= 5] & [domain_0 >= 1]) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 1); + assert_eq!(nogood.len(), 1); assert_eq!( - PropositionalConjunction::from(predicates), + PropositionalConjunction::from(nogood), conjunction!([domain_0 >= 5]) ); } @@ -500,16 +607,23 @@ mod tests { #[test] fn hole_push_lb() { let mut p = SemanticMinimiser::default(); - let mut assignments = Assignments::default(); - let domain_0 = assignments.grow(0, 10); + let mut state = State::default(); + let domain_0 = state.new_interval_variable(0, 10, None); - let nogood = + let mut nogood = conjunction!([domain_0 != 2] & [domain_0 != 3] & [domain_0 >= 1] & [domain_0 != 1]) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + counters: &mut SolverStatistics::default(), + state: &mut state, + }; + p.minimise(context, &mut nogood); - assert_eq!(predicates.len(), 1); - assert_eq!(predicates[0], predicate![domain_0 >= 4]); + assert_eq!(nogood.len(), 1); + assert_eq!(nogood[0], predicate![domain_0 >= 4]); } } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs index 57a51cd27..d29031a71 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/resolvers/resolution_resolver.rs @@ -1,3 +1,5 @@ +use std::ops::Deref; + use super::ConflictResolver; use crate::basic_types::PredicateId; use crate::basic_types::PredicateIdGenerator; @@ -7,7 +9,9 @@ use crate::containers::KeyValueHeap; use crate::containers::StorageKey; use crate::engine::Lbd; use crate::engine::conflict_analysis::ConflictAnalysisContext; +use crate::engine::conflict_analysis::MinimisationContext; use crate::engine::conflict_analysis::Mode; +use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::conflict_analysis::RecursiveMinimiser; use crate::engine::constraint_satisfaction_solver::NogoodLabel; use crate::engine::propagation::CurrentNogood; @@ -405,39 +409,115 @@ impl ResolutionResolver { // First we minimise the nogood using semantic minimisation to remove duplicates but we // avoid equality merging (since some of these literals could potentailly be removed by // recursive minimisation) - let mut clean_nogood: Vec = context.semantic_minimiser.minimise( - &self.processed_nogood_predicates, - &context.state.assignments, - if !context.should_minimise { + context + .semantic_minimiser + .set_mode(if !context.should_minimise { // If we do not minimise then we do the equality // merging in the first iteration of removing // duplicates Mode::EnableEqualityMerging } else { Mode::DisableEqualityMerging + }); + context.semantic_minimiser.minimise( + MinimisationContext { + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + counters: context.counters, + state: context.state, }, + &mut self.processed_nogood_predicates, ); if context.should_minimise { // Then we perform recursive minimisation to remove the dominated predicates - self.recursive_minimiser - .remove_dominated_predicates(&mut clean_nogood, context); + self.recursive_minimiser.minimise( + MinimisationContext { + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + counters: context.counters, + state: context.state, + }, + &mut self.processed_nogood_predicates, + ); // We perform a final semantic minimisation call which allows the merging of the // equality predicates which remain in the nogood - let size_before_semantic_minimisation = clean_nogood.len(); - clean_nogood = context.semantic_minimiser.minimise( - &clean_nogood, - &context.state.assignments, - Mode::EnableEqualityMerging, + let size_before_semantic_minimisation = self.processed_nogood_predicates.len(); + context + .semantic_minimiser + .set_mode(Mode::EnableEqualityMerging); + context.semantic_minimiser.minimise( + MinimisationContext { + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + counters: context.counters, + state: context.state, + }, + &mut self.processed_nogood_predicates, ); context .counters .learned_clause_statistics .average_number_of_removed_atomic_constraints_semantic - .add_term((size_before_semantic_minimisation - clean_nogood.len()) as u64); + .add_term( + (size_before_semantic_minimisation - self.processed_nogood_predicates.len()) + as u64, + ); + } + + let learned_nogood = + LearnedNogood::create_from_vec(self.processed_nogood_predicates.clone(), context); + + pumpkin_assert_advanced!( + learned_nogood + .predicates + .iter() + .skip(1) + .all(|p| context.state.assignments.is_predicate_satisfied(*p)) + ); + + // TODO: asserting predicate may be bumped twice, probably not a problem. + for predicate in learned_nogood.predicates.iter() { + context + .brancher + .on_appearance_in_conflict_predicate(*predicate); } + learned_nogood + } +} + +/// A structure which stores a learned nogood +/// +/// There are two assumptions: +/// - The asserting literal (i.e. the literal of the current decision level) is placed at the `0`th +/// index of [`LearnedNogood::literals`]. +/// - A literal from the second-highest decision level is placed at the `1`st index of +/// [`LearnedNogood::literals`]. +#[derive(Clone, Debug)] +pub(crate) struct LearnedNogood { + pub(crate) predicates: Vec, + pub(crate) backjump_level: usize, +} + +impl Deref for LearnedNogood { + type Target = [Predicate]; + + fn deref(&self) -> &Self::Target { + &self.predicates + } +} + +impl LearnedNogood { + /// Creates a [`LearnedNogood`] from the provided [`Vec`]. + /// + /// This method automatically ensures that the invariants of nogoods hold; see [`LearnedNogood`] + /// for more details on these invariants. + pub(crate) fn create_from_vec( + mut clean_nogood: Vec, + context: &ConflictAnalysisContext, + ) -> Self { // We perform a linear scan to maintain the two invariants: // - The predicate from the current decision level is placed at index 0 // - The predicate from the highest decision level below the current is placed at index 1 @@ -473,36 +553,9 @@ impl ResolutionResolver { 0 }; - pumpkin_assert_advanced!( - clean_nogood - .iter() - .skip(1) - .all(|p| context.state.truth_value(*p) == Some(true)) - ); - - // TODO: asserting predicate may be bumped twice, probably not a problem. - for predicate in clean_nogood.iter() { - context - .brancher - .on_appearance_in_conflict_predicate(*predicate); - } - - LearnedNogood { - backjump_level, + Self { predicates: clean_nogood, + backjump_level, } } } - -/// A structure which stores a learned nogood -/// -/// There are two assumptions: -/// - The asserting literal (i.e. the literal of the current decision level) is placed at the `0`th -/// index of [`LearnedNogood::literals`]. -/// - A literal from the second-highest decision level is placed at the `1`st index of -/// [`LearnedNogood::literals`]. -#[derive(Clone, Debug)] -pub(crate) struct LearnedNogood { - pub(crate) predicates: Vec, - pub(crate) backjump_level: usize, -} diff --git a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs b/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs index f059bb6a6..e9835e8b1 100644 --- a/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs +++ b/pumpkin-crates/core/src/engine/cp/propagation/contexts/propagation_context.rs @@ -248,6 +248,14 @@ pub(crate) trait ReadDomains: HasAssignments { .is_some_and(|truth_value| !truth_value) } + fn is_decision_predicate(&self, predicate: &Predicate) -> bool { + self.assignments().is_decision_predicate(predicate) + } + + fn get_checkpoint_for_predicate(&self, predicate: &Predicate) -> Option { + self.assignments().get_checkpoint_for_predicate(predicate) + } + fn is_literal_true(&self, literal: &Literal) -> bool { literal .get_integer_variable() diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 92adc4d82..47f79a310 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -1119,6 +1119,8 @@ impl NogoodPropagator { // change since the initial time the semantic minimiser recorded it, so it would not know // that a previously nonroot bound is now actually a root bound. + // We assume that duplicate predicates have been removed + // Check if the nogood cannot be violated, i.e., it has a falsified predicate. if nogood.is_empty() || nogood.iter().any(|p| context.is_predicate_falsified(*p)) { *nogood = vec![Predicate::trivially_false()];