From 2249e21bc27d168c4e802b6ccd98b1a7c927a13c Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Thu, 26 Feb 2026 04:46:35 +1100 Subject: [PATCH 01/43] Move inference checker to its own file --- .../checking/src/inference_checker.rs | 49 +++++++++++++++++++ pumpkin-crates/checking/src/lib.rs | 48 +----------------- 2 files changed, 51 insertions(+), 46 deletions(-) create mode 100644 pumpkin-crates/checking/src/inference_checker.rs diff --git a/pumpkin-crates/checking/src/inference_checker.rs b/pumpkin-crates/checking/src/inference_checker.rs new file mode 100644 index 000000000..f8eed5554 --- /dev/null +++ b/pumpkin-crates/checking/src/inference_checker.rs @@ -0,0 +1,49 @@ +use std::fmt::Debug; + +use dyn_clone::DynClone; + +use crate::AtomicConstraint; +use crate::VariableState; + +/// An inference checker tests whether the given state is a conflict under the sematics of an +/// inference rule. +pub trait InferenceChecker: Debug + DynClone { + /// Returns `true` if `state` is a conflict, and `false` if not. + /// + /// For the conflict check, all the premises are true in the state and the consequent, if + /// present, if false. + fn check( + &self, + state: VariableState, + premises: &[Atomic], + consequent: Option<&Atomic>, + ) -> bool; +} + +/// Wrapper around `Box>` that implements [`Clone`]. +#[derive(Debug)] +pub struct BoxedChecker(Box>); + +impl Clone for BoxedChecker { + fn clone(&self) -> Self { + BoxedChecker(dyn_clone::clone_box(&*self.0)) + } +} + +impl From>> for BoxedChecker { + fn from(value: Box>) -> Self { + BoxedChecker(value) + } +} + +impl BoxedChecker { + /// See [`InferenceChecker::check`]. + pub fn check( + &self, + variable_state: VariableState, + premises: &[Atomic], + consequent: Option<&Atomic>, + ) -> bool { + self.0.check(variable_state, premises, consequent) + } +} diff --git a/pumpkin-crates/checking/src/lib.rs b/pumpkin-crates/checking/src/lib.rs index 6fb8fc265..47899a12d 100644 --- a/pumpkin-crates/checking/src/lib.rs +++ b/pumpkin-crates/checking/src/lib.rs @@ -4,59 +4,15 @@ //! inferences are sound w.r.t. an inference rule. mod atomic_constraint; +mod inference_checker; mod int_ext; mod union; mod variable; mod variable_state; -use std::fmt::Debug; - pub use atomic_constraint::*; -use dyn_clone::DynClone; +pub use inference_checker::*; pub use int_ext::*; pub use union::*; pub use variable::*; pub use variable_state::*; - -/// An inference checker tests whether the given state is a conflict under the sematics of an -/// inference rule. -pub trait InferenceChecker: Debug + DynClone { - /// Returns `true` if `state` is a conflict, and `false` if not. - /// - /// For the conflict check, all the premises are true in the state and the consequent, if - /// present, if false. - fn check( - &self, - state: VariableState, - premises: &[Atomic], - consequent: Option<&Atomic>, - ) -> bool; -} - -/// Wrapper around `Box>` that implements [`Clone`]. -#[derive(Debug)] -pub struct BoxedChecker(Box>); - -impl Clone for BoxedChecker { - fn clone(&self) -> Self { - BoxedChecker(dyn_clone::clone_box(&*self.0)) - } -} - -impl From>> for BoxedChecker { - fn from(value: Box>) -> Self { - BoxedChecker(value) - } -} - -impl BoxedChecker { - /// See [`InferenceChecker::check`]. - pub fn check( - &self, - variable_state: VariableState, - premises: &[Atomic], - consequent: Option<&Atomic>, - ) -> bool { - self.0.check(variable_state, premises, consequent) - } -} From 32d3af641e4ea9ae7664f9507847cb0921c154bb Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Thu, 26 Feb 2026 05:49:58 +1100 Subject: [PATCH 02/43] Move the deduction checker to `pumpkin_checking` --- Cargo.lock | 1 + pumpkin-checker/src/deductions.rs | 278 +++++------------- pumpkin-checker/src/inferences/mod.rs | 12 +- pumpkin-checker/src/test_utils.rs | 17 -- pumpkin-crates/checking/Cargo.toml | 1 + .../checking/src/atomic_constraint.rs | 33 ++- .../checking/src/deduction_checker.rs | 210 +++++++++++++ pumpkin-crates/checking/src/lib.rs | 2 + 8 files changed, 333 insertions(+), 221 deletions(-) create mode 100644 pumpkin-crates/checking/src/deduction_checker.rs diff --git a/Cargo.lock b/Cargo.lock index cd058e9e9..2597a7083 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -952,6 +952,7 @@ version = "0.3.0" dependencies = [ "dyn-clone", "fnv", + "thiserror", ] [[package]] diff --git a/pumpkin-checker/src/deductions.rs b/pumpkin-checker/src/deductions.rs index eafe740b3..2c6e15994 100644 --- a/pumpkin-checker/src/deductions.rs +++ b/pumpkin-checker/src/deductions.rs @@ -3,10 +3,10 @@ use std::rc::Rc; use drcp_format::ConstraintId; use drcp_format::IntAtomic; -use pumpkin_checking::AtomicConstraint; -use pumpkin_checking::VariableState; +use pumpkin_checking::SupportingInference; use crate::inferences::Fact; +use crate::model::Atomic; use crate::model::Nogood; /// An inference that was ignored when checking a deduction. @@ -46,212 +46,86 @@ pub fn verify_deduction( deduction: &drcp_format::Deduction, i32>, facts_in_proof_stage: &BTreeMap, ) -> Result { - // To verify a deduction, we assume that the premises are true. Then we go over all the - // facts in the sequence, and if all the premises are satisfied, we apply the consequent. - // At some point, this should either reach a fact without a consequent or derive an - // inconsistent domain. - - let mut variable_state = VariableState::prepare_for_conflict_check( - deduction.premises.iter().cloned().map(Into::into), - None, - ) - .map_err(|_| InvalidDeduction::InconsistentPremises)?; - - let mut unused_inferences = Vec::new(); - - for constraint_id in deduction.sequence.iter() { - // Get the fact associated with the constraint ID from the sequence. - let fact = facts_in_proof_stage - .get(constraint_id) - .ok_or(InvalidDeduction::UnknownInference(*constraint_id))?; - - // Collect all premises that do not evaluate to `true` under the current variable - // state. - let unsatisfied_premises: Vec> = fact - .premises - .iter() - .filter_map::, _>(|premise| { - if variable_state.is_true(premise) { - None - } else { - // We need to convert the premise name from a `Rc` to a - // `String`. The former does not implement `Send`, but that is - // required for our error type to be used with anyhow. - Some(IntAtomic { - name: String::from(premise.identifier().as_ref()), - comparison: match premise.comparison() { - pumpkin_checking::Comparison::GreaterEqual => { - drcp_format::IntComparison::GreaterEqual - } - pumpkin_checking::Comparison::LessEqual => { - drcp_format::IntComparison::LessEqual - } - pumpkin_checking::Comparison::Equal => { - drcp_format::IntComparison::Equal - } - pumpkin_checking::Comparison::NotEqual => { - drcp_format::IntComparison::NotEqual - } - }, - value: premise.value(), - }) - } - }) - .collect::>(); - - // If at least one premise is unassigned, this fact is ignored for the conflict - // check and recorded as unused. - if !unsatisfied_premises.is_empty() { - unused_inferences.push(IgnoredInference { - constraint_id: *constraint_id, - unsatisfied_premises, - }); + // First we convert the deduction sequence to the types from the checking library. + let inferences = deduction + .sequence + .iter() + .map(|cid| { + facts_in_proof_stage + .get(cid) + .map(|fact| SupportingInference { + premises: fact.premises.clone(), + consequent: fact.consequent.clone(), + }) + .ok_or(InvalidDeduction::UnknownInference(*cid)) + }) + .collect::, _>>()?; + + // Then we convert the deduction premise to the types from the checking library. + let premises = deduction.premises.iter().cloned().map(Atomic::IntAtomic); + + match pumpkin_checking::verify_deduction(premises.clone(), inferences) { + Ok(_) => Ok(Nogood::from(premises)), + Err(error) => Err(convert_error(error, facts_in_proof_stage)), + } +} - continue; +fn convert_error( + error: pumpkin_checking::InvalidDeduction, + facts_in_proof_stage: &BTreeMap, +) -> InvalidDeduction { + match error { + pumpkin_checking::InvalidDeduction::NoConflict(ignored_inferences) => { + let mapped_ignored_inferences = ignored_inferences + .into_iter() + .map(|ignored_inference| { + convert_ignored_inferences(ignored_inference, facts_in_proof_stage) + }) + .collect(); + + InvalidDeduction::NoConflict(mapped_ignored_inferences) } - - // At this point the premises are satisfied so we handle the consequent of the - // inference. - match &fact.consequent { - Some(consequent) => { - if !variable_state.apply(consequent) { - // If applying the consequent yields an empty domain for a - // variable, then the deduction is valid. - return Ok(Nogood::from(deduction.premises.clone())); - } - } - // If the consequent is explicitly false, then the deduction is valid. - None => return Ok(Nogood::from(deduction.premises.clone())), + pumpkin_checking::InvalidDeduction::InconsistentPremises => { + InvalidDeduction::InconsistentPremises } } - - // Reaching this point means that the conjunction of inferences did not yield to a - // conflict. Therefore the deduction is invalid. - Err(InvalidDeduction::NoConflict(unused_inferences)) } -#[cfg(test)] -mod tests { - use super::*; - use crate::atomic; - use crate::fact; - use crate::test_utils::constraint_id; - use crate::test_utils::deduction; - - macro_rules! facts { - {$($k: expr => $v: expr),* $(,)?} => { - ::std::collections::BTreeMap::from([$(($crate::test_utils::constraint_id($k), $v),)*]) - }; - } - - #[test] - fn a_sequence_is_correctly_traversed() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [1, 2, 3]); - - let facts_in_proof_stage = facts! { - 1 => fact!([x >= 5] -> [y <= 4]), - 2 => fact!([y <= 7] -> [z != 10]), - 3 => fact!([y <= 5] & [z != 10] -> [x <= 4]), - }; - - let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction"); - assert_eq!(Nogood::from(premises), nogood); - } - - #[test] - fn an_inference_implying_false_is_a_valid_stopping_condition() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [1, 2, 3]); - - let facts_in_proof_stage = facts! { - 1 => fact!([x >= 5] -> [y <= 4]), - 2 => fact!([y <= 7] -> [z != 10]), - 3 => fact!([y <= 5] & [z != 10] -> false), - }; - - let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction"); - assert_eq!(Nogood::from(premises), nogood); - } - - #[test] - fn inference_order_does_not_need_to_be_by_constraint_id() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [2, 1, 4]); - - let facts_in_proof_stage = facts! { - 2 => fact!([x >= 5] -> [y <= 4]), - 1 => fact!([y <= 7] -> [z != 10]), - 4 => fact!([y <= 5] & [z != 10] -> false), - }; - - let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction"); - assert_eq!(Nogood::from(premises), nogood); - } - - #[test] - fn inconsistent_premises_are_identified() { - let premises = vec![atomic!([x >= 5]), atomic!([x <= 4])]; - let deduction = deduction(5, premises.clone(), [2]); - - let facts_in_proof_stage = facts! { - 2 => fact!([x == 5] -> false), - }; - - let error = - verify_deduction(&deduction, &facts_in_proof_stage).expect_err("inconsistent premises"); - assert_eq!(InvalidDeduction::InconsistentPremises, error); - } - - #[test] - fn all_inferences_in_sequence_must_be_in_fact_database() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [1, 2]); - - let facts_in_proof_stage = facts! { - 2 => fact!([x == 5] -> false), - }; - - let error = - verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference"); - assert_eq!(InvalidDeduction::UnknownInference(constraint_id(1)), error); - } - - #[test] - fn sequence_that_does_not_terminate_in_conflict_is_rejected() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [2, 1]); - - let facts_in_proof_stage = facts! { - 2 => fact!([x >= 5] -> [y <= 4]), - 1 => fact!([y <= 7] -> [z != 10]), - 4 => fact!([y <= 5] & [z != 10] -> false), - }; - - let error = - verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference"); - assert_eq!(InvalidDeduction::NoConflict(vec![]), error); - } - - #[test] - fn inferences_with_unsatisfied_premises_are_ignored() { - let premises = vec![atomic!([x >= 5])]; - let deduction = deduction(5, premises.clone(), [2, 1]); - - let facts_in_proof_stage = facts! { - 2 => fact!([x >= 5] -> [y <= 4]), - 1 => fact!([y <= 7] & [x >= 6] -> [z != 10]), - 4 => fact!([y <= 5] & [z != 10] -> false), - }; +fn convert_ignored_inferences( + ignored_inference: pumpkin_checking::IgnoredInference, + facts_in_proof_stage: &BTreeMap, +) -> IgnoredInference { + IgnoredInference { + constraint_id: facts_in_proof_stage + .iter() + .find_map(|(constraint_id, inference)| { + let constraint_id = *constraint_id; + let checker_inference = inference.clone(); + let ignored_inference_as_checker = Fact::from(ignored_inference.inference.clone()); - let error = - verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference"); - assert_eq!( - InvalidDeduction::NoConflict(vec![IgnoredInference { - constraint_id: constraint_id(1), - unsatisfied_premises: vec![atomic!([x string >= 6])], - }]), - error - ); + if checker_inference == ignored_inference_as_checker { + Some(constraint_id) + } else { + None + } + }) + .expect("one of these will match"), + + unsatisfied_premises: ignored_inference + .unsatisfied_premises + .into_iter() + .map(|premise| match premise { + Atomic::True | Atomic::False => unreachable!(), + + Atomic::IntAtomic(int_atomic) => IntAtomic { + // Note: String is required here since the error type needs to + // implement `Send`. By default we use `Rc` everywhere, which + // does not implement `Send`. + name: String::from(int_atomic.name.as_ref()), + comparison: int_atomic.comparison, + value: int_atomic.value, + }, + }) + .collect(), } } diff --git a/pumpkin-checker/src/inferences/mod.rs b/pumpkin-checker/src/inferences/mod.rs index f83e5dc39..cc6262f5c 100644 --- a/pumpkin-checker/src/inferences/mod.rs +++ b/pumpkin-checker/src/inferences/mod.rs @@ -4,17 +4,27 @@ mod linear; mod nogood; mod time_table; +use pumpkin_checking::SupportingInference; use pumpkin_checking::VariableState; use crate::model::Atomic; use crate::model::Model; -#[derive(Clone, Debug)] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct Fact { pub premises: Vec, pub consequent: Option, } +impl From> for Fact { + fn from(value: SupportingInference) -> Self { + Fact { + premises: value.premises, + consequent: value.consequent, + } + } +} + impl Fact { /// Create a fact `premises -> false`. pub fn nogood(premises: Vec) -> Self { diff --git a/pumpkin-checker/src/test_utils.rs b/pumpkin-checker/src/test_utils.rs index af003e707..b05888c3d 100644 --- a/pumpkin-checker/src/test_utils.rs +++ b/pumpkin-checker/src/test_utils.rs @@ -1,10 +1,8 @@ //! Contains a bunch of utilities to help write tests for the checker. use std::num::NonZero; -use std::rc::Rc; use drcp_format::ConstraintId; -use drcp_format::IntAtomic; /// Create a constraint ID from the given number. /// @@ -90,18 +88,3 @@ macro_rules! fact { } }; } - -pub(crate) fn deduction( - id: u32, - premises: impl Into, i32>>>, - sequence: impl IntoIterator, -) -> drcp_format::Deduction, i32> { - drcp_format::Deduction { - constraint_id: constraint_id(id), - premises: premises.into(), - sequence: sequence - .into_iter() - .map(|id| NonZero::new(id).expect("constraint ids should be non-zero")) - .collect(), - } -} diff --git a/pumpkin-crates/checking/Cargo.toml b/pumpkin-crates/checking/Cargo.toml index 485564df6..2bda5514a 100644 --- a/pumpkin-crates/checking/Cargo.toml +++ b/pumpkin-crates/checking/Cargo.toml @@ -10,6 +10,7 @@ authors.workspace = true [dependencies] dyn-clone = "1.0.20" fnv = "1.0.7" +thiserror = "2.0.18" [lints] workspace = true diff --git a/pumpkin-crates/checking/src/atomic_constraint.rs b/pumpkin-crates/checking/src/atomic_constraint.rs index 6be4a9508..bfeddaa3a 100644 --- a/pumpkin-crates/checking/src/atomic_constraint.rs +++ b/pumpkin-crates/checking/src/atomic_constraint.rs @@ -8,7 +8,7 @@ use std::hash::Hash; /// - `identifier` identifies a variable, /// - `op` is a [`Comparison`], /// - and `value` is an integer. -pub trait AtomicConstraint: Sized + Debug { +pub trait AtomicConstraint: Clone + Debug + Sized { /// The type of identifier used for variables. type Identifier: Hash + Eq; @@ -87,3 +87,34 @@ impl AtomicConstraint for TestAtomic { } } } + +/// Create a [`TestAtomic`] using a DSL. +/// +/// # Example +/// ``` +/// pumpkin_checking::test_atomic!([x >= 5]); +/// pumpkin_checking::test_atomic!([y != 10]); +/// ``` +#[macro_export] +macro_rules! test_atomic { + (@to_comparison >=) => { + $crate::Comparison::GreaterEqual + }; + (@to_comparison <=) => { + $crate::Comparison::LessEqual + }; + (@to_comparison ==) => { + $crate::Comparison::Equal + }; + (@to_comparison !=) => { + $crate::Comparison::NotEqual + }; + + ([$name:ident $comp:tt $value:expr]) => { + $crate::TestAtomic { + name: stringify!($name), + comparison: $crate::test_atomic!(@to_comparison $comp), + value: $value, + } + }; +} diff --git a/pumpkin-crates/checking/src/deduction_checker.rs b/pumpkin-crates/checking/src/deduction_checker.rs new file mode 100644 index 000000000..17a63a779 --- /dev/null +++ b/pumpkin-crates/checking/src/deduction_checker.rs @@ -0,0 +1,210 @@ +use crate::AtomicConstraint; +use crate::VariableState; + +/// An inference that was ignored when checking a deduction. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct IgnoredInference { + /// The inference that was ignored. + pub inference: SupportingInference, + + /// The premises that were not satisfied when the inference was evaluated. + pub unsatisfied_premises: Vec, +} + +/// A deduction is rejected by the checker. +#[derive(thiserror::Error, Debug, PartialEq, Eq)] +#[error("invalid deduction")] +pub enum InvalidDeduction { + /// The inferences in the proof stage do not derive an empty domain or an explicit + /// conflict. + #[error("no conflict was derived after applying all inferences")] + NoConflict(Vec>), + + /// The premise contains mutually exclusive atomic constraints. + #[error("the deduction contains inconsistent premises")] + InconsistentPremises, +} + +/// An inference used to support a deduction. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct SupportingInference { + /// The premises of the inference. + pub premises: Vec, + /// The consequent of the inference. + /// + /// [`None`] represents the literal false. I.e., if the consequent is [`None`], then the + /// premises imply false. + pub consequent: Option, +} + +/// Verify that a deduction is valid given the inferences in the proof stage. +/// +/// The `inferences` are considered in the order they are provided. +pub fn verify_deduction( + premises: impl IntoIterator, + inferences: impl IntoIterator>, +) -> Result<(), InvalidDeduction> +where + Atomic: AtomicConstraint, +{ + // To verify a deduction, we assume that the premises are true. Then we go over all the + // facts in the sequence, and if all the premises are satisfied, we apply the consequent. + // At some point, this should either reach a fact without a consequent or derive an + // inconsistent domain. + + let mut variable_state = VariableState::prepare_for_conflict_check(premises, None) + .map_err(|_| InvalidDeduction::InconsistentPremises)?; + + let mut unused_inferences = Vec::new(); + + for inference in inferences.into_iter() { + // Collect all premises that do not evaluate to `true` under the current variable + // state. + let unsatisfied_premises = inference + .premises + .iter() + .filter(|premise| !variable_state.is_true(premise)) + .cloned() + .collect::>(); + + // If at least one premise is unassigned, this fact is ignored for the conflict + // check and recorded as unused. + if !unsatisfied_premises.is_empty() { + unused_inferences.push(IgnoredInference { + inference, + unsatisfied_premises, + }); + + continue; + } + + // At this point the premises are satisfied so we handle the consequent of the + // inference. + match &inference.consequent { + Some(consequent) => { + if !variable_state.apply(consequent) { + // If applying the consequent yields an empty domain for a + // variable, then the deduction is valid. + return Ok(()); + } + } + // If the consequent is explicitly false, then the deduction is valid. + None => return Ok(()), + } + } + + // Reaching this point means that the conjunction of inferences did not yield to a + // conflict. Therefore the deduction is invalid. + Err(InvalidDeduction::NoConflict(unused_inferences)) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::test_atomic; + + /// Create a [`SupportingInference`] in a DSL. + /// + /// # Example + /// ``` + /// inference!([x >= 5] & [y <= 10] -> [z == 5]); + /// inference!([x >= 5] & [y <= 10] -> false); + /// ``` + #[macro_export] + macro_rules! inference { + // Case: consequent is an Atomic + ( + $($prem:tt)&+ -> [$($cons:tt)+] + ) => { + SupportingInference { + premises: vec![$( test_atomic!($prem) ),+], + consequent: Some(test_atomic!([$($cons)+])), + } + }; + + // Case: consequent is false (i.e., None) + ( + $($prem:tt)&+ -> false + ) => { + SupportingInference { + premises: vec![$( test_atomic!($prem) ),+], + consequent: None, + } + }; + } + + #[test] + fn a_sequence_is_correctly_traversed() { + let premises = vec![test_atomic!([x >= 5])]; + + let inferences = vec![ + inference!([x >= 5] -> [y <= 4]), + inference!([y <= 7] -> [z != 10]), + inference!([y <= 5] & [z != 10] -> [x <= 4]), + ]; + + verify_deduction(premises, inferences).expect("valid deduction"); + } + + #[test] + fn an_inference_implying_false_is_a_valid_stopping_condition() { + let premises = vec![test_atomic!([x >= 5])]; + + let inferences = vec![ + inference!([x >= 5] -> [y <= 4]), + inference!([y <= 7] -> [z != 10]), + inference!([y <= 5] & [z != 10] -> false), + ]; + + verify_deduction(premises, inferences).expect("valid deduction"); + } + + #[test] + fn inconsistent_premises_are_identified() { + let premises = vec![test_atomic!([x >= 5]), test_atomic!([x <= 4])]; + + let inferences = vec![inference!([x == 5] -> false)]; + + let error = verify_deduction(premises, inferences).expect_err("inconsistent premises"); + assert_eq!(InvalidDeduction::InconsistentPremises, error); + } + + #[test] + fn sequence_that_does_not_terminate_in_conflict_is_rejected() { + let premises = vec![test_atomic!([x >= 5])]; + + let inferences = vec![ + inference!([x >= 5] -> [y <= 4]), + inference!([y <= 7] -> [z != 10]), + ]; + + let error = verify_deduction(premises, inferences).expect_err("conflict is not reached"); + assert_eq!(InvalidDeduction::NoConflict(vec![]), error); + } + + #[test] + fn inferences_with_unsatisfied_premises_are_ignored() { + let premises = vec![test_atomic!([x >= 5])]; + + let inferences = vec![ + inference!([x >= 5] -> [y <= 4]), + inference!([y <= 7] & [x >= 6] -> [z != 10]), + inference!([y <= 5] & [z != 10] -> false), + ]; + + let error = verify_deduction(premises, inferences).expect_err("premises are not satisfied"); + assert_eq!( + InvalidDeduction::NoConflict(vec![ + IgnoredInference { + inference: inference!([y <= 7] & [x >= 6] -> [z != 10]), + unsatisfied_premises: vec![test_atomic!([x >= 6])], + }, + IgnoredInference { + inference: inference!([y <= 5] & [z != 10] -> false), + unsatisfied_premises: vec![test_atomic!([z != 10])], + } + ]), + error + ); + } +} diff --git a/pumpkin-crates/checking/src/lib.rs b/pumpkin-crates/checking/src/lib.rs index 47899a12d..88ffd94e9 100644 --- a/pumpkin-crates/checking/src/lib.rs +++ b/pumpkin-crates/checking/src/lib.rs @@ -4,6 +4,7 @@ //! inferences are sound w.r.t. an inference rule. mod atomic_constraint; +mod deduction_checker; mod inference_checker; mod int_ext; mod union; @@ -11,6 +12,7 @@ mod variable; mod variable_state; pub use atomic_constraint::*; +pub use deduction_checker::*; pub use inference_checker::*; pub use int_ext::*; pub use union::*; From f8e808033a7fc58be1dcbb4a2b15e5ba82c59e2e Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 2 Mar 2026 17:17:04 +1100 Subject: [PATCH 03/43] Build runtime verification into the resolution conflict resolver --- Cargo.lock | 1 + pumpkin-crates/conflict-resolvers/Cargo.toml | 4 +++ .../src/minimisers/recursive_minimiser.rs | 2 +- .../src/resolvers/resolution_resolver.rs | 27 +++++++++++++++++-- .../conflict_analysis_context.rs | 14 +++++++--- .../engine/constraint_satisfaction_solver.rs | 2 +- pumpkin-crates/core/src/proof/finalizer.rs | 2 +- 7 files changed, 43 insertions(+), 9 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2597a7083..fa1eb8bcf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -959,6 +959,7 @@ dependencies = [ name = "pumpkin-conflict-resolvers" version = "0.3.0" dependencies = [ + "pumpkin-checking", "pumpkin-core", ] diff --git a/pumpkin-crates/conflict-resolvers/Cargo.toml b/pumpkin-crates/conflict-resolvers/Cargo.toml index de3438062..b7c13fa7a 100644 --- a/pumpkin-crates/conflict-resolvers/Cargo.toml +++ b/pumpkin-crates/conflict-resolvers/Cargo.toml @@ -11,4 +11,8 @@ description = "The conflict resolvers of the Pumpkin constraint programming solv workspace = true [dependencies] +pumpkin-checking = { version = "0.3.0", path = "../checking" } pumpkin-core = { version = "0.3.0", path = "../core" } + +[features] +check-deductions = [] diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs index 871482f20..8ed7f2c2a 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs @@ -123,7 +123,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( + let _ = context.get_propagation_reason( input_predicate, CurrentNogood::from(current_nogood), &mut reason, diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 1996fc7f8..b557bf090 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,3 +1,5 @@ +use pumpkin_checking::SupportingInference; +use pumpkin_checking::verify_deduction; use pumpkin_core::asserts::pumpkin_assert_advanced; use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; @@ -64,6 +66,10 @@ pub struct ResolutionResolver { statistics: LearnedNogoodStatistics, + /// The inferences supporting the current deduction. Used for runtime verification of the + /// learned nogood. + used_inferences: Vec>, + should_minimise: bool, } @@ -145,6 +151,7 @@ impl ResolutionResolver { recursive_minimiser: Default::default(), semantic_minimiser: Default::default(), statistics: Default::default(), + used_inferences: Default::default(), should_minimise, } } @@ -191,7 +198,8 @@ impl ResolutionResolver { // 2) Get the reason for the predicate and add it to the nogood. self.reason_buffer.clear(); - context.get_propagation_reason( + + let possible_inference_code = context.get_propagation_reason( next_predicate, CurrentNogood::new( &self.to_process_heap, @@ -204,9 +212,24 @@ impl ResolutionResolver { for i in 0..self.reason_buffer.len() { self.add_predicate_to_conflict_nogood(self.reason_buffer[i], self.mode, context); } + + if cfg!(feature = "check-deductions") && possible_inference_code.is_some() { + self.used_inferences.push(SupportingInference { + premises: self.reason_buffer.clone(), + consequent: Some(next_predicate), + }); + } } - self.extract_final_nogood(context) + self.extract_final_nogood(context); + + if cfg!(feature = "check-deductions") { + verify_deduction( + self.processed_nogood_predicates.clone(), + std::mem::take(&mut self.used_inferences), + ) + .expect("the deduction is valid"); + } } /// Clears all data structures to prepare for the new conflict analysis. diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index 0a5173925..6878818de 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -139,12 +139,14 @@ impl ConflictAnalysisContext<'_> { /// `reason_buffer`. /// /// If `predicate` is not true, or it is a decision, then this function will panic. + /// + /// Returns the [`InferenceCode`] if one was attached to this reason. pub fn get_propagation_reason( &mut self, predicate: Predicate, current_nogood: CurrentNogood<'_>, reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), - ) { + ) -> Option { Self::get_propagation_reason_inner( predicate, current_nogood, @@ -152,7 +154,7 @@ impl ConflictAnalysisContext<'_> { self.unit_nogood_inference_codes, reason_buffer, self.state, - ); + ) } /// Returns the last decision which was made by the solver (if such a decision exists). @@ -264,6 +266,8 @@ impl ConflictAnalysisContext<'_> { /// `reason_buffer`. /// /// If `predicate` is not true, or it is a decision, then this function will panic. + /// + /// Returns the [`InferenceCode`] if one was attached to this reason. pub(crate) fn get_propagation_reason_inner( predicate: Predicate, current_nogood: CurrentNogood<'_>, @@ -271,7 +275,7 @@ impl ConflictAnalysisContext<'_> { unit_nogood_inference_codes: &HashMap, reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), state: &mut State, - ) { + ) -> Option { let inference_code = state.get_propagation_reason(predicate, reason_buffer, current_nogood); if inference_code.is_some() { @@ -280,7 +284,7 @@ impl ConflictAnalysisContext<'_> { ); let trail_entry = state.assignments.get_trail_entry(trail_index); let Some((reason_ref, inference_code)) = trail_entry.reason else { - return; + return inference_code; }; let propagator_id = state.reason_store.get_propagator(reason_ref); @@ -329,6 +333,8 @@ impl ConflictAnalysisContext<'_> { ); } } + + inference_code } fn compute_conflict_nogood( diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 08b3d031c..aa9d3e756 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -437,7 +437,7 @@ impl ConstraintSatisfactionSolver { continue; } - ConflictAnalysisContext::get_propagation_reason_inner( + let _ = ConflictAnalysisContext::get_propagation_reason_inner( predicate, CurrentNogood::empty(), context.proof_log, diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index 97cef32c0..b038ca112 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -102,7 +102,7 @@ fn finalize_proof_impl( // There must be some combination of other factors. let mut reason = vec![]; - ConflictAnalysisContext::get_propagation_reason_inner( + let _ = ConflictAnalysisContext::get_propagation_reason_inner( predicate, CurrentNogood::empty(), context.proof_log, From 4232ef96f93781c68935ad8fbc210d9a2357a4a8 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 2 Mar 2026 17:18:10 +1100 Subject: [PATCH 04/43] Run deduction verification during tests --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4d919643a..d91b1891d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: target/ key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} - uses: dtolnay/rust-toolchain@stable - - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations + - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations pumpkin-conflict-resolvers/check-deductions wasm-test: name: Test Suite for pumpkin-core in WebAssembly From c7f31474c39cf3b839eebdc87a123ae40d16fd49 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 2 Mar 2026 17:26:04 +1100 Subject: [PATCH 05/43] Fix CI to actually run deduction checks --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d91b1891d..63fc1b0e1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: target/ key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} - uses: dtolnay/rust-toolchain@stable - - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations pumpkin-conflict-resolvers/check-deductions + - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations --features pumpkin-conflict-resolvers/check-deductions wasm-test: name: Test Suite for pumpkin-core in WebAssembly From e33f843132d3887427cf4f3c69e248d42c709f51 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 2 Mar 2026 17:32:40 +1100 Subject: [PATCH 06/43] Implement better printing of failed deduction checks --- .../src/resolvers/resolution_resolver.rs | 29 +++++++++++++++++-- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index b557bf090..e4f57ba34 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,3 +1,4 @@ +use pumpkin_checking::InvalidDeduction; use pumpkin_checking::SupportingInference; use pumpkin_checking::verify_deduction; use pumpkin_core::asserts::pumpkin_assert_advanced; @@ -224,11 +225,33 @@ impl ResolutionResolver { self.extract_final_nogood(context); if cfg!(feature = "check-deductions") { - verify_deduction( + match verify_deduction( self.processed_nogood_predicates.clone(), std::mem::take(&mut self.used_inferences), - ) - .expect("the deduction is valid"); + ) { + Ok(_) => {} + Err(error) => { + match error { + InvalidDeduction::NoConflict(ignored_inferences) => { + for ignored_inference in ignored_inferences { + eprintln!( + "{:?} -> {:?}", + ignored_inference.inference.premises, + ignored_inference.inference.consequent + ); + } + panic!("Using inferences that cannot be applied:"); + } + InvalidDeduction::InconsistentPremises => { + eprintln!("Inconsistent predicates in learned nogood") + } + } + panic!( + "Failed to verify deduction: {:?}", + self.processed_nogood_predicates + ); + } + } } } From 74a38a1f3bc5e12d2c700fbb87a7a899b1b06f5a Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Mon, 2 Mar 2026 17:52:28 +1100 Subject: [PATCH 07/43] Collect initial domains and the last propagation as supporting inferences --- .../src/resolvers/resolution_resolver.rs | 28 ++++++++----- .../conflict_analysis_context.rs | 40 ++++++++++++++----- .../engine/constraint_satisfaction_solver.rs | 4 +- 3 files changed, 52 insertions(+), 20 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index e4f57ba34..86cb5d9ec 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -160,7 +160,8 @@ impl ResolutionResolver { pub(crate) fn learn_nogood(&mut self, context: &mut ConflictAnalysisContext) { self.clean_up(); - let conflict_nogood = context.get_conflict_nogood(); + let (conflict_nogood, supporting_inference) = context.get_conflict_nogood(); + self.used_inferences.extend(supporting_inference); // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { @@ -227,20 +228,22 @@ impl ResolutionResolver { if cfg!(feature = "check-deductions") { match verify_deduction( self.processed_nogood_predicates.clone(), - std::mem::take(&mut self.used_inferences), + self.used_inferences.drain(..).rev(), ) { Ok(_) => {} Err(error) => { match error { InvalidDeduction::NoConflict(ignored_inferences) => { - for ignored_inference in ignored_inferences { - eprintln!( - "{:?} -> {:?}", - ignored_inference.inference.premises, - ignored_inference.inference.consequent - ); + if !ignored_inferences.is_empty() { + eprintln!("Using inferences that cannot be applied:"); + for ignored_inference in ignored_inferences { + eprintln!( + "{:?} -> {:?}", + ignored_inference.inference.premises, + ignored_inference.inference.consequent + ); + } } - panic!("Using inferences that cannot be applied:"); } InvalidDeduction::InconsistentPremises => { eprintln!("Inconsistent predicates in learned nogood") @@ -283,6 +286,13 @@ impl ResolutionResolver { }); // Ignore root level predicates. if dec_level == 0 { + if context.is_initial_bound(predicate) { + self.used_inferences.push(SupportingInference { + premises: vec![], + consequent: Some(predicate), + }); + } + context.explain_root_assignment(predicate); } // 1UIP diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index 6878818de..12249bf25 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -1,5 +1,7 @@ use std::fmt::Debug; +use pumpkin_checking::SupportingInference; + use crate::Random; use crate::basic_types::StoredConflictInfo; use crate::branching::Brancher; @@ -88,8 +90,10 @@ impl ConflictAnalysisContext<'_> { /// Returns a nogood which led to the conflict, excluding predicates from the root decision /// level. - pub fn get_conflict_nogood(&mut self) -> Vec { - let conflict_nogood = match self.solver_state.get_conflict_info() { + pub fn get_conflict_nogood( + &mut self, + ) -> (Vec, Option>) { + let (conflict_nogood, supporting_inference) = match self.solver_state.get_conflict_info() { StoredConflictInfo::Propagator(conflict) => { let _ = self.proof_log.log_inference( &mut self.state.constraint_tags, @@ -100,14 +104,25 @@ impl ConflictAnalysisContext<'_> { &self.state.assignments, ); - conflict.conjunction + ( + conflict.conjunction.clone(), + Some(SupportingInference { + premises: conflict.conjunction.to_vec(), + consequent: None, + }), + ) + } + StoredConflictInfo::EmptyDomain(conflict) => { + let (conflict_nogood, supporting_inference) = + self.compute_conflict_nogood(conflict); + + (conflict_nogood, Some(supporting_inference)) } - StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict), StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } StoredConflictInfo::InconsistentAssumptions(predicate) => { - vec![predicate, !predicate].into() + (vec![predicate, !predicate].into(), None) } }; @@ -129,10 +144,12 @@ impl ConflictAnalysisContext<'_> { } } - conflict_nogood + let nogood = conflict_nogood .into_iter() .filter(|&p| self.state.get_checkpoint_for_predicate(p).unwrap() > 0) - .collect() + .collect(); + + (nogood, supporting_inference) } /// Compute the reason for `predicate` being true. The reason will be stored in @@ -340,7 +357,7 @@ impl ConflictAnalysisContext<'_> { fn compute_conflict_nogood( &mut self, conflict: EmptyDomainConflict, - ) -> PropositionalConjunction { + ) -> (PropositionalConjunction, SupportingInference) { let conflict_domain = conflict.domain(); // Look up the reason for the bound that changed. @@ -369,6 +386,11 @@ impl ConflictAnalysisContext<'_> { &self.state.assignments, ); + let supporting_inference = SupportingInference { + premises: empty_domain_reason.clone(), + consequent: Some(conflict.trigger_predicate), + }; + let old_lower_bound = self.state.lower_bound(conflict_domain); let old_upper_bound = self.state.upper_bound(conflict_domain); @@ -427,7 +449,7 @@ impl ConflictAnalysisContext<'_> { } } - empty_domain_reason.into() + (empty_domain_reason.into(), supporting_inference) } } diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index aa9d3e756..2214b81fd 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -229,7 +229,7 @@ impl ConstraintSatisfactionSolver { rng: &mut self.internal_parameters.random_generator, }; - let conflict = conflict_analysis_context.get_conflict_nogood(); + let (conflict, _) = conflict_analysis_context.get_conflict_nogood(); let context = FinalizingContext { conflict: conflict.into(), @@ -428,7 +428,7 @@ impl ConstraintSatisfactionSolver { rng: &mut self.internal_parameters.random_generator, }; - let mut predicates = context.get_conflict_nogood(); + let (mut predicates, _) = context.get_conflict_nogood(); let mut core: HashSet = HashSet::default(); while let Some(predicate) = predicates.pop() { From b52740ba9b5774ed688f1a4d69d1eeb700d07473 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Tue, 3 Mar 2026 14:40:02 +1100 Subject: [PATCH 08/43] Do runtime verification of deductions when they are logged --- Cargo.lock | 1 - pumpkin-crates/conflict-resolvers/Cargo.toml | 3 - .../src/resolvers/resolution_resolver.rs | 60 +------------------ pumpkin-crates/core/Cargo.toml | 1 + .../conflict_analysis_context.rs | 42 ++++--------- .../engine/constraint_satisfaction_solver.rs | 4 +- pumpkin-crates/core/src/proof/finalizer.rs | 2 +- pumpkin-crates/core/src/proof/mod.rs | 56 ++++++++++++++++- 8 files changed, 71 insertions(+), 98 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fa1eb8bcf..2597a7083 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -959,7 +959,6 @@ dependencies = [ name = "pumpkin-conflict-resolvers" version = "0.3.0" dependencies = [ - "pumpkin-checking", "pumpkin-core", ] diff --git a/pumpkin-crates/conflict-resolvers/Cargo.toml b/pumpkin-crates/conflict-resolvers/Cargo.toml index b7c13fa7a..b40a679ad 100644 --- a/pumpkin-crates/conflict-resolvers/Cargo.toml +++ b/pumpkin-crates/conflict-resolvers/Cargo.toml @@ -11,8 +11,5 @@ description = "The conflict resolvers of the Pumpkin constraint programming solv workspace = true [dependencies] -pumpkin-checking = { version = "0.3.0", path = "../checking" } pumpkin-core = { version = "0.3.0", path = "../core" } -[features] -check-deductions = [] diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 86cb5d9ec..e70b28ef5 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,6 +1,3 @@ -use pumpkin_checking::InvalidDeduction; -use pumpkin_checking::SupportingInference; -use pumpkin_checking::verify_deduction; use pumpkin_core::asserts::pumpkin_assert_advanced; use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; @@ -67,10 +64,6 @@ pub struct ResolutionResolver { statistics: LearnedNogoodStatistics, - /// The inferences supporting the current deduction. Used for runtime verification of the - /// learned nogood. - used_inferences: Vec>, - should_minimise: bool, } @@ -152,7 +145,6 @@ impl ResolutionResolver { recursive_minimiser: Default::default(), semantic_minimiser: Default::default(), statistics: Default::default(), - used_inferences: Default::default(), should_minimise, } } @@ -160,8 +152,7 @@ impl ResolutionResolver { pub(crate) fn learn_nogood(&mut self, context: &mut ConflictAnalysisContext) { self.clean_up(); - let (conflict_nogood, supporting_inference) = context.get_conflict_nogood(); - self.used_inferences.extend(supporting_inference); + let conflict_nogood = context.get_conflict_nogood(); // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { @@ -201,7 +192,7 @@ impl ResolutionResolver { // 2) Get the reason for the predicate and add it to the nogood. self.reason_buffer.clear(); - let possible_inference_code = context.get_propagation_reason( + let _ = context.get_propagation_reason( next_predicate, CurrentNogood::new( &self.to_process_heap, @@ -214,48 +205,9 @@ impl ResolutionResolver { for i in 0..self.reason_buffer.len() { self.add_predicate_to_conflict_nogood(self.reason_buffer[i], self.mode, context); } - - if cfg!(feature = "check-deductions") && possible_inference_code.is_some() { - self.used_inferences.push(SupportingInference { - premises: self.reason_buffer.clone(), - consequent: Some(next_predicate), - }); - } } self.extract_final_nogood(context); - - if cfg!(feature = "check-deductions") { - match verify_deduction( - self.processed_nogood_predicates.clone(), - self.used_inferences.drain(..).rev(), - ) { - Ok(_) => {} - Err(error) => { - match error { - InvalidDeduction::NoConflict(ignored_inferences) => { - if !ignored_inferences.is_empty() { - eprintln!("Using inferences that cannot be applied:"); - for ignored_inference in ignored_inferences { - eprintln!( - "{:?} -> {:?}", - ignored_inference.inference.premises, - ignored_inference.inference.consequent - ); - } - } - } - InvalidDeduction::InconsistentPremises => { - eprintln!("Inconsistent predicates in learned nogood") - } - } - panic!( - "Failed to verify deduction: {:?}", - self.processed_nogood_predicates - ); - } - } - } } /// Clears all data structures to prepare for the new conflict analysis. @@ -286,13 +238,6 @@ impl ResolutionResolver { }); // Ignore root level predicates. if dec_level == 0 { - if context.is_initial_bound(predicate) { - self.used_inferences.push(SupportingInference { - premises: vec![], - consequent: Some(predicate), - }); - } - context.explain_root_assignment(predicate); } // 1UIP @@ -388,6 +333,7 @@ impl ResolutionResolver { fn extract_final_nogood(&mut self, context: &mut ConflictAnalysisContext) { // The final nogood is composed of the predicates encountered from the lower decision // levels, plus the predicate remaining in the heap. + // // First we obtain a semantically minimised nogood. // diff --git a/pumpkin-crates/core/Cargo.toml b/pumpkin-crates/core/Cargo.toml index dc0f5d410..f8243eb48 100644 --- a/pumpkin-crates/core/Cargo.toml +++ b/pumpkin-crates/core/Cargo.toml @@ -40,5 +40,6 @@ wasm-bindgen-test = "0.3" [features] check-propagations = [] +check-deductions = [] debug-checks = [] clap = ["dep:clap"] diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index 12249bf25..1f72dd95f 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -1,7 +1,5 @@ use std::fmt::Debug; -use pumpkin_checking::SupportingInference; - use crate::Random; use crate::basic_types::StoredConflictInfo; use crate::branching::Brancher; @@ -90,10 +88,8 @@ impl ConflictAnalysisContext<'_> { /// Returns a nogood which led to the conflict, excluding predicates from the root decision /// level. - pub fn get_conflict_nogood( - &mut self, - ) -> (Vec, Option>) { - let (conflict_nogood, supporting_inference) = match self.solver_state.get_conflict_info() { + pub fn get_conflict_nogood(&mut self) -> Vec { + let conflict_nogood = match self.solver_state.get_conflict_info() { StoredConflictInfo::Propagator(conflict) => { let _ = self.proof_log.log_inference( &mut self.state.constraint_tags, @@ -104,25 +100,14 @@ impl ConflictAnalysisContext<'_> { &self.state.assignments, ); - ( - conflict.conjunction.clone(), - Some(SupportingInference { - premises: conflict.conjunction.to_vec(), - consequent: None, - }), - ) - } - StoredConflictInfo::EmptyDomain(conflict) => { - let (conflict_nogood, supporting_inference) = - self.compute_conflict_nogood(conflict); - - (conflict_nogood, Some(supporting_inference)) + conflict.conjunction.clone() } + StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict), StoredConflictInfo::RootLevelConflict(_) => { unreachable!("Should never attempt to learn a nogood from a root level conflict") } StoredConflictInfo::InconsistentAssumptions(predicate) => { - (vec![predicate, !predicate].into(), None) + vec![predicate, !predicate].into() } }; @@ -144,12 +129,10 @@ impl ConflictAnalysisContext<'_> { } } - let nogood = conflict_nogood + conflict_nogood .into_iter() .filter(|&p| self.state.get_checkpoint_for_predicate(p).unwrap() > 0) - .collect(); - - (nogood, supporting_inference) + .collect() } /// Compute the reason for `predicate` being true. The reason will be stored in @@ -200,7 +183,7 @@ impl ConflictAnalysisContext<'_> { /// order. pub fn log_deduction( &mut self, - premises: impl IntoIterator, + premises: impl IntoIterator + Clone, ) -> ConstraintTag { self.proof_log .log_deduction( @@ -357,7 +340,7 @@ impl ConflictAnalysisContext<'_> { fn compute_conflict_nogood( &mut self, conflict: EmptyDomainConflict, - ) -> (PropositionalConjunction, SupportingInference) { + ) -> PropositionalConjunction { let conflict_domain = conflict.domain(); // Look up the reason for the bound that changed. @@ -386,11 +369,6 @@ impl ConflictAnalysisContext<'_> { &self.state.assignments, ); - let supporting_inference = SupportingInference { - premises: empty_domain_reason.clone(), - consequent: Some(conflict.trigger_predicate), - }; - let old_lower_bound = self.state.lower_bound(conflict_domain); let old_upper_bound = self.state.upper_bound(conflict_domain); @@ -449,7 +427,7 @@ impl ConflictAnalysisContext<'_> { } } - (empty_domain_reason.into(), supporting_inference) + 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 2214b81fd..aa9d3e756 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -229,7 +229,7 @@ impl ConstraintSatisfactionSolver { rng: &mut self.internal_parameters.random_generator, }; - let (conflict, _) = conflict_analysis_context.get_conflict_nogood(); + let conflict = conflict_analysis_context.get_conflict_nogood(); let context = FinalizingContext { conflict: conflict.into(), @@ -428,7 +428,7 @@ impl ConstraintSatisfactionSolver { rng: &mut self.internal_parameters.random_generator, }; - let (mut predicates, _) = context.get_conflict_nogood(); + let mut predicates = context.get_conflict_nogood(); let mut core: HashSet = HashSet::default(); while let Some(predicate) = predicates.pop() { diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index b038ca112..a49157eef 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -145,7 +145,7 @@ pub(crate) fn explain_root_assignment( Some(0) ); - if !context.proof_log.is_logging_inferences() { + if !context.proof_log.is_logging_inferences() && cfg!(not(feature = "check-deductions")) { return; } diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index e51ab37f7..1c006cb03 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -20,6 +20,9 @@ use drcp_format::writer::ProofWriter; pub(crate) use finalizer::*; pub use inference_code::*; use proof_atomics::ProofAtomics; +use pumpkin_checking::InvalidDeduction; +use pumpkin_checking::SupportingInference; +use pumpkin_checking::verify_deduction; #[cfg(doc)] use crate::Solver; @@ -39,6 +42,7 @@ use crate::variables::Literal; #[derive(Debug, Default)] pub struct ProofLog { internal_proof: Option, + supporting_inferences: Vec>, } impl ProofLog { @@ -64,6 +68,7 @@ impl ProofLog { logged_domain_inferences: HashMap::default(), proof_atomics: ProofAtomics::default(), }), + supporting_inferences: vec![], }) } @@ -72,6 +77,7 @@ impl ProofLog { let file = File::create(file_path)?; Ok(ProofLog { internal_proof: Some(ProofImpl::DimacsProof(DimacsProof::new(file))), + supporting_inferences: vec![], }) } @@ -80,13 +86,20 @@ impl ProofLog { &mut self, constraint_tags: &mut KeyGenerator, inference_code: InferenceCode, - premises: impl IntoIterator, + premises: impl IntoIterator + Clone, propagated: Option, variable_names: &VariableNames, assignments: &Assignments, ) -> std::io::Result { let inference_tag = constraint_tags.next_key(); + if cfg!(feature = "check-deductions") { + self.supporting_inferences.push(SupportingInference { + premises: premises.clone().into_iter().collect(), + consequent: propagated, + }); + } + let Some(ProofImpl::CpProof { writer, propagation_order_hint: Some(propagation_sequence), @@ -184,13 +197,15 @@ impl ProofLog { /// order. pub(crate) fn log_deduction( &mut self, - premises: impl IntoIterator, + premises: impl IntoIterator + Clone, variable_names: &VariableNames, constraint_tags: &mut KeyGenerator, assignments: &Assignments, ) -> std::io::Result { let constraint_tag = constraint_tags.next_key(); + self.verify_deduction_at_runtime(premises.clone()); + match &mut self.internal_proof { Some(ProofImpl::CpProof { writer, @@ -304,6 +319,43 @@ impl ProofLog { pub(crate) fn is_logging_proof(&self) -> bool { self.internal_proof.is_some() } + + fn verify_deduction_at_runtime( + &mut self, + premises: impl IntoIterator + Clone, + ) { + if cfg!(not(feature = "check-deductions")) { + return; + } + + match verify_deduction(premises.clone(), self.supporting_inferences.drain(..).rev()) { + Ok(_) => {} + Err(error) => { + match error { + InvalidDeduction::NoConflict(ignored_inferences) => { + if !ignored_inferences.is_empty() { + eprintln!("Using inferences that cannot be applied:"); + for ignored_inference in ignored_inferences { + eprintln!( + "{:?} -> {:?}", + ignored_inference.inference.premises, + ignored_inference.inference.consequent + ); + } + } + } + InvalidDeduction::InconsistentPremises => { + eprintln!("Inconsistent predicates in learned nogood") + } + } + + panic!( + "Failed to verify deduction: {:?}", + itertools::join(premises, " & ") + ); + } + } + } } /// Returns `true` if the given predicate is likely a constant from the model that was unnamed. From dbd40563639bc458899ae4bd2e56e29a4640dae8 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Tue, 3 Mar 2026 14:42:05 +1100 Subject: [PATCH 09/43] Verify deductions in tests --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 63fc1b0e1..208eca27c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: target/ key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} - uses: dtolnay/rust-toolchain@stable - - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations --features pumpkin-conflict-resolvers/check-deductions + - run: cargo test --release --no-fail-fast --features pumpkin-solver/check-propagations --features pumpkin-core/check-deductions wasm-test: name: Test Suite for pumpkin-core in WebAssembly From e46a611914a4f0b743c600cb22bff445158385e1 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 28 Mar 2026 15:45:29 +1100 Subject: [PATCH 10/43] refactor(pumpkin-conflict-resolvers): Correctly log domain inferences in semantic minimiser --- .../src/minimisers/semantic_minimiser.rs | 23 +++++++++++++++++++ .../conflict_analysis_context.rs | 14 +++++++++++ pumpkin-crates/core/src/proof/mod.rs | 23 ++++++++++++++++--- 3 files changed, 57 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/semantic_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/semantic_minimiser.rs index 6f4e827ed..6cb3dd9ab 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/semantic_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/semantic_minimiser.rs @@ -81,6 +81,7 @@ impl NogoodMinimiser for SemanticMinimiser { return; } self.domains[domain_id].add_domain_description_to_vector( + context, *domain_id, &self.original_domains[domain_id], &mut self.helper, @@ -149,6 +150,7 @@ impl SemanticMinimiser { fn grow(&mut self, lower_bound: i32, upper_bound: i32, holes: Vec) { let mut initial_domain = SimpleIntegerDomain { + assigned_to: None, lower_bound, upper_bound, holes: HashSet::from_iter(holes.iter().cloned()), @@ -177,6 +179,14 @@ impl SemanticMinimiser { #[derive(Clone, Default, Debug)] struct SimpleIntegerDomain { + /// The value this domain was assigned to with an equality predicate. + /// + /// An input nogood `[x == 3] -> false` can be minimized to `[x >= 3] -> false` + /// if `[x <= 3]` is an initial domain bound. However, that initial domain bound + /// should be logged to the proof. This is only necessary in this situation, since if the + /// domain is assigned by a conjunction of multiple predicates, those will all have been + /// justified to the proof before reaching minimization. + assigned_to: Option, lower_bound: i32, upper_bound: i32, holes: HashSet, @@ -202,6 +212,8 @@ impl SimpleIntegerDomain { } fn assign(&mut self, value: i32) { + self.assigned_to = Some(value); + // If the domains are inconsistent, or if the assigned value would make the domain // inconsistent, declare inconsistency and stop. if self.lower_bound > self.upper_bound @@ -250,6 +262,7 @@ impl SimpleIntegerDomain { fn add_domain_description_to_vector( &self, + context: &mut ConflictAnalysisContext<'_>, domain_id: DomainId, original_domain: &SimpleIntegerDomain, description: &mut Vec, @@ -269,10 +282,20 @@ impl SimpleIntegerDomain { // Add bounds but avoid root assignments. if self.lower_bound != original_domain.lower_bound { description.push(predicate![domain_id >= self.lower_bound]); + } else if self + .assigned_to + .is_some_and(|value| value == original_domain.lower_bound) + { + context.log_domain_inference(predicate![domain_id >= original_domain.lower_bound]); } if self.upper_bound != original_domain.upper_bound { description.push(predicate![domain_id <= self.upper_bound]); + } else if self + .assigned_to + .is_some_and(|value| value == original_domain.upper_bound) + { + context.log_domain_inference(predicate![domain_id <= original_domain.upper_bound]); } // Add nonroot holes. diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index 1f72dd95f..6d573beed 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -177,6 +177,20 @@ impl ConflictAnalysisContext<'_> { ); } + /// Indicate to the proof that the initial domain `predicate` is used in the next + /// deduction. + pub fn log_domain_inference(&mut self, predicate: Predicate) { + let _ = self + .proof_log + .log_domain_inference( + predicate, + &self.state.variable_names, + &mut self.state.constraint_tags, + &self.state.assignments, + ) + .expect("Failed to write proof log"); + } + /// Log a deduction (learned nogood) to the proof. /// /// The inferences and marked propagations are assumed to be recorded in reverse-application diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 1c006cb03..41779ff4c 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -141,6 +141,13 @@ impl ProofLog { ) -> std::io::Result> { assert!(assignments.is_initial_bound(predicate)); + if cfg!(feature = "check-deductions") { + self.supporting_inferences.push(SupportingInference { + premises: vec![], + consequent: Some(predicate), + }); + } + if is_likely_a_constant(predicate, variable_names, assignments) { // The predicate is over a constant variable. We assume we do not want to // log these if they have no name. @@ -328,8 +335,13 @@ impl ProofLog { return; } - match verify_deduction(premises.clone(), self.supporting_inferences.drain(..).rev()) { - Ok(_) => {} + match verify_deduction( + premises.clone(), + self.supporting_inferences.iter().cloned().rev(), + ) { + Ok(_) => { + self.supporting_inferences.clear(); + } Err(error) => { match error { InvalidDeduction::NoConflict(ignored_inferences) => { @@ -342,6 +354,11 @@ impl ProofLog { ignored_inference.inference.consequent ); } + + eprintln!("All inferences:"); + for inference in self.supporting_inferences.iter() { + eprintln!("{:?} -> {:?}", inference.premises, inference.consequent); + } } } InvalidDeduction::InconsistentPremises => { @@ -350,7 +367,7 @@ impl ProofLog { } panic!( - "Failed to verify deduction: {:?}", + "Failed to verify deduction: {:?} -> false", itertools::join(premises, " & ") ); } From 9b9e7ee9c512950c5b0b4644b6ed7072053f50fd Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 28 Mar 2026 15:53:10 +1100 Subject: [PATCH 11/43] fix(pumpkin-conflict-resolvers): Log inference for freshly added falsified clause --- .../engine/constraint_satisfaction_solver.rs | 17 ++++++++++++++++- pumpkin-crates/core/src/proof/mod.rs | 12 ++++++------ 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index aa9d3e756..4841ef3a6 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -983,7 +983,23 @@ impl ConstraintSatisfactionSolver { return Err(ConstraintOperationError::InfeasibleClause); } + let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); if are_all_falsified_at_root { + // Since the propagation is not actually performed, we log the inference + // explicitly here for the proof. + let _ = self + .internal_parameters + .proof_log + .log_inference( + &mut self.state.constraint_tags, + inference_code, + predicates.iter().copied(), + None, + &self.state.variable_names, + &self.state.assignments, + ) + .expect("failed to write to proof"); + finalize_proof(FinalizingContext { conflict: predicates.into(), proof_log: &mut self.internal_parameters.proof_log, @@ -997,7 +1013,6 @@ impl ConstraintSatisfactionSolver { return Err(ConstraintOperationError::InfeasibleClause); } - let inference_code = InferenceCode::new(constraint_tag, NogoodLabel); if let Err(constraint_operation_error) = self.add_nogood(predicates, inference_code) { let _ = self.conclude_proof_unsat(); diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 41779ff4c..37821d7bc 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -345,8 +345,13 @@ impl ProofLog { Err(error) => { match error { InvalidDeduction::NoConflict(ignored_inferences) => { + eprintln!("Supporting inferences:"); + for inference in self.supporting_inferences.iter() { + eprintln!("{:?} -> {:?}", inference.premises, inference.consequent); + } + if !ignored_inferences.is_empty() { - eprintln!("Using inferences that cannot be applied:"); + eprintln!("Ignored inferences:"); for ignored_inference in ignored_inferences { eprintln!( "{:?} -> {:?}", @@ -354,11 +359,6 @@ impl ProofLog { ignored_inference.inference.consequent ); } - - eprintln!("All inferences:"); - for inference in self.supporting_inferences.iter() { - eprintln!("{:?} -> {:?}", inference.premises, inference.consequent); - } } } InvalidDeduction::InconsistentPremises => { From c1565e19c138c709b2e85996ebf0e342ba0da90e Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 28 Mar 2026 16:01:10 +1100 Subject: [PATCH 12/43] Fix docs for atomic! macro --- pumpkin-crates/checking/src/atomic_constraint.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-crates/checking/src/atomic_constraint.rs b/pumpkin-crates/checking/src/atomic_constraint.rs index bfeddaa3a..38711717f 100644 --- a/pumpkin-crates/checking/src/atomic_constraint.rs +++ b/pumpkin-crates/checking/src/atomic_constraint.rs @@ -88,7 +88,7 @@ impl AtomicConstraint for TestAtomic { } } -/// Create a [`TestAtomic`] using a DSL. +/// A convenient way to construct a [`TestAtomic`]. /// /// # Example /// ``` From 5064db2fdef32078d534087d678001c305dac877 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sat, 28 Mar 2026 16:07:13 +1100 Subject: [PATCH 13/43] Apply fixes based on feedback in review --- pumpkin-crates/checking/src/deduction_checker.rs | 3 +++ pumpkin-crates/checking/src/inference_checker.rs | 2 +- pumpkin-crates/conflict-resolvers/Cargo.toml | 1 - .../src/resolvers/resolution_resolver.rs | 1 - .../src/conflict_resolving/conflict_analysis_context.rs | 2 +- pumpkin-crates/core/src/proof/mod.rs | 8 +++----- 6 files changed, 8 insertions(+), 9 deletions(-) diff --git a/pumpkin-crates/checking/src/deduction_checker.rs b/pumpkin-crates/checking/src/deduction_checker.rs index 17a63a779..d6647d148 100644 --- a/pumpkin-crates/checking/src/deduction_checker.rs +++ b/pumpkin-crates/checking/src/deduction_checker.rs @@ -2,6 +2,9 @@ use crate::AtomicConstraint; use crate::VariableState; /// An inference that was ignored when checking a deduction. +/// +/// Returned as an error when checking a deduction. These inferences were added to the proof stage, +/// but never used. Hence, they likely point to why the proof stage is rejected. #[derive(Clone, Debug, PartialEq, Eq)] pub struct IgnoredInference { /// The inference that was ignored. diff --git a/pumpkin-crates/checking/src/inference_checker.rs b/pumpkin-crates/checking/src/inference_checker.rs index f8eed5554..badb75d8e 100644 --- a/pumpkin-crates/checking/src/inference_checker.rs +++ b/pumpkin-crates/checking/src/inference_checker.rs @@ -11,7 +11,7 @@ pub trait InferenceChecker: Debug + DynClone { /// Returns `true` if `state` is a conflict, and `false` if not. /// /// For the conflict check, all the premises are true in the state and the consequent, if - /// present, if false. + /// present, is false. fn check( &self, state: VariableState, diff --git a/pumpkin-crates/conflict-resolvers/Cargo.toml b/pumpkin-crates/conflict-resolvers/Cargo.toml index b40a679ad..de3438062 100644 --- a/pumpkin-crates/conflict-resolvers/Cargo.toml +++ b/pumpkin-crates/conflict-resolvers/Cargo.toml @@ -12,4 +12,3 @@ workspace = true [dependencies] pumpkin-core = { version = "0.3.0", path = "../core" } - diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index e70b28ef5..cd2c763f8 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -333,7 +333,6 @@ impl ResolutionResolver { fn extract_final_nogood(&mut self, context: &mut ConflictAnalysisContext) { // The final nogood is composed of the predicates encountered from the lower decision // levels, plus the predicate remaining in the heap. - // // First we obtain a semantically minimised nogood. // diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index 6d573beed..c1585bf34 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -100,7 +100,7 @@ impl ConflictAnalysisContext<'_> { &self.state.assignments, ); - conflict.conjunction.clone() + conflict.conjunction } StoredConflictInfo::EmptyDomain(conflict) => self.compute_conflict_nogood(conflict), StoredConflictInfo::RootLevelConflict(_) => { diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 37821d7bc..67315b4df 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -211,7 +211,9 @@ impl ProofLog { ) -> std::io::Result { let constraint_tag = constraint_tags.next_key(); - self.verify_deduction_at_runtime(premises.clone()); + if cfg!(feature = "check-deductions") { + self.verify_deduction_at_runtime(premises.clone()); + } match &mut self.internal_proof { Some(ProofImpl::CpProof { @@ -331,10 +333,6 @@ impl ProofLog { &mut self, premises: impl IntoIterator + Clone, ) { - if cfg!(not(feature = "check-deductions")) { - return; - } - match verify_deduction( premises.clone(), self.supporting_inferences.iter().cloned().rev(), From 18aa665446876231657e3dc4966dc983b2419ead Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 12:30:31 +1100 Subject: [PATCH 14/43] Correctly log inferences for minimisation --- .../src/minimisers/recursive_minimiser.rs | 33 ++++++++++++--- .../conflict_analysis_context.rs | 41 +++++++++++++++++++ pumpkin-crates/core/src/proof/finalizer.rs | 2 +- pumpkin-crates/core/src/proof/mod.rs | 2 +- 4 files changed, 71 insertions(+), 7 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs index 8ed7f2c2a..0c660354e 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs @@ -31,6 +31,9 @@ pub struct RecursiveMinimiser { allowed_decision_levels: HashSet, // could consider direct hashing here label_assignments: HashMap>, + /// Marks the predicates which had their reason logged to the proof. + logged_predicates: HashSet, + statistics: RecursiveMinimiserStatistics, } @@ -60,6 +63,8 @@ impl NogoodMinimiser for RecursiveMinimiser { if label == Label::Poison || label == Label::Keep { nogood[end_position] = learned_predicate; end_position += 1; + } else if context.is_proof_logging_inferences() { + self.add_inferences_for(context, learned_predicate); } } @@ -123,7 +128,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![]; - let _ = context.get_propagation_reason( + let _ = context.get_propagation_reason_without_proof_log( input_predicate, CurrentNogood::from(current_nogood), &mut reason, @@ -136,10 +141,6 @@ impl RecursiveMinimiser { .unwrap() == 0 { - // The minimisation can introduce new inferences in the proof. If those inferences - // contain root-level antecedents, which we identified here, we need to make sure - // the proof is aware that that root-level assignment is used. - context.explain_root_assignment(antecedent_predicate); continue; } @@ -167,6 +168,7 @@ impl RecursiveMinimiser { } } } + // If the code reaches this part (it did not get into one of the previous 'return' // statements, so all antecedents of the literal are either KEEP or REMOVABLE), // meaning this literal is REMOVABLE. @@ -223,6 +225,8 @@ impl RecursiveMinimiser { ) { pumpkin_assert_simple!(self.current_depth == 0); + self.logged_predicates.clear(); + // Mark literals from the initial learned nogood. for &predicate in nogood { // Predicates from the current decision level are always kept. @@ -257,6 +261,25 @@ impl RecursiveMinimiser { pumpkin_assert_moderate!(self.current_depth <= 500); self.current_depth == 500 } + + fn add_inferences_for(&mut self, context: &mut ConflictAnalysisContext, predicate: Predicate) { + if context.get_checkpoint_for_predicate(predicate).unwrap() == 0 { + context.explain_root_assignment(predicate); + return; + } + + if [Label::Keep, Label::Poison].contains(&self.get_predicate_label(predicate)) { + return; + } + + let mut reason_buffer = vec![]; + let _ = + context.get_propagation_reason(predicate, CurrentNogood::empty(), &mut reason_buffer); + + for antecedent in reason_buffer { + self.add_inferences_for(context, antecedent); + } + } } #[derive(PartialEq, Copy, Clone, Debug)] diff --git a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs index c1585bf34..390ec9631 100644 --- a/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs +++ b/pumpkin-crates/core/src/conflict_resolving/conflict_analysis_context.rs @@ -135,6 +135,23 @@ impl ConflictAnalysisContext<'_> { .collect() } + /// Get the reason for `predicate` being true, without logging that reason to the proof. + pub fn get_propagation_reason_without_proof_log( + &mut self, + predicate: Predicate, + current_nogood: CurrentNogood<'_>, + reason_buffer: &mut (impl Extend + AsRef<[Predicate]>), + ) -> Option { + Self::get_propagation_reason_inner( + predicate, + current_nogood, + &mut ProofLog::default(), + self.unit_nogood_inference_codes, + reason_buffer, + self.state, + ) + } + /// Compute the reason for `predicate` being true. The reason will be stored in /// `reason_buffer`. /// @@ -161,6 +178,10 @@ impl ConflictAnalysisContext<'_> { pub fn find_last_decision(&mut self) -> Option { self.state.assignments.find_last_decision() } + + pub fn is_proof_logging_inferences(&self) -> bool { + self.proof_log.is_logging_inferences() + } } /// Methods used for proof logging @@ -177,6 +198,26 @@ impl ConflictAnalysisContext<'_> { ); } + /// Log an inference to the proof. + pub fn log_inference( + &mut self, + inference_code: InferenceCode, + premises: impl IntoIterator + Clone, + consequent: Option, + ) { + let _ = self + .proof_log + .log_inference( + &mut self.state.constraint_tags, + inference_code, + premises, + consequent, + &self.state.variable_names, + &self.state.assignments, + ) + .expect("Failed to write proof log"); + } + /// Indicate to the proof that the initial domain `predicate` is used in the next /// deduction. pub fn log_domain_inference(&mut self, predicate: Predicate) { diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index a49157eef..b038ca112 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -145,7 +145,7 @@ pub(crate) fn explain_root_assignment( Some(0) ); - if !context.proof_log.is_logging_inferences() && cfg!(not(feature = "check-deductions")) { + if !context.proof_log.is_logging_inferences() { return; } diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 67315b4df..5a8725f1f 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -310,7 +310,7 @@ impl ProofLog { propagation_order_hint: Some(_), .. }) - ) + ) || cfg!(feature = "check-deductions") } pub(crate) fn reify_predicate(&mut self, literal: Literal, predicate: Predicate) { From 56e5a14a09f2a26cb3db7db4c7cc707c8f675275 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 12:56:39 +1100 Subject: [PATCH 15/43] Remove redundant inferences introduced through minimisation --- .../src/minimisers/recursive_minimiser.rs | 67 ++++++++++++------ pumpkin-crates/core/src/api/mod.rs | 1 + pumpkin-crates/core/src/engine/mod.rs | 2 + .../core/src/engine/predicate_heap.rs | 70 +++++++++++++++++++ 4 files changed, 117 insertions(+), 23 deletions(-) create mode 100644 pumpkin-crates/core/src/engine/predicate_heap.rs diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs index 0c660354e..0bf7dc0af 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/recursive_minimiser.rs @@ -1,3 +1,4 @@ +use pumpkin_core::asserts::pumpkin_assert_eq_simple; use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; @@ -7,6 +8,7 @@ use pumpkin_core::create_statistics_struct; use pumpkin_core::predicates::Predicate; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::state::CurrentNogood; +use pumpkin_core::state::PredicateHeap; use pumpkin_core::statistics::moving_averages::CumulativeMovingAverage; use pumpkin_core::statistics::moving_averages::MovingAverage; @@ -31,8 +33,8 @@ pub struct RecursiveMinimiser { allowed_decision_levels: HashSet, // could consider direct hashing here label_assignments: HashMap>, - /// Marks the predicates which had their reason logged to the proof. - logged_predicates: HashSet, + /// The predicates which need to be explained in the proof. + predicates_to_log: PredicateHeap, statistics: RecursiveMinimiserStatistics, } @@ -48,23 +50,33 @@ impl NogoodMinimiser for RecursiveMinimiser { self.initialise_minimisation_data_structures(nogood, context); + // For each predicate in the learned nogood, check whether it is implied by other + // predicates in the nogood. + for predicate in nogood.iter().copied() { + self.compute_label(predicate, context, nogood); + + // If the predicate is removable, mark it to be explained. + if self.get_predicate_label(predicate) == Label::Removable { + self.predicates_to_log.push(predicate, context.get_state()); + } + } + + self.add_inferences_for_removed_predicates(context); + // Iterate over each predicate and check whether it is a dominated predicate. let mut end_position: usize = 0; let initial_nogood_size = nogood.len(); for i in 0..initial_nogood_size { let learned_predicate = nogood[i]; - self.compute_label(learned_predicate, context, nogood); - let label = self.get_predicate_label(learned_predicate); + // Keep the predicate in case it was not deemed deemed redundant. // Note that in other cases, since 'end_position' is not incremented, // the predicate is effectively removed. if label == Label::Poison || label == Label::Keep { nogood[end_position] = learned_predicate; end_position += 1; - } else if context.is_proof_logging_inferences() { - self.add_inferences_for(context, learned_predicate); } } @@ -223,9 +235,8 @@ impl RecursiveMinimiser { nogood: &Vec, context: &ConflictAnalysisContext, ) { - pumpkin_assert_simple!(self.current_depth == 0); - - self.logged_predicates.clear(); + pumpkin_assert_eq_simple!(self.current_depth, 0); + pumpkin_assert_simple!(self.predicates_to_log.is_empty()); // Mark literals from the initial learned nogood. for &predicate in nogood { @@ -251,7 +262,8 @@ impl RecursiveMinimiser { } fn clean_up_minimisation(&mut self) { - pumpkin_assert_simple!(self.current_depth == 0); + pumpkin_assert_eq_simple!(self.current_depth, 0); + pumpkin_assert_simple!(self.predicates_to_log.is_empty()); self.allowed_decision_levels.clear(); self.label_assignments.clear(); @@ -262,22 +274,31 @@ impl RecursiveMinimiser { self.current_depth == 500 } - fn add_inferences_for(&mut self, context: &mut ConflictAnalysisContext, predicate: Predicate) { - if context.get_checkpoint_for_predicate(predicate).unwrap() == 0 { - context.explain_root_assignment(predicate); - return; - } + /// Adds the inferences for predicates that will be removed from the learned nogood. + /// + /// Assumes `self.predicates_to_log` is initialized with the predicates that have the + /// `Removable` label. + fn add_inferences_for_removed_predicates(&mut self, context: &mut ConflictAnalysisContext) { + while let Some(predicate) = self.predicates_to_log.pop() { + if context.get_checkpoint_for_predicate(predicate).unwrap() == 0 { + context.explain_root_assignment(predicate); + continue; + } - if [Label::Keep, Label::Poison].contains(&self.get_predicate_label(predicate)) { - return; - } + if [Label::Keep, Label::Poison].contains(&self.get_predicate_label(predicate)) { + continue; + } - let mut reason_buffer = vec![]; - let _ = - context.get_propagation_reason(predicate, CurrentNogood::empty(), &mut reason_buffer); + let mut reason_buffer = vec![]; + let _ = context.get_propagation_reason( + predicate, + CurrentNogood::empty(), + &mut reason_buffer, + ); - for antecedent in reason_buffer { - self.add_inferences_for(context, antecedent); + for antecedent in reason_buffer { + self.predicates_to_log.push(antecedent, context.get_state()); + } } } } diff --git a/pumpkin-crates/core/src/api/mod.rs b/pumpkin-crates/core/src/api/mod.rs index 854be5cdf..22f3a90d7 100644 --- a/pumpkin-crates/core/src/api/mod.rs +++ b/pumpkin-crates/core/src/api/mod.rs @@ -121,6 +121,7 @@ pub mod state { pub use crate::engine::Conflict; pub use crate::engine::EmptyDomain; pub use crate::engine::EmptyDomainConflict; + pub use crate::engine::PredicateHeap; pub use crate::engine::PropagationStatusCP; pub use crate::engine::PropagatorConflict; pub use crate::engine::State; diff --git a/pumpkin-crates/core/src/engine/mod.rs b/pumpkin-crates/core/src/engine/mod.rs index c3854bec0..22da37fbe 100644 --- a/pumpkin-crates/core/src/engine/mod.rs +++ b/pumpkin-crates/core/src/engine/mod.rs @@ -5,6 +5,7 @@ pub(crate) mod cp; mod debug_helper; mod literal_block_distance; pub(crate) mod notifications; +mod predicate_heap; pub(crate) mod predicates; mod restart_strategy; mod solver_statistics; @@ -22,6 +23,7 @@ pub(crate) use cp::*; pub(crate) use debug_helper::DebugDyn; pub(crate) use debug_helper::DebugHelper; pub use literal_block_distance::Lbd; +pub use predicate_heap::*; pub use reason::Reason; pub use restart_strategy::RestartOptions; pub(crate) use restart_strategy::RestartStrategy; diff --git a/pumpkin-crates/core/src/engine/predicate_heap.rs b/pumpkin-crates/core/src/engine/predicate_heap.rs new file mode 100644 index 000000000..83ffe5e2d --- /dev/null +++ b/pumpkin-crates/core/src/engine/predicate_heap.rs @@ -0,0 +1,70 @@ +use std::cmp::Ordering; +use std::collections::BinaryHeap; + +use crate::predicates::Predicate; +use crate::state::State; + +/// A max-heap of predicates. The keys are based on the trail positions of the predicates in the +/// state, meaning predicates are popped in reverse trail order. Implied predicates are popped +/// before the predicate on the trail that implies the predicate. +#[derive(Clone, Debug, Default)] +pub struct PredicateHeap { + heap: BinaryHeap, +} + +impl PredicateHeap { + /// See [`BinaryHeap::is_empty`]. + pub fn is_empty(&self) -> bool { + self.heap.is_empty() + } + + /// See [`BinaryHeap::pop`]. + pub fn pop(&mut self) -> Option { + self.heap.pop().map(|to_explain| to_explain.predicate) + } + + /// Push a new predicate onto the heap. + /// + /// Its priority will be based on its trail position in the given `state`. This heap will + /// return elements through [`Self::pop`] by reverse-trail order. + /// + /// If the predicate is not true in the given state, this method panics. + pub fn push(&mut self, predicate: Predicate, state: &State) { + let trail_position = state + .trail_position(predicate) + .expect("predicate must be true in given state"); + + let priority = if state.is_on_trail(predicate) { + trail_position * 2 + } else { + trail_position * 2 + 1 + }; + + self.heap.push(PredicateToExplain { + predicate, + priority, + }); + } +} + +/// Used to order the predicates in the [`PredicateHeap`]. +/// +/// The priority is calculated based on the trail position of the predicate and whether the +/// predicate is on the trail or implied. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct PredicateToExplain { + predicate: Predicate, + priority: usize, +} + +impl PartialOrd for PredicateToExplain { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} + +impl Ord for PredicateToExplain { + fn cmp(&self, other: &Self) -> Ordering { + self.priority.cmp(&other.priority) + } +} From e1c97284ea36b173f47f727845e2763ead9c9006 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 12:57:37 +1100 Subject: [PATCH 16/43] Do not disable recursive minimisation when proof logging --- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 1edc75199..7b9ac5939 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -567,17 +567,11 @@ fn run() -> PumpkinResult<()> { activity_bump_increment: 1.0, }; - let should_minimise_nogoods = if args.proof_type == ProofType::Full { - warn!("Recursive minimisation is disabled when logging the full proof."); - false - } else { - !args.no_learning_clause_minimisation - }; let solver_options = SolverOptions { // 1 MB is 1_000_000 bytes memory_preallocated: args.memory_preallocated, restart_options, - should_minimise_nogoods, + should_minimise_nogoods: !args.no_learning_clause_minimisation, random_generator: SmallRng::seed_from_u64(args.random_seed), proof_log, learning_options, From 5be0213c67e9d10b87a81604f649e0cd5b17e2ee Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 13:02:00 +1100 Subject: [PATCH 17/43] Fix compile error --- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 7b9ac5939..68719848f 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -630,7 +630,10 @@ fn run() -> PumpkinResult<()> { proof_type: args.proof_path.map(|_| args.proof_type), verbose: args.verbose, }, - ResolutionResolver::new(AnalysisMode::OneUIP, should_minimise_nogoods), + ResolutionResolver::new( + AnalysisMode::OneUIP, + !args.no_learning_clause_minimisation, + ), )?, }, } From 0194f6565dd7a322168a4c23bb1b1852c3b05f22 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 13:29:46 +1100 Subject: [PATCH 18/43] Work around assumptions by introducing them as initial domains --- pumpkin-crates/core/src/proof/finalizer.rs | 18 +++++++++++++++++- pumpkin-crates/core/src/proof/mod.rs | 2 -- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/core/src/proof/finalizer.rs b/pumpkin-crates/core/src/proof/finalizer.rs index b038ca112..6a4592eba 100644 --- a/pumpkin-crates/core/src/proof/finalizer.rs +++ b/pumpkin-crates/core/src/proof/finalizer.rs @@ -157,5 +157,21 @@ pub(crate) fn explain_root_assignment( [predicate].into_iter().collect(), )]); - let _ = finalize_proof_impl(context, to_explain); + let required_assumptions = finalize_proof_impl(context, to_explain); + + // This can happen when solving under assumptions. However, we do not have a good way to + // handle assumptions in the proof format yet. So, we introduce them as initial domains. + // This would never pass an external checker, but will satisfy the runtime deduction + // verification. + for assumption in required_assumptions { + let _ = context + .proof_log + .log_domain_inference( + assumption, + &context.state.variable_names, + &mut context.state.constraint_tags, + &context.state.assignments, + ) + .expect("failed to write to proof"); + } } diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 5a8725f1f..ed62a256f 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -139,8 +139,6 @@ impl ProofLog { constraint_tags: &mut KeyGenerator, assignments: &Assignments, ) -> std::io::Result> { - assert!(assignments.is_initial_bound(predicate)); - if cfg!(feature = "check-deductions") { self.supporting_inferences.push(SupportingInference { premises: vec![], From 9f3cc2f4808060089de868e2caeb8fd2ea41f8d4 Mon Sep 17 00:00:00 2001 From: Maarten Flippo Date: Sun, 29 Mar 2026 13:53:29 +1100 Subject: [PATCH 19/43] Allow inconsistent premises in the deduction --- pumpkin-checker/src/deductions.rs | 27 +++++--------- .../checking/src/deduction_checker.rs | 33 ++++++++--------- pumpkin-crates/core/src/proof/mod.rs | 35 ++++++++----------- 3 files changed, 37 insertions(+), 58 deletions(-) diff --git a/pumpkin-checker/src/deductions.rs b/pumpkin-checker/src/deductions.rs index 2c6e15994..5ad15a316 100644 --- a/pumpkin-checker/src/deductions.rs +++ b/pumpkin-checker/src/deductions.rs @@ -35,10 +35,6 @@ pub enum InvalidDeduction { /// conflict. #[error("no conflict was derived after applying all inferences")] NoConflict(Vec), - - /// The premise contains mutually exclusive atomic constraints. - #[error("the deduction contains inconsistent premises")] - InconsistentPremises, } /// Verify that a deduction is valid given the inferences in the proof stage. @@ -74,21 +70,16 @@ fn convert_error( error: pumpkin_checking::InvalidDeduction, facts_in_proof_stage: &BTreeMap, ) -> InvalidDeduction { - match error { - pumpkin_checking::InvalidDeduction::NoConflict(ignored_inferences) => { - let mapped_ignored_inferences = ignored_inferences - .into_iter() - .map(|ignored_inference| { - convert_ignored_inferences(ignored_inference, facts_in_proof_stage) - }) - .collect(); + let pumpkin_checking::InvalidDeduction(ignored_inferences) = error; - InvalidDeduction::NoConflict(mapped_ignored_inferences) - } - pumpkin_checking::InvalidDeduction::InconsistentPremises => { - InvalidDeduction::InconsistentPremises - } - } + let mapped_ignored_inferences = ignored_inferences + .into_iter() + .map(|ignored_inference| { + convert_ignored_inferences(ignored_inference, facts_in_proof_stage) + }) + .collect(); + + InvalidDeduction::NoConflict(mapped_ignored_inferences) } fn convert_ignored_inferences( diff --git a/pumpkin-crates/checking/src/deduction_checker.rs b/pumpkin-crates/checking/src/deduction_checker.rs index d6647d148..d0866a31d 100644 --- a/pumpkin-crates/checking/src/deduction_checker.rs +++ b/pumpkin-crates/checking/src/deduction_checker.rs @@ -15,18 +15,12 @@ pub struct IgnoredInference { } /// A deduction is rejected by the checker. +/// +/// The inferences in the proof stage do not derive an empty domain or an explicit +/// conflict. #[derive(thiserror::Error, Debug, PartialEq, Eq)] -#[error("invalid deduction")] -pub enum InvalidDeduction { - /// The inferences in the proof stage do not derive an empty domain or an explicit - /// conflict. - #[error("no conflict was derived after applying all inferences")] - NoConflict(Vec>), - - /// The premise contains mutually exclusive atomic constraints. - #[error("the deduction contains inconsistent premises")] - InconsistentPremises, -} +#[error("no conflict was derived after applying all inferences")] +pub struct InvalidDeduction(pub Vec>); /// An inference used to support a deduction. #[derive(Clone, Debug, PartialEq, Eq)] @@ -55,8 +49,10 @@ where // At some point, this should either reach a fact without a consequent or derive an // inconsistent domain. - let mut variable_state = VariableState::prepare_for_conflict_check(premises, None) - .map_err(|_| InvalidDeduction::InconsistentPremises)?; + let Ok(mut variable_state) = VariableState::prepare_for_conflict_check(premises, None) else { + // If the deduction contains inconsistent premises, its trivially valid. + return Ok(()); + }; let mut unused_inferences = Vec::new(); @@ -98,7 +94,7 @@ where // Reaching this point means that the conjunction of inferences did not yield to a // conflict. Therefore the deduction is invalid. - Err(InvalidDeduction::NoConflict(unused_inferences)) + Err(InvalidDeduction(unused_inferences)) } #[cfg(test)] @@ -163,13 +159,12 @@ mod tests { } #[test] - fn inconsistent_premises_are_identified() { + fn inconsistent_premises_are_no_problem() { let premises = vec![test_atomic!([x >= 5]), test_atomic!([x <= 4])]; let inferences = vec![inference!([x == 5] -> false)]; - let error = verify_deduction(premises, inferences).expect_err("inconsistent premises"); - assert_eq!(InvalidDeduction::InconsistentPremises, error); + verify_deduction(premises, inferences).expect("no inconsistency"); } #[test] @@ -182,7 +177,7 @@ mod tests { ]; let error = verify_deduction(premises, inferences).expect_err("conflict is not reached"); - assert_eq!(InvalidDeduction::NoConflict(vec![]), error); + assert_eq!(InvalidDeduction(vec![]), error); } #[test] @@ -197,7 +192,7 @@ mod tests { let error = verify_deduction(premises, inferences).expect_err("premises are not satisfied"); assert_eq!( - InvalidDeduction::NoConflict(vec![ + InvalidDeduction(vec![ IgnoredInference { inference: inference!([y <= 7] & [x >= 6] -> [z != 10]), unsatisfied_premises: vec![test_atomic!([x >= 6])], diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index ed62a256f..082f97e63 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -338,27 +338,20 @@ impl ProofLog { Ok(_) => { self.supporting_inferences.clear(); } - Err(error) => { - match error { - InvalidDeduction::NoConflict(ignored_inferences) => { - eprintln!("Supporting inferences:"); - for inference in self.supporting_inferences.iter() { - eprintln!("{:?} -> {:?}", inference.premises, inference.consequent); - } - - if !ignored_inferences.is_empty() { - eprintln!("Ignored inferences:"); - for ignored_inference in ignored_inferences { - eprintln!( - "{:?} -> {:?}", - ignored_inference.inference.premises, - ignored_inference.inference.consequent - ); - } - } - } - InvalidDeduction::InconsistentPremises => { - eprintln!("Inconsistent predicates in learned nogood") + Err(InvalidDeduction(ignored_inferences)) => { + eprintln!("Supporting inferences:"); + for inference in self.supporting_inferences.iter() { + eprintln!("{:?} -> {:?}", inference.premises, inference.consequent); + } + + if !ignored_inferences.is_empty() { + eprintln!("Ignored inferences:"); + for ignored_inference in ignored_inferences { + eprintln!( + "{:?} -> {:?}", + ignored_inference.inference.premises, + ignored_inference.inference.consequent + ); } } From ce38731c0e6fd2e5ed6914fe62e9d697269e2f81 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 14:01:14 +0200 Subject: [PATCH 20/43] feat: setup for removing elements during conflict analysis --- .../src/resolvers/resolution_resolver.rs | 154 ++++++++++++------ .../core/src/containers/key_value_heap.rs | 12 +- 2 files changed, 117 insertions(+), 49 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index cd2c763f8..c703a0c40 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -6,9 +6,11 @@ use pumpkin_core::conflict_resolving::ConflictResolver; use pumpkin_core::containers::KeyValueHeap; use pumpkin_core::containers::StorageKey; use pumpkin_core::create_statistics_struct; +use pumpkin_core::predicate; use pumpkin_core::predicates::Lbd; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateIdGenerator; +use pumpkin_core::predicates::PredicateType; use pumpkin_core::propagation::PredicateId; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::state::CurrentNogood; @@ -268,56 +270,95 @@ impl ResolutionResolver { self.to_process_heap.delete_key(next_id); } - // Then we check whether the predicate was not already present in the heap, if - // this is not the case then we insert it - if !self.to_process_heap.is_key_present(predicate_id) - && *self.to_process_heap.get_value(predicate_id) == 0 + context.predicate_appeared_in_conflict(predicate); + + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); + + for element in self + .to_process_heap + .keys() + .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) + .filter(|element| { + element.get_domain() == predicate.get_domain() + && context.get_state().trail_position(*element) + != context.get_state().trail_position(predicate) + }) + .collect::>() { - context.predicate_appeared_in_conflict(predicate); - - // The goal is to traverse predicate in reverse order of the trail. - // - // However some predicates may share the trail position. For example, if a - // predicate that was posted to trail resulted in - // some other predicates being true, then all - // these predicates would have the same trail position. - // - // When considering the predicates in reverse order of the trail, the - // implicitly set predicates are posted after the - // explicitly set one, but they all have the same - // trail position. - // - // To remedy this, we make a tie-breaking scheme to prioritise implied - // predicates over explicit predicates. This is done - // by assigning explicitly set predicates the - // value `2 * trail_position`, whereas implied predicates get `2 * - // trail_position + 1`. - let heap_value = if context.get_state().is_on_trail(predicate) { - context - .get_state() - .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") - * 2 - } else { - context - .get_state() - .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") - * 2 - + 1 - }; - - // We restore the key and since we know that the value is 0, we can safely - // increment with `heap_value` - self.to_process_heap.restore_key(predicate_id); - self.to_process_heap - .increment(predicate_id, heap_value as u32); - - pumpkin_assert_moderate!( - *self.to_process_heap.get_value(predicate_id) == heap_value.try_into().unwrap(), - "The value in the heap should be the same as was added" - ) + match (element.get_predicate_type(), predicate.get_predicate_type()) { + (PredicateType::Equal, PredicateType::NotEqual) => return, + (PredicateType::Equal, PredicateType::UpperBound) => return, + (PredicateType::Equal, PredicateType::LowerBound) => return, + (PredicateType::UpperBound, PredicateType::UpperBound) => { + if element.get_right_hand_side() <= predicate.get_right_hand_side() { + return; + } else { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + } + } + (PredicateType::UpperBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + // todo!() + } else if element.get_right_hand_side() < predicate.get_right_hand_side() { + return; + } + } + (PredicateType::LowerBound, PredicateType::LowerBound) => { + if element.get_right_hand_side() >= predicate.get_right_hand_side() { + return; + } else { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + } + } + (PredicateType::LowerBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + // todo!() + } else if element.get_right_hand_side() > predicate.get_right_hand_side() { + return; + } + } + (PredicateType::UpperBound, PredicateType::LowerBound) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + // todo!() + } + } + + _ => {} + } } + + // The goal is to traverse predicate in reverse order of the trail. + // + // However some predicates may share the trail position. For example, if a + // predicate that was posted to trail resulted in + // some other predicates being true, then all + // these predicates would have the same trail position. + // + // When considering the predicates in reverse order of the trail, the + // implicitly set predicates are posted after the + // explicitly set one, but they all have the same + // trail position. + // + // To remedy this, we make a tie-breaking scheme to prioritise implied + // predicates over explicit predicates. This is done + // by assigning explicitly set predicates the + // value `2 * trail_position`, whereas implied predicates get `2 * + // trail_position + 1`. + let heap_value = get_heap_value(predicate, context); + + // We restore the key and since we know that the value is 0, we can safely + // increment with `heap_value` + self.to_process_heap.restore_key(predicate_id); + self.to_process_heap + .set_value(predicate_id, heap_value as u32); + + pumpkin_assert_simple!( + *self.to_process_heap.get_value(predicate_id) == heap_value.try_into().unwrap(), + "The value in the heap should be the same as was added" + ) } else { // We do not check for duplicate, we simply add the predicate. // Semantic minimisation will later remove duplicates and do other processing. @@ -393,3 +434,20 @@ impl ResolutionResolver { } } } + +fn get_heap_value(predicate: Predicate, context: &mut ConflictAnalysisContext<'_>) -> usize { + if context.get_state().is_on_trail(predicate) { + context + .get_state() + .trail_position(predicate) + .expect("Predicate should be true during conflict analysis") + * 2 + } else { + context + .get_state() + .trail_position(predicate) + .expect("Predicate should be true during conflict analysis") + * 2 + + 1 + } +} diff --git a/pumpkin-crates/core/src/containers/key_value_heap.rs b/pumpkin-crates/core/src/containers/key_value_heap.rs index 12334728f..4a9b0246e 100644 --- a/pumpkin-crates/core/src/containers/key_value_heap.rs +++ b/pumpkin-crates/core/src/containers/key_value_heap.rs @@ -62,7 +62,7 @@ where /// Get the keys in the heap. /// /// The order in which the keys are yielded is unspecified. - pub(crate) fn keys(&self) -> impl Iterator + '_ { + pub fn keys(&self) -> impl Iterator + '_ { self.map_position_to_key[..self.end_position] .iter() .copied() @@ -123,6 +123,16 @@ where } } + pub fn set_value(&mut self, key: Key, value: Value) { + let position = self.map_key_to_position[key]; + self.values[position] = value; + // Recall that increment may be applied to keys not present + // So we only apply sift up in case the key is present + if self.is_key_present(key) { + self.sift_up(position); + } + } + /// Restores the entry with key 'key' to the heap if the key is not present, otherwise does /// nothing. Its value is the previous value used before 'delete_key' was called. /// From 69e6e7cd7854b085ebd3f0a576eaea99584e64fe Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 14:08:09 +0200 Subject: [PATCH 21/43] feat: adding statistics --- .../src/resolvers/resolution_resolver.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index c703a0c40..c29e2d63f 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,5 +1,4 @@ use pumpkin_core::asserts::pumpkin_assert_advanced; -use pumpkin_core::asserts::pumpkin_assert_moderate; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; use pumpkin_core::conflict_resolving::ConflictResolver; @@ -88,6 +87,7 @@ create_statistics_struct!( average_backtrack_amount: CumulativeMovingAverage, /// The average literal-block distance (LBD) metric for newly added learned nogoods average_lbd: CumulativeMovingAverage, + num_removed_during_analysis: usize, }); #[derive(Debug, Clone, Copy, Default)] @@ -292,8 +292,10 @@ impl ResolutionResolver { (PredicateType::Equal, PredicateType::LowerBound) => return, (PredicateType::UpperBound, PredicateType::UpperBound) => { if element.get_right_hand_side() <= predicate.get_right_hand_side() { + self.statistics.num_removed_during_analysis += 1; return; } else { + self.statistics.num_removed_during_analysis += 1; let element_id = self.predicate_id_generator.get_id(element); self.to_process_heap.delete_key(element_id); } @@ -302,13 +304,16 @@ impl ResolutionResolver { if element.get_right_hand_side() == predicate.get_right_hand_side() { // todo!() } else if element.get_right_hand_side() < predicate.get_right_hand_side() { + self.statistics.num_removed_during_analysis += 1; return; } } (PredicateType::LowerBound, PredicateType::LowerBound) => { if element.get_right_hand_side() >= predicate.get_right_hand_side() { + self.statistics.num_removed_during_analysis += 1; return; } else { + self.statistics.num_removed_during_analysis += 1; let element_id = self.predicate_id_generator.get_id(element); self.to_process_heap.delete_key(element_id); } @@ -317,6 +322,7 @@ impl ResolutionResolver { if element.get_right_hand_side() == predicate.get_right_hand_side() { // todo!() } else if element.get_right_hand_side() > predicate.get_right_hand_side() { + self.statistics.num_removed_during_analysis += 1; return; } } From a6cdcb4ff44cf255aad38dfa2fccbf013382984c Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 15:19:05 +0200 Subject: [PATCH 22/43] fix: time-table checker not passing with holes --- .../cumulative/time_table/checker.rs | 203 ++++++++---------- 1 file changed, 88 insertions(+), 115 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 83790b842..6a33ddbb9 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -6,8 +6,6 @@ use pumpkin_checking::InferenceChecker; use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; -use crate::cumulative::time_table::time_table_util::has_overlap_with_interval; - #[derive(Clone, Debug)] pub struct TimeTableChecker { pub tasks: Box<[CheckerTask]>, @@ -21,66 +19,12 @@ pub struct CheckerTask { pub processing_time: i32, } -fn lower_bound_can_be_propagated_by_profile< - Var: CheckerVariable, - Atomic: AtomicConstraint, ->( - context: &VariableState, - lower_bound: i32, +fn can_be_propagated_by_profile, Atomic: AtomicConstraint>( task: &CheckerTask, - start: i32, - end: i32, height: i32, capacity: i32, ) -> bool { - let upper_bound = task - .start_time - .induced_upper_bound(context) - .try_into() - .unwrap(); - height + task.resource_usage > capacity - && !(upper_bound < (lower_bound + task.processing_time) - && has_overlap_with_interval( - upper_bound, - lower_bound + task.processing_time, - start, - end, - )) - && has_overlap_with_interval(lower_bound, upper_bound + task.processing_time, start, end) - && (lower_bound + task.processing_time) > start - && lower_bound <= end -} - -fn upper_bound_can_be_propagated_by_profile< - Var: CheckerVariable, - Atomic: AtomicConstraint, ->( - context: &VariableState, - upper_bound: i32, - task: &CheckerTask, - start: i32, - end: i32, - height: i32, - capacity: i32, -) -> bool { - let lower_bound = task - .start_time - .induced_lower_bound(context) - .try_into() - .unwrap(); - - height + task.resource_usage > capacity - && !(upper_bound < (lower_bound + task.processing_time) - && has_overlap_with_interval( - upper_bound, - lower_bound + task.processing_time, - start, - end, - )) - && has_overlap_with_interval(lower_bound, upper_bound + task.processing_time, start, end) - && (upper_bound + task.processing_time) > end - && upper_bound <= end } impl InferenceChecker for TimeTableChecker @@ -90,7 +34,7 @@ where { fn check( &self, - state: VariableState, + mut state: VariableState, _: &[Atomic], consequent: Option<&Atomic>, ) -> bool { @@ -117,30 +61,12 @@ where .try_into() .unwrap(); - if lst < est + task.processing_time { - *profile.entry(lst).or_insert(0) += task.resource_usage; - *profile.entry(est + task.processing_time).or_insert(0) -= task.resource_usage; - } - } - - let mut profiles = Vec::new(); - let mut current_usage = 0; - let mut previous_time_point = *profile - .first_key_value() - .expect("Expected at least one mandatory part") - .0; - for (time_point, usage) in profile.iter() { - if current_usage > 0 && *time_point != previous_time_point { - profiles.push((previous_time_point, *time_point - 1, current_usage)) - } - - current_usage += *usage; - - if current_usage > self.capacity { - return true; + for t in lst..est + task.processing_time { + *profile.entry(t).or_insert(0) += task.resource_usage; + if *profile.get(&t).unwrap() > self.capacity { + return true; + } } - - previous_time_point = *time_point; } if let Some(propagating_task) = consequent.map(|consequent| { @@ -149,48 +75,32 @@ where .find(|task| task.start_time.does_atomic_constrain_self(consequent)) .expect("If there is a consequent, then there should be a propagating task") }) { - let mut lower_bound: i32 = propagating_task + let lst: i32 = propagating_task .start_time - .induced_lower_bound(&state) + .induced_upper_bound(&state) .try_into() .unwrap(); - for (start, end_inclusive, height) in profiles.iter() { - if lower_bound_can_be_propagated_by_profile( - &state, - lower_bound, - propagating_task, - *start, - *end_inclusive, - *height, - self.capacity, - ) { - lower_bound = end_inclusive + 1; - } - } - if lower_bound > propagating_task.start_time.induced_upper_bound(&state) { - return true; - } - - let mut upper_bound: i32 = propagating_task + let est: i32 = propagating_task .start_time - .induced_upper_bound(&state) + .induced_lower_bound(&state) .try_into() .unwrap(); - for (start, end_inclusive, height) in profiles.iter().rev() { - if upper_bound_can_be_propagated_by_profile( - &state, - upper_bound, - propagating_task, - *start, - *end_inclusive, - *height, - self.capacity, - ) { - upper_bound = start - propagating_task.processing_time; + + for t in lst..est + propagating_task.processing_time { + *profile.entry(t).or_insert(0) += propagating_task.resource_usage; + if *profile.get(&t).unwrap() > self.capacity { + return true; } } - if upper_bound < propagating_task.start_time.induced_lower_bound(&state) { - return true; + + for (t, height) in profile.iter() { + if can_be_propagated_by_profile(propagating_task, *height, self.capacity) { + for t in (t - propagating_task.processing_time + 1)..=*t { + if !state.apply(&propagating_task.start_time.atomic_not_equal(t)) { + return true; + } + } + } } } false @@ -573,4 +483,67 @@ mod tests { assert!(checker.check(state, &premises, consequent.as_ref())); } + + #[test] + fn test_holes_in_domain() { + let premises = [ + TestAtomic { + name: "x3", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 1, + }, + TestAtomic { + name: "x3", + comparison: pumpkin_checking::Comparison::LessEqual, + value: 3, + }, + TestAtomic { + name: "x1", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 4, + }, + TestAtomic { + name: "x1", + comparison: pumpkin_checking::Comparison::LessEqual, + value: 4, + }, + TestAtomic { + name: "x2", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 2, + }, + ]; + + let consequent = Some(TestAtomic { + name: "x2", + comparison: pumpkin_checking::Comparison::GreaterEqual, + value: 5, + }); + let state = VariableState::prepare_for_conflict_check(premises, consequent) + .expect("no conflicting atomics"); + + let checker = TimeTableChecker { + tasks: vec![ + CheckerTask { + start_time: "x3", + resource_usage: 1, + processing_time: 3, + }, + CheckerTask { + start_time: "x2", + resource_usage: 2, + processing_time: 2, + }, + CheckerTask { + start_time: "x1", + resource_usage: 1, + processing_time: 1, + }, + ] + .into(), + capacity: 2, + }; + + assert!(checker.check(state, &premises, consequent.as_ref())); + } } From b99b962e26b066ffb44efa7f808f23216690d6ab Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Mon, 30 Mar 2026 16:03:58 +0200 Subject: [PATCH 23/43] fix: swapping around of values --- .../src/propagators/cumulative/time_table/checker.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 6a33ddbb9..31d08cb28 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -61,7 +61,7 @@ where .try_into() .unwrap(); - for t in lst..est + task.processing_time { + for t in est + task.processing_time..lst { *profile.entry(t).or_insert(0) += task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; @@ -86,7 +86,7 @@ where .try_into() .unwrap(); - for t in lst..est + propagating_task.processing_time { + for t in est + propagating_task.processing_time..lst { *profile.entry(t).or_insert(0) += propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; From 2c70913794b52b4e5f3827c834117313bbd23b77 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 08:42:16 +0200 Subject: [PATCH 24/43] Revert "fix: swapping around of values" This reverts commit b99b962e26b066ffb44efa7f808f23216690d6ab. --- .../src/propagators/cumulative/time_table/checker.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 31d08cb28..6a33ddbb9 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -61,7 +61,7 @@ where .try_into() .unwrap(); - for t in est + task.processing_time..lst { + for t in lst..est + task.processing_time { *profile.entry(t).or_insert(0) += task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; @@ -86,7 +86,7 @@ where .try_into() .unwrap(); - for t in est + propagating_task.processing_time..lst { + for t in lst..est + propagating_task.processing_time { *profile.entry(t).or_insert(0) += propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; From a34897a36623598f62b27fcec8e2ccc979706ac5 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 08:47:07 +0200 Subject: [PATCH 25/43] fix: remove instead of add --- .../src/propagators/cumulative/time_table/checker.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs index 6a33ddbb9..d475463d6 100644 --- a/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs +++ b/pumpkin-crates/propagators/src/propagators/cumulative/time_table/checker.rs @@ -87,7 +87,7 @@ where .unwrap(); for t in lst..est + propagating_task.processing_time { - *profile.entry(t).or_insert(0) += propagating_task.resource_usage; + *profile.entry(t).or_insert(0) -= propagating_task.resource_usage; if *profile.get(&t).unwrap() > self.capacity { return true; } From 954aba4c5c57b3cbd1e4ea3cea649d7e4b932096 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 09:31:17 +0200 Subject: [PATCH 26/43] feat: replacing predicates with new predicates + improving statistic logging --- .../src/resolvers/resolution_resolver.rs | 381 +++++++++++++++--- .../core/src/containers/key_value_heap.rs | 2 +- 2 files changed, 317 insertions(+), 66 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index c29e2d63f..9ff42affc 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -1,3 +1,5 @@ +use std::ops::ControlFlow; + use pumpkin_core::asserts::pumpkin_assert_advanced; use pumpkin_core::asserts::pumpkin_assert_simple; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; @@ -87,7 +89,16 @@ create_statistics_struct!( average_backtrack_amount: CumulativeMovingAverage, /// The average literal-block distance (LBD) metric for newly added learned nogoods average_lbd: CumulativeMovingAverage, - num_removed_during_analysis: usize, + iterative_minimisation: IterativeMinimisationStatistics +}); + +create_statistics_struct!(IterativeMinimisationStatistics { + num_removed: usize, + num_replaced_with_new_current_dl: usize, + num_replaced_with_new_previous_dl: usize, + + num_removed_previous_dl: usize, + num_removed_current_dl: usize, }); #[derive(Debug, Clone, Copy, Default)] @@ -275,65 +286,12 @@ impl ResolutionResolver { self.to_process_heap.set_value(predicate_id, 0); self.to_process_heap.delete_key(predicate_id); - for element in self - .to_process_heap - .keys() - .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) - .filter(|element| { - element.get_domain() == predicate.get_domain() - && context.get_state().trail_position(*element) - != context.get_state().trail_position(predicate) - }) - .collect::>() + if let ControlFlow::Break(_) = self.check_redundancy_previous_level(predicate, context) { - match (element.get_predicate_type(), predicate.get_predicate_type()) { - (PredicateType::Equal, PredicateType::NotEqual) => return, - (PredicateType::Equal, PredicateType::UpperBound) => return, - (PredicateType::Equal, PredicateType::LowerBound) => return, - (PredicateType::UpperBound, PredicateType::UpperBound) => { - if element.get_right_hand_side() <= predicate.get_right_hand_side() { - self.statistics.num_removed_during_analysis += 1; - return; - } else { - self.statistics.num_removed_during_analysis += 1; - let element_id = self.predicate_id_generator.get_id(element); - self.to_process_heap.delete_key(element_id); - } - } - (PredicateType::UpperBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - // todo!() - } else if element.get_right_hand_side() < predicate.get_right_hand_side() { - self.statistics.num_removed_during_analysis += 1; - return; - } - } - (PredicateType::LowerBound, PredicateType::LowerBound) => { - if element.get_right_hand_side() >= predicate.get_right_hand_side() { - self.statistics.num_removed_during_analysis += 1; - return; - } else { - self.statistics.num_removed_during_analysis += 1; - let element_id = self.predicate_id_generator.get_id(element); - self.to_process_heap.delete_key(element_id); - } - } - (PredicateType::LowerBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - // todo!() - } else if element.get_right_hand_side() > predicate.get_right_hand_side() { - self.statistics.num_removed_during_analysis += 1; - return; - } - } - (PredicateType::UpperBound, PredicateType::LowerBound) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - // todo!() - } - } - - _ => {} - } + return; + } + if let ControlFlow::Break(_) = self.check_redundancy_current_level(predicate, context) { + return; } // The goal is to traverse predicate in reverse order of the trail. @@ -358,11 +316,10 @@ impl ResolutionResolver { // We restore the key and since we know that the value is 0, we can safely // increment with `heap_value` self.to_process_heap.restore_key(predicate_id); - self.to_process_heap - .set_value(predicate_id, heap_value as u32); + self.to_process_heap.set_value(predicate_id, heap_value); pumpkin_assert_simple!( - *self.to_process_heap.get_value(predicate_id) == heap_value.try_into().unwrap(), + *self.to_process_heap.get_value(predicate_id) == heap_value, "The value in the heap should be the same as was added" ) } else { @@ -372,6 +329,300 @@ impl ResolutionResolver { } } + fn check_redundancy_current_level( + &mut self, + predicate: Predicate, + context: &mut ConflictAnalysisContext<'_>, + ) -> ControlFlow<()> { + for element in self + .to_process_heap + .keys() + .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) + .filter(|element| { + element.get_domain() == predicate.get_domain() + && context.get_state().trail_position(*element) + != context.get_state().trail_position(predicate) + }) + .collect::>() + { + match (element.get_predicate_type(), predicate.get_predicate_type()) { + (PredicateType::Equal, PredicateType::NotEqual) + | (PredicateType::Equal, PredicateType::UpperBound) + | (PredicateType::Equal, PredicateType::LowerBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + return ControlFlow::Break(()); + } + (PredicateType::UpperBound, PredicateType::UpperBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + if element.get_right_hand_side() <= predicate.get_right_hand_side() { + return ControlFlow::Break(()); + } else { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + } + } + (PredicateType::UpperBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_current_dl += 1; + let domain = element.get_domain(); + + let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); + self.replace_if_possible_current_level(context, element, new_predicate)?; + } else if element.get_right_hand_side() < predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + self.statistics.iterative_minimisation.num_removed += 1; + return ControlFlow::Break(()); + } + } + (PredicateType::LowerBound, PredicateType::LowerBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + if element.get_right_hand_side() >= predicate.get_right_hand_side() { + return ControlFlow::Break(()); + } else { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + } + } + (PredicateType::LowerBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_current_dl += 1; + let domain = element.get_domain(); + + let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); + self.replace_if_possible_current_level(context, element, new_predicate)?; + } else if element.get_right_hand_side() > predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + return ControlFlow::Break(()); + } + } + (PredicateType::UpperBound, PredicateType::LowerBound) + if element.get_right_hand_side() == predicate.get_right_hand_side() => + { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_current_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_current_dl += 1; + let domain = element.get_domain(); + + let new_predicate = predicate!(domain == element.get_right_hand_side()); + self.replace_if_possible_current_level(context, element, new_predicate)?; + } + + _ => {} + } + } + ControlFlow::Continue(()) + } + + fn replace_if_possible_current_level( + &mut self, + context: &mut ConflictAnalysisContext<'_>, + element: Predicate, + new_predicate: Predicate, + ) -> ControlFlow<()> { + let heap_value = get_heap_value(new_predicate, context); + + if heap_value + < self + .to_process_heap + .peek_max() + .map(|(_, value)| *value) + .unwrap_or_default() + { + let element_id = self.predicate_id_generator.get_id(element); + self.to_process_heap.delete_key(element_id); + + self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); + + return ControlFlow::Break(()); + } + ControlFlow::Continue(()) + } + + fn check_redundancy_previous_level( + &mut self, + predicate: Predicate, + context: &mut ConflictAnalysisContext<'_>, + ) -> ControlFlow<()> { + for element in self + .processed_nogood_predicates + .iter() + .filter(|element| { + element.get_domain() == predicate.get_domain() + && context.get_state().trail_position(**element) + != context.get_state().trail_position(predicate) + }) + .copied() + .collect::>() + { + match (element.get_predicate_type(), predicate.get_predicate_type()) { + (PredicateType::Equal, PredicateType::NotEqual) + | (PredicateType::Equal, PredicateType::UpperBound) + | (PredicateType::Equal, PredicateType::LowerBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + return ControlFlow::Break(()); + } + (PredicateType::UpperBound, PredicateType::UpperBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + if element.get_right_hand_side() <= predicate.get_right_hand_side() { + return ControlFlow::Break(()); + } else { + if let Some(index) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == element) + { + let _ = self.processed_nogood_predicates.remove(index); + } + } + } + (PredicateType::UpperBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_previous_dl += 1; + + let domain = element.get_domain(); + let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); + self.replace_if_possible_previous_level(context, element, new_predicate)?; + } else if element.get_right_hand_side() < predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + return ControlFlow::Break(()); + } + } + (PredicateType::LowerBound, PredicateType::LowerBound) => { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + if element.get_right_hand_side() >= predicate.get_right_hand_side() { + return ControlFlow::Break(()); + } else { + if let Some(index) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == element) + { + let _ = self.processed_nogood_predicates.remove(index); + } + } + } + (PredicateType::LowerBound, PredicateType::NotEqual) => { + if element.get_right_hand_side() == predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_previous_dl += 1; + + let domain = element.get_domain(); + let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); + self.replace_if_possible_previous_level(context, element, new_predicate)?; + } else if element.get_right_hand_side() > predicate.get_right_hand_side() { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + return ControlFlow::Break(()); + } + } + (PredicateType::UpperBound, PredicateType::LowerBound) + if element.get_right_hand_side() == predicate.get_right_hand_side() => + { + self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation + .num_removed_previous_dl += 1; + self.statistics + .iterative_minimisation + .num_replaced_with_new_previous_dl += 1; + + let domain = element.get_domain(); + let new_predicate = predicate!(domain == element.get_right_hand_side()); + self.replace_if_possible_previous_level(context, element, new_predicate)?; + } + + _ => {} + } + } + ControlFlow::Continue(()) + } + + fn replace_if_possible_previous_level( + &mut self, + context: &mut ConflictAnalysisContext<'_>, + element: Predicate, + new_predicate: Predicate, + ) -> ControlFlow<()> { + let heap_value = get_heap_value(new_predicate, context); + + if heap_value + < self + .to_process_heap + .peek_max() + .map(|(_, value)| *value) + .unwrap_or_default() + { + if let Some(index) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == element) + { + let _ = self.processed_nogood_predicates.remove(index); + } + + self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); + + return ControlFlow::Break(()); + } + ControlFlow::Continue(()) + } + fn pop_predicate_from_conflict_nogood(&mut self) -> Predicate { let next_predicate_id = self.to_process_heap.pop_max().unwrap(); self.predicate_id_generator.get_predicate(next_predicate_id) @@ -441,18 +692,18 @@ impl ResolutionResolver { } } -fn get_heap_value(predicate: Predicate, context: &mut ConflictAnalysisContext<'_>) -> usize { +fn get_heap_value(predicate: Predicate, context: &mut ConflictAnalysisContext<'_>) -> u32 { if context.get_state().is_on_trail(predicate) { context .get_state() .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") + .expect("Predicate should be true during conflict analysis") as u32 * 2 } else { context .get_state() .trail_position(predicate) - .expect("Predicate should be true during conflict analysis") + .expect("Predicate should be true during conflict analysis") as u32 * 2 + 1 } diff --git a/pumpkin-crates/core/src/containers/key_value_heap.rs b/pumpkin-crates/core/src/containers/key_value_heap.rs index 4a9b0246e..4c1a49d44 100644 --- a/pumpkin-crates/core/src/containers/key_value_heap.rs +++ b/pumpkin-crates/core/src/containers/key_value_heap.rs @@ -72,7 +72,7 @@ where /// this does not delete the key (see [`KeyValueHeap::pop_max`] to get and delete). /// /// The time-complexity of this operation is O(1) - pub(crate) fn peek_max(&self) -> Option<(&Key, &Value)> { + pub fn peek_max(&self) -> Option<(&Key, &Value)> { if self.has_no_nonremoved_elements() { None } else { From 3df8f04e5a76b494dada4e4646f36449ecf70b70 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 09:54:48 +0200 Subject: [PATCH 27/43] feat: add flag for running with iterative minimisation --- .../src/resolvers/resolution_resolver.rs | 206 +++++++++++------- .../engine/constraint_satisfaction_solver.rs | 3 + 2 files changed, 129 insertions(+), 80 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 9ff42affc..9923d1928 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -68,11 +68,12 @@ pub struct ResolutionResolver { statistics: LearnedNogoodStatistics, should_minimise: bool, + iterative_minimisation: bool, } impl Default for ResolutionResolver { fn default() -> Self { - ResolutionResolver::new(AnalysisMode::OneUIP, true) + ResolutionResolver::new(AnalysisMode::OneUIP, true, false) } } @@ -89,7 +90,7 @@ create_statistics_struct!( average_backtrack_amount: CumulativeMovingAverage, /// The average literal-block distance (LBD) metric for newly added learned nogoods average_lbd: CumulativeMovingAverage, - iterative_minimisation: IterativeMinimisationStatistics + iterative_minimisation_statistics: IterativeMinimisationStatistics }); create_statistics_struct!(IterativeMinimisationStatistics { @@ -147,7 +148,7 @@ impl ConflictResolver for ResolutionResolver { } impl ResolutionResolver { - pub fn new(mode: AnalysisMode, should_minimise: bool) -> Self { + pub fn new(mode: AnalysisMode, should_minimise: bool, iterative_minimisation: bool) -> Self { Self { mode, to_process_heap: Default::default(), @@ -159,6 +160,7 @@ impl ResolutionResolver { semantic_minimiser: Default::default(), statistics: Default::default(), should_minimise, + iterative_minimisation, } } @@ -281,47 +283,57 @@ impl ResolutionResolver { self.to_process_heap.delete_key(next_id); } - context.predicate_appeared_in_conflict(predicate); - - self.to_process_heap.set_value(predicate_id, 0); - self.to_process_heap.delete_key(predicate_id); - - if let ControlFlow::Break(_) = self.check_redundancy_previous_level(predicate, context) + if self.iterative_minimisation + || (!self.to_process_heap.is_key_present(predicate_id) + && *self.to_process_heap.get_value(predicate_id) == 0) { - return; - } - if let ControlFlow::Break(_) = self.check_redundancy_current_level(predicate, context) { - return; - } + context.predicate_appeared_in_conflict(predicate); - // The goal is to traverse predicate in reverse order of the trail. - // - // However some predicates may share the trail position. For example, if a - // predicate that was posted to trail resulted in - // some other predicates being true, then all - // these predicates would have the same trail position. - // - // When considering the predicates in reverse order of the trail, the - // implicitly set predicates are posted after the - // explicitly set one, but they all have the same - // trail position. - // - // To remedy this, we make a tie-breaking scheme to prioritise implied - // predicates over explicit predicates. This is done - // by assigning explicitly set predicates the - // value `2 * trail_position`, whereas implied predicates get `2 * - // trail_position + 1`. - let heap_value = get_heap_value(predicate, context); - - // We restore the key and since we know that the value is 0, we can safely - // increment with `heap_value` - self.to_process_heap.restore_key(predicate_id); - self.to_process_heap.set_value(predicate_id, heap_value); + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); - pumpkin_assert_simple!( - *self.to_process_heap.get_value(predicate_id) == heap_value, - "The value in the heap should be the same as was added" - ) + if self.iterative_minimisation { + if let ControlFlow::Break(_) = + self.check_redundancy_previous_level(predicate, context) + { + return; + } + if let ControlFlow::Break(_) = + self.check_redundancy_current_level(predicate, context) + { + return; + } + } + + // The goal is to traverse predicate in reverse order of the trail. + // + // However some predicates may share the trail position. For example, if a + // predicate that was posted to trail resulted in + // some other predicates being true, then all + // these predicates would have the same trail position. + // + // When considering the predicates in reverse order of the trail, the + // implicitly set predicates are posted after the + // explicitly set one, but they all have the same + // trail position. + // + // To remedy this, we make a tie-breaking scheme to prioritise implied + // predicates over explicit predicates. This is done + // by assigning explicitly set predicates the + // value `2 * trail_position`, whereas implied predicates get `2 * + // trail_position + 1`. + let heap_value = get_heap_value(predicate, context); + + // We restore the key and since we know that the value is 0, we can safely + // increment with `heap_value` + self.to_process_heap.restore_key(predicate_id); + self.to_process_heap.set_value(predicate_id, heap_value); + + pumpkin_assert_simple!( + *self.to_process_heap.get_value(predicate_id) == heap_value, + "The value in the heap should be the same as was added" + ); + } } else { // We do not check for duplicate, we simply add the predicate. // Semantic minimisation will later remove duplicates and do other processing. @@ -349,16 +361,20 @@ impl ResolutionResolver { (PredicateType::Equal, PredicateType::NotEqual) | (PredicateType::Equal, PredicateType::UpperBound) | (PredicateType::Equal, PredicateType::LowerBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; return ControlFlow::Break(()); } (PredicateType::UpperBound, PredicateType::UpperBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; if element.get_right_hand_side() <= predicate.get_right_hand_side() { return ControlFlow::Break(()); @@ -369,30 +385,38 @@ impl ResolutionResolver { } (PredicateType::UpperBound, PredicateType::NotEqual) => { if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_current_dl += 1; let domain = element.get_domain(); let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); self.replace_if_possible_current_level(context, element, new_predicate)?; } else if element.get_right_hand_side() < predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; - self.statistics.iterative_minimisation.num_removed += 1; + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; return ControlFlow::Break(()); } } (PredicateType::LowerBound, PredicateType::LowerBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; if element.get_right_hand_side() >= predicate.get_right_hand_side() { return ControlFlow::Break(()); @@ -403,21 +427,25 @@ impl ResolutionResolver { } (PredicateType::LowerBound, PredicateType::NotEqual) => { if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_current_dl += 1; let domain = element.get_domain(); let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); self.replace_if_possible_current_level(context, element, new_predicate)?; } else if element.get_right_hand_side() > predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; return ControlFlow::Break(()); } @@ -425,12 +453,14 @@ impl ResolutionResolver { (PredicateType::UpperBound, PredicateType::LowerBound) if element.get_right_hand_side() == predicate.get_right_hand_side() => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_current_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_current_dl += 1; let domain = element.get_domain(); @@ -489,16 +519,20 @@ impl ResolutionResolver { (PredicateType::Equal, PredicateType::NotEqual) | (PredicateType::Equal, PredicateType::UpperBound) | (PredicateType::Equal, PredicateType::LowerBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; return ControlFlow::Break(()); } (PredicateType::UpperBound, PredicateType::UpperBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; if element.get_right_hand_side() <= predicate.get_right_hand_side() { return ControlFlow::Break(()); @@ -514,29 +548,35 @@ impl ResolutionResolver { } (PredicateType::UpperBound, PredicateType::NotEqual) => { if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_previous_dl += 1; let domain = element.get_domain(); let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); self.replace_if_possible_previous_level(context, element, new_predicate)?; } else if element.get_right_hand_side() < predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; return ControlFlow::Break(()); } } (PredicateType::LowerBound, PredicateType::LowerBound) => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; if element.get_right_hand_side() >= predicate.get_right_hand_side() { return ControlFlow::Break(()); @@ -552,21 +592,25 @@ impl ResolutionResolver { } (PredicateType::LowerBound, PredicateType::NotEqual) => { if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_previous_dl += 1; let domain = element.get_domain(); let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); self.replace_if_possible_previous_level(context, element, new_predicate)?; } else if element.get_right_hand_side() > predicate.get_right_hand_side() { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; return ControlFlow::Break(()); } @@ -574,12 +618,14 @@ impl ResolutionResolver { (PredicateType::UpperBound, PredicateType::LowerBound) if element.get_right_hand_side() == predicate.get_right_hand_side() => { - self.statistics.iterative_minimisation.num_removed += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics + .num_removed += 1; + self.statistics + .iterative_minimisation_statistics .num_removed_previous_dl += 1; self.statistics - .iterative_minimisation + .iterative_minimisation_statistics .num_replaced_with_new_previous_dl += 1; let domain = element.get_domain(); diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 4841ef3a6..78f3e7fdf 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -162,6 +162,8 @@ pub struct SatisfactionSolverOptions { pub learning_options: LearningOptions, /// The number of MBs which are preallocated by the nogood propagator. pub memory_preallocated: usize, + /// Whether semantic minimisation is applied during conflict analysis. + pub iterative_minimisation: bool, } impl Default for SatisfactionSolverOptions { @@ -173,6 +175,7 @@ impl Default for SatisfactionSolverOptions { proof_log: ProofLog::default(), learning_options: LearningOptions::default(), memory_preallocated: 50, + iterative_minimisation: false, } } } From 49b50f24d1da867fd317f50213545b0a9cf89ec0 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 10:05:33 +0200 Subject: [PATCH 28/43] chore: left over files --- .../src/resolvers/resolution_resolver.rs | 6 ++++-- pumpkin-solver/src/bin/pumpkin-solver/main.rs | 11 +++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 9923d1928..6c10d343f 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -289,8 +289,10 @@ impl ResolutionResolver { { context.predicate_appeared_in_conflict(predicate); - self.to_process_heap.set_value(predicate_id, 0); - self.to_process_heap.delete_key(predicate_id); + if self.iterative_minimisation { + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); + } if self.iterative_minimisation { if let ControlFlow::Break(_) = diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 68719848f..6b25be69c 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -171,6 +171,15 @@ struct Args { #[arg(long = "no-learning-minimise", verbatim_doc_comment)] no_learning_clause_minimisation: bool, + /// Decides whether to apply semantic minimisation during conflict analysis; according to the + /// idea proposed in "Semantic Learning for Lazy Clause Generation - Feydy et al. (2013)". + /// + /// If this flag is present then the minimisation is turned on. + /// + /// Possible values: bool + #[arg(long = "iterative-minimisation", verbatim_doc_comment)] + iterative_minimisation: bool, + /// Decides the sequence based on which the restarts are performed. /// /// - The "constant" approach uses a constant number of conflicts before another restart is @@ -575,6 +584,7 @@ fn run() -> PumpkinResult<()> { random_generator: SmallRng::seed_from_u64(args.random_seed), proof_log, learning_options, + iterative_minimisation: args.iterative_minimisation, }; let time_limit = args.time_limit.map(Duration::from_millis); @@ -633,6 +643,7 @@ fn run() -> PumpkinResult<()> { ResolutionResolver::new( AnalysisMode::OneUIP, !args.no_learning_clause_minimisation, + args.iterative_minimisation, ), )?, }, From fefee6a8c3c1d7f54b8982425df066571ec3181a Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 11:56:54 +0200 Subject: [PATCH 29/43] feat: initial attempt at making minimisation during ca more efficient --- .../src/minimisers/iterative_minimiser.rs | 238 ++++++++++++++++++ .../conflict-resolvers/src/minimisers/mod.rs | 2 + 2 files changed, 240 insertions(+) create mode 100644 pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs new file mode 100644 index 000000000..1dffb647a --- /dev/null +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -0,0 +1,238 @@ +use pumpkin_core::containers::HashMap; +use pumpkin_core::containers::HashSet; +use pumpkin_core::containers::KeyedVec; +use pumpkin_core::predicate; +use pumpkin_core::predicates::Predicate; +use pumpkin_core::predicates::PredicateType; +use pumpkin_core::variables::DomainId; + +pub(crate) struct IterativeMinimiser { + domains: KeyedVec, +} + +#[derive(Debug, Clone, Copy)] +pub(crate) enum ProcessingResult { + Redundant, + ReplacedPresent { + removed: Predicate, + }, + ReplacedWithNew { + previous: Predicate, + new_predicate: Predicate, + }, + NotRedundant, +} + +#[derive(Debug, Clone)] +struct IterativeDomain { + lower_bound_updates: Vec, + upper_bound_updates: Vec, + holes: HashMap, + + lower_bound: i32, + upper_bound: i32, +} + +impl Default for IterativeDomain { + fn default() -> Self { + Self { + lower_bound_updates: Default::default(), + upper_bound_updates: Default::default(), + holes: Default::default(), + lower_bound: i32::MIN, + upper_bound: i32::MAX, + } + } +} + +impl IterativeDomain { + pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { + match predicate.get_predicate_type() { + PredicateType::LowerBound => { + if predicate.get_right_hand_side() > self.lower_bound { + self.lower_bound = predicate.get_right_hand_side(); + self.lower_bound_updates + .push(predicate.get_right_hand_side()); + } + } + PredicateType::UpperBound => { + if predicate.get_right_hand_side() < self.upper_bound { + self.upper_bound = predicate.get_right_hand_side(); + self.upper_bound_updates + .push(predicate.get_right_hand_side()); + } + } + PredicateType::NotEqual => { + let mut lb_caused_update = false; + let mut ub_caused_update = false; + if predicate.get_right_hand_side() == self.lower_bound { + lb_caused_update = true; + self.lower_bound = predicate.get_right_hand_side() + 1; + self.lower_bound_updates + .push(predicate.get_right_hand_side() + 1); + } + if predicate.get_right_hand_side() == self.upper_bound { + ub_caused_update = true; + self.upper_bound = predicate.get_right_hand_side() - 1; + self.upper_bound_updates + .push(predicate.get_right_hand_side() - 1); + } + + let _ = self.holes.insert( + predicate.get_right_hand_side(), + (lb_caused_update, ub_caused_update), + ); + } + PredicateType::Equal => { + self.upper_bound = predicate.get_right_hand_side(); + self.upper_bound_updates + .push(predicate.get_right_hand_side()); + + self.lower_bound = predicate.get_right_hand_side(); + self.lower_bound_updates + .push(predicate.get_right_hand_side()); + } + } + } + + pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { + match predicate.get_predicate_type() { + PredicateType::LowerBound => { + let position = self + .lower_bound_updates + .iter() + .rev() + .position(|value| *value == predicate.get_right_hand_side()) + .expect("Expected removed lower-bound to be present"); + + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + } + PredicateType::UpperBound => { + let position = self + .upper_bound_updates + .iter() + .rev() + .position(|value| *value == predicate.get_right_hand_side()) + .expect("Expected removed lower-bound to be present"); + + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + } + PredicateType::NotEqual => { + let (lb_caused_update, ub_caused_update) = self + .holes + .get(&predicate.get_right_hand_side()) + .expect("Expected removed not equals to be present"); + + if *lb_caused_update { + let position = self + .lower_bound_updates + .iter() + .rev() + .position(|value| *value == predicate.get_right_hand_side() + 1) + .expect("Expected removed lower-bound to be present"); + + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + } + + if *ub_caused_update { + let position = self + .upper_bound_updates + .iter() + .rev() + .position(|value| *value == predicate.get_right_hand_side() - 1) + .expect("Expected removed lower-bound to be present"); + + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + } + } + PredicateType::Equal => { + assert_eq!(self.lower_bound, self.upper_bound); + assert_eq!(self.lower_bound, predicate.get_right_hand_side()); + + let _ = self.lower_bound_updates.pop(); + let _ = self.upper_bound_updates.pop(); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + } + } + } +} + +impl IterativeMinimiser { + pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { + let domain = predicate.get_domain(); + self.domains[domain].remove_predicate(predicate); + } + + pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { + let domain = predicate.get_domain(); + self.domains[domain].apply_predicate(predicate); + } + + pub(crate) fn process_predicate(&mut self, predicate: Predicate) -> ProcessingResult { + let domain = predicate.get_domain(); + self.domains.accomodate(domain, IterativeDomain::default()); + + let lower_bound = self.domains[domain].lower_bound; + let upper_bound = self.domains[domain].upper_bound; + + if lower_bound == upper_bound { + return ProcessingResult::Redundant; + } + + match predicate.get_predicate_type() { + PredicateType::LowerBound => { + if predicate.get_right_hand_side() == upper_bound { + return ProcessingResult::ReplacedWithNew { + previous: predicate!(domain <= upper_bound), + new_predicate: predicate!(domain == upper_bound), + }; + } else if predicate.get_right_hand_side() > lower_bound { + return ProcessingResult::ReplacedPresent { + removed: predicate!(domain >= lower_bound), + }; + } else { + return ProcessingResult::Redundant; + } + } + PredicateType::UpperBound => { + if predicate.get_right_hand_side() == lower_bound { + return ProcessingResult::ReplacedWithNew { + previous: predicate!(domain >= lower_bound), + new_predicate: predicate!(domain == lower_bound), + }; + } else if predicate.get_right_hand_side() < upper_bound { + return ProcessingResult::ReplacedPresent { + removed: predicate!(domain <= upper_bound), + }; + } else { + return ProcessingResult::Redundant; + } + } + PredicateType::NotEqual => { + if predicate.get_right_hand_side() == upper_bound { + return ProcessingResult::ReplacedWithNew { + previous: predicate!(domain <= upper_bound), + new_predicate: predicate!(domain <= upper_bound - 1), + }; + } else if predicate.get_right_hand_side() > upper_bound { + return ProcessingResult::Redundant; + } else if predicate.get_right_hand_side() == lower_bound { + return ProcessingResult::ReplacedWithNew { + previous: predicate!(domain >= lower_bound), + new_predicate: predicate!(domain >= lower_bound + 1), + }; + } else if predicate.get_right_hand_side() < lower_bound { + return ProcessingResult::Redundant; + } else { + return ProcessingResult::NotRedundant; + } + } + PredicateType::Equal => ProcessingResult::NotRedundant, + } + } +} diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs index 99b2efb5d..78c885180 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/mod.rs @@ -1,8 +1,10 @@ //! Contains the nogood minimisers. +mod iterative_minimiser; mod minimiser; mod recursive_minimiser; mod semantic_minimiser; +pub(crate) use iterative_minimiser::*; pub use minimiser::NogoodMinimiser; pub use recursive_minimiser::RecursiveMinimiser; pub use semantic_minimiser::SemanticMinimisationMode; From e737f835e74ed722eebc157c0c573d01c8ade761 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Tue, 31 Mar 2026 15:46:13 +0200 Subject: [PATCH 30/43] WIP: making progress --- Cargo.lock | 44 +- .../src/minimisers/iterative_minimiser.rs | 160 +++- .../src/resolvers/resolution_resolver.rs | 776 ++++++++++-------- .../core/src/containers/key_value_heap.rs | 14 +- .../engine/constraint_satisfaction_solver.rs | 3 - pumpkin-solver/src/bin/pumpkin-solver/main.rs | 3 +- pumpkin-solver/tests/helpers/mod.rs | 5 +- 7 files changed, 605 insertions(+), 400 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d912b678f..d25088877 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -30,7 +30,22 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a" dependencies = [ "anstyle", - "anstyle-parse", + "anstyle-parse 0.2.7", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + +[[package]] +name = "anstream" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" +dependencies = [ + "anstyle", + "anstyle-parse 1.0.0", "anstyle-query", "anstyle-wincon", "colorchoice", @@ -53,6 +68,15 @@ dependencies = [ "utf8parse", ] +[[package]] +name = "anstyle-parse" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e" +dependencies = [ + "utf8parse", +] + [[package]] name = "anstyle-query" version = "1.1.5" @@ -246,7 +270,7 @@ version = "4.5.57" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7b12c8b680195a62a8364d16b8447b01b6c2c8f9aaf68bee653be34d4245e238" dependencies = [ - "anstream", + "anstream 0.6.21", "anstyle", "clap_lex", "strsim", @@ -603,11 +627,11 @@ dependencies = [ [[package]] name = "env_logger" -version = "0.11.9" +version = "0.11.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2daee4ea451f429a58296525ddf28b45a3b64f1acf6587e2067437bb11e218d" +checksum = "0621c04f2196ac3f488dd583365b9c09be011a4ab8b9f37248ffcc8f6198b56a" dependencies = [ - "anstream", + "anstream 1.0.0", "anstyle", "env_filter", "jiff", @@ -1671,9 +1695,9 @@ checksum = "92ecc6618181def0457392ccd0ee51198e065e016d1d527a7ac1b6dc7c1f09d2" [[package]] name = "jiff" -version = "0.2.20" +version = "0.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c867c356cc096b33f4981825ab281ecba3db0acefe60329f044c1789d94c6543" +checksum = "1a3546dc96b6d42c5f24902af9e2538e82e39ad350b0c766eb3fbf2d8f3d8359" dependencies = [ "jiff-static", "jiff-tzdb-platform", @@ -1686,9 +1710,9 @@ dependencies = [ [[package]] name = "jiff-static" -version = "0.2.20" +version = "0.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f7946b4325269738f270bb55b3c19ab5c5040525f83fd625259422a9d25d9be5" +checksum = "2a8c8b344124222efd714b73bb41f8b5120b27a7cc1c75593a6ff768d9d05aa4" dependencies = [ "proc-macro2", "quote", @@ -2192,7 +2216,7 @@ dependencies = [ "clap", "clap-verbosity-flag", "drcp-format", - "env_logger 0.11.9", + "env_logger 0.11.10", "escargot", "flate2", "fzn-rs", diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 1dffb647a..86ba643a9 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -1,13 +1,14 @@ use pumpkin_core::containers::HashMap; -use pumpkin_core::containers::HashSet; use pumpkin_core::containers::KeyedVec; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateType; use pumpkin_core::variables::DomainId; +#[derive(Debug, Clone, Default)] pub(crate) struct IterativeMinimiser { domains: KeyedVec, + replacement_with_equals: bool, } #[derive(Debug, Clone, Copy)] @@ -46,7 +47,7 @@ impl Default for IterativeDomain { } impl IterativeDomain { - pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { + pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) { match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() > self.lower_bound { @@ -84,13 +85,21 @@ impl IterativeDomain { ); } PredicateType::Equal => { - self.upper_bound = predicate.get_right_hand_side(); + if replacement { + if self.lower_bound == predicate.get_right_hand_side() { + let _ = self.lower_bound_updates.pop(); + } else if self.upper_bound == predicate.get_right_hand_side() { + let _ = self.upper_bound_updates.pop(); + } + } + + self.lower_bound_updates + .push(predicate.get_right_hand_side()); self.upper_bound_updates .push(predicate.get_right_hand_side()); + self.upper_bound = predicate.get_right_hand_side(); self.lower_bound = predicate.get_right_hand_side(); - self.lower_bound_updates - .push(predicate.get_right_hand_side()); } } } @@ -101,23 +110,61 @@ impl IterativeDomain { let position = self .lower_bound_updates .iter() - .rev() .position(|value| *value == predicate.get_right_hand_side()) .expect("Expected removed lower-bound to be present"); let _ = self.lower_bound_updates.remove(position); self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + + if self + .holes + .get(&predicate.get_right_hand_side()) + .map(|(lb_updated, _)| *lb_updated) + .unwrap_or_default() + { + if let Some(position) = self + .lower_bound_updates + .iter() + .position(|value| *value == predicate.get_right_hand_side() + 1) + { + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = + self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + } + } } PredicateType::UpperBound => { let position = self .upper_bound_updates .iter() - .rev() .position(|value| *value == predicate.get_right_hand_side()) - .expect("Expected removed lower-bound to be present"); + .unwrap_or_else(|| { + panic!( + "Expected removed upper-bound {} to be present\n{:?}", + predicate.get_right_hand_side(), + self.upper_bound_updates + ) + }); let _ = self.upper_bound_updates.remove(position); - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); + + if self + .holes + .get(&predicate.get_right_hand_side()) + .map(|(_, ub_updated)| *ub_updated) + .unwrap_or_default() + { + if let Some(position) = self + .upper_bound_updates + .iter() + .position(|value| *value == predicate.get_right_hand_side() - 1) + { + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = + self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); + } + } } PredicateType::NotEqual => { let (lb_caused_update, ub_caused_update) = self @@ -126,51 +173,61 @@ impl IterativeDomain { .expect("Expected removed not equals to be present"); if *lb_caused_update { - let position = self + if let Some(position) = self .lower_bound_updates .iter() - .rev() .position(|value| *value == predicate.get_right_hand_side() + 1) - .expect("Expected removed lower-bound to be present"); - - let _ = self.lower_bound_updates.remove(position); - self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + { + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = + self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + } } if *ub_caused_update { - let position = self + if let Some(position) = self .upper_bound_updates .iter() - .rev() .position(|value| *value == predicate.get_right_hand_side() - 1) - .expect("Expected removed lower-bound to be present"); - - let _ = self.upper_bound_updates.remove(position); - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + { + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = + self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); + } } } PredicateType::Equal => { assert_eq!(self.lower_bound, self.upper_bound); assert_eq!(self.lower_bound, predicate.get_right_hand_side()); - let _ = self.lower_bound_updates.pop(); - let _ = self.upper_bound_updates.pop(); + self.lower_bound_updates.pop(); + self.upper_bound_updates.pop(); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MIN); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); } } } } impl IterativeMinimiser { + pub(crate) fn did_not_replace(&mut self) { + self.replacement_with_equals = false; + } + pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { let domain = predicate.get_domain(); self.domains[domain].remove_predicate(predicate); } - pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { + pub(crate) fn apply_predicate(&mut self, predicate: Predicate) -> bool { + println!( + "\t\tApplying ({}) {predicate:?}", + self.replacement_with_equals + ); let domain = predicate.get_domain(); - self.domains[domain].apply_predicate(predicate); + self.domains.accomodate(domain, IterativeDomain::default()); + self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); } pub(crate) fn process_predicate(&mut self, predicate: Predicate) -> ProcessingResult { @@ -180,6 +237,8 @@ impl IterativeMinimiser { let lower_bound = self.domains[domain].lower_bound; let upper_bound = self.domains[domain].upper_bound; + // println!("TEST: {predicate:?} - {:?}", self.domains[domain]); + if lower_bound == upper_bound { return ProcessingResult::Redundant; } @@ -187,49 +246,60 @@ impl IterativeMinimiser { match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() == upper_bound { - return ProcessingResult::ReplacedWithNew { + self.replacement_with_equals = true; + ProcessingResult::ReplacedWithNew { previous: predicate!(domain <= upper_bound), new_predicate: predicate!(domain == upper_bound), - }; + } } else if predicate.get_right_hand_side() > lower_bound { - return ProcessingResult::ReplacedPresent { - removed: predicate!(domain >= lower_bound), - }; + if lower_bound != i32::MIN { + ProcessingResult::ReplacedPresent { + removed: predicate!(domain >= lower_bound), + } + } else { + ProcessingResult::NotRedundant + } } else { - return ProcessingResult::Redundant; + ProcessingResult::Redundant } } PredicateType::UpperBound => { if predicate.get_right_hand_side() == lower_bound { - return ProcessingResult::ReplacedWithNew { + self.replacement_with_equals = true; + ProcessingResult::ReplacedWithNew { previous: predicate!(domain >= lower_bound), new_predicate: predicate!(domain == lower_bound), - }; + } } else if predicate.get_right_hand_side() < upper_bound { - return ProcessingResult::ReplacedPresent { - removed: predicate!(domain <= upper_bound), - }; + if upper_bound != i32::MAX { + ProcessingResult::ReplacedPresent { + removed: predicate!(domain <= upper_bound), + } + } else { + ProcessingResult::NotRedundant + } } else { - return ProcessingResult::Redundant; + ProcessingResult::Redundant } } PredicateType::NotEqual => { if predicate.get_right_hand_side() == upper_bound { - return ProcessingResult::ReplacedWithNew { + ProcessingResult::ReplacedWithNew { previous: predicate!(domain <= upper_bound), new_predicate: predicate!(domain <= upper_bound - 1), - }; + } } else if predicate.get_right_hand_side() > upper_bound { - return ProcessingResult::Redundant; + // println!("REACHED: {predicate:?} - {upper_bound}"); + ProcessingResult::Redundant } else if predicate.get_right_hand_side() == lower_bound { - return ProcessingResult::ReplacedWithNew { + ProcessingResult::ReplacedWithNew { previous: predicate!(domain >= lower_bound), new_predicate: predicate!(domain >= lower_bound + 1), - }; + } } else if predicate.get_right_hand_side() < lower_bound { - return ProcessingResult::Redundant; + ProcessingResult::Redundant } else { - return ProcessingResult::NotRedundant; + ProcessingResult::NotRedundant } } PredicateType::Equal => ProcessingResult::NotRedundant, diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 6c10d343f..86b5638a3 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -7,11 +7,9 @@ use pumpkin_core::conflict_resolving::ConflictResolver; use pumpkin_core::containers::KeyValueHeap; use pumpkin_core::containers::StorageKey; use pumpkin_core::create_statistics_struct; -use pumpkin_core::predicate; use pumpkin_core::predicates::Lbd; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateIdGenerator; -use pumpkin_core::predicates::PredicateType; use pumpkin_core::propagation::PredicateId; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::state::CurrentNogood; @@ -20,7 +18,9 @@ use pumpkin_core::statistics::StatisticLogger; use pumpkin_core::statistics::moving_averages::CumulativeMovingAverage; use pumpkin_core::statistics::moving_averages::MovingAverage; +use crate::minimisers::IterativeMinimiser; use crate::minimisers::NogoodMinimiser; +use crate::minimisers::ProcessingResult; use crate::minimisers::RecursiveMinimiser; use crate::minimisers::SemanticMinimisationMode; use crate::minimisers::SemanticMinimiser; @@ -69,6 +69,8 @@ pub struct ResolutionResolver { should_minimise: bool, iterative_minimisation: bool, + + iterative_minimiser: IterativeMinimiser, } impl Default for ResolutionResolver { @@ -93,14 +95,7 @@ create_statistics_struct!( iterative_minimisation_statistics: IterativeMinimisationStatistics }); -create_statistics_struct!(IterativeMinimisationStatistics { - num_removed: usize, - num_replaced_with_new_current_dl: usize, - num_replaced_with_new_previous_dl: usize, - - num_removed_previous_dl: usize, - num_removed_current_dl: usize, -}); +create_statistics_struct!(IterativeMinimisationStatistics { num_removed: usize }); #[derive(Debug, Clone, Copy, Default)] /// Determines which type of learning is performed by the [`ResolutionResolver`]. @@ -161,6 +156,7 @@ impl ResolutionResolver { statistics: Default::default(), should_minimise, iterative_minimisation, + iterative_minimiser: Default::default(), } } @@ -169,6 +165,8 @@ impl ResolutionResolver { let conflict_nogood = context.get_conflict_nogood(); + println!("C: {conflict_nogood:?}"); + // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { self.add_predicate_to_conflict_nogood(*predicate, self.mode, context); @@ -198,11 +196,27 @@ impl ResolutionResolver { AnalysisMode::AllDecision => self.to_process_heap.num_nonremoved_elements() > 0, } } { + println!( + "WORKING NOGOOD: {:?}", + self.processed_nogood_predicates + .iter() + .copied() + .chain( + self.to_process_heap + .keys() + .map(|id| self.predicate_id_generator.get_predicate(id)) + ) + .collect::>() + ); // Replace the predicate from the nogood that has been assigned last on the trail. // // This is done in two steps: // 1) Pop the predicate last assigned on the trail from the nogood. let next_predicate = self.pop_predicate_from_conflict_nogood(); + if self.iterative_minimisation { + println!("Removing {next_predicate:?}"); + self.iterative_minimiser.remove_predicate(next_predicate); + } // 2) Get the reason for the predicate and add it to the nogood. self.reason_buffer.clear(); @@ -217,6 +231,8 @@ impl ResolutionResolver { &mut self.reason_buffer, ); + println!("R: {:?} -> {next_predicate}", self.reason_buffer); + for i in 0..self.reason_buffer.len() { self.add_predicate_to_conflict_nogood(self.reason_buffer[i], self.mode, context); } @@ -230,6 +246,11 @@ impl ResolutionResolver { self.processed_nogood_predicates.clear(); self.predicate_id_generator.clear(); self.to_process_heap.clear(); + + // TODO: make more efficient + if self.iterative_minimisation { + self.iterative_minimiser = IterativeMinimiser::default() + } } /// Add the predicate to the current conflict nogood if we know it needs to be added. @@ -253,6 +274,8 @@ impl ResolutionResolver { }); // Ignore root level predicates. if dec_level == 0 { + println!("{predicate:?} ROOT LEVEL"); + self.iterative_minimiser.apply_predicate(predicate); context.explain_root_assignment(predicate); } // 1UIP @@ -262,220 +285,295 @@ impl ResolutionResolver { // All-decision Learning // If the variables are not decisions then we want to potentially add them to the heap, // otherwise we add it to the decision predicates which have been discovered previously - else if match mode { - AnalysisMode::OneUIP => dec_level == context.get_checkpoint(), - AnalysisMode::AllDecision => !context.is_decision_predicate(predicate), - } { + else { let predicate_id = self.predicate_id_generator.get_id(predicate); - // The first time we encounter the predicate, we initialise its value in the - // heap. - // - // Note that if the predicate is already in the heap, no action needs to be - // taken. It can happen that a predicate is returned - // multiple times as a reason for other predicates. - - // TODO: could improve the heap structure to be more user-friendly. - - // Here we manually adjust the size of the heap to accommodate new elements. - while self.to_process_heap.len() <= predicate_id.index() { - let next_id = PredicateId::create_from_index(self.to_process_heap.len()); - self.to_process_heap.grow(next_id, 0); - self.to_process_heap.delete_key(next_id); + if self.iterative_minimisation { + if let ControlFlow::Break(_) = + self.check_for_iterative_redundancy(predicate, context, predicate_id) + { + return; + } } + if match mode { + AnalysisMode::OneUIP => dec_level == context.get_checkpoint(), + AnalysisMode::AllDecision => !context.is_decision_predicate(predicate), + } { + // The first time we encounter the predicate, we initialise its value in the + // heap. + // + // Note that if the predicate is already in the heap, no action needs to be + // taken. It can happen that a predicate is returned + // multiple times as a reason for other predicates. - if self.iterative_minimisation - || (!self.to_process_heap.is_key_present(predicate_id) - && *self.to_process_heap.get_value(predicate_id) == 0) - { - context.predicate_appeared_in_conflict(predicate); + // TODO: could improve the heap structure to be more user-friendly. - if self.iterative_minimisation { - self.to_process_heap.set_value(predicate_id, 0); - self.to_process_heap.delete_key(predicate_id); + // Here we manually adjust the size of the heap to accommodate new elements. + while self.to_process_heap.len() <= predicate_id.index() { + let next_id = PredicateId::create_from_index(self.to_process_heap.len()); + self.to_process_heap.grow(next_id, 0); + self.to_process_heap.delete_key(next_id); } - if self.iterative_minimisation { - if let ControlFlow::Break(_) = - self.check_redundancy_previous_level(predicate, context) - { - return; - } - if let ControlFlow::Break(_) = - self.check_redundancy_current_level(predicate, context) - { - return; - } + if self.iterative_minimisation + || (!self.to_process_heap.is_key_present(predicate_id) + && *self.to_process_heap.get_value(predicate_id) == 0) + { + context.predicate_appeared_in_conflict(predicate); + + // The goal is to traverse predicate in reverse order of the trail. + // + // However some predicates may share the trail position. For example, if a + // predicate that was posted to trail resulted in + // some other predicates being true, then all + // these predicates would have the same trail position. + // + // When considering the predicates in reverse order of the trail, the + // implicitly set predicates are posted after the + // explicitly set one, but they all have the same + // trail position. + // + // To remedy this, we make a tie-breaking scheme to prioritise implied + // predicates over explicit predicates. This is done + // by assigning explicitly set predicates the + // value `2 * trail_position`, whereas implied predicates get `2 * + // trail_position + 1`. + let heap_value = get_heap_value(predicate, context); + + // We restore the key and since we know that the value is 0, we can safely + // increment with `heap_value` + self.to_process_heap.restore_key(predicate_id); + self.to_process_heap.set_value(predicate_id, heap_value); + + pumpkin_assert_simple!( + *self.to_process_heap.get_value(predicate_id) == heap_value, + "The value in the heap should be the same as was added" + ); } - - // The goal is to traverse predicate in reverse order of the trail. - // - // However some predicates may share the trail position. For example, if a - // predicate that was posted to trail resulted in - // some other predicates being true, then all - // these predicates would have the same trail position. - // - // When considering the predicates in reverse order of the trail, the - // implicitly set predicates are posted after the - // explicitly set one, but they all have the same - // trail position. - // - // To remedy this, we make a tie-breaking scheme to prioritise implied - // predicates over explicit predicates. This is done - // by assigning explicitly set predicates the - // value `2 * trail_position`, whereas implied predicates get `2 * - // trail_position + 1`. - let heap_value = get_heap_value(predicate, context); - - // We restore the key and since we know that the value is 0, we can safely - // increment with `heap_value` - self.to_process_heap.restore_key(predicate_id); - self.to_process_heap.set_value(predicate_id, heap_value); - - pumpkin_assert_simple!( - *self.to_process_heap.get_value(predicate_id) == heap_value, - "The value in the heap should be the same as was added" - ); + } else { + // We do not check for duplicate, we simply add the predicate. + // Semantic minimisation will later remove duplicates and do other processing. + self.processed_nogood_predicates.push(predicate); } - } else { - // We do not check for duplicate, we simply add the predicate. - // Semantic minimisation will later remove duplicates and do other processing. - self.processed_nogood_predicates.push(predicate); } } - fn check_redundancy_current_level( + fn check_for_iterative_redundancy( &mut self, predicate: Predicate, context: &mut ConflictAnalysisContext<'_>, + predicate_id: PredicateId, ) -> ControlFlow<()> { - for element in self - .to_process_heap - .keys() - .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) - .filter(|element| { - element.get_domain() == predicate.get_domain() - && context.get_state().trail_position(*element) - != context.get_state().trail_position(predicate) - }) - .collect::>() - { - match (element.get_predicate_type(), predicate.get_predicate_type()) { - (PredicateType::Equal, PredicateType::NotEqual) - | (PredicateType::Equal, PredicateType::UpperBound) - | (PredicateType::Equal, PredicateType::LowerBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - return ControlFlow::Break(()); - } - (PredicateType::UpperBound, PredicateType::UpperBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - if element.get_right_hand_side() <= predicate.get_right_hand_side() { - return ControlFlow::Break(()); - } else { - let element_id = self.predicate_id_generator.get_id(element); - self.to_process_heap.delete_key(element_id); + let process_predicate = self.iterative_minimiser.process_predicate(predicate); + println!("\tRESULT ({predicate:?}): {process_predicate:?}"); + match process_predicate { + ProcessingResult::Redundant => { + if !self.to_process_heap.is_key_present(predicate_id) { + println!("\t\tNot present - {predicate:?}"); + if predicate_id.index() < self.to_process_heap.len() { + self.to_process_heap.set_value(predicate_id, 0); } + self.to_process_heap.delete_key(predicate_id); } - (PredicateType::UpperBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_current_dl += 1; - let domain = element.get_domain(); - - let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); - self.replace_if_possible_current_level(context, element, new_predicate)?; - } else if element.get_right_hand_side() < predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - return ControlFlow::Break(()); + + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + return ControlFlow::Break(()); + } + ProcessingResult::ReplacedPresent { removed } => { + self.iterative_minimiser.remove_predicate(removed); + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + + let removed_id = self.predicate_id_generator.get_id(removed); + if self.to_process_heap.is_key_present(removed_id) { + self.to_process_heap.delete_key(removed_id); + } else { + if let Some(position) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == removed) + { + let _ = self.processed_nogood_predicates.remove(position); } } - (PredicateType::LowerBound, PredicateType::LowerBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - if element.get_right_hand_side() >= predicate.get_right_hand_side() { + self.iterative_minimiser.apply_predicate(predicate); + } + ProcessingResult::ReplacedWithNew { + previous, + new_predicate, + } => { + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + + if context.get_checkpoint_for_predicate(new_predicate).unwrap() + == context.get_checkpoint() + { + if let ControlFlow::Break(_) = + self.replace_if_possible_current_level(context, previous, new_predicate) + { + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); return ControlFlow::Break(()); } else { - let element_id = self.predicate_id_generator.get_id(element); - self.to_process_heap.delete_key(element_id); + self.iterative_minimiser.did_not_replace(); + self.iterative_minimiser.apply_predicate(predicate); } - } - (PredicateType::LowerBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_current_dl += 1; - let domain = element.get_domain(); - - let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); - self.replace_if_possible_current_level(context, element, new_predicate)?; - } else if element.get_right_hand_side() > predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; + } else { + if let ControlFlow::Break(_) = + self.replace_if_possible_previous_level(context, previous, new_predicate) + { + self.to_process_heap.set_value(predicate_id, 0); + self.to_process_heap.delete_key(predicate_id); return ControlFlow::Break(()); + } else { + self.iterative_minimiser.did_not_replace(); + self.iterative_minimiser.apply_predicate(predicate); } } - (PredicateType::UpperBound, PredicateType::LowerBound) - if element.get_right_hand_side() == predicate.get_right_hand_side() => - { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_current_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_current_dl += 1; - let domain = element.get_domain(); - - let new_predicate = predicate!(domain == element.get_right_hand_side()); - self.replace_if_possible_current_level(context, element, new_predicate)?; - } - - _ => {} + } + ProcessingResult::NotRedundant => { + self.iterative_minimiser.apply_predicate(predicate); } } ControlFlow::Continue(()) } + // fn check_redundancy_current_level( + // &mut self, + // predicate: Predicate, + // context: &mut ConflictAnalysisContext<'_>, + // ) -> ControlFlow<()> { + // for element in self + // .to_process_heap + // .keys() + // .map(|predicate_id| self.predicate_id_generator.get_predicate(predicate_id)) + // .filter(|element| { + // element.get_domain() == predicate.get_domain() + // && context.get_state().trail_position(*element) + // != context.get_state().trail_position(predicate) + // }) + // .collect::>() + // { + // match (element.get_predicate_type(), predicate.get_predicate_type()) { + // (PredicateType::Equal, PredicateType::NotEqual) + // | (PredicateType::Equal, PredicateType::UpperBound) + // | (PredicateType::Equal, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // return ControlFlow::Break(()); + // } + // (PredicateType::UpperBound, PredicateType::UpperBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // if element.get_right_hand_side() <= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // let element_id = self.predicate_id_generator.get_id(element); + // self.to_process_heap.delete_key(element_id); + // } + // } + // (PredicateType::UpperBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain <= element.get_right_hand_side() - + // 1); self.replace_if_possible_current_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() < + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::LowerBound, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // if element.get_right_hand_side() >= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // let element_id = self.predicate_id_generator.get_id(element); + // self.to_process_heap.delete_key(element_id); + // } + // } + // (PredicateType::LowerBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain >= element.get_right_hand_side() + + // 1); self.replace_if_possible_current_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() > + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::UpperBound, PredicateType::LowerBound) + // if element.get_right_hand_side() == predicate.get_right_hand_side() => + // { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_current_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_current_dl += 1; + // let domain = element.get_domain(); + // + // let new_predicate = predicate!(domain == element.get_right_hand_side()); + // self.replace_if_possible_current_level(context, element, new_predicate)?; + // } + // + // _ => {} + // } + // } + // ControlFlow::Continue(()) + // } + fn replace_if_possible_current_level( &mut self, context: &mut ConflictAnalysisContext<'_>, @@ -501,145 +599,145 @@ impl ResolutionResolver { ControlFlow::Continue(()) } - fn check_redundancy_previous_level( - &mut self, - predicate: Predicate, - context: &mut ConflictAnalysisContext<'_>, - ) -> ControlFlow<()> { - for element in self - .processed_nogood_predicates - .iter() - .filter(|element| { - element.get_domain() == predicate.get_domain() - && context.get_state().trail_position(**element) - != context.get_state().trail_position(predicate) - }) - .copied() - .collect::>() - { - match (element.get_predicate_type(), predicate.get_predicate_type()) { - (PredicateType::Equal, PredicateType::NotEqual) - | (PredicateType::Equal, PredicateType::UpperBound) - | (PredicateType::Equal, PredicateType::LowerBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - return ControlFlow::Break(()); - } - (PredicateType::UpperBound, PredicateType::UpperBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - if element.get_right_hand_side() <= predicate.get_right_hand_side() { - return ControlFlow::Break(()); - } else { - if let Some(index) = self - .processed_nogood_predicates - .iter() - .position(|predicate| *predicate == element) - { - let _ = self.processed_nogood_predicates.remove(index); - } - } - } - (PredicateType::UpperBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_previous_dl += 1; - - let domain = element.get_domain(); - let new_predicate = predicate!(domain <= element.get_right_hand_side() - 1); - self.replace_if_possible_previous_level(context, element, new_predicate)?; - } else if element.get_right_hand_side() < predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - return ControlFlow::Break(()); - } - } - (PredicateType::LowerBound, PredicateType::LowerBound) => { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - if element.get_right_hand_side() >= predicate.get_right_hand_side() { - return ControlFlow::Break(()); - } else { - if let Some(index) = self - .processed_nogood_predicates - .iter() - .position(|predicate| *predicate == element) - { - let _ = self.processed_nogood_predicates.remove(index); - } - } - } - (PredicateType::LowerBound, PredicateType::NotEqual) => { - if element.get_right_hand_side() == predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_previous_dl += 1; - - let domain = element.get_domain(); - let new_predicate = predicate!(domain >= element.get_right_hand_side() + 1); - self.replace_if_possible_previous_level(context, element, new_predicate)?; - } else if element.get_right_hand_side() > predicate.get_right_hand_side() { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - return ControlFlow::Break(()); - } - } - (PredicateType::UpperBound, PredicateType::LowerBound) - if element.get_right_hand_side() == predicate.get_right_hand_side() => - { - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - self.statistics - .iterative_minimisation_statistics - .num_removed_previous_dl += 1; - self.statistics - .iterative_minimisation_statistics - .num_replaced_with_new_previous_dl += 1; - - let domain = element.get_domain(); - let new_predicate = predicate!(domain == element.get_right_hand_side()); - self.replace_if_possible_previous_level(context, element, new_predicate)?; - } - - _ => {} - } - } - ControlFlow::Continue(()) - } + // fn check_redundancy_previous_level( + // &mut self, + // predicate: Predicate, + // context: &mut ConflictAnalysisContext<'_>, + // ) -> ControlFlow<()> { + // for element in self + // .processed_nogood_predicates + // .iter() + // .filter(|element| { + // element.get_domain() == predicate.get_domain() + // && context.get_state().trail_position(**element) + // != context.get_state().trail_position(predicate) + // }) + // .copied() + // .collect::>() + // { + // match (element.get_predicate_type(), predicate.get_predicate_type()) { + // (PredicateType::Equal, PredicateType::NotEqual) + // | (PredicateType::Equal, PredicateType::UpperBound) + // | (PredicateType::Equal, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // (PredicateType::UpperBound, PredicateType::UpperBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // if element.get_right_hand_side() <= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // if let Some(index) = self + // .processed_nogood_predicates + // .iter() + // .position(|predicate| *predicate == element) + // { + // let _ = self.processed_nogood_predicates.remove(index); + // } + // } + // } + // (PredicateType::UpperBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain <= element.get_right_hand_side() - + // 1); self.replace_if_possible_previous_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() < + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::LowerBound, PredicateType::LowerBound) => { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // if element.get_right_hand_side() >= predicate.get_right_hand_side() { + // return ControlFlow::Break(()); + // } else { + // if let Some(index) = self + // .processed_nogood_predicates + // .iter() + // .position(|predicate| *predicate == element) + // { + // let _ = self.processed_nogood_predicates.remove(index); + // } + // } + // } + // (PredicateType::LowerBound, PredicateType::NotEqual) => { + // if element.get_right_hand_side() == predicate.get_right_hand_side() { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain >= element.get_right_hand_side() + + // 1); self.replace_if_possible_previous_level(context, element, + // new_predicate)?; } else if element.get_right_hand_side() > + // predicate.get_right_hand_side() { self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // return ControlFlow::Break(()); + // } + // } + // (PredicateType::UpperBound, PredicateType::LowerBound) + // if element.get_right_hand_side() == predicate.get_right_hand_side() => + // { + // self.statistics + // .iterative_minimisation_statistics + // .num_removed += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_removed_previous_dl += 1; + // self.statistics + // .iterative_minimisation_statistics + // .num_replaced_with_new_previous_dl += 1; + // + // let domain = element.get_domain(); + // let new_predicate = predicate!(domain == element.get_right_hand_side()); + // self.replace_if_possible_previous_level(context, element, new_predicate)?; + // } + // + // _ => {} + // } + // } + // ControlFlow::Continue(()) + // } fn replace_if_possible_previous_level( &mut self, @@ -683,6 +781,18 @@ impl ResolutionResolver { // First we obtain a semantically minimised nogood. // // We reuse the vector with lower decision levels for simplicity. + println!( + "FINAL NOGOOD: {:?}", + self.processed_nogood_predicates + .iter() + .copied() + .chain( + self.to_process_heap + .keys() + .map(|id| self.predicate_id_generator.get_predicate(id)) + ) + .collect::>() + ); if self.to_process_heap.num_nonremoved_elements() > 0 { let last_predicate = self.pop_predicate_from_conflict_nogood(); self.processed_nogood_predicates.push(last_predicate); diff --git a/pumpkin-crates/core/src/containers/key_value_heap.rs b/pumpkin-crates/core/src/containers/key_value_heap.rs index 4c1a49d44..490d50c29 100644 --- a/pumpkin-crates/core/src/containers/key_value_heap.rs +++ b/pumpkin-crates/core/src/containers/key_value_heap.rs @@ -124,12 +124,14 @@ where } pub fn set_value(&mut self, key: Key, value: Value) { - let position = self.map_key_to_position[key]; - self.values[position] = value; - // Recall that increment may be applied to keys not present - // So we only apply sift up in case the key is present - if self.is_key_present(key) { - self.sift_up(position); + if key.index() < self.len() { + let position = self.map_key_to_position[key]; + self.values[position] = value; + // Recall that increment may be applied to keys not present + // So we only apply sift up in case the key is present + if self.is_key_present(key) { + self.sift_up(position); + } } } diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 78f3e7fdf..4841ef3a6 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -162,8 +162,6 @@ pub struct SatisfactionSolverOptions { pub learning_options: LearningOptions, /// The number of MBs which are preallocated by the nogood propagator. pub memory_preallocated: usize, - /// Whether semantic minimisation is applied during conflict analysis. - pub iterative_minimisation: bool, } impl Default for SatisfactionSolverOptions { @@ -175,7 +173,6 @@ impl Default for SatisfactionSolverOptions { proof_log: ProofLog::default(), learning_options: LearningOptions::default(), memory_preallocated: 50, - iterative_minimisation: false, } } } diff --git a/pumpkin-solver/src/bin/pumpkin-solver/main.rs b/pumpkin-solver/src/bin/pumpkin-solver/main.rs index 6b25be69c..ae2ae6308 100644 --- a/pumpkin-solver/src/bin/pumpkin-solver/main.rs +++ b/pumpkin-solver/src/bin/pumpkin-solver/main.rs @@ -584,7 +584,6 @@ fn run() -> PumpkinResult<()> { random_generator: SmallRng::seed_from_u64(args.random_seed), proof_log, learning_options, - iterative_minimisation: args.iterative_minimisation, }; let time_limit = args.time_limit.map(Duration::from_millis); @@ -643,7 +642,7 @@ fn run() -> PumpkinResult<()> { ResolutionResolver::new( AnalysisMode::OneUIP, !args.no_learning_clause_minimisation, - args.iterative_minimisation, + !args.iterative_minimisation, ), )?, }, diff --git a/pumpkin-solver/tests/helpers/mod.rs b/pumpkin-solver/tests/helpers/mod.rs index cff79aa31..3bbe80569 100644 --- a/pumpkin-solver/tests/helpers/mod.rs +++ b/pumpkin-solver/tests/helpers/mod.rs @@ -97,7 +97,10 @@ pub(crate) fn run_solver_with_options( match child.wait_timeout(TEST_TIMEOUT) { Ok(None) => panic!("solver took more than {} seconds", TEST_TIMEOUT.as_secs()), Ok(Some(status)) if status.success() => {} - Ok(Some(e)) => panic!("error solving instance {e}"), + Ok(Some(e)) => panic!( + "error solving instance {e}\n{:?}", + std::fs::read_to_string(err_file_path) + ), Err(e) => panic!("error starting solver: {e}"), } From ec13f556f4b410c4f97d4846d514b26a5c36d0a7 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 09:52:51 +0200 Subject: [PATCH 31/43] fix: logging root-level deductions when inferring redundancy --- .../src/minimisers/iterative_minimiser.rs | 60 +++++++++++++++-- .../src/resolvers/resolution_resolver.rs | 67 ++++++++++--------- 2 files changed, 88 insertions(+), 39 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 86ba643a9..21dab1af1 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -1,8 +1,10 @@ +use pumpkin_core::conflict_resolving::ConflictAnalysisContext; use pumpkin_core::containers::HashMap; use pumpkin_core::containers::KeyedVec; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateType; +use pumpkin_core::propagation::ReadDomains; use pumpkin_core::variables::DomainId; #[derive(Debug, Clone, Default)] @@ -47,7 +49,10 @@ impl Default for IterativeDomain { } impl IterativeDomain { - pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) { + pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) -> bool { + let prev_lb = self.lower_bound; + let prev_ub = self.upper_bound; + match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() > self.lower_bound { @@ -102,6 +107,8 @@ impl IterativeDomain { self.lower_bound = predicate.get_right_hand_side(); } } + + prev_lb != prev_ub && self.lower_bound == self.upper_bound } pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { @@ -221,31 +228,49 @@ impl IterativeMinimiser { } pub(crate) fn apply_predicate(&mut self, predicate: Predicate) -> bool { - println!( - "\t\tApplying ({}) {predicate:?}", - self.replacement_with_equals - ); + // println!( + // "\t\tApplying ({}) {predicate:?}", + // self.replacement_with_equals + // ); let domain = predicate.get_domain(); self.domains.accomodate(domain, IterativeDomain::default()); - self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); + self.domains[domain].apply_predicate(predicate, self.replacement_with_equals) } - pub(crate) fn process_predicate(&mut self, predicate: Predicate) -> ProcessingResult { + pub(crate) fn process_predicate( + &mut self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) -> ProcessingResult { let domain = predicate.get_domain(); self.domains.accomodate(domain, IterativeDomain::default()); let lower_bound = self.domains[domain].lower_bound; let upper_bound = self.domains[domain].upper_bound; + let lower_bound_is_initial_bound = + context.is_initial_bound(predicate!(domain >= lower_bound)); + let upper_bound_is_initial_bound = + context.is_initial_bound(predicate!(domain <= upper_bound)); + // println!("TEST: {predicate:?} - {:?}", self.domains[domain]); if lower_bound == upper_bound { + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } return ProcessingResult::Redundant; } match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() == upper_bound { + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } self.replacement_with_equals = true; ProcessingResult::ReplacedWithNew { previous: predicate!(domain <= upper_bound), @@ -260,11 +285,17 @@ impl IterativeMinimiser { ProcessingResult::NotRedundant } } else { + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } ProcessingResult::Redundant } } PredicateType::UpperBound => { if predicate.get_right_hand_side() == lower_bound { + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } self.replacement_with_equals = true; ProcessingResult::ReplacedWithNew { previous: predicate!(domain >= lower_bound), @@ -279,24 +310,39 @@ impl IterativeMinimiser { ProcessingResult::NotRedundant } } else { + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } ProcessingResult::Redundant } } PredicateType::NotEqual => { if predicate.get_right_hand_side() == upper_bound { + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } ProcessingResult::ReplacedWithNew { previous: predicate!(domain <= upper_bound), new_predicate: predicate!(domain <= upper_bound - 1), } } else if predicate.get_right_hand_side() > upper_bound { // println!("REACHED: {predicate:?} - {upper_bound}"); + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } ProcessingResult::Redundant } else if predicate.get_right_hand_side() == lower_bound { + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } ProcessingResult::ReplacedWithNew { previous: predicate!(domain >= lower_bound), new_predicate: predicate!(domain >= lower_bound + 1), } } else if predicate.get_right_hand_side() < lower_bound { + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } ProcessingResult::Redundant } else { ProcessingResult::NotRedundant diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 86b5638a3..65a9f233c 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -165,7 +165,7 @@ impl ResolutionResolver { let conflict_nogood = context.get_conflict_nogood(); - println!("C: {conflict_nogood:?}"); + // println!("C: {conflict_nogood:?}"); // Initialise the data structures with the conflict nogood. for predicate in conflict_nogood.iter() { @@ -196,25 +196,25 @@ impl ResolutionResolver { AnalysisMode::AllDecision => self.to_process_heap.num_nonremoved_elements() > 0, } } { - println!( - "WORKING NOGOOD: {:?}", - self.processed_nogood_predicates - .iter() - .copied() - .chain( - self.to_process_heap - .keys() - .map(|id| self.predicate_id_generator.get_predicate(id)) - ) - .collect::>() - ); + // println!( + // "WORKING NOGOOD: {:?}", + // self.processed_nogood_predicates + // .iter() + // .copied() + // .chain( + // self.to_process_heap + // .keys() + // .map(|id| self.predicate_id_generator.get_predicate(id)) + // ) + // .collect::>() + // ); // Replace the predicate from the nogood that has been assigned last on the trail. // // This is done in two steps: // 1) Pop the predicate last assigned on the trail from the nogood. let next_predicate = self.pop_predicate_from_conflict_nogood(); if self.iterative_minimisation { - println!("Removing {next_predicate:?}"); + // println!("Removing {next_predicate:?}"); self.iterative_minimiser.remove_predicate(next_predicate); } @@ -231,7 +231,7 @@ impl ResolutionResolver { &mut self.reason_buffer, ); - println!("R: {:?} -> {next_predicate}", self.reason_buffer); + // println!("R: {:?} -> {next_predicate}", self.reason_buffer); for i in 0..self.reason_buffer.len() { self.add_predicate_to_conflict_nogood(self.reason_buffer[i], self.mode, context); @@ -274,8 +274,9 @@ impl ResolutionResolver { }); // Ignore root level predicates. if dec_level == 0 { - println!("{predicate:?} ROOT LEVEL"); - self.iterative_minimiser.apply_predicate(predicate); + // println!("{predicate:?} ROOT LEVEL"); + let _ = self.iterative_minimiser.apply_predicate(predicate); + context.explain_root_assignment(predicate); } // 1UIP @@ -363,12 +364,14 @@ impl ResolutionResolver { context: &mut ConflictAnalysisContext<'_>, predicate_id: PredicateId, ) -> ControlFlow<()> { - let process_predicate = self.iterative_minimiser.process_predicate(predicate); - println!("\tRESULT ({predicate:?}): {process_predicate:?}"); + let process_predicate = self + .iterative_minimiser + .process_predicate(predicate, context); + // println!("\tRESULT ({predicate:?}): {process_predicate:?}"); match process_predicate { ProcessingResult::Redundant => { if !self.to_process_heap.is_key_present(predicate_id) { - println!("\t\tNot present - {predicate:?}"); + // println!("\t\tNot present - {predicate:?}"); if predicate_id.index() < self.to_process_heap.len() { self.to_process_heap.set_value(predicate_id, 0); } @@ -781,18 +784,18 @@ impl ResolutionResolver { // First we obtain a semantically minimised nogood. // // We reuse the vector with lower decision levels for simplicity. - println!( - "FINAL NOGOOD: {:?}", - self.processed_nogood_predicates - .iter() - .copied() - .chain( - self.to_process_heap - .keys() - .map(|id| self.predicate_id_generator.get_predicate(id)) - ) - .collect::>() - ); + // println!( + // "FINAL NOGOOD: {:?}", + // self.processed_nogood_predicates + // .iter() + // .copied() + // .chain( + // self.to_process_heap + // .keys() + // .map(|id| self.predicate_id_generator.get_predicate(id)) + // ) + // .collect::>() + // ); if self.to_process_heap.num_nonremoved_elements() > 0 { let last_predicate = self.pop_predicate_from_conflict_nogood(); self.processed_nogood_predicates.push(last_predicate); From 787449b487a6dc0dcf1dee87e546482d75c24e6c Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 11:11:03 +0200 Subject: [PATCH 32/43] fix: logging more root-level inferences + remove predicate from iterative minimiser when when replaced --- pumpkin-crates/checking/src/variable_state.rs | 8 +++++--- .../src/minimisers/iterative_minimiser.rs | 17 +++++++++++------ .../src/resolvers/resolution_resolver.rs | 6 ++++++ 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/pumpkin-crates/checking/src/variable_state.rs b/pumpkin-crates/checking/src/variable_state.rs index 07cb1d253..ab75d02d0 100644 --- a/pumpkin-crates/checking/src/variable_state.rs +++ b/pumpkin-crates/checking/src/variable_state.rs @@ -308,9 +308,11 @@ impl Domain { self.upper_bound = IntExt::Int(bound); - // Note the '+ 1' to keep the elements <= the upper bound instead of < - // the upper bound. - let _ = self.holes.split_off(&(bound + 1)); + if bound < i32::MAX { + // Note the '+ 1' to keep the elements <= the upper bound instead of < + // the upper bound. + let _ = self.holes.split_off(&(bound + 1)); + } // Take care of the condition where the new bound is already a hole in the domain. if self.holes.contains(&bound) { diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 21dab1af1..ed2a57a98 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -252,16 +252,21 @@ impl IterativeMinimiser { context.is_initial_bound(predicate!(domain >= lower_bound)); let upper_bound_is_initial_bound = context.is_initial_bound(predicate!(domain <= upper_bound)); + if lower_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } + if upper_bound_is_initial_bound { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } + for hole in self.domains[domain].holes.keys() { + if context.get_checkpoint_for_predicate(predicate!(domain != *hole)) == Some(0) { + context.explain_root_assignment(predicate!(domain != *hole)); + } + } // println!("TEST: {predicate:?} - {:?}", self.domains[domain]); if lower_bound == upper_bound { - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } return ProcessingResult::Redundant; } diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 65a9f233c..bfe59ccda 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -165,6 +165,7 @@ impl ResolutionResolver { let conflict_nogood = context.get_conflict_nogood(); + // println!("======================================================================"); // println!("C: {conflict_nogood:?}"); // Initialise the data structures with the conflict nogood. @@ -595,6 +596,8 @@ impl ResolutionResolver { let element_id = self.predicate_id_generator.get_id(element); self.to_process_heap.delete_key(element_id); + // println!("Removing previous: {element:?}"); + self.iterative_minimiser.remove_predicate(element); self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); return ControlFlow::Break(()); @@ -765,6 +768,9 @@ impl ResolutionResolver { let _ = self.processed_nogood_predicates.remove(index); } + // println!("Removing previous: {element:?}"); + self.iterative_minimiser.remove_predicate(element); + self.add_predicate_to_conflict_nogood(new_predicate, self.mode, context); return ControlFlow::Break(()); From ac03d342573723d21e4538ef3bce4c568dce7392 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 11:19:00 +0200 Subject: [PATCH 33/43] chore: clippy warnings --- .../src/minimisers/iterative_minimiser.rs | 64 ++++++++----------- .../src/resolvers/resolution_resolver.rs | 11 ++-- 2 files changed, 31 insertions(+), 44 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index ed2a57a98..ea3c07813 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -49,10 +49,7 @@ impl Default for IterativeDomain { } impl IterativeDomain { - pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) -> bool { - let prev_lb = self.lower_bound; - let prev_ub = self.upper_bound; - + pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) { match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() > self.lower_bound { @@ -107,8 +104,6 @@ impl IterativeDomain { self.lower_bound = predicate.get_right_hand_side(); } } - - prev_lb != prev_ub && self.lower_bound == self.upper_bound } pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { @@ -128,16 +123,13 @@ impl IterativeDomain { .get(&predicate.get_right_hand_side()) .map(|(lb_updated, _)| *lb_updated) .unwrap_or_default() - { - if let Some(position) = self + && let Some(position) = self .lower_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() + 1) - { - let _ = self.lower_bound_updates.remove(position); - self.lower_bound = - self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - } + { + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); } } PredicateType::UpperBound => { @@ -161,16 +153,13 @@ impl IterativeDomain { .get(&predicate.get_right_hand_side()) .map(|(_, ub_updated)| *ub_updated) .unwrap_or_default() - { - if let Some(position) = self + && let Some(position) = self .upper_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() - 1) - { - let _ = self.upper_bound_updates.remove(position); - self.upper_bound = - self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - } + { + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); } } PredicateType::NotEqual => { @@ -179,36 +168,35 @@ impl IterativeDomain { .get(&predicate.get_right_hand_side()) .expect("Expected removed not equals to be present"); - if *lb_caused_update { - if let Some(position) = self + if *lb_caused_update + && let Some(position) = self .lower_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() + 1) - { - let _ = self.lower_bound_updates.remove(position); - self.lower_bound = - self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - } + { + let _ = self.lower_bound_updates.remove(position); + self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); } - if *ub_caused_update { - if let Some(position) = self + if *ub_caused_update + && let Some(position) = self .upper_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() - 1) - { - let _ = self.upper_bound_updates.remove(position); - self.upper_bound = - self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - } + { + let _ = self.upper_bound_updates.remove(position); + self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); } } PredicateType::Equal => { assert_eq!(self.lower_bound, self.upper_bound); assert_eq!(self.lower_bound, predicate.get_right_hand_side()); - self.lower_bound_updates.pop(); - self.upper_bound_updates.pop(); + let popped_lb = self.lower_bound_updates.pop(); + assert_eq!(popped_lb, Some(predicate.get_right_hand_side())); + + let popped_ub = self.upper_bound_updates.pop(); + assert_eq!(popped_ub, Some(predicate.get_right_hand_side())); self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); @@ -227,14 +215,14 @@ impl IterativeMinimiser { self.domains[domain].remove_predicate(predicate); } - pub(crate) fn apply_predicate(&mut self, predicate: Predicate) -> bool { + pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { // println!( // "\t\tApplying ({}) {predicate:?}", // self.replacement_with_equals // ); let domain = predicate.get_domain(); self.domains.accomodate(domain, IterativeDomain::default()); - self.domains[domain].apply_predicate(predicate, self.replacement_with_equals) + self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); } pub(crate) fn process_predicate( diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index bfe59ccda..684971756 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -276,7 +276,7 @@ impl ResolutionResolver { // Ignore root level predicates. if dec_level == 0 { // println!("{predicate:?} ROOT LEVEL"); - let _ = self.iterative_minimiser.apply_predicate(predicate); + self.iterative_minimiser.apply_predicate(predicate); context.explain_root_assignment(predicate); } @@ -289,12 +289,11 @@ impl ResolutionResolver { // otherwise we add it to the decision predicates which have been discovered previously else { let predicate_id = self.predicate_id_generator.get_id(predicate); - if self.iterative_minimisation { - if let ControlFlow::Break(_) = + if self.iterative_minimisation + && let ControlFlow::Break(_) = self.check_for_iterative_redundancy(predicate, context, predicate_id) - { - return; - } + { + return; } if match mode { AnalysisMode::OneUIP => dec_level == context.get_checkpoint(), From 479b5e43f4db63cf1745255153bdb7a6f356e269 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 12:14:22 +0200 Subject: [PATCH 34/43] chore: clippy warnings duplicate crate --- clippy.toml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/clippy.toml b/clippy.toml index db93913b0..b66be827f 100644 --- a/clippy.toml +++ b/clippy.toml @@ -4,4 +4,6 @@ allowed-duplicate-crates = [ "windows-sys", "regex-syntax", "regex-automata", + "anstream", + "anstyle-parse" ] From 7de5ba3a7a96f74c1ac0147758e3c1a07e800370 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 13:18:13 +0200 Subject: [PATCH 35/43] docs: adding documentation --- .../src/minimisers/iterative_minimiser.rs | 134 +++++++++++++++--- .../src/resolvers/resolution_resolver.rs | 4 +- 2 files changed, 118 insertions(+), 20 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index ea3c07813..8f806ebb0 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -13,26 +13,50 @@ pub(crate) struct IterativeMinimiser { replacement_with_equals: bool, } +/// The result of processing a predicate, indicating its redundancy. #[derive(Debug, Clone, Copy)] pub(crate) enum ProcessingResult { + /// The predicate to process was redundant. Redundant, - ReplacedPresent { + /// The predicate to process was not redundant, and it replaced + /// [`ProcessingResult::ReplacedPresent::removed`]. + /// + /// e.g., [x >= 5] can replace [x >= 2]. + ReplacedPresent { removed: Predicate }, + /// The predicate to process was replaced with + /// [`ProcessingResult::PossiblyReplacedWithNew::new_predicate`] and it also removed + /// [`ProcessingResult::PossiblyReplacedWithNew::removed`]. + /// + /// Note that it is not always possible to replace with `new_predicate` (since it can lead to + /// infinite loops), so it is not guaranteed that `new_predicate` is added. + /// + /// e.g., if [x >= 5] is in the nogood, and the predicate [x <= 5] is added, then [x >= 5] is + /// removed and replaced with [x == 5] (and [x <= 5] is not added). + PossiblyReplacedWithNew { removed: Predicate, - }, - ReplacedWithNew { - previous: Predicate, new_predicate: Predicate, }, + /// The predicate was found to be not redundant. NotRedundant, } +/// A concise domain representation used by the [`IterativeMinimiser`]. +/// +/// Note that this does not contain elements which are part of the intial domain, but only part of +/// the nogood. #[derive(Debug, Clone)] struct IterativeDomain { + /// The updates that have occurred to the lower-bound. lower_bound_updates: Vec, + /// The updates that have occurred to the upper-bound. upper_bound_updates: Vec, + /// A mapping of a hole in the domain to whether it caused a lower-bound or upper-bound update + /// respectively. holes: HashMap, + /// An easy way to access the lower-bound. lower_bound: i32, + /// An easy way to access the upper-bound. upper_bound: i32, } @@ -49,9 +73,15 @@ impl Default for IterativeDomain { } impl IterativeDomain { + /// Applies the given predicate to the state. + /// + /// If `replacement` is true, then it indicates that this predicate was added due to a + /// [`ProcessingResult::PossiblyReplacedWithNew`] event. This influences how the updates to the + /// bounds are processed. pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) { match predicate.get_predicate_type() { PredicateType::LowerBound => { + // We update the lower-bound if it larger. if predicate.get_right_hand_side() > self.lower_bound { self.lower_bound = predicate.get_right_hand_side(); self.lower_bound_updates @@ -59,6 +89,7 @@ impl IterativeDomain { } } PredicateType::UpperBound => { + // We update the upper-bound if it is smaller. if predicate.get_right_hand_side() < self.upper_bound { self.upper_bound = predicate.get_right_hand_side(); self.upper_bound_updates @@ -68,12 +99,22 @@ impl IterativeDomain { PredicateType::NotEqual => { let mut lb_caused_update = false; let mut ub_caused_update = false; + + // We update the lower-bound if it coincides with the right-hand side of the not + // equals predicate. + // + // TODO: Could move bound based on other holes? if predicate.get_right_hand_side() == self.lower_bound { lb_caused_update = true; self.lower_bound = predicate.get_right_hand_side() + 1; self.lower_bound_updates .push(predicate.get_right_hand_side() + 1); } + + // We update the upper-bound if it coincides with the right-hand side of the not + // equals predicate. + // + // TODO: Could move bound based on other holes? if predicate.get_right_hand_side() == self.upper_bound { ub_caused_update = true; self.upper_bound = predicate.get_right_hand_side() - 1; @@ -81,34 +122,43 @@ impl IterativeDomain { .push(predicate.get_right_hand_side() - 1); } + // We also insert it into the existing holes let _ = self.holes.insert( predicate.get_right_hand_side(), (lb_caused_update, ub_caused_update), ); } PredicateType::Equal => { + // We pop the previous bound if this equality predicate is a replacement of a + // previous predicate. if replacement { if self.lower_bound == predicate.get_right_hand_side() { - let _ = self.lower_bound_updates.pop(); + let lb_u = self.lower_bound_updates.pop(); + assert_eq!(lb_u, Some(predicate.get_right_hand_side())); } else if self.upper_bound == predicate.get_right_hand_side() { - let _ = self.upper_bound_updates.pop(); + let ub_u = self.upper_bound_updates.pop(); + assert_eq!(ub_u, Some(predicate.get_right_hand_side())); } } + // We push fresh bound variables due to this predicate. self.lower_bound_updates .push(predicate.get_right_hand_side()); self.upper_bound_updates .push(predicate.get_right_hand_side()); + // And update the lower- and upper-bound. self.upper_bound = predicate.get_right_hand_side(); self.lower_bound = predicate.get_right_hand_side(); } } } + /// Removes the provided predicate from the domain. pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { match predicate.get_predicate_type() { PredicateType::LowerBound => { + // We find the update corresponding to the predicate and remove it. let position = self .lower_bound_updates .iter() @@ -116,23 +166,35 @@ impl IterativeDomain { .expect("Expected removed lower-bound to be present"); let _ = self.lower_bound_updates.remove(position); + + // We update the lower-bound to its value or the minimum possible lower-bound. self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + // Now we need to check whether the lower-bound was caused by an update of a hole. + // + // If this is the case, then we need to revert the lower-bound to its value before + // it was applied. if self .holes .get(&predicate.get_right_hand_side()) .map(|(lb_updated, _)| *lb_updated) .unwrap_or_default() + // There is a hole which has the same rhs as the removed predicate, and it was responsible for updating the lower-bound. && let Some(position) = self .lower_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() + 1) + // There exists a lower-bound update which represents the update due to the + // predicate and a hole in the domain. { + // We remove the lower-bound which is now not true anymore. let _ = self.lower_bound_updates.remove(position); + // And update the lower-bound. self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); } } PredicateType::UpperBound => { + // We find the update corresponding to the predicate and remove it. let position = self .upper_bound_updates .iter() @@ -144,21 +206,31 @@ impl IterativeDomain { self.upper_bound_updates ) }); - let _ = self.upper_bound_updates.remove(position); + + // We update the lower-bound to its value or the minimum possible lower-bound. self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); + // Now we need to check whether the upper-bound was caused by an update of a hole. + // + // If this is the case, then we need to revert the upper-bound to its value before + // it was applied. if self .holes .get(&predicate.get_right_hand_side()) .map(|(_, ub_updated)| *ub_updated) .unwrap_or_default() + // There is a hole which has the same rhs as the removed predicate, and it was responsible for updating the lower-bound. && let Some(position) = self .upper_bound_updates .iter() .position(|value| *value == predicate.get_right_hand_side() - 1) + // There exists a lower-bound update which represents the update due to the + // predicate and a hole in the domain. { + // We remove the upper-bound which is now not true anymore. let _ = self.upper_bound_updates.remove(position); + // And update the upper-bound self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); } } @@ -168,6 +240,7 @@ impl IterativeDomain { .get(&predicate.get_right_hand_side()) .expect("Expected removed not equals to be present"); + // We remove the updated lower-bound if it is present if *lb_caused_update && let Some(position) = self .lower_bound_updates @@ -178,6 +251,7 @@ impl IterativeDomain { self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); } + // We remove the updated upper-bound if it is present if *ub_caused_update && let Some(position) = self .upper_bound_updates @@ -189,6 +263,7 @@ impl IterativeDomain { } } PredicateType::Equal => { + // We remove the last update and reset the bounds assert_eq!(self.lower_bound, self.upper_bound); assert_eq!(self.lower_bound, predicate.get_right_hand_side()); @@ -206,15 +281,20 @@ impl IterativeDomain { } impl IterativeMinimiser { + /// The [`IterativeMinimiser`] indicated (via [`ProcessingResult::PossiblyReplacedWithNew`]) + /// that a new predicate could be inserted; this method indicates that acutally could not/did + /// not happen. pub(crate) fn did_not_replace(&mut self) { self.replacement_with_equals = false; } + /// Removes the given predicate from the nogood. pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { let domain = predicate.get_domain(); self.domains[domain].remove_predicate(predicate); } + /// Applies the given predicate from the nogood. pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { // println!( // "\t\tApplying ({}) {predicate:?}", @@ -225,6 +305,7 @@ impl IterativeMinimiser { self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); } + /// Processes the predicate, indicating via [`ProcessingResult`] what can happen to it. pub(crate) fn process_predicate( &mut self, predicate: Predicate, @@ -236,6 +317,10 @@ impl IterativeMinimiser { let lower_bound = self.domains[domain].lower_bound; let upper_bound = self.domains[domain].upper_bound; + // First, we log initial bounds which could be responsible for removing a predicate from + // the nogood. + // + // TODO: Should only log when relevant. let lower_bound_is_initial_bound = context.is_initial_bound(predicate!(domain >= lower_bound)); let upper_bound_is_initial_bound = @@ -252,8 +337,12 @@ impl IterativeMinimiser { } } - // println!("TEST: {predicate:?} - {:?}", self.domains[domain]); - + // If the domain is assigned, then the added predicate is redundant. + // + // Encompasses the rules: + // - [x = v], [x != v'] => [x = v] + // - [x = v], [x <= v'] => [x = v] + // - [x = v], [x >= v'] => [x = v] if lower_bound == upper_bound { return ProcessingResult::Redundant; } @@ -261,15 +350,17 @@ impl IterativeMinimiser { match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() == upper_bound { + // [x <= v], [x >= v] => [x = v] if upper_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain <= upper_bound)); } self.replacement_with_equals = true; - ProcessingResult::ReplacedWithNew { - previous: predicate!(domain <= upper_bound), + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain <= upper_bound), new_predicate: predicate!(domain == upper_bound), } } else if predicate.get_right_hand_side() > lower_bound { + // [x >= v], [x >= v'] => [x >= v'] if v' > v if lower_bound != i32::MIN { ProcessingResult::ReplacedPresent { removed: predicate!(domain >= lower_bound), @@ -278,6 +369,7 @@ impl IterativeMinimiser { ProcessingResult::NotRedundant } } else { + // [x >= v], [x >= v'] => [x >= v] if v > v' if lower_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain >= lower_bound)); } @@ -285,16 +377,18 @@ impl IterativeMinimiser { } } PredicateType::UpperBound => { + // [x >= v], [x <= v] => [x = v] if predicate.get_right_hand_side() == lower_bound { if lower_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain >= lower_bound)); } self.replacement_with_equals = true; - ProcessingResult::ReplacedWithNew { - previous: predicate!(domain >= lower_bound), + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain >= lower_bound), new_predicate: predicate!(domain == lower_bound), } } else if predicate.get_right_hand_side() < upper_bound { + // [x <= v], [x <= v'] => [x <= v'] if v' < v if upper_bound != i32::MAX { ProcessingResult::ReplacedPresent { removed: predicate!(domain <= upper_bound), @@ -303,6 +397,7 @@ impl IterativeMinimiser { ProcessingResult::NotRedundant } } else { + // [x <= v], [x <= v'] => [x <= v] if v < v' if upper_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain <= upper_bound)); } @@ -311,28 +406,31 @@ impl IterativeMinimiser { } PredicateType::NotEqual => { if predicate.get_right_hand_side() == upper_bound { + // [x <= v], [x != v] => [x <= v - 1] if upper_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain <= upper_bound)); } - ProcessingResult::ReplacedWithNew { - previous: predicate!(domain <= upper_bound), + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain <= upper_bound), new_predicate: predicate!(domain <= upper_bound - 1), } } else if predicate.get_right_hand_side() > upper_bound { - // println!("REACHED: {predicate:?} - {upper_bound}"); + // [x <= v], [x != v'] => [x <= v] where v' > v if upper_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain <= upper_bound)); } ProcessingResult::Redundant } else if predicate.get_right_hand_side() == lower_bound { + // [x >= v], [x != v] => [x <= v + 1] if lower_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain >= lower_bound)); } - ProcessingResult::ReplacedWithNew { - previous: predicate!(domain >= lower_bound), + ProcessingResult::PossiblyReplacedWithNew { + removed: predicate!(domain >= lower_bound), new_predicate: predicate!(domain >= lower_bound + 1), } } else if predicate.get_right_hand_side() < lower_bound { + // [x >= v], [x != v'] => [x >= v] where v' < v if lower_bound_is_initial_bound { context.explain_root_assignment(predicate!(domain >= lower_bound)); } diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index 684971756..dc122f1d9 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -403,8 +403,8 @@ impl ResolutionResolver { } self.iterative_minimiser.apply_predicate(predicate); } - ProcessingResult::ReplacedWithNew { - previous, + ProcessingResult::PossiblyReplacedWithNew { + removed: previous, new_predicate, } => { self.statistics From f95f12717ecbfd7725b76fa2913a2b4da0b1550f Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 13:37:27 +0200 Subject: [PATCH 36/43] fix: only log in proof when necessary --- .../src/minimisers/iterative_minimiser.rs | 105 ++++++++++-------- 1 file changed, 61 insertions(+), 44 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 8f806ebb0..0178a22e6 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -305,6 +305,57 @@ impl IterativeMinimiser { self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); } + /// Explains the lower-bound in the proof log. + fn explain_lower_bound_in_proof( + &self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) { + if context.is_proof_logging_inferences() { + let domain = predicate.get_domain(); + let mut lower_bound = self.domains[domain].lower_bound; + + if context.get_checkpoint_for_predicate(predicate!(domain >= lower_bound)) == Some(0) { + context.explain_root_assignment(predicate!(domain >= lower_bound)); + } + + while lower_bound != i32::MIN + && let Some((lb_updated, _)) = self.domains[domain].holes.get(&(lower_bound - 1)) + && *lb_updated + && context.get_checkpoint_for_predicate(predicate!(domain != lower_bound - 1)) + == Some(0) + { + lower_bound -= 1; + context.explain_root_assignment(predicate!(domain != lower_bound)); + } + } + } + + fn explain_upper_bound_in_proof( + &self, + predicate: Predicate, + context: &mut ConflictAnalysisContext, + ) { + if context.is_proof_logging_inferences() { + let domain = predicate.get_domain(); + let mut upper_bound = self.domains[domain].upper_bound; + + if context.get_checkpoint_for_predicate(predicate!(domain <= upper_bound)) == Some(0) { + context.explain_root_assignment(predicate!(domain <= upper_bound)); + } + + while upper_bound != i32::MAX + && let Some((_, ub_updated)) = self.domains[domain].holes.get(&(upper_bound + 1)) + && *ub_updated + && context.get_checkpoint_for_predicate(predicate!(domain != upper_bound + 1)) + == Some(0) + { + upper_bound += 1; + context.explain_root_assignment(predicate!(domain != upper_bound)); + } + } + } + /// Processes the predicate, indicating via [`ProcessingResult`] what can happen to it. pub(crate) fn process_predicate( &mut self, @@ -317,26 +368,6 @@ impl IterativeMinimiser { let lower_bound = self.domains[domain].lower_bound; let upper_bound = self.domains[domain].upper_bound; - // First, we log initial bounds which could be responsible for removing a predicate from - // the nogood. - // - // TODO: Should only log when relevant. - let lower_bound_is_initial_bound = - context.is_initial_bound(predicate!(domain >= lower_bound)); - let upper_bound_is_initial_bound = - context.is_initial_bound(predicate!(domain <= upper_bound)); - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } - for hole in self.domains[domain].holes.keys() { - if context.get_checkpoint_for_predicate(predicate!(domain != *hole)) == Some(0) { - context.explain_root_assignment(predicate!(domain != *hole)); - } - } - // If the domain is assigned, then the added predicate is redundant. // // Encompasses the rules: @@ -344,16 +375,16 @@ impl IterativeMinimiser { // - [x = v], [x <= v'] => [x = v] // - [x = v], [x >= v'] => [x = v] if lower_bound == upper_bound { + self.explain_lower_bound_in_proof(predicate, context); + self.explain_upper_bound_in_proof(predicate, context); return ProcessingResult::Redundant; } match predicate.get_predicate_type() { PredicateType::LowerBound => { if predicate.get_right_hand_side() == upper_bound { + self.explain_upper_bound_in_proof(predicate, context); // [x <= v], [x >= v] => [x = v] - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } self.replacement_with_equals = true; ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain <= upper_bound), @@ -370,18 +401,14 @@ impl IterativeMinimiser { } } else { // [x >= v], [x >= v'] => [x >= v] if v > v' - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } + self.explain_lower_bound_in_proof(predicate, context); ProcessingResult::Redundant } } PredicateType::UpperBound => { // [x >= v], [x <= v] => [x = v] if predicate.get_right_hand_side() == lower_bound { - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } + self.explain_lower_bound_in_proof(predicate, context); self.replacement_with_equals = true; ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain >= lower_bound), @@ -398,42 +425,32 @@ impl IterativeMinimiser { } } else { // [x <= v], [x <= v'] => [x <= v] if v < v' - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } + self.explain_upper_bound_in_proof(predicate, context); ProcessingResult::Redundant } } PredicateType::NotEqual => { if predicate.get_right_hand_side() == upper_bound { // [x <= v], [x != v] => [x <= v - 1] - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } + self.explain_upper_bound_in_proof(predicate, context); ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain <= upper_bound), new_predicate: predicate!(domain <= upper_bound - 1), } } else if predicate.get_right_hand_side() > upper_bound { // [x <= v], [x != v'] => [x <= v] where v' > v - if upper_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain <= upper_bound)); - } + self.explain_upper_bound_in_proof(predicate, context); ProcessingResult::Redundant } else if predicate.get_right_hand_side() == lower_bound { // [x >= v], [x != v] => [x <= v + 1] - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } + self.explain_lower_bound_in_proof(predicate, context); ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain >= lower_bound), new_predicate: predicate!(domain >= lower_bound + 1), } } else if predicate.get_right_hand_side() < lower_bound { // [x >= v], [x != v'] => [x >= v] where v' < v - if lower_bound_is_initial_bound { - context.explain_root_assignment(predicate!(domain >= lower_bound)); - } + self.explain_lower_bound_in_proof(predicate, context); ProcessingResult::Redundant } else { ProcessingResult::NotRedundant From 607659deea8efa0e74bcce7eaf611a257d70f11a Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 13:50:38 +0200 Subject: [PATCH 37/43] chore: remove unnecessary logging of unset parameters --- .../src/minimisers/iterative_minimiser.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 0178a22e6..044b94f4f 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -314,6 +314,9 @@ impl IterativeMinimiser { if context.is_proof_logging_inferences() { let domain = predicate.get_domain(); let mut lower_bound = self.domains[domain].lower_bound; + if lower_bound == i32::MIN { + return; + } if context.get_checkpoint_for_predicate(predicate!(domain >= lower_bound)) == Some(0) { context.explain_root_assignment(predicate!(domain >= lower_bound)); @@ -339,6 +342,9 @@ impl IterativeMinimiser { if context.is_proof_logging_inferences() { let domain = predicate.get_domain(); let mut upper_bound = self.domains[domain].upper_bound; + if upper_bound == i32::MAX { + return; + } if context.get_checkpoint_for_predicate(predicate!(domain <= upper_bound)) == Some(0) { context.explain_root_assignment(predicate!(domain <= upper_bound)); From 61f2253d74f5fbf39fc86c125b5b1858c4a14826 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Wed, 1 Apr 2026 14:14:58 +0200 Subject: [PATCH 38/43] fix: hole update after removing lower or upper-bound --- .../src/minimisers/iterative_minimiser.rs | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 044b94f4f..899437cee 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -191,6 +191,12 @@ impl IterativeDomain { let _ = self.lower_bound_updates.remove(position); // And update the lower-bound. self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); + // Then we also set the update of the lb to be false again. + self.holes + .get_mut(&predicate.get_right_hand_side()) + .as_mut() + .unwrap() + .0 = false; } } PredicateType::UpperBound => { @@ -232,16 +238,22 @@ impl IterativeDomain { let _ = self.upper_bound_updates.remove(position); // And update the upper-bound self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); + // Then we also set the update of the ub to be false again. + self.holes + .get_mut(&predicate.get_right_hand_side()) + .as_mut() + .unwrap() + .1 = false; } } PredicateType::NotEqual => { let (lb_caused_update, ub_caused_update) = self .holes - .get(&predicate.get_right_hand_side()) + .remove(&predicate.get_right_hand_side()) .expect("Expected removed not equals to be present"); // We remove the updated lower-bound if it is present - if *lb_caused_update + if lb_caused_update && let Some(position) = self .lower_bound_updates .iter() @@ -252,7 +264,7 @@ impl IterativeDomain { } // We remove the updated upper-bound if it is present - if *ub_caused_update + if ub_caused_update && let Some(position) = self .upper_bound_updates .iter() From 081a5c79f2393b07e1bc9766c6a679c240ee169d Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 2 Apr 2026 08:06:33 +0200 Subject: [PATCH 39/43] docs: adding documentation to iterative minimiser --- .../src/minimisers/iterative_minimiser.rs | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 899437cee..b034a3212 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -7,9 +7,49 @@ use pumpkin_core::predicates::PredicateType; use pumpkin_core::propagation::ReadDomains; use pumpkin_core::variables::DomainId; +/// A minimiser which iteratively applies rewrite rules based on the semantic meaning of predicates +/// *during* conflict analysis. +/// +/// The implementation is heavily inspired by \[1\]. +/// +/// There are a couple of limitations to note: +/// - Currently, whenever a hole is created at a lower- or upper-bound, the bound is only moved by 1 +/// (even if there are multiple holes which could cause a higher lower-bound). This simplifies a +/// lot of the logic. +/// - Currently, it is unclear how the rules are applied in \[1\]. This means that certain rules are +/// invalid (for, as of yet, unknown reasons), for example, removing all other elements concerning +/// `x` when `[x = v]` is added leads to wrong solutions. +/// - This leads to another slightly nuanced point; which is that when an element is removed from +/// the nogood, it could be that there are other bounds which should be restored. +/// +/// For example, it could be that the nogood contains (among others) the predicates `[x >= v]` +/// and `[x = v + 1]`. In this case, once `[x = v + 1]` gets removed, the lower-bound should be +/// moved back to `v`. +/// +/// ## Developer Notes +/// - The predicates from the previous decision level should also be added to the +/// [`IterativeMinimiser`]; this is due to the fact that they are not guaranteed to be +/// semantically minimised away. +/// +/// Imagine the situation where we have `[x >= v]` from a previous +/// decision level and `[x >= v']` from the current decision level (where `v' > v`). If we then +/// do not process `[x >= v]`, then it would get added to the nogood directly rather than removed +/// due to redundancy. If we now resolve on [`x >= v'`] and the nogood becomes asserting, then +/// there are no other elements over `x` and the predicate from the previous decision level does +/// not get removed. +/// +/// # Bibliography +/// \[1\] T. Feydy, A. Schutt, and P. Stuckey, ‘Semantic learning for lazy clause generation’, in +/// TRICS workshop, held alongside CP, 2013. #[derive(Debug, Clone, Default)] pub(crate) struct IterativeMinimiser { + /// Keeps track of the domains induced by the current working nogood. domains: KeyedVec, + /// Used to keep track of situations where `[x <= v]` or `[x >= v]` gets replaced with `[x = + /// v]` due to the addition of `[x >= v]` or `[x <= v]`, respectively. + /// + /// This is used to make sure that the bounds stored in the [`IterativeDomain`] remain + /// consistent. replacement_with_equals: bool, } From 699c6afce29eedacfaa4b332b13f6f4e66b14b7f Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 2 Apr 2026 16:04:55 +0200 Subject: [PATCH 40/43] refactor: changing to variable state --- Cargo.lock | 1 + pumpkin-crates/checking/src/variable_state.rs | 4 + pumpkin-crates/conflict-resolvers/Cargo.toml | 1 + .../src/minimisers/iterative_minimiser.rs | 366 +++--------------- .../src/resolvers/resolution_resolver.rs | 2 - 5 files changed, 63 insertions(+), 311 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d25088877..cf31f1139 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2157,6 +2157,7 @@ dependencies = [ name = "pumpkin-conflict-resolvers" version = "0.3.0" dependencies = [ + "pumpkin-checking", "pumpkin-core", ] diff --git a/pumpkin-crates/checking/src/variable_state.rs b/pumpkin-crates/checking/src/variable_state.rs index ab75d02d0..9167b0ab9 100644 --- a/pumpkin-crates/checking/src/variable_state.rs +++ b/pumpkin-crates/checking/src/variable_state.rs @@ -31,6 +31,10 @@ impl VariableState where Atomic: AtomicConstraint, { + pub fn reset_domain(&mut self, identified: Atomic::Identifier) { + let _ = self.domains.insert(identified, Domain::all_integers()); + } + /// Create a variable state that applies all the premises and, if present, the negation of the /// consequent. /// diff --git a/pumpkin-crates/conflict-resolvers/Cargo.toml b/pumpkin-crates/conflict-resolvers/Cargo.toml index de3438062..0a8c57cc4 100644 --- a/pumpkin-crates/conflict-resolvers/Cargo.toml +++ b/pumpkin-crates/conflict-resolvers/Cargo.toml @@ -12,3 +12,4 @@ workspace = true [dependencies] pumpkin-core = { version = "0.3.0", path = "../core" } +pumpkin-checking = { version = "0.3.0", path = "../checking" } diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index b034a3212..0b7cc2863 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -1,5 +1,6 @@ +use pumpkin_checking::IntExt; +use pumpkin_checking::VariableState; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; -use pumpkin_core::containers::HashMap; use pumpkin_core::containers::KeyedVec; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; @@ -44,13 +45,8 @@ use pumpkin_core::variables::DomainId; #[derive(Debug, Clone, Default)] pub(crate) struct IterativeMinimiser { /// Keeps track of the domains induced by the current working nogood. - domains: KeyedVec, - /// Used to keep track of situations where `[x <= v]` or `[x >= v]` gets replaced with `[x = - /// v]` due to the addition of `[x >= v]` or `[x <= v]`, respectively. - /// - /// This is used to make sure that the bounds stored in the [`IterativeDomain`] remain - /// consistent. - replacement_with_equals: bool, + state: VariableState, + domains: KeyedVec>, } /// The result of processing a predicate, indicating its redundancy. @@ -80,281 +76,23 @@ pub(crate) enum ProcessingResult { NotRedundant, } -/// A concise domain representation used by the [`IterativeMinimiser`]. -/// -/// Note that this does not contain elements which are part of the intial domain, but only part of -/// the nogood. -#[derive(Debug, Clone)] -struct IterativeDomain { - /// The updates that have occurred to the lower-bound. - lower_bound_updates: Vec, - /// The updates that have occurred to the upper-bound. - upper_bound_updates: Vec, - /// A mapping of a hole in the domain to whether it caused a lower-bound or upper-bound update - /// respectively. - holes: HashMap, - - /// An easy way to access the lower-bound. - lower_bound: i32, - /// An easy way to access the upper-bound. - upper_bound: i32, -} - -impl Default for IterativeDomain { - fn default() -> Self { - Self { - lower_bound_updates: Default::default(), - upper_bound_updates: Default::default(), - holes: Default::default(), - lower_bound: i32::MIN, - upper_bound: i32::MAX, - } - } -} - -impl IterativeDomain { - /// Applies the given predicate to the state. - /// - /// If `replacement` is true, then it indicates that this predicate was added due to a - /// [`ProcessingResult::PossiblyReplacedWithNew`] event. This influences how the updates to the - /// bounds are processed. - pub(crate) fn apply_predicate(&mut self, predicate: Predicate, replacement: bool) { - match predicate.get_predicate_type() { - PredicateType::LowerBound => { - // We update the lower-bound if it larger. - if predicate.get_right_hand_side() > self.lower_bound { - self.lower_bound = predicate.get_right_hand_side(); - self.lower_bound_updates - .push(predicate.get_right_hand_side()); - } - } - PredicateType::UpperBound => { - // We update the upper-bound if it is smaller. - if predicate.get_right_hand_side() < self.upper_bound { - self.upper_bound = predicate.get_right_hand_side(); - self.upper_bound_updates - .push(predicate.get_right_hand_side()); - } - } - PredicateType::NotEqual => { - let mut lb_caused_update = false; - let mut ub_caused_update = false; - - // We update the lower-bound if it coincides with the right-hand side of the not - // equals predicate. - // - // TODO: Could move bound based on other holes? - if predicate.get_right_hand_side() == self.lower_bound { - lb_caused_update = true; - self.lower_bound = predicate.get_right_hand_side() + 1; - self.lower_bound_updates - .push(predicate.get_right_hand_side() + 1); - } - - // We update the upper-bound if it coincides with the right-hand side of the not - // equals predicate. - // - // TODO: Could move bound based on other holes? - if predicate.get_right_hand_side() == self.upper_bound { - ub_caused_update = true; - self.upper_bound = predicate.get_right_hand_side() - 1; - self.upper_bound_updates - .push(predicate.get_right_hand_side() - 1); - } - - // We also insert it into the existing holes - let _ = self.holes.insert( - predicate.get_right_hand_side(), - (lb_caused_update, ub_caused_update), - ); - } - PredicateType::Equal => { - // We pop the previous bound if this equality predicate is a replacement of a - // previous predicate. - if replacement { - if self.lower_bound == predicate.get_right_hand_side() { - let lb_u = self.lower_bound_updates.pop(); - assert_eq!(lb_u, Some(predicate.get_right_hand_side())); - } else if self.upper_bound == predicate.get_right_hand_side() { - let ub_u = self.upper_bound_updates.pop(); - assert_eq!(ub_u, Some(predicate.get_right_hand_side())); - } - } - - // We push fresh bound variables due to this predicate. - self.lower_bound_updates - .push(predicate.get_right_hand_side()); - self.upper_bound_updates - .push(predicate.get_right_hand_side()); - - // And update the lower- and upper-bound. - self.upper_bound = predicate.get_right_hand_side(); - self.lower_bound = predicate.get_right_hand_side(); - } - } - } - - /// Removes the provided predicate from the domain. - pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { - match predicate.get_predicate_type() { - PredicateType::LowerBound => { - // We find the update corresponding to the predicate and remove it. - let position = self - .lower_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side()) - .expect("Expected removed lower-bound to be present"); - - let _ = self.lower_bound_updates.remove(position); - - // We update the lower-bound to its value or the minimum possible lower-bound. - self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - - // Now we need to check whether the lower-bound was caused by an update of a hole. - // - // If this is the case, then we need to revert the lower-bound to its value before - // it was applied. - if self - .holes - .get(&predicate.get_right_hand_side()) - .map(|(lb_updated, _)| *lb_updated) - .unwrap_or_default() - // There is a hole which has the same rhs as the removed predicate, and it was responsible for updating the lower-bound. - && let Some(position) = self - .lower_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side() + 1) - // There exists a lower-bound update which represents the update due to the - // predicate and a hole in the domain. - { - // We remove the lower-bound which is now not true anymore. - let _ = self.lower_bound_updates.remove(position); - // And update the lower-bound. - self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - // Then we also set the update of the lb to be false again. - self.holes - .get_mut(&predicate.get_right_hand_side()) - .as_mut() - .unwrap() - .0 = false; - } - } - PredicateType::UpperBound => { - // We find the update corresponding to the predicate and remove it. - let position = self - .upper_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side()) - .unwrap_or_else(|| { - panic!( - "Expected removed upper-bound {} to be present\n{:?}", - predicate.get_right_hand_side(), - self.upper_bound_updates - ) - }); - let _ = self.upper_bound_updates.remove(position); - - // We update the lower-bound to its value or the minimum possible lower-bound. - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - - // Now we need to check whether the upper-bound was caused by an update of a hole. - // - // If this is the case, then we need to revert the upper-bound to its value before - // it was applied. - if self - .holes - .get(&predicate.get_right_hand_side()) - .map(|(_, ub_updated)| *ub_updated) - .unwrap_or_default() - // There is a hole which has the same rhs as the removed predicate, and it was responsible for updating the lower-bound. - && let Some(position) = self - .upper_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side() - 1) - // There exists a lower-bound update which represents the update due to the - // predicate and a hole in the domain. - { - // We remove the upper-bound which is now not true anymore. - let _ = self.upper_bound_updates.remove(position); - // And update the upper-bound - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - // Then we also set the update of the ub to be false again. - self.holes - .get_mut(&predicate.get_right_hand_side()) - .as_mut() - .unwrap() - .1 = false; - } - } - PredicateType::NotEqual => { - let (lb_caused_update, ub_caused_update) = self - .holes - .remove(&predicate.get_right_hand_side()) - .expect("Expected removed not equals to be present"); - - // We remove the updated lower-bound if it is present - if lb_caused_update - && let Some(position) = self - .lower_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side() + 1) - { - let _ = self.lower_bound_updates.remove(position); - self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - } - - // We remove the updated upper-bound if it is present - if ub_caused_update - && let Some(position) = self - .upper_bound_updates - .iter() - .position(|value| *value == predicate.get_right_hand_side() - 1) - { - let _ = self.upper_bound_updates.remove(position); - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - } - } - PredicateType::Equal => { - // We remove the last update and reset the bounds - assert_eq!(self.lower_bound, self.upper_bound); - assert_eq!(self.lower_bound, predicate.get_right_hand_side()); - - let popped_lb = self.lower_bound_updates.pop(); - assert_eq!(popped_lb, Some(predicate.get_right_hand_side())); - - let popped_ub = self.upper_bound_updates.pop(); - assert_eq!(popped_ub, Some(predicate.get_right_hand_side())); - - self.lower_bound = self.lower_bound_updates.last().copied().unwrap_or(i32::MIN); - self.upper_bound = self.upper_bound_updates.last().copied().unwrap_or(i32::MAX); - } - } - } -} - impl IterativeMinimiser { - /// The [`IterativeMinimiser`] indicated (via [`ProcessingResult::PossiblyReplacedWithNew`]) - /// that a new predicate could be inserted; this method indicates that acutally could not/did - /// not happen. - pub(crate) fn did_not_replace(&mut self) { - self.replacement_with_equals = false; - } - /// Removes the given predicate from the nogood. pub(crate) fn remove_predicate(&mut self, predicate: Predicate) { let domain = predicate.get_domain(); - self.domains[domain].remove_predicate(predicate); + if let Some(to_remove_position) = self.domains[domain] + .iter() + .position(|element| *element == predicate) + { + let _ = self.domains[domain].remove(to_remove_position); + } } /// Applies the given predicate from the nogood. pub(crate) fn apply_predicate(&mut self, predicate: Predicate) { - // println!( - // "\t\tApplying ({}) {predicate:?}", - // self.replacement_with_equals - // ); let domain = predicate.get_domain(); - self.domains.accomodate(domain, IterativeDomain::default()); - self.domains[domain].apply_predicate(predicate, self.replacement_with_equals); + self.domains.accomodate(domain, Default::default()); + self.domains[domain].push(predicate) } /// Explains the lower-bound in the proof log. @@ -365,23 +103,18 @@ impl IterativeMinimiser { ) { if context.is_proof_logging_inferences() { let domain = predicate.get_domain(); - let mut lower_bound = self.domains[domain].lower_bound; - if lower_bound == i32::MIN { - return; - } - if context.get_checkpoint_for_predicate(predicate!(domain >= lower_bound)) == Some(0) { + if let IntExt::Int(lower_bound) = self.state.lower_bound(&domain) + && context.get_checkpoint_for_predicate(predicate!(domain >= lower_bound)) + == Some(0) + { context.explain_root_assignment(predicate!(domain >= lower_bound)); } - while lower_bound != i32::MIN - && let Some((lb_updated, _)) = self.domains[domain].holes.get(&(lower_bound - 1)) - && *lb_updated - && context.get_checkpoint_for_predicate(predicate!(domain != lower_bound - 1)) - == Some(0) - { - lower_bound -= 1; - context.explain_root_assignment(predicate!(domain != lower_bound)); + for hole in self.state.holes(&domain) { + if context.get_checkpoint_for_predicate(predicate!(domain != hole)) == Some(0) { + context.explain_root_assignment(predicate!(domain != hole)); + } } } } @@ -393,23 +126,18 @@ impl IterativeMinimiser { ) { if context.is_proof_logging_inferences() { let domain = predicate.get_domain(); - let mut upper_bound = self.domains[domain].upper_bound; - if upper_bound == i32::MAX { - return; - } - if context.get_checkpoint_for_predicate(predicate!(domain <= upper_bound)) == Some(0) { + if let IntExt::Int(upper_bound) = self.state.upper_bound(&domain) + && context.get_checkpoint_for_predicate(predicate!(domain <= upper_bound)) + == Some(0) + { context.explain_root_assignment(predicate!(domain <= upper_bound)); } - while upper_bound != i32::MAX - && let Some((_, ub_updated)) = self.domains[domain].holes.get(&(upper_bound + 1)) - && *ub_updated - && context.get_checkpoint_for_predicate(predicate!(domain != upper_bound + 1)) - == Some(0) - { - upper_bound += 1; - context.explain_root_assignment(predicate!(domain != upper_bound)); + for hole in self.state.holes(&domain) { + if context.get_checkpoint_for_predicate(predicate!(domain != hole)) == Some(0) { + context.explain_root_assignment(predicate!(domain != hole)); + } } } } @@ -421,10 +149,24 @@ impl IterativeMinimiser { context: &mut ConflictAnalysisContext, ) -> ProcessingResult { let domain = predicate.get_domain(); - self.domains.accomodate(domain, IterativeDomain::default()); + self.domains.accomodate(domain, Default::default()); + + self.state.reset_domain(domain); + for predicate in self.domains[predicate.get_domain()].iter() { + let consistent = self.state.apply(predicate); + assert!(consistent) + } - let lower_bound = self.domains[domain].lower_bound; - let upper_bound = self.domains[domain].upper_bound; + let lower_bound = self + .state + .lower_bound(&predicate.get_domain()) + .try_into() + .unwrap_or(i32::MIN); + let upper_bound = self + .state + .upper_bound(&predicate.get_domain()) + .try_into() + .unwrap_or(i32::MAX); // If the domain is assigned, then the added predicate is redundant. // @@ -443,16 +185,19 @@ impl IterativeMinimiser { if predicate.get_right_hand_side() == upper_bound { self.explain_upper_bound_in_proof(predicate, context); // [x <= v], [x >= v] => [x = v] - self.replacement_with_equals = true; ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain <= upper_bound), new_predicate: predicate!(domain == upper_bound), } } else if predicate.get_right_hand_side() > lower_bound { // [x >= v], [x >= v'] => [x >= v'] if v' > v - if lower_bound != i32::MIN { + if let Some(to_remove) = self.domains[predicate.get_domain()] + .iter() + .filter(|element| element.is_lower_bound_predicate()) + .max_by_key(|element| element.get_right_hand_side()) + { ProcessingResult::ReplacedPresent { - removed: predicate!(domain >= lower_bound), + removed: *to_remove, } } else { ProcessingResult::NotRedundant @@ -467,16 +212,19 @@ impl IterativeMinimiser { // [x >= v], [x <= v] => [x = v] if predicate.get_right_hand_side() == lower_bound { self.explain_lower_bound_in_proof(predicate, context); - self.replacement_with_equals = true; ProcessingResult::PossiblyReplacedWithNew { removed: predicate!(domain >= lower_bound), new_predicate: predicate!(domain == lower_bound), } } else if predicate.get_right_hand_side() < upper_bound { // [x <= v], [x <= v'] => [x <= v'] if v' < v - if upper_bound != i32::MAX { + if let Some(to_remove) = self.domains[predicate.get_domain()] + .iter() + .filter(|element| element.is_upper_bound_predicate()) + .min_by_key(|element| element.get_right_hand_side()) + { ProcessingResult::ReplacedPresent { - removed: predicate!(domain <= upper_bound), + removed: *to_remove, } } else { ProcessingResult::NotRedundant diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index dc122f1d9..ad7f63e62 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -421,7 +421,6 @@ impl ResolutionResolver { self.to_process_heap.delete_key(predicate_id); return ControlFlow::Break(()); } else { - self.iterative_minimiser.did_not_replace(); self.iterative_minimiser.apply_predicate(predicate); } } else { @@ -432,7 +431,6 @@ impl ResolutionResolver { self.to_process_heap.delete_key(predicate_id); return ControlFlow::Break(()); } else { - self.iterative_minimiser.did_not_replace(); self.iterative_minimiser.apply_predicate(predicate); } } From 0cc079b611fb9717e84d1a23b5d1a093150a8798 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 2 Apr 2026 16:09:20 +0200 Subject: [PATCH 41/43] refactor: allow removing of multiple elements at once --- .../src/minimisers/iterative_minimiser.rs | 27 ++++++++-------- .../src/resolvers/resolution_resolver.rs | 32 ++++++++++--------- 2 files changed, 30 insertions(+), 29 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 0b7cc2863..58c81dfd0 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -50,7 +50,7 @@ pub(crate) struct IterativeMinimiser { } /// The result of processing a predicate, indicating its redundancy. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone)] pub(crate) enum ProcessingResult { /// The predicate to process was redundant. Redundant, @@ -58,7 +58,7 @@ pub(crate) enum ProcessingResult { /// [`ProcessingResult::ReplacedPresent::removed`]. /// /// e.g., [x >= 5] can replace [x >= 2]. - ReplacedPresent { removed: Predicate }, + ReplacedPresent { removed: Vec }, /// The predicate to process was replaced with /// [`ProcessingResult::PossiblyReplacedWithNew::new_predicate`] and it also removed /// [`ProcessingResult::PossiblyReplacedWithNew::removed`]. @@ -191,14 +191,14 @@ impl IterativeMinimiser { } } else if predicate.get_right_hand_side() > lower_bound { // [x >= v], [x >= v'] => [x >= v'] if v' > v - if let Some(to_remove) = self.domains[predicate.get_domain()] + let to_remove = self.domains[predicate.get_domain()] .iter() .filter(|element| element.is_lower_bound_predicate()) - .max_by_key(|element| element.get_right_hand_side()) - { - ProcessingResult::ReplacedPresent { - removed: *to_remove, - } + .copied() + .collect::>(); + + if !to_remove.is_empty() { + ProcessingResult::ReplacedPresent { removed: to_remove } } else { ProcessingResult::NotRedundant } @@ -218,14 +218,13 @@ impl IterativeMinimiser { } } else if predicate.get_right_hand_side() < upper_bound { // [x <= v], [x <= v'] => [x <= v'] if v' < v - if let Some(to_remove) = self.domains[predicate.get_domain()] + let to_remove = self.domains[predicate.get_domain()] .iter() .filter(|element| element.is_upper_bound_predicate()) - .min_by_key(|element| element.get_right_hand_side()) - { - ProcessingResult::ReplacedPresent { - removed: *to_remove, - } + .copied() + .collect::>(); + if !to_remove.is_empty() { + ProcessingResult::ReplacedPresent { removed: to_remove } } else { ProcessingResult::NotRedundant } diff --git a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs index ad7f63e62..24b961312 100644 --- a/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs +++ b/pumpkin-crates/conflict-resolvers/src/resolvers/resolution_resolver.rs @@ -384,23 +384,25 @@ impl ResolutionResolver { return ControlFlow::Break(()); } ProcessingResult::ReplacedPresent { removed } => { - self.iterative_minimiser.remove_predicate(removed); - self.statistics - .iterative_minimisation_statistics - .num_removed += 1; - - let removed_id = self.predicate_id_generator.get_id(removed); - if self.to_process_heap.is_key_present(removed_id) { - self.to_process_heap.delete_key(removed_id); - } else { - if let Some(position) = self - .processed_nogood_predicates - .iter() - .position(|predicate| *predicate == removed) - { - let _ = self.processed_nogood_predicates.remove(position); + for removed_predicate in removed { + self.statistics + .iterative_minimisation_statistics + .num_removed += 1; + self.iterative_minimiser.remove_predicate(removed_predicate); + let removed_id = self.predicate_id_generator.get_id(removed_predicate); + if self.to_process_heap.is_key_present(removed_id) { + self.to_process_heap.delete_key(removed_id); + } else { + if let Some(position) = self + .processed_nogood_predicates + .iter() + .position(|predicate| *predicate == removed_predicate) + { + let _ = self.processed_nogood_predicates.remove(position); + } } } + self.iterative_minimiser.apply_predicate(predicate); } ProcessingResult::PossiblyReplacedWithNew { From 99c115043b7d252c515c668933845a46e72b6f54 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Thu, 2 Apr 2026 16:29:43 +0200 Subject: [PATCH 42/43] refactor: do not allocate or reset when unnecessary --- .../conflict-resolvers/src/minimisers/iterative_minimiser.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 58c81dfd0..82e6a7db4 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -2,6 +2,7 @@ use pumpkin_checking::IntExt; use pumpkin_checking::VariableState; use pumpkin_core::conflict_resolving::ConflictAnalysisContext; use pumpkin_core::containers::KeyedVec; +use pumpkin_core::containers::StorageKey; use pumpkin_core::predicate; use pumpkin_core::predicates::Predicate; use pumpkin_core::predicates::PredicateType; @@ -149,6 +150,9 @@ impl IterativeMinimiser { context: &mut ConflictAnalysisContext, ) -> ProcessingResult { let domain = predicate.get_domain(); + if domain.index() >= self.domains.len() || self.domains[domain].is_empty() { + return ProcessingResult::NotRedundant; + } self.domains.accomodate(domain, Default::default()); self.state.reset_domain(domain); From 606834cc24782eba061b458605cfca3952187753 Mon Sep 17 00:00:00 2001 From: Imko Marijnissen Date: Fri, 3 Apr 2026 10:59:37 +0200 Subject: [PATCH 43/43] refactor: also remove not equals when introducing lower-bound --- .../src/minimisers/iterative_minimiser.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs index 82e6a7db4..72b8ac617 100644 --- a/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs +++ b/pumpkin-crates/conflict-resolvers/src/minimisers/iterative_minimiser.rs @@ -197,7 +197,12 @@ impl IterativeMinimiser { // [x >= v], [x >= v'] => [x >= v'] if v' > v let to_remove = self.domains[predicate.get_domain()] .iter() - .filter(|element| element.is_lower_bound_predicate()) + .filter(|element| { + element.is_lower_bound_predicate() + || (element.is_not_equal_predicate() + && element.get_right_hand_side() + < predicate.get_right_hand_side()) + }) .copied() .collect::>(); @@ -224,7 +229,12 @@ impl IterativeMinimiser { // [x <= v], [x <= v'] => [x <= v'] if v' < v let to_remove = self.domains[predicate.get_domain()] .iter() - .filter(|element| element.is_upper_bound_predicate()) + .filter(|element| { + element.is_upper_bound_predicate() + || (element.is_not_equal_predicate() + && element.get_right_hand_side() + > predicate.get_right_hand_side()) + }) .copied() .collect::>(); if !to_remove.is_empty() {