From 7ab903d78b21a5a51fa077b0e4b6a44f9b24a9ab Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Tue, 11 Nov 2025 12:13:11 +0100 Subject: [PATCH 1/5] refactor: Store the conflict info as the predicate and reason --- .../src/basic_types/stored_conflict_info.rs | 9 +- .../conflict_analysis_context.rs | 102 +++++++++++- .../engine/constraint_satisfaction_solver.rs | 157 ++++-------------- .../core/src/engine/cp/assignments.rs | 10 +- 4 files changed, 148 insertions(+), 130 deletions(-) diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index e9176255a..59c95ea02 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -1,10 +1,12 @@ -use super::PropositionalConjunction; use super::propagation_status_cp::PropagatorConflict; use crate::ConstraintOperationError; #[cfg(doc)] use crate::engine::ConstraintSatisfactionSolver; #[cfg(doc)] use crate::engine::propagation::Propagator; +use crate::engine::reason::ReasonRef; +use crate::predicates::Predicate; +use crate::proof::InferenceCode; /// A conflict info which can be stored in the solver. /// Two (related) conflicts can happen: @@ -14,7 +16,10 @@ use crate::engine::propagation::Propagator; pub(crate) enum StoredConflictInfo { Propagator(PropagatorConflict), EmptyDomain { - conflict_nogood: PropositionalConjunction, + trigger_predicate: Predicate, + trigger_reason: ReasonRef, + trigger_inference_code: InferenceCode, }, + InfeasibleAssumptions(Predicate), RootLevelConflict(ConstraintOperationError), } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 4a8e0ff19..486e75f2b 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -23,6 +23,7 @@ use crate::engine::reason::ReasonRef; use crate::engine::reason::ReasonStore; use crate::engine::solver_statistics::SolverStatistics; use crate::predicate; +use crate::predicates::PropositionalConjunction; use crate::proof::InferenceCode; use crate::proof::ProofLog; use crate::proof::RootExplanationContext; @@ -120,10 +121,21 @@ impl ConflictAnalysisContext<'_> { conflict.conjunction } - StoredConflictInfo::EmptyDomain { conflict_nogood } => conflict_nogood, + StoredConflictInfo::EmptyDomain { + trigger_predicate, + trigger_reason, + trigger_inference_code, + } => self.compute_conflict_nogood( + trigger_predicate, + trigger_reason, + trigger_inference_code, + ), StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } + StoredConflictInfo::InfeasibleAssumptions(predicate) => { + vec![predicate, !predicate].into() + } }; for &predicate in conflict_nogood.iter() { @@ -495,4 +507,92 @@ impl ConflictAnalysisContext<'_> { }; } } + + fn compute_conflict_nogood( + &mut self, + trigger_predicate: Predicate, + trigger_reason: ReasonRef, + trigger_inference_code: InferenceCode, + ) -> PropositionalConjunction { + let conflict_domain = trigger_predicate.get_domain(); + + // Look up the reason for the bound that changed. + // The reason for changing the bound cannot be a decision, so we can safely unwrap. + let mut empty_domain_reason: Vec = vec![]; + let _ = self.reason_store.get_or_compute( + trigger_reason, + ExplanationContext::without_working_nogood( + self.assignments, + self.assignments.num_trail_entries() - 1, + self.notification_engine, + ), + self.propagators, + &mut empty_domain_reason, + ); + + // We also need to log this last propagation to the proof log as an inference. + let _ = self.proof_log.log_inference( + trigger_inference_code, + empty_domain_reason.iter().copied(), + Some(trigger_predicate), + self.variable_names, + ); + + let old_lower_bound = self.assignments.get_lower_bound(conflict_domain); + let old_upper_bound = self.assignments.get_upper_bound(conflict_domain); + + // Now we get the explanation for the bound which was conflicting with the last trail entry + match trigger_predicate.get_predicate_type() { + PredicateType::LowerBound => { + // The last trail entry was a lower-bound propagation meaning that the empty domain + // was caused by the upper-bound + // + // We lift so that it is the most general upper-bound possible while still causing + // the empty domain + empty_domain_reason.push(predicate!( + conflict_domain <= trigger_predicate.get_right_hand_side() - 1 + )); + } + PredicateType::UpperBound => { + // The last trail entry was an upper-bound propagation meaning that the empty domain + // was caused by the lower-bound + // + // We lift so that it is the most general lower-bound possible while still causing + // the empty domain + empty_domain_reason.push(predicate!( + conflict_domain >= trigger_predicate.get_right_hand_side() + 1 + )); + } + PredicateType::NotEqual => { + empty_domain_reason.push(trigger_predicate); + } + PredicateType::Equal => { + // The last trail entry was an equality propagation; we split into three cases. + if trigger_predicate.get_right_hand_side() < old_lower_bound { + // 1) The assigned value was lower than the lower-bound + // + // We lift so that it is the most general lower-bound possible while still + // causing the empty domain + empty_domain_reason.push(predicate!( + conflict_domain >= trigger_predicate.get_right_hand_side() + 1 + )); + } else if trigger_predicate.get_right_hand_side() > old_upper_bound { + // 2) The assigned value was larger than the upper-bound + // + // We lift so that it is the most general upper-bound possible while still + // causing the empty domain + empty_domain_reason.push(predicate!( + conflict_domain <= trigger_predicate.get_right_hand_side() - 1 + )); + } else { + // 3) The assigned value was equal to a hole in the domain + empty_domain_reason.push(predicate!( + conflict_domain != trigger_predicate.get_right_hand_side() + )) + } + } + } + + empty_domain_reason.into() + } } diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 9ee67c8ff..b6a96c594 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -29,7 +29,6 @@ use crate::basic_types::CSPSolverExecutionFlag; use crate::basic_types::ConstraintOperationError; use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; -use crate::basic_types::PropositionalConjunction; use crate::basic_types::Random; use crate::basic_types::SolutionReference; use crate::basic_types::StoredConflictInfo; @@ -52,8 +51,6 @@ use crate::engine::propagation::constructor::PropagatorConstructorContext; use crate::engine::propagation::store::PropagatorHandle; use crate::engine::reason::ReasonStore; use crate::engine::variables::DomainId; -use crate::predicate; -use crate::predicates::PredicateType; use crate::proof::ConstraintTag; use crate::proof::FinalizingContext; use crate::proof::InferenceCode; @@ -234,25 +231,41 @@ impl ConstraintSatisfactionSolver { } fn complete_proof(&mut self) { - let conflict = match self.state.get_conflict_info() { - StoredConflictInfo::Propagator(conflict) => { - let _ = self.internal_parameters.proof_log.log_inference( - conflict.inference_code, - conflict.conjunction.iter().copied(), - None, - &self.variable_names, - ); + struct DummyBrancher; - conflict.conjunction.clone() + impl Brancher for DummyBrancher { + fn next_decision(&mut self, _: &mut SelectionContext) -> Option { + unreachable!() } - StoredConflictInfo::EmptyDomain { conflict_nogood } => conflict_nogood.clone(), - StoredConflictInfo::RootLevelConflict(_) => { - unreachable!("There should always be a specified conflicting constraint.") + + fn subscribe_to_events(&self) -> Vec { + unreachable!() } + } + + let mut conflict_analysis_context = ConflictAnalysisContext { + assignments: &mut self.assignments, + counters: &mut self.solver_statistics, + solver_state: &mut self.state, + reason_store: &mut self.reason_store, + brancher: &mut DummyBrancher, + semantic_minimiser: &mut self.semantic_minimiser, + propagators: &mut self.propagators, + notification_engine: &mut self.notification_engine, + propagator_queue: &mut self.propagator_queue, + should_minimise: self.internal_parameters.learning_clause_minimisation, + proof_log: &mut self.internal_parameters.proof_log, + unit_nogood_inference_codes: &mut self.unit_nogood_inference_codes, + trailed_values: &mut self.trailed_values, + variable_names: &self.variable_names, + rng: &mut self.internal_parameters.random_generator, + restart_strategy: &mut self.restart_strategy, }; + let conflict = conflict_analysis_context.get_conflict_nogood(); + let context = FinalizingContext { - conflict, + conflict: conflict.into(), propagators: &mut self.propagators, proof_log: &mut self.internal_parameters.proof_log, unit_nogood_inference_codes: &self.unit_nogood_inference_codes, @@ -925,105 +938,6 @@ impl ConstraintSatisfactionSolver { notification_engine.synchronise(backtrack_level, assignments, trailed_values); } - pub(crate) fn compute_reason_for_empty_domain(&mut self) -> PropositionalConjunction { - // The empty domain happened after posting the last predicate on the trail. - // The reason for this empty domain is computed as the reason for the bounds before the last - // trail predicate was posted, plus the reason for the last trail predicate. - - // The last predicate on the trail reveals the domain id that has resulted - // in an empty domain. - let entry = self.assignments.get_last_entry_on_trail(); - let (entry_reason, entry_inference_code) = entry - .reason - .expect("Cannot cause an empty domain using a decision."); - let conflict_domain = entry.predicate.get_domain(); - assert!( - entry.old_lower_bound != self.assignments.get_lower_bound(conflict_domain) - || entry.old_upper_bound != self.assignments.get_upper_bound(conflict_domain), - "One of the two bounds had to change." - ); - - // Look up the reason for the bound that changed. - // The reason for changing the bound cannot be a decision, so we can safely unwrap. - let mut empty_domain_reason: Vec = vec![]; - let _ = self.reason_store.get_or_compute( - entry_reason, - ExplanationContext::without_working_nogood( - &self.assignments, - self.assignments.num_trail_entries() - 1, - &mut self.notification_engine, - ), - &mut self.propagators, - &mut empty_domain_reason, - ); - - // We also need to log this last propagation to the proof log as an inference. - let _ = self.internal_parameters.proof_log.log_inference( - entry_inference_code, - empty_domain_reason.iter().copied(), - Some(entry.predicate), - &self.variable_names, - ); - - // Now we get the explanation for the bound which was conflicting with the last trail entry - match entry.predicate.get_predicate_type() { - PredicateType::LowerBound => { - // The last trail entry was a lower-bound propagation meaning that the empty domain - // was caused by the upper-bound - // - // We lift so that it is the most general upper-bound possible while still causing - // the empty domain - empty_domain_reason.push(predicate!( - conflict_domain <= entry.predicate.get_right_hand_side() - 1 - )); - } - PredicateType::UpperBound => { - // The last trail entry was an upper-bound propagation meaning that the empty domain - // was caused by the lower-bound - // - // We lift so that it is the most general lower-bound possible while still causing - // the empty domain - empty_domain_reason.push(predicate!( - conflict_domain >= entry.predicate.get_right_hand_side() + 1 - )); - } - PredicateType::NotEqual => { - // The last trail entry was a not equals propagation meaning that the empty domain - // was due to the domain being assigned to the removed value - pumpkin_assert_eq_simple!(entry.old_upper_bound, entry.old_lower_bound); - - empty_domain_reason.push(predicate!(conflict_domain == entry.old_lower_bound)); - } - PredicateType::Equal => { - // The last trail entry was an equality propagation; we split into three cases. - if entry.predicate.get_right_hand_side() < entry.old_lower_bound { - // 1) The assigned value was lower than the lower-bound - // - // We lift so that it is the most general lower-bound possible while still - // causing the empty domain - empty_domain_reason.push(predicate!( - conflict_domain >= entry.predicate.get_right_hand_side() + 1 - )); - } else if entry.predicate.get_right_hand_side() > entry.old_upper_bound { - // 2) The assigned value was larger than the upper-bound - // - // We lift so that it is the most general upper-bound possible while still - // causing the empty domain - empty_domain_reason.push(predicate!( - conflict_domain <= entry.predicate.get_right_hand_side() - 1 - )); - } else { - // 3) The assigned value was equal to a hole in the domain - empty_domain_reason.push(predicate!( - conflict_domain != entry.predicate.get_right_hand_side() - )) - } - } - } - - empty_domain_reason.into() - } - /// Main propagation loop. pub(crate) fn propagate(&mut self) { // Record the number of predicates on the trail for statistics purposes. @@ -1355,16 +1269,17 @@ impl ConstraintSatisfactionSolver { return; } - let empty_domain_reason = self.compute_reason_for_empty_domain(); - // TODO: As a temporary solution, we remove the last trail element. // This way we guarantee that the assignment is consistent, which is needed // for the conflict analysis data structures. The proper alternative would // be to forbid the assignments from getting into an inconsistent state. - self.assignments.remove_last_trail_element(); + let (trigger_predicate, trigger_reason, trigger_inference_code) = + self.assignments.remove_last_trail_element(); let stored_conflict_info = StoredConflictInfo::EmptyDomain { - conflict_nogood: empty_domain_reason, + trigger_predicate, + trigger_reason, + trigger_inference_code, }; self.state.declare_conflict(stored_conflict_info); } @@ -1525,9 +1440,7 @@ impl CSPSolverState { CSPSolverStateInternal::Conflict { conflict_info } => conflict_info.clone(), CSPSolverStateInternal::InfeasibleUnderAssumptions { violated_assumption, - } => StoredConflictInfo::EmptyDomain { - conflict_nogood: vec![*violated_assumption, !(*violated_assumption)].into(), - }, + } => StoredConflictInfo::InfeasibleAssumptions(*violated_assumption), _ => { panic!("Cannot extract conflict clause if solver is not in a conflict."); } diff --git a/pumpkin-crates/core/src/engine/cp/assignments.rs b/pumpkin-crates/core/src/engine/cp/assignments.rs index a8cf8975c..1aae1fde9 100644 --- a/pumpkin-crates/core/src/engine/cp/assignments.rs +++ b/pumpkin-crates/core/src/engine/cp/assignments.rs @@ -112,10 +112,6 @@ impl Assignments { self.trail[index] } - pub(crate) fn get_last_entry_on_trail(&self) -> ConstraintProgrammingTrailEntry { - *self.trail.last().unwrap() - } - // registers the domain of a new integer variable // note that this is an internal method that does _not_ allocate additional information // necessary for the solver apart from the domain when creating a new integer variable, use @@ -782,11 +778,15 @@ impl Assignments { } /// todo: This is a temporary hack, not to be used in general. - pub(crate) fn remove_last_trail_element(&mut self) { + pub(crate) fn remove_last_trail_element(&mut self) -> (Predicate, ReasonRef, InferenceCode) { let entry = self.trail.pop().unwrap(); let domain_id = entry.predicate.get_domain(); self.domains[domain_id].undo_trail_entry(&entry); self.update_bounds_snapshot(domain_id); + + let (reason, inference_code) = entry.reason.unwrap(); + + (entry.predicate, reason, inference_code) } /// Get the number of values pruned from all the domains. From bc900a124ab23cc11fd0aef5c0c48d52d13705fd Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 09:40:31 +0100 Subject: [PATCH 2/5] refactor: Introduce a dedicated `EmptyDomainConflict` --- pumpkin-crates/core/src/basic_types/mod.rs | 2 +- .../src/basic_types/stored_conflict_info.rs | 25 ++++++++--- .../conflict_analysis_context.rs | 41 ++++++++----------- .../engine/constraint_satisfaction_solver.rs | 5 ++- 4 files changed, 40 insertions(+), 33 deletions(-) diff --git a/pumpkin-crates/core/src/basic_types/mod.rs b/pumpkin-crates/core/src/basic_types/mod.rs index eb2114b3e..c670a7ac7 100644 --- a/pumpkin-crates/core/src/basic_types/mod.rs +++ b/pumpkin-crates/core/src/basic_types/mod.rs @@ -23,5 +23,5 @@ pub use random::*; pub use solution::ProblemSolution; pub use solution::Solution; pub use solution::SolutionReference; -pub(crate) use stored_conflict_info::StoredConflictInfo; +pub(crate) use stored_conflict_info::*; pub(crate) use trail::Trail; diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index 59c95ea02..bf392834b 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -7,6 +7,7 @@ use crate::engine::propagation::Propagator; use crate::engine::reason::ReasonRef; use crate::predicates::Predicate; use crate::proof::InferenceCode; +use crate::variables::DomainId; /// A conflict info which can be stored in the solver. /// Two (related) conflicts can happen: @@ -15,11 +16,25 @@ use crate::proof::InferenceCode; #[derive(Debug, PartialEq, Eq, Clone)] pub(crate) enum StoredConflictInfo { Propagator(PropagatorConflict), - EmptyDomain { - trigger_predicate: Predicate, - trigger_reason: ReasonRef, - trigger_inference_code: InferenceCode, - }, + EmptyDomain(EmptyDomainConflict), InfeasibleAssumptions(Predicate), RootLevelConflict(ConstraintOperationError), } + +/// A conflict because a domain became empty. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) struct EmptyDomainConflict { + /// The predicate that caused a domain to become empty. + pub(crate) trigger_predicate: Predicate, + /// The reason for [`EmptyDomainConflict::trigger_predicate`] to be true. + pub(crate) trigger_reason: ReasonRef, + /// The [`InferenceCode`] that accompanies [`EmptyDomainConflict::trigger_reason`]. + pub(crate) trigger_inference_code: InferenceCode, +} + +impl EmptyDomainConflict { + /// The domain that became empty. + pub(crate) fn domain(&self) -> DomainId { + self.trigger_predicate.get_domain() + } +} diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 486e75f2b..54ecd0d7e 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -2,6 +2,7 @@ use std::fmt::Debug; use super::minimisers::SemanticMinimiser; use crate::Random; +use crate::basic_types::EmptyDomainConflict; use crate::basic_types::StoredConflictInfo; use crate::branching::Brancher; use crate::containers::HashMap; @@ -121,15 +122,7 @@ impl ConflictAnalysisContext<'_> { conflict.conjunction } - StoredConflictInfo::EmptyDomain { - trigger_predicate, - trigger_reason, - trigger_inference_code, - } => self.compute_conflict_nogood( - trigger_predicate, - trigger_reason, - trigger_inference_code, - ), + StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict), StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } @@ -510,17 +503,15 @@ impl ConflictAnalysisContext<'_> { fn compute_conflict_nogood( &mut self, - trigger_predicate: Predicate, - trigger_reason: ReasonRef, - trigger_inference_code: InferenceCode, + conflict: EmptyDomainConflict, ) -> PropositionalConjunction { - let conflict_domain = trigger_predicate.get_domain(); + let conflict_domain = conflict.domain(); // Look up the reason for the bound that changed. // The reason for changing the bound cannot be a decision, so we can safely unwrap. let mut empty_domain_reason: Vec = vec![]; let _ = self.reason_store.get_or_compute( - trigger_reason, + conflict.trigger_reason, ExplanationContext::without_working_nogood( self.assignments, self.assignments.num_trail_entries() - 1, @@ -532,9 +523,9 @@ impl ConflictAnalysisContext<'_> { // We also need to log this last propagation to the proof log as an inference. let _ = self.proof_log.log_inference( - trigger_inference_code, + conflict.trigger_inference_code, empty_domain_reason.iter().copied(), - Some(trigger_predicate), + Some(conflict.trigger_predicate), self.variable_names, ); @@ -542,7 +533,7 @@ impl ConflictAnalysisContext<'_> { let old_upper_bound = self.assignments.get_upper_bound(conflict_domain); // Now we get the explanation for the bound which was conflicting with the last trail entry - match trigger_predicate.get_predicate_type() { + match conflict.trigger_predicate.get_predicate_type() { PredicateType::LowerBound => { // The last trail entry was a lower-bound propagation meaning that the empty domain // was caused by the upper-bound @@ -550,7 +541,7 @@ impl ConflictAnalysisContext<'_> { // We lift so that it is the most general upper-bound possible while still causing // the empty domain empty_domain_reason.push(predicate!( - conflict_domain <= trigger_predicate.get_right_hand_side() - 1 + conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1 )); } PredicateType::UpperBound => { @@ -560,34 +551,34 @@ impl ConflictAnalysisContext<'_> { // We lift so that it is the most general lower-bound possible while still causing // the empty domain empty_domain_reason.push(predicate!( - conflict_domain >= trigger_predicate.get_right_hand_side() + 1 + conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1 )); } PredicateType::NotEqual => { - empty_domain_reason.push(trigger_predicate); + empty_domain_reason.push(conflict.trigger_predicate); } PredicateType::Equal => { // The last trail entry was an equality propagation; we split into three cases. - if trigger_predicate.get_right_hand_side() < old_lower_bound { + if conflict.trigger_predicate.get_right_hand_side() < old_lower_bound { // 1) The assigned value was lower than the lower-bound // // We lift so that it is the most general lower-bound possible while still // causing the empty domain empty_domain_reason.push(predicate!( - conflict_domain >= trigger_predicate.get_right_hand_side() + 1 + conflict_domain >= conflict.trigger_predicate.get_right_hand_side() + 1 )); - } else if trigger_predicate.get_right_hand_side() > old_upper_bound { + } else if conflict.trigger_predicate.get_right_hand_side() > old_upper_bound { // 2) The assigned value was larger than the upper-bound // // We lift so that it is the most general upper-bound possible while still // causing the empty domain empty_domain_reason.push(predicate!( - conflict_domain <= trigger_predicate.get_right_hand_side() - 1 + conflict_domain <= conflict.trigger_predicate.get_right_hand_side() - 1 )); } else { // 3) The assigned value was equal to a hole in the domain empty_domain_reason.push(predicate!( - conflict_domain != trigger_predicate.get_right_hand_side() + conflict_domain != conflict.trigger_predicate.get_right_hand_side() )) } } diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index b6a96c594..e42bf7b21 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -27,6 +27,7 @@ use super::variables::Literal; use crate::Solver; use crate::basic_types::CSPSolverExecutionFlag; use crate::basic_types::ConstraintOperationError; +use crate::basic_types::EmptyDomainConflict; use crate::basic_types::Inconsistency; use crate::basic_types::PredicateId; use crate::basic_types::Random; @@ -1276,11 +1277,11 @@ impl ConstraintSatisfactionSolver { let (trigger_predicate, trigger_reason, trigger_inference_code) = self.assignments.remove_last_trail_element(); - let stored_conflict_info = StoredConflictInfo::EmptyDomain { + let stored_conflict_info = StoredConflictInfo::EmptyDomain(EmptyDomainConflict { trigger_predicate, trigger_reason, trigger_inference_code, - }; + }); self.state.declare_conflict(stored_conflict_info); } From 6a2baf98b66e0041e28001d7aa0a57e618801e25 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 09:43:11 +0100 Subject: [PATCH 3/5] docs: Clarify InconsistentAssumptions and its predicate --- pumpkin-crates/core/src/basic_types/stored_conflict_info.rs | 5 ++++- .../engine/conflict_analysis/conflict_analysis_context.rs | 2 +- .../core/src/engine/constraint_satisfaction_solver.rs | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs index bf392834b..1537ad7fc 100644 --- a/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs +++ b/pumpkin-crates/core/src/basic_types/stored_conflict_info.rs @@ -17,7 +17,10 @@ use crate::variables::DomainId; pub(crate) enum StoredConflictInfo { Propagator(PropagatorConflict), EmptyDomain(EmptyDomainConflict), - InfeasibleAssumptions(Predicate), + /// The conflict is due to inconsistent assumptions. + /// + /// The provided predicate and its negation are both assumptions. + InconsistentAssumptions(Predicate), RootLevelConflict(ConstraintOperationError), } diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 54ecd0d7e..3ac5a9d1f 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -126,7 +126,7 @@ impl ConflictAnalysisContext<'_> { StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } - StoredConflictInfo::InfeasibleAssumptions(predicate) => { + StoredConflictInfo::InconsistentAssumptions(predicate) => { vec![predicate, !predicate].into() } }; diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index e42bf7b21..93ad459b9 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -1441,7 +1441,7 @@ impl CSPSolverState { CSPSolverStateInternal::Conflict { conflict_info } => conflict_info.clone(), CSPSolverStateInternal::InfeasibleUnderAssumptions { violated_assumption, - } => StoredConflictInfo::InfeasibleAssumptions(*violated_assumption), + } => StoredConflictInfo::InconsistentAssumptions(*violated_assumption), _ => { panic!("Cannot extract conflict clause if solver is not in a conflict."); } From 091892011e43cf495d5a6f0b145ba9ecc16efc57 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 09:55:13 +0100 Subject: [PATCH 4/5] fix: computation of conflict nogood for empty domain --- .../conflict_analysis_context.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index 3ac5a9d1f..f33576014 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -30,6 +30,7 @@ use crate::proof::ProofLog; use crate::proof::RootExplanationContext; use crate::proof::explain_root_assignment; use crate::propagators::nogoods::NogoodPropagator; +use crate::pumpkin_assert_eq_simple; use crate::pumpkin_assert_simple; /// Used during conflict analysis to provide the necessary information. @@ -132,12 +133,12 @@ impl ConflictAnalysisContext<'_> { }; for &predicate in conflict_nogood.iter() { - if self + let predicate_dl = self .assignments .get_decision_level_for_predicate(&predicate) - .unwrap() - == 0 - { + .unwrap(); + + if predicate_dl == 0 { explain_root_assignment( &mut RootExplanationContext { propagators: self.propagators, @@ -532,7 +533,6 @@ impl ConflictAnalysisContext<'_> { let old_lower_bound = self.assignments.get_lower_bound(conflict_domain); let old_upper_bound = self.assignments.get_upper_bound(conflict_domain); - // Now we get the explanation for the bound which was conflicting with the last trail entry match conflict.trigger_predicate.get_predicate_type() { PredicateType::LowerBound => { // The last trail entry was a lower-bound propagation meaning that the empty domain @@ -555,7 +555,11 @@ impl ConflictAnalysisContext<'_> { )); } PredicateType::NotEqual => { - empty_domain_reason.push(conflict.trigger_predicate); + // The last trail entry was a not equals propagation meaning that the empty domain + // was due to the domain being assigned to the removed value + pumpkin_assert_eq_simple!(old_upper_bound, old_lower_bound); + + empty_domain_reason.push(predicate!(conflict_domain == old_lower_bound)); } PredicateType::Equal => { // The last trail entry was an equality propagation; we split into three cases. From 6dca9eac36fad55999878659d26eb44ec49d800b Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Wed, 12 Nov 2025 16:16:21 +0100 Subject: [PATCH 5/5] refactor: Clarify that all predicates are true in conflict nogood --- .../src/engine/conflict_analysis/conflict_analysis_context.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs index f33576014..ef4af5328 100644 --- a/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/engine/conflict_analysis/conflict_analysis_context.rs @@ -136,7 +136,7 @@ impl ConflictAnalysisContext<'_> { let predicate_dl = self .assignments .get_decision_level_for_predicate(&predicate) - .unwrap(); + .expect("all predicates in the conflict nogood should be assigned to true"); if predicate_dl == 0 { explain_root_assignment(