feat(pumpkin-solver): Implement consistency checker infrastructure

.github/workflows/ci.yml

@@ -26,7 +26,13 @@ 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-core/check-deductions
+    - run: |
+        cargo test                                     \
+          --release                                    \
+          --no-fail-fast                               \
+          --features pumpkin-solver/check-propagations \
+          --features pumpkin-core/check-consistency    \
+          --features pumpkin-core/check-deductions
 
   wasm-test:
     name: Test Suite for pumpkin-core in WebAssembly

README.md

@@ -23,10 +23,10 @@ A unique feature of Pumpkin is that it can produce a certificate of unsatisfiabi
 
 The solver currently supports integer variables and a number of (global) constraints:
 
-- [Cumulative global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/core/src/propagators/cumulative).
-- [Disjunctive global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/core/src/propagators/disjunctive)
-- [Element global constraint](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/element.rs).
-- [Arithmetic constraints](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/core/src/propagators/arithmetic): [linear integer (in)equalities](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/arithmetic/linear_less_or_equal.rs), [integer division](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/arithmetic/integer_division.rs), [integer multiplication](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/arithmetic/integer_multiplication.rs), [maximum](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/arithmetic/maximum.rs), [absolute value](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/core/src/propagators/arithmetic/absolute_value.rs).
+- [Cumulative global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/propagators/src/propagators/cumulative).
+- [Disjunctive global constraint](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/propagators/src/propagators/disjunctive)
+- [Element global constraint](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/element.rs).
+- [Arithmetic constraints](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/propagators/src/propagators/arithmetic): [linear integer (in)equalities](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/arithmetic/linear_less_or_equal.rs), [integer division](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/arithmetic/integer_division.rs), [integer multiplication](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs), [maximum](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/arithmetic/maximum.rs), [absolute value](https://github.com/ConSol-Lab/Pumpkin/blob/main/pumpkin-crates/propagators/src/propagators/arithmetic/absolute_value.rs).
 - Clausal constraints.
 
 We are actively developing Pumpkin and would be happy to hear from you should you have any questions or feature requests!
@@ -98,13 +98,22 @@ To use it as such a backend, follow the following steps:
 - Step 3: Add the following to the `MZN_SOLVER_PATH` environment variable: `<path_to_pumpkin>/minizinc` (see [this thread](https://askubuntu.com/questions/58814/how-do-i-add-environment-variables) on how to do this using a shell).
 - Step 4: Check whether the installation worked using the command `minizinc --help pumpkin`.
 
-## Components
-Pumpkin consists of 3 different crates:
+This will add Pumpkin and PumpkinProof (which uses a flattening library specific for proof logging).
 
-- The library contained in [core](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/core); defines the API through which the solver can be used via Rust.
-- The CLI contained in [pumpkin-solver](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver/src/bin/pumpkin-solver); defines the usage of Pumpkin through a command line.
-- The proof logging contained in [drcp-format](https://github.com/ConSol-Lab/Pumpkin/tree/main/drcp-format); defines proof logging which can be used in combination with Pumpkin.
-- The python bindings contained in [pumpkin-solver-py](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver-py); defines the python interface for Pumpkin
+## Components
+Pumpkin consists of several different components:
+
+- The crates contained in [pumpkin-crates](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates):
+    - [pumpkin-core](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/core); defines the API through which the solver can be used via Rust.
+    - [pumpkin-propagators](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/propagators); contains (most of) the propagators used by Pumpkin.
+    - [pumpkin-constraints](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/constraints); contains convenient ways to add one or more propagators modelling certain constraints to the solver.
+    - [pumpkin-conflict-resolvers](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/conflict-resolvers); contains the conflict resolvers (e.g., 1UIP or All-Decision conflit resolvers) used by Pumpkin.
+    - [pumpkin-checking](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-crates/checking); contains the types used for checking the soundness of propagators in Pumpkin.
+- The CLI contained in [pumpkin-solver](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver).
+- The python bindings contained in [pumpkin-solver-py](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-solver-py).
+- The proof logging contained in [drcp-format](https://github.com/ConSol-Lab/Pumpkin/tree/main/drcp-format); a file reader and writer for the DRCP proof format (the proof format used by Pumpkin).
+- The (unverified) proof processor contained in [pumpkin-proof-processor](https://github.com/ConSol-Lab/Pumpkin/tree/main/pumpkin-proof-processor).
+- A debugger for DRCP proofs contained in [drcp-debugger](https://github.com/ConSol-Lab/Pumpkin/tree/main/drcp-debugger).
 
 The easiest way to get to know the different modules is through the documentation. This documentation can be created automatically using the command:
 ```sh

minizinc/pumpkin-for-proofs.msc

@@ -1,6 +1,6 @@
 {
-    "name": "Pumpkin",
-    "id": "nl.tudelft.algorithmics.pumpkin",
+    "name": "PumpkinProof",
+    "id": "nl.tudelft.algorithmics.pumpkin_proof",
     "version": "0.1",
     "executable": "../target/release/pumpkin-solver",
     "mznlib": "./lib-for-proofs/",

pumpkin-crates/constraints/src/constraints/arithmetic/mod.rs

@@ -3,13 +3,14 @@ mod inequality;
 
 pub use equality::*;
 pub use inequality::*;
+use pumpkin_core::checkers::support::SupportsValue;
 use pumpkin_core::constraints::Constraint;
 use pumpkin_core::proof::ConstraintTag;
 use pumpkin_core::variables::IntegerVariable;
 use pumpkin_propagators::arithmetic::AbsoluteValueArgs;
 use pumpkin_propagators::arithmetic::DivisionArgs;
 use pumpkin_propagators::arithmetic::IntegerMultiplicationArgs;
-use pumpkin_propagators::arithmetic::MaximumArgs;
+use pumpkin_propagators::arithmetic::MaximumConstructor;
 
 /// Creates the [`Constraint`] `a + b = c`.
 pub fn plus<Var: IntegerVariable + 'static>(
@@ -23,9 +24,9 @@ pub fn plus<Var: IntegerVariable + 'static>(
 
 /// Creates the [`Constraint`] `a * b = c`.
 pub fn times(
-    a: impl IntegerVariable + 'static,
-    b: impl IntegerVariable + 'static,
-    c: impl IntegerVariable + 'static,
+    a: impl IntegerVariable + SupportsValue<f32> + 'static,
+    b: impl IntegerVariable + SupportsValue<f32> + 'static,
+    c: impl IntegerVariable + SupportsValue<f32> + 'static,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
     IntegerMultiplicationArgs {
@@ -75,7 +76,7 @@ pub fn maximum<Var: IntegerVariable + 'static>(
     rhs: impl IntegerVariable + 'static,
     constraint_tag: ConstraintTag,
 ) -> impl Constraint {
-    MaximumArgs {
+    MaximumConstructor {
         array: array.into_iter().collect(),
         rhs,
         constraint_tag,

pumpkin-crates/core/Cargo.toml

@@ -15,7 +15,7 @@ pumpkin-checking = { version = "0.3.0", path = "../checking" }
 thiserror = "2.0.12"
 log = "0.4.17"
 bitfield = "0.19.4"
-enumset = "1.1.12"
+enumset = "1.1.13"
 fnv = "1.0.7" # We require features which are on the `main` branch of the repository but are not on crates.io
 rand = { version = "0.10.1", features = [ "alloc" ] }
 once_cell = "1.19.0"
@@ -30,6 +30,8 @@ clap = { version = "4.5.40", optional = true, features=["derive"] }
 indexmap = "2.10.0"
 dyn-clone = "1.0.20"
 flate2 = { version = "1.1.2" }
+bit-set = "0.10.0"
+replace_with = "0.1.8"
 
 [target.'cfg(target_arch = "wasm32")'.dependencies]
 web-time = "1.1"
@@ -39,6 +41,7 @@ getrandom = { version = "0.4.2", features = ["wasm_js"] }
 wasm-bindgen-test = "0.3"
 
 [features]
+check-consistency = []
 check-propagations = []
 check-deductions = []
 debug-checks = []

pumpkin-crates/core/src/api/mod.rs

@@ -69,8 +69,8 @@ pub mod options {
     pub use crate::engine::ConflictResolverType;
     pub use crate::engine::RestartOptions;
     pub use crate::engine::SatisfactionSolverOptions as SolverOptions;
+    pub use crate::propagators::ReifiedPropagatorArgs;
     pub use crate::propagators::nogoods::LearningOptions;
-    pub use crate::propagators::reified_propagator::ReifiedPropagatorArgs;
 }
 
 pub mod termination {

pumpkin-crates/core/src/basic_types/mod.rs

@@ -4,7 +4,6 @@ mod function;
 mod predicate_id_generators;
 mod propositional_conjunction;
 mod random;
-mod ref_or_owned;
 pub(crate) mod sequence_generators;
 mod solution;
 mod stored_conflict_info;
@@ -19,7 +18,6 @@ pub use predicate_id_generators::PredicateId;
 pub use predicate_id_generators::PredicateIdGenerator;
 pub use propositional_conjunction::PropositionalConjunction;
 pub use random::*;
-pub(crate) use ref_or_owned::*;
 pub use solution::ProblemSolution;
 pub use solution::Solution;
 pub use solution::SolutionReference;

pumpkin-crates/core/src/basic_types/propositional_conjunction.rs

@@ -21,6 +21,12 @@ impl Deref for PropositionalConjunction {
     }
 }
 
+impl From<PropositionalConjunction> for Box<[Predicate]> {
+    fn from(val: PropositionalConjunction) -> Self {
+        val.predicates_in_conjunction.into()
+    }
+}
+
 impl PropositionalConjunction {
     pub fn new(predicates_in_conjunction: Vec<Predicate>) -> Self {
         PropositionalConjunction {

pumpkin-crates/core/src/checkers/mod.rs

@@ -0,0 +1,16 @@
+mod propagation_checker;
+mod retention_checker;
+mod scope;
+mod self_disabling;
+mod store;
+mod strong_retention_checker;
+pub mod support;
+mod weak_retention_checker;
+
+pub use propagation_checker::*;
+pub use retention_checker::*;
+pub use scope::*;
+pub use self_disabling::*;
+pub use store::*;
+pub use strong_retention_checker::*;
+pub use weak_retention_checker::*;

pumpkin-crates/core/src/checkers/propagation_checker.rs

@@ -0,0 +1,64 @@
+use pumpkin_checking::BoxedChecker;
+use pumpkin_checking::VariableState;
+
+use crate::predicates::Predicate;
+use crate::propagation::Domains;
+use crate::propagation::ReadDomains;
+use crate::variables::DomainId;
+
+/// Tests whether an inference is correct given the solver state.
+///
+/// An inference is correct when:
+/// 1. All premises are satisfied.
+/// 2. The conjunction of the premises and negation of the consequent is consistent.
+/// 3. The consequent is logically entailed given the inference code.
+#[derive(Clone, Debug)]
+pub struct PropagationChecker {
+    inference_checker: BoxedChecker<Predicate>,
+}
+
+impl PropagationChecker {
+    /// Create a new propagation checker given an inference checker and inference code.
+    pub fn new(inference_checker: BoxedChecker<Predicate>) -> PropagationChecker {
+        PropagationChecker { inference_checker }
+    }
+
+    /// Run the propagation checker for the given inference.
+    pub fn check(
+        &self,
+        premises: &[Predicate],
+        consequent: Option<Predicate>,
+        domains: Domains<'_>,
+    ) -> Result<(), InvalidInference> {
+        let premises_satisfied = premises
+            .iter()
+            .all(|&premise| domains.evaluate_predicate(premise) == Some(true));
+
+        if !premises_satisfied {
+            return Err(InvalidInference::UnsatisfiedPremises);
+        }
+
+        let variable_state =
+            VariableState::prepare_for_conflict_check(premises.iter().copied(), consequent)
+                .map_err(InvalidInference::InconsistentPredicates)?;
+
+        if self
+            .inference_checker
+            .check(variable_state, premises, consequent.as_ref())
+        {
+            Ok(())
+        } else {
+            Err(InvalidInference::Unsound)
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum InvalidInference {
+    /// Not all premises are true given the current state.
+    UnsatisfiedPremises,
+    /// The predicates that make up the inference are trivially inconsistent.
+    InconsistentPredicates(DomainId),
+    /// Cannot establish that the inference is sound.
+    Unsound,
+}