From 528f83003b97a22e26dfe54de313a6b8d1178995 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 27 Nov 2025 10:49:46 +0100 Subject: [PATCH 1/6] feat: nogood minimisation interface + implement it for recursive minimisation --- .../minimisers/minimisation_context.rs | 334 ++++++++++++++++++ .../conflict_analysis/minimisers/minimiser.rs | 9 + .../conflict_analysis/minimisers/mod.rs | 4 + .../minimisers/recursive_minimiser.rs | 43 +-- .../resolvers/resolution_resolver.rs | 101 ++++-- .../contexts/propagation_context.rs | 9 + 6 files changed, 441 insertions(+), 59 deletions(-) create mode 100644 pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs create mode 100644 pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs 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..b55fa2c44 --- /dev/null +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -0,0 +1,334 @@ +use crate::containers::HashMap; +use crate::engine::Assignments; +use crate::engine::SolverStatistics; +use crate::engine::VariableNames; +use crate::engine::conflict_analysis::ConflictAnalysisContext; +use crate::engine::notifications::NotificationEngine; +use crate::engine::propagation::CurrentNogood; +use crate::engine::propagation::ExplanationContext; +use crate::engine::propagation::contexts::HasAssignments; +use crate::engine::propagation::store::PropagatorStore; +use crate::engine::reason::ReasonStore; +use crate::predicate; +use crate::predicates::Predicate; +use crate::predicates::PredicateType; +use crate::proof::InferenceCode; +use crate::proof::ProofLog; +use crate::pumpkin_assert_simple; + +pub(crate) struct MinimisationContext<'a> { + pub(crate) assignments: &'a Assignments, + pub(crate) reason_store: &'a mut ReasonStore, + pub(crate) notification_engine: &'a mut NotificationEngine, + pub(crate) propagators: &'a mut PropagatorStore, + + pub(crate) proof_log: &'a mut ProofLog, + pub(crate) unit_nogood_inference_codes: &'a HashMap, + pub(crate) variable_names: &'a VariableNames, + + pub(crate) counters: &'a mut SolverStatistics, +} + +impl<'a> MinimisationContext<'a> { + pub(crate) fn new( + assignments: &'a Assignments, + reason_store: &'a mut ReasonStore, + notification_engine: &'a mut NotificationEngine, + propagators: &'a mut PropagatorStore, + proof_log: &'a mut ProofLog, + unit_nogood_inference_codes: &'a HashMap, + variable_names: &'a VariableNames, + counters: &'a mut SolverStatistics, + ) -> Self { + Self { + assignments, + reason_store, + notification_engine, + propagators, + proof_log, + unit_nogood_inference_codes, + variable_names, + counters, + } + } + /// 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, + predicate: Predicate, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + ) { + if self.assignments.is_initial_bound(predicate) { + return; + } + + let trail_position = self + .assignments + .get_trail_position(&predicate) + .expect("The predicate must be true during conflict analysis."); + + let trail_entry = self.assignments.get_trail_entry(trail_position); + + // We distinguish between three cases: + // 1) The predicate is explicitly present on the trail. + if trail_entry.predicate == predicate { + let (reason_ref, _) = trail_entry + .reason + .expect("Cannot be a null reason for propagation."); + + let explanation_context = ExplanationContext::new( + self.assignments, + CurrentNogood::empty(), + trail_position, + self.notification_engine, + ); + + let reason_exists = self.reason_store.get_or_compute( + reason_ref, + explanation_context, + self.propagators, + reason_buffer, + ); + + assert!(reason_exists, "reason reference should not be stale"); + } + // 2) The predicate is true due to a propagation, and not explicitly on the trail. + // It is necessary to further analyse what was the reason for setting the predicate true. + else { + // The reason for propagation depends on: + // 1) The predicate on the trail at the moment the input predicate became true, and + // 2) The input predicate. + match ( + trail_entry.predicate.get_predicate_type(), + predicate.get_predicate_type(), + ) { + (PredicateType::LowerBound, PredicateType::LowerBound) => { + let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_lower_bound = predicate.get_right_hand_side(); + // Both the input predicate and the trail predicate are lower bound + // literals. Two cases to consider: + // 1) The trail predicate has a greater right-hand side, meaning + // the reason for the input predicate is true is because a stronger + // right-hand side predicate was posted. We can reuse the same + // reason as for the trail bound. + // todo: could consider lifting here, since the trail bound + // might be too strong. + if trail_lower_bound > input_lower_bound { + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + // Otherwise, the input bound is strictly greater than the trailed + // bound. This means the reason is due to holes in the domain. + else { + // Note that the bounds cannot be equal. + // If the bound were equal, the predicate would be explicitly on the + // trail, so we would have detected this case earlier. + pumpkin_assert_simple!(trail_lower_bound < input_lower_bound); + + // The reason for the propagation of the input predicate [x >= a] is + // because [x >= a-1] & [x != a]. Conflict analysis will then + // recursively decompose these further. + + // Note that we do not need to worry about decreasing the lower + // bounds so much so that it reaches its root lower bound, for which + // there is no reason since it is given as input to the problem. + // We cannot reach the original lower bound since in the 1uip, we + // only look for reasons for predicates from the current decision + // level, and we never look for reasons at the root level. + + let one_less_bound_predicate = + predicate!(domain_id >= input_lower_bound - 1); + + let not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); + reason_buffer.extend(std::iter::once(one_less_bound_predicate)); + reason_buffer.extend(std::iter::once(not_equals_predicate)); + } + } + (PredicateType::LowerBound, PredicateType::NotEqual) => { + let trail_lower_bound = trail_entry.predicate.get_right_hand_side(); + let not_equal_constant = predicate.get_right_hand_side(); + // The trail entry is a lower bound literal, + // and the input predicate is a not equals. + // Only one case to consider: + // The trail lower bound is greater than the not_equals_constant, + // so it safe to take the reason from the trail. + // todo: lifting could be used here + pumpkin_assert_simple!(trail_lower_bound > not_equal_constant); + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + (PredicateType::LowerBound, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The input predicate is an equality predicate, and the trail predicate + // is a lower bound predicate. This means that the time of posting the + // trail predicate is when the input predicate became true. + + // Note that the input equality constant does _not_ necessarily equal + // the trail lower bound. This would be the + // case when the the trail lower bound is lower than the input equality + // constant, but due to holes in the domain, the lower bound got raised + // to just the value of the equality constant. + // For example, {1, 2, 3, 10}, then posting [x >= 5] will raise the + // lower bound to x >= 10. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + (PredicateType::UpperBound, PredicateType::UpperBound) => { + let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_upper_bound = predicate.get_right_hand_side(); + // Both the input and trail predicates are upper bound predicates. + // There are two scenarios to consider: + // 1) The input upper bound is greater than the trail upper bound, meaning that + // the reason for the input predicate is the propagation of a stronger upper + // bound. We can safely use the reason for of the trail predicate as the + // reason for the input predicate. + // todo: lifting could be applied here. + if trail_upper_bound < input_upper_bound { + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } else { + // I think it cannot be that the bounds are equal, since otherwise we + // would have found the predicate explicitly on the trail. + pumpkin_assert_simple!(trail_upper_bound > input_upper_bound); + + // The input upper bound is greater than the trail predicate, meaning + // that holes in the domain also played a rule in lowering the upper + // bound. + + // The reason of the input predicate [x <= a] is computed recursively as + // the reason for [x <= a + 1] & [x != a + 1]. + + let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); + let not_equal_predicate = predicate!(domain_id != input_upper_bound + 1); + reason_buffer.extend(std::iter::once(new_ub_predicate)); + reason_buffer.extend(std::iter::once(not_equal_predicate)); + } + } + (PredicateType::UpperBound, PredicateType::NotEqual) => { + let trail_upper_bound = trail_entry.predicate.get_right_hand_side(); + let not_equal_constant = predicate.get_right_hand_side(); + // The input predicate is a not equal predicate, and the trail predicate is + // an upper bound predicate. This is only possible when the upper bound was + // pushed below the not equals value. Otherwise the hole would have been + // explicitly placed on the trail and we would have found it earlier. + pumpkin_assert_simple!(not_equal_constant > trail_upper_bound); + + // The bound was set past the not equals, so we can safely returns the trail + // reason. todo: can do lifting here. + reason_buffer.extend(std::iter::once(trail_entry.predicate)); + } + (PredicateType::UpperBound, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The input predicate is an equality predicate, and the trail predicate + // is an upper bound predicate. This means that the time of posting the + // trail predicate is when the input predicate became true. + + // Note that the input equality constant does _not_ necessarily equal + // the trail upper bound. This would be the + // case when the the trail upper bound is greater than the input equality + // constant, but due to holes in the domain, the upper bound got lowered + // to just the value of the equality constant. + // For example, x = {1, 2, 3, 8, 15}, setting [x <= 12] would lower the + // upper bound to x <= 8. + + // Note that it could be that one of the two predicates are decision + // predicates, so we need to use the substitute functions. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + (PredicateType::NotEqual, PredicateType::LowerBound) => { + let not_equal_constant = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_lower_bound = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is a lower + // bound predicate. This means that creating the hole in the domain resulted + // in raising the lower bound. + + // I think this holds. The not_equals_constant cannot be greater, since that + // would not impact the lower bound. It can also not be the same, since + // creating a hole cannot result in the lower bound being raised to the + // hole, there must be some other reason for that to happen, which we would + // find earlier. + pumpkin_assert_simple!(input_lower_bound > not_equal_constant); + + // The reason for the input predicate [x >= a] is computed recursively as + // the reason for [x >= a - 1] & [x != a - 1]. + let new_lb_predicate = predicate!(domain_id >= input_lower_bound - 1); + let new_not_equals_predicate = predicate!(domain_id != input_lower_bound - 1); + + reason_buffer.extend(std::iter::once(new_lb_predicate)); + reason_buffer.extend(std::iter::once(new_not_equals_predicate)); + } + (PredicateType::NotEqual, PredicateType::UpperBound) => { + let not_equal_constant = trail_entry.predicate.get_right_hand_side(); + let domain_id = predicate.get_domain(); + let input_upper_bound = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is an upper + // bound predicate. This means that creating the hole in the domain resulted + // in lower the upper bound. + + // I think this holds. The not_equals_constant cannot be smaller, since that + // would not impact the upper bound. It can also not be the same, since + // creating a hole cannot result in the upper bound being lower to the + // hole, there must be some other reason for that to happen, which we would + // find earlier. + pumpkin_assert_simple!(input_upper_bound < not_equal_constant); + + // The reason for the input predicate [x <= a] is computed recursively as + // the reason for [x <= a + 1] & [x != a + 1]. + let new_ub_predicate = predicate!(domain_id <= input_upper_bound + 1); + let new_not_equals_predicate = predicate!(domain_id != input_upper_bound + 1); + + reason_buffer.extend(std::iter::once(new_ub_predicate)); + reason_buffer.extend(std::iter::once(new_not_equals_predicate)); + } + (PredicateType::NotEqual, PredicateType::Equal) => { + let domain_id = predicate.get_domain(); + let equality_constant = predicate.get_right_hand_side(); + // The trail predicate is not equals, but the input predicate is + // equals. The only time this could is when the not equals forces the + // lower/upper bounds to meet. So we simply look for the reasons for those + // bounds recursively. + + // Note that it could be that one of the two predicates are decision + // predicates, so we need to use the substitute functions. + + let predicate_lb = predicate!(domain_id >= equality_constant); + let predicate_ub = predicate!(domain_id <= equality_constant); + + reason_buffer.extend(std::iter::once(predicate_lb)); + reason_buffer.extend(std::iter::once(predicate_ub)); + } + ( + PredicateType::Equal, + PredicateType::LowerBound | PredicateType::UpperBound | PredicateType::NotEqual, + ) => { + // The trail predicate is equality, but the input predicate is either a + // lower-bound, upper-bound, or not equals. + // + // TODO: could consider lifting here + reason_buffer.extend(std::iter::once(trail_entry.predicate)) + } + _ => unreachable!( + "Unreachable combination of {} and {}", + trail_entry.predicate, predicate + ), + }; + } + } +} + +impl<'a> HasAssignments for MinimisationContext<'a> { + fn assignments(&self) -> &Assignments { + self.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..ee5a98a85 --- /dev/null +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs @@ -0,0 +1,9 @@ +use crate::engine::conflict_analysis::LearnedNogood; +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 [`LearnedNogood`] and minimises the nogood based on some strategy. + 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 ee9bf26f5..aae48e7cb 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,9 +1,12 @@ +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::LearnedNogood; +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; @@ -17,7 +20,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 @@ -33,14 +36,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.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; @@ -48,7 +47,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. @@ -71,14 +70,16 @@ 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_moderate!(context.assignments.is_predicate_satisfied(input_predicate)); + pumpkin_assert_moderate!(context.is_predicate_satisfied(input_predicate)); self.current_depth += 1; @@ -98,7 +99,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.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; @@ -108,7 +109,6 @@ impl RecursiveMinimiser { // (levels from the original learned clause) cannot be removed. if !self.is_decision_level_allowed( context - .assignments .get_decision_level_for_predicate(&input_predicate) .unwrap(), ) { @@ -120,23 +120,10 @@ 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( - input_predicate, - context.assignments, - CurrentNogood::from(current_nogood), - context.reason_store, - context.propagators, - context.proof_log, - context.unit_nogood_inference_codes, - &mut reason, - context.notification_engine, - context.variable_names, - ); - + context.get_propagation_reason(input_predicate, &mut reason); for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context - .assignments .get_decision_level_for_predicate(&antecedent_predicate) .unwrap() == 0 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 4f85187c3..04250e7c8 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::PropagatorHandle; use crate::basic_types::PredicateId; @@ -9,7 +11,9 @@ use crate::containers::StorageKey; use crate::engine::Assignments; 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; @@ -437,8 +441,19 @@ impl ResolutionResolver { 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 { + assignments: context.assignments, + reason_store: context.reason_store, + notification_engine: context.notification_engine, + propagators: context.propagators, + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + variable_names: context.variable_names, + counters: context.counters, + }, + &mut clean_nogood, + ); // We perform a final semantic minimisation call which allows the merging of the // equality predicates which remain in the nogood @@ -455,6 +470,57 @@ impl ResolutionResolver { .add_term((size_before_semantic_minimisation - clean_nogood.len()) as u64); } + let learned_nogood = LearnedNogood::create_from_vec(clean_nogood, context); + + pumpkin_assert_advanced!( + learned_nogood + .predicates + .iter() + .skip(1) + .all(|p| context.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 = Vec; + + 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 @@ -490,36 +556,9 @@ impl ResolutionResolver { 0 }; - pumpkin_assert_advanced!( - clean_nogood - .iter() - .skip(1) - .all(|p| context.assignments.is_predicate_satisfied(*p)) - ); - - // 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 71f1ce605..d3ee9e3ce 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 @@ -236,6 +236,15 @@ 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_decision_level_for_predicate(&self, predicate: &Predicate) -> Option { + self.assignments() + .get_decision_level_for_predicate(predicate) + } + fn is_literal_true(&self, literal: &Literal) -> bool { literal .get_integer_variable() From a09d9613923daba7b13d986d51635be63afbbab7 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 4 Dec 2025 12:17:34 +0100 Subject: [PATCH 2/6] refactor: use minimisation trait in semantic minimiser --- .../minimisers/minimisation_context.rs | 22 -- .../conflict_analysis/minimisers/minimiser.rs | 1 - .../minimisers/recursive_minimiser.rs | 12 +- .../minimisers/semantic_minimiser.rs | 322 ++++++++++++++---- .../resolvers/resolution_resolver.rs | 51 ++- .../engine/constraint_satisfaction_solver.rs | 2 - pumpkin-crates/core/src/engine/cp/mod.rs | 7 - .../contexts/propagation_context.rs | 4 - .../core/src/engine/cp/test_solver.rs | 6 - .../core/src/engine/debug_helper.rs | 9 - .../time_table/propagation_handler.rs | 5 - .../propagators/nogoods/nogood_propagator.rs | 11 +- 12 files changed, 290 insertions(+), 162 deletions(-) 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 index b55fa2c44..8abe113d2 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -2,7 +2,6 @@ use crate::containers::HashMap; use crate::engine::Assignments; use crate::engine::SolverStatistics; use crate::engine::VariableNames; -use crate::engine::conflict_analysis::ConflictAnalysisContext; use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::CurrentNogood; use crate::engine::propagation::ExplanationContext; @@ -30,27 +29,6 @@ pub(crate) struct MinimisationContext<'a> { } impl<'a> MinimisationContext<'a> { - pub(crate) fn new( - assignments: &'a Assignments, - reason_store: &'a mut ReasonStore, - notification_engine: &'a mut NotificationEngine, - propagators: &'a mut PropagatorStore, - proof_log: &'a mut ProofLog, - unit_nogood_inference_codes: &'a HashMap, - variable_names: &'a VariableNames, - counters: &'a mut SolverStatistics, - ) -> Self { - Self { - assignments, - reason_store, - notification_engine, - propagators, - proof_log, - unit_nogood_inference_codes, - variable_names, - counters, - } - } /// Compute the reason for `predicate` being true. The reason will be stored in /// `reason_buffer`. /// diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs index ee5a98a85..791964891 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs @@ -1,4 +1,3 @@ -use crate::engine::conflict_analysis::LearnedNogood; use crate::engine::conflict_analysis::MinimisationContext; use crate::predicates::Predicate; 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 aae48e7cb..76152fdcc 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 @@ -3,7 +3,6 @@ use crate::basic_types::moving_averages::MovingAverage; use crate::containers::HashMap; use crate::containers::HashSet; use crate::engine::Assignments; -use crate::engine::conflict_analysis::LearnedNogood; use crate::engine::conflict_analysis::NogoodMinimiser; use crate::engine::propagation::ReadDomains; use crate::engine::propagation::contexts::HasAssignments; @@ -47,7 +46,7 @@ impl NogoodMinimiser for RecursiveMinimiser { for i in 0..initial_nogood_size { let learned_predicate = nogood[i]; - self.compute_label(learned_predicate, &mut context, nogood); + self.compute_label(learned_predicate, &mut context); let label = self.get_predicate_label(learned_predicate); // Keep the predicate in case it was not deemed deemed redundant. @@ -73,12 +72,7 @@ impl NogoodMinimiser for RecursiveMinimiser { } impl RecursiveMinimiser { - fn compute_label( - &mut self, - input_predicate: Predicate, - context: &mut MinimisationContext, - current_nogood: &[Predicate], - ) { + fn compute_label(&mut self, input_predicate: Predicate, context: &mut MinimisationContext) { pumpkin_assert_moderate!(context.is_predicate_satisfied(input_predicate)); self.current_depth += 1; @@ -147,7 +141,7 @@ impl RecursiveMinimiser { } // Compute the label of the antecedent predicate. - self.compute_label(antecedent_predicate, context, current_nogood); + self.compute_label(antecedent_predicate, context); // In case one of the antecedents is Poison, // the input predicate is not deemed redundant. 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..1cda655c9 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,23 +261,44 @@ impl SimpleIntegerDomain { #[cfg(test)] mod tests { use crate::conjunction; + use crate::containers::HashMap; use crate::engine::Assignments; + use crate::engine::SolverStatistics; + use crate::engine::VariableNames; + 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::engine::notifications::NotificationEngine; + use crate::engine::propagation::store::PropagatorStore; + use crate::engine::reason::ReasonStore; use crate::predicate; use crate::predicates::Predicate; use crate::predicates::PropositionalConjunction; + use crate::proof::ProofLog; #[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 nogood: Vec = + vec![predicate!(domain_id >= 0), predicate!(domain_id <= 10)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + p.minimise(context, &mut nogood); - assert!(p.is_empty()); + assert!(nogood.is_empty()); } #[test] @@ -278,12 +306,24 @@ mod tests { 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 nogood: Vec = + vec![predicate!(domain_id >= 5), predicate!(domain_id <= 4)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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] @@ -291,16 +331,27 @@ mod tests { let mut p = SemanticMinimiser::default(); let mut assignments = Assignments::default(); let domain_id = assignments.grow(0, 10); - let nogood: Vec = vec![ + 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 { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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] @@ -308,12 +359,24 @@ mod tests { 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 nogood: Vec = + vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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] @@ -321,13 +384,36 @@ mod tests { 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 p = p.minimise(&vec![], &assignments, Mode::EnableEqualityMerging); + let mut nogood: Vec = + vec![predicate!(domain_id != 5), predicate!(domain_id == 5)]; + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + p.minimise(context, &mut nogood); + + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + let mut other = Vec::default(); + p.minimise(context, &mut other); - assert!(p.is_empty()); + assert!(other.is_empty()); } #[test] @@ -337,15 +423,26 @@ mod tests { let domain_0 = assignments.grow(0, 10); let domain_1 = assignments.grow(0, 5); - 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 { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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]) ); } @@ -357,16 +454,27 @@ mod tests { let domain_0 = assignments.grow(0, 10); let domain_1 = assignments.grow(0, 5); - 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 { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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]) ); } @@ -378,7 +486,7 @@ mod tests { let domain_0 = assignments.grow(0, 10); let domain_1 = assignments.grow(0, 5); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -390,11 +498,22 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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] @@ -413,7 +532,7 @@ mod tests { let domain_0 = assignments.grow(0, 10); let domain_1 = assignments.grow(0, 5); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -426,11 +545,22 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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]) ); } @@ -442,7 +572,7 @@ mod tests { let domain_0 = assignments.grow(0, 10); let domain_1 = assignments.grow(0, 5); - let nogood = conjunction!( + let mut nogood = conjunction!( [domain_0 >= 5] & [domain_0 <= 9] & [domain_1 >= 0] @@ -455,11 +585,22 @@ mod tests { ) .into(); - let predicates = p.minimise(&nogood, &assignments, Mode::DisableEqualityMerging); + p.set_mode(Mode::DisableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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]) ); } @@ -470,12 +611,23 @@ mod tests { let mut assignments = Assignments::default(); let domain_0 = assignments.grow(0, 10); - let nogood = conjunction!([domain_0 >= 2] & [domain_0 >= 1] & [domain_0 >= 5]).into(); - - let predicates = p.minimise(&nogood, &assignments, Mode::EnableEqualityMerging); + let mut nogood = conjunction!([domain_0 >= 2] & [domain_0 >= 1] & [domain_0 >= 5]).into(); + + p.set_mode(Mode::EnableEqualityMerging); + let context = MinimisationContext { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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] @@ -484,15 +636,26 @@ mod tests { let mut assignments = Assignments::default(); let domain_0 = assignments.grow(0, 10); - 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 { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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]) ); } @@ -503,13 +666,24 @@ mod tests { let mut assignments = Assignments::default(); let domain_0 = assignments.grow(0, 10); - 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 { + assignments: &assignments, + reason_store: &mut ReasonStore::default(), + notification_engine: &mut NotificationEngine::default(), + propagators: &mut PropagatorStore::default(), + proof_log: &mut ProofLog::default(), + unit_nogood_inference_codes: &mut HashMap::default(), + variable_names: &VariableNames::default(), + counters: &mut SolverStatistics::default(), + }; + 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 04250e7c8..19098a4b1 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 @@ -268,7 +268,6 @@ impl ResolutionResolver { context.trailed_values, context.assignments, context.reason_store, - context.semantic_minimiser, context.notification_engine, self.nogood_propagator_handle.propagator_id(), ); @@ -426,17 +425,28 @@ 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.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 { + assignments: context.assignments, + reason_store: context.reason_store, + notification_engine: context.notification_engine, + propagators: context.propagators, + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + variable_names: context.variable_names, + counters: context.counters, }, + &mut self.processed_nogood_predicates, ); if context.should_minimise { @@ -452,25 +462,40 @@ impl ResolutionResolver { variable_names: context.variable_names, counters: context.counters, }, - &mut clean_nogood, + &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.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 { + assignments: context.assignments, + reason_store: context.reason_store, + notification_engine: context.notification_engine, + propagators: context.propagators, + proof_log: context.proof_log, + unit_nogood_inference_codes: context.unit_nogood_inference_codes, + variable_names: context.variable_names, + counters: context.counters, + }, + &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(clean_nogood, context); + let learned_nogood = + LearnedNogood::create_from_vec(self.processed_nogood_predicates.clone(), context); pumpkin_assert_advanced!( learned_nogood diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 9d75a5b14..049237445 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -968,7 +968,6 @@ impl ConstraintSatisfactionSolver { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut self.semantic_minimiser, &mut self.notification_engine, propagator_id, ); @@ -1230,7 +1229,6 @@ impl ConstraintSatisfactionSolver { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut self.semantic_minimiser, &mut self.notification_engine, self.nogood_propagator_handle.propagator_id(), ); diff --git a/pumpkin-crates/core/src/engine/cp/mod.rs b/pumpkin-crates/core/src/engine/cp/mod.rs index 84ef1014c..82091d2ea 100644 --- a/pumpkin-crates/core/src/engine/cp/mod.rs +++ b/pumpkin-crates/core/src/engine/cp/mod.rs @@ -17,7 +17,6 @@ mod tests { use crate::conjunction; use crate::containers::StorageKey; use crate::engine::TrailedValues; - use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::cp::assignments; use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::PropagationContextMut; @@ -35,13 +34,11 @@ mod tests { let mut reason_store = ReasonStore::default(); assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); @@ -66,13 +63,11 @@ mod tests { assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); @@ -97,13 +92,11 @@ mod tests { assert_eq!(reason_store.len(), 0); { - let mut semantic_miniser = SemanticMinimiser::default(); let mut notification_engine = NotificationEngine::default(); let mut context = PropagationContextMut::new( &mut trailed_values, &mut assignments, &mut reason_store, - &mut semantic_miniser, &mut notification_engine, PropagatorId(0), ); 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 d3ee9e3ce..fa1f83edd 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 @@ -3,7 +3,6 @@ use crate::engine::Assignments; use crate::engine::EmptyDomain; use crate::engine::TrailedInteger; use crate::engine::TrailedValues; -use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::notifications::NotificationEngine; use crate::engine::notifications::PredicateIdAssignments; use crate::engine::predicates::predicate::Predicate; @@ -67,7 +66,6 @@ pub(crate) struct PropagationContextMut<'a> { pub(crate) assignments: &'a mut Assignments, pub(crate) reason_store: &'a mut ReasonStore, pub(crate) propagator_id: PropagatorId, - pub(crate) semantic_minimiser: &'a mut SemanticMinimiser, pub(crate) notification_engine: &'a mut NotificationEngine, reification_literal: Option, } @@ -77,7 +75,6 @@ impl<'a> PropagationContextMut<'a> { trailed_values: &'a mut TrailedValues, assignments: &'a mut Assignments, reason_store: &'a mut ReasonStore, - semantic_minimiser: &'a mut SemanticMinimiser, notification_engine: &'a mut NotificationEngine, propagator_id: PropagatorId, ) -> Self { @@ -87,7 +84,6 @@ impl<'a> PropagationContextMut<'a> { reason_store, propagator_id, notification_engine, - semantic_minimiser, reification_literal: None, } } diff --git a/pumpkin-crates/core/src/engine/cp/test_solver.rs b/pumpkin-crates/core/src/engine/cp/test_solver.rs index 92053c1ee..3b11432f0 100644 --- a/pumpkin-crates/core/src/engine/cp/test_solver.rs +++ b/pumpkin-crates/core/src/engine/cp/test_solver.rs @@ -15,7 +15,6 @@ use crate::basic_types::Inconsistency; use crate::containers::KeyGenerator; use crate::engine::Assignments; use crate::engine::EmptyDomain; -use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::PropagationContext; @@ -37,7 +36,6 @@ pub(crate) struct TestSolver { pub assignments: Assignments, pub propagator_store: PropagatorStore, pub reason_store: ReasonStore, - pub semantic_minimiser: SemanticMinimiser, pub trailed_values: TrailedValues, pub notification_engine: NotificationEngine, constraint_tags: KeyGenerator, @@ -50,7 +48,6 @@ impl Default for TestSolver { assignments: Default::default(), reason_store: Default::default(), propagator_store: Default::default(), - semantic_minimiser: Default::default(), notification_engine: Default::default(), trailed_values: Default::default(), constraint_tags: Default::default(), @@ -118,7 +115,6 @@ impl TestSolver { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut self.semantic_minimiser, &mut self.notification_engine, PropagatorId(0), ); @@ -273,7 +269,6 @@ impl TestSolver { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut self.semantic_minimiser, &mut self.notification_engine, PropagatorId(0), ); @@ -293,7 +288,6 @@ impl TestSolver { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut self.semantic_minimiser, &mut self.notification_engine, PropagatorId(0), ); diff --git a/pumpkin-crates/core/src/engine/debug_helper.rs b/pumpkin-crates/core/src/engine/debug_helper.rs index bf51dfc97..1e5b0d936 100644 --- a/pumpkin-crates/core/src/engine/debug_helper.rs +++ b/pumpkin-crates/core/src/engine/debug_helper.rs @@ -6,7 +6,6 @@ use log::debug; use log::warn; use super::TrailedValues; -use super::conflict_analysis::SemanticMinimiser; use super::notifications::NotificationEngine; use super::predicates::predicate::Predicate; use super::propagation::ExplanationContext; @@ -79,12 +78,10 @@ impl DebugHelper { let num_entries_on_trail_before_propagation = assignments_clone.num_trail_entries(); let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, PropagatorId(propagator_id as u32), ); @@ -260,12 +257,10 @@ impl DebugHelper { if adding_predicates_was_successful { // Now propagate using the debug propagation method. let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); @@ -366,7 +361,6 @@ impl DebugHelper { if adding_predicates_was_successful { // now propagate using the debug propagation method let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); // Note that it might take multiple iterations before the conflict is reached due // to the assumption that some propagators make on that they are not idempotent! @@ -382,7 +376,6 @@ impl DebugHelper { &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); @@ -446,12 +439,10 @@ impl DebugHelper { if adding_predicates_was_successful { // now propagate using the debug propagation method let mut reason_store = Default::default(); - let mut semantic_minimiser = SemanticMinimiser::default(); let context = PropagationContextMut::new( &mut trailed_values_clone, &mut assignments_clone, &mut reason_store, - &mut semantic_minimiser, &mut notification_engine_clone, propagator_id, ); diff --git a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs index e490b14ed..17a7ccde7 100644 --- a/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs +++ b/pumpkin-crates/core/src/propagators/cumulative/time_table/propagation_handler.rs @@ -485,7 +485,6 @@ pub(crate) mod test_propagation_handler { use crate::containers::StorageKey; use crate::engine::Assignments; use crate::engine::TrailedValues; - use crate::engine::conflict_analysis::SemanticMinimiser; use crate::engine::notifications::NotificationEngine; use crate::engine::propagation::ExplanationContext; use crate::engine::propagation::LocalId; @@ -594,7 +593,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -659,7 +657,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -710,7 +707,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), @@ -775,7 +771,6 @@ pub(crate) mod test_propagation_handler { &mut self.trailed_values, &mut self.assignments, &mut self.reason_store, - &mut SemanticMinimiser::default(), &mut self.notification_engine, PropagatorId(0), ), diff --git a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs index 4cbc3a49f..93999c4d5 100644 --- a/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs +++ b/pumpkin-crates/core/src/propagators/nogoods/nogood_propagator.rs @@ -19,7 +19,6 @@ use crate::engine::Assignments; use crate::engine::Lbd; use crate::engine::SolverStatistics; use crate::engine::TrailedValues; -use crate::engine::conflict_analysis::Mode; use crate::engine::notifications::NotificationEngine; use crate::engine::predicates::predicate::Predicate; use crate::engine::propagation::ExplanationContext; @@ -1120,13 +1119,7 @@ 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. - // Semantic minimisation will take care of removing duplicate predicates, conflicting - // nogoods, and may result in few predicates since it removes redundancies. - *nogood = context.semantic_minimiser.minimise( - nogood, - context.assignments, - Mode::EnableEqualityMerging, - ); + // 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)) { @@ -1317,7 +1310,6 @@ mod tests { &mut solver.trailed_values, &mut solver.assignments, &mut solver.reason_store, - &mut solver.semantic_minimiser, &mut solver.notification_engine, handle.propagator_id(), ); @@ -1367,7 +1359,6 @@ mod tests { &mut solver.trailed_values, &mut solver.assignments, &mut solver.reason_store, - &mut solver.semantic_minimiser, &mut solver.notification_engine, handle.propagator_id(), ); From 0918fdd43500195744cb84bce13e51f0b65bfa29 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 4 Dec 2025 13:20:58 +0100 Subject: [PATCH 3/6] fix: pass current nogood when getting current reason in minimisation context --- .../minimisers/minimisation_context.rs | 3 ++- .../conflict_analysis/minimisers/minimiser.rs | 3 ++- .../minimisers/recursive_minimiser.rs | 13 +++++++++---- 3 files changed, 13 insertions(+), 6 deletions(-) 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 index 8abe113d2..e448a5749 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -37,6 +37,7 @@ impl<'a> MinimisationContext<'a> { &mut self, predicate: Predicate, reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + current_nogood: CurrentNogood, ) { if self.assignments.is_initial_bound(predicate) { return; @@ -58,7 +59,7 @@ impl<'a> MinimisationContext<'a> { let explanation_context = ExplanationContext::new( self.assignments, - CurrentNogood::empty(), + current_nogood, trail_position, self.notification_engine, ); diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs index 791964891..5752c6bd9 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimiser.rs @@ -3,6 +3,7 @@ use crate::predicates::Predicate; /// A trait for the behaviour of nogood minimisation approaches. pub(crate) trait NogoodMinimiser: Default { - /// Takes as input a [`LearnedNogood`] and minimises the nogood based on some strategy. + /// 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/recursive_minimiser.rs b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs index 76152fdcc..04cdc6af4 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 @@ -46,7 +46,7 @@ impl NogoodMinimiser for RecursiveMinimiser { for i in 0..initial_nogood_size { let learned_predicate = nogood[i]; - self.compute_label(learned_predicate, &mut context); + 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,7 +72,12 @@ impl NogoodMinimiser for RecursiveMinimiser { } impl RecursiveMinimiser { - fn compute_label(&mut self, input_predicate: Predicate, context: &mut MinimisationContext) { + fn compute_label( + &mut self, + input_predicate: Predicate, + context: &mut MinimisationContext, + current_nogood: &[Predicate], + ) { pumpkin_assert_moderate!(context.is_predicate_satisfied(input_predicate)); self.current_depth += 1; @@ -114,7 +119,7 @@ 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![]; - context.get_propagation_reason(input_predicate, &mut reason); + context.get_propagation_reason(input_predicate, &mut reason, current_nogood.into()); for antecedent_predicate in reason.iter().copied() { // Root assignments can be safely ignored. if context @@ -141,7 +146,7 @@ impl RecursiveMinimiser { } // Compute the label of the antecedent predicate. - self.compute_label(antecedent_predicate, context); + self.compute_label(antecedent_predicate, context, current_nogood); // In case one of the antecedents is Poison, // the input predicate is not deemed redundant. From 1763bda944a366564064528559b8d8e156afa7fc Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Fri, 12 Dec 2025 12:07:00 +0100 Subject: [PATCH 4/6] refactor: use explicit helper methods --- .../minimisers/minimisation_context.rs | 19 +++++++++++++++ .../minimisers/recursive_minimiser.rs | 24 +++++++------------ .../contexts/propagation_context.rs | 8 +++++++ 3 files changed, 35 insertions(+), 16 deletions(-) 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 index c1d4dae17..154714e6f 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -1,10 +1,12 @@ use crate::containers::HashMap; use crate::engine::Assignments; use crate::engine::SolverStatistics; +use crate::engine::conflict_analysis::ConflictAnalysisContext; 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; pub(crate) struct MinimisationContext<'a> { @@ -15,6 +17,23 @@ pub(crate) struct MinimisationContext<'a> { pub(crate) counters: &'a mut SolverStatistics, } +impl<'a> MinimisationContext<'a> { + 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 { 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 e80580de6..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 @@ -3,8 +3,9 @@ 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::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; @@ -39,7 +40,7 @@ impl NogoodMinimiser for RecursiveMinimiser { 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; @@ -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/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() From cae297a93be90cd197e63ea615561e8dd308ac91 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Fri, 12 Dec 2025 12:19:52 +0100 Subject: [PATCH 5/6] docs: adding documentation to minimisation context --- .../minimisers/minimisation_context.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) 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 index 154714e6f..fb6e8439e 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/minimisers/minimisation_context.rs @@ -2,6 +2,8 @@ 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; @@ -9,6 +11,11 @@ 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, @@ -18,6 +25,10 @@ pub(crate) struct MinimisationContext<'a> { 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]>), From a6cd9b936b36cf2de517d076ce7e9fd49ea3b3ab Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Fri, 12 Dec 2025 12:20:23 +0100 Subject: [PATCH 6/6] chore: deref for learned nogood is slice instead of vec --- .../engine/conflict_analysis/resolvers/resolution_resolver.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 da306102f..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 @@ -502,7 +502,7 @@ pub(crate) struct LearnedNogood { } impl Deref for LearnedNogood { - type Target = Vec; + type Target = [Predicate]; fn deref(&self) -> &Self::Target { &self.predicates