feat(pumpkin-checker): Introduce the uncertified proof checker (#328)

Introduce an uncertified proof checker. This checker can be used to
verify DRCP proofs produced by Pumpkin.

In this initial version, we support the following constraints:
- Integer linear inequality (`int_lin_le`)
- Integer linear equality (`int_lin_eq`)
- Cumulative (`pumpkin_cumulative`)
- All Different (`pumpkin_all_different`)

For those constraints the checker implements the following inferences:
- Linear bounds for integer linear (in)equalities
- Binary equality for an integer equality over two variables
- Binary disequality for all different
- Hall set inferences for all different
- Time table for cumulative
- Nogoods

Author: maartenflippo

Cargo.lock

@@ -1,5 +1,5 @@
 [workspace]
-members = ["./pumpkin-solver", "./drcp-format", "./pumpkin-solver-py", "./pumpkin-macros", "./drcp-debugger", "./pumpkin-crates/*", "./fzn-rs", "./fzn-rs-derive"]
+members = ["./pumpkin-solver", "./pumpkin-checker", "./drcp-format", "./pumpkin-solver-py", "./pumpkin-macros", "./drcp-debugger", "./pumpkin-crates/*", "./fzn-rs", "./fzn-rs-derive"]
 resolver = "2"
 
 [workspace.package]

Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "pumpkin-checker"
+version = "0.1.0"
+repository.workspace = true
+edition.workspace = true
+license.workspace = true
+authors.workspace = true
+
+[dependencies]
+anyhow = "1.0.99"
+clap = { version = "4.5.47", features = ["derive"] }
+drcp-format = { version = "0.3.0", path = "../drcp-format" }
+flate2 = "1.1.2"
+fzn-rs = { version = "0.1.0", path = "../fzn-rs" }
+thiserror = "2.0.16"
+
+[lints]
+workspace = true

pumpkin-checker/Cargo.toml

@@ -0,0 +1,115 @@
+use std::collections::BTreeMap;
+use std::rc::Rc;
+
+use drcp_format::ConstraintId;
+use drcp_format::IntAtomic;
+
+use crate::inferences::Fact;
+use crate::model::Nogood;
+use crate::state::VariableState;
+
+/// An inference that was ignored when checking a deduction.
+#[derive(Clone, Debug)]
+pub struct IgnoredInference {
+    /// The ID of the ignored inference.
+    pub constraint_id: ConstraintId,
+
+    /// The premises that were not satisfied when the inference was evaluated.
+    pub unsatisfied_premises: Vec<IntAtomic<String, i32>>,
+}
+
+/// A deduction is rejected by the checker.
+#[derive(thiserror::Error, Debug)]
+#[error("invalid deduction")]
+pub enum InvalidDeduction {
+    /// The constraint ID of the deduction is already used by an existing constraint.
+    #[error("constraint id {0} already in use")]
+    DuplicateConstraintId(ConstraintId),
+
+    /// An inference in the deduction sequence does not exist in the proof stage.
+    #[error("inference {0} does not exist")]
+    UnknownInference(ConstraintId),
+
+    /// 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<IgnoredInference>),
+
+    /// 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.
+pub fn verify_deduction(
+    deduction: &drcp_format::Deduction<Rc<str>, i32>,
+    facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
+) -> Result<Nogood, InvalidDeduction> {
+    // 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(&Fact::nogood(deduction.premises.clone()))
+            .ok_or(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<IntAtomic<String, i32>> = fact
+            .premises
+            .iter()
+            .filter_map::<IntAtomic<String, i32>, _>(|premise| {
+                if variable_state.is_true(premise) {
+                    None
+                } else {
+                    // We need to convert the premise name from a `Rc<str>` 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.name.as_ref()),
+                        comparison: premise.comparison,
+                        value: premise.value,
+                    })
+                }
+            })
+            .collect::<Vec<_>>();
+
+        // 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,
+            });
+
+            continue;
+        }
+
+        // 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())),
+        }
+    }
+
+    // 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))
+}

pumpkin-checker/src/deductions.rs

@@ -0,0 +1,51 @@
+use std::collections::HashSet;
+
+use super::Fact;
+use crate::inferences::InvalidInference;
+use crate::model::Constraint;
+use crate::state::VariableState;
+
+/// Verify an `all_different` inference.
+///
+/// The checker tests that the premises and the negation of the consequent form a hall-set. If that
+/// is the case, the inference is accepted. Otherwise, the inference is rejected.
+///
+/// The checker will reject inferences with redundant atomic constraints.
+pub(crate) fn verify_all_different(
+    fact: &Fact,
+    constraint: &Constraint,
+) -> Result<(), InvalidInference> {
+    // This checker takes the union of the domains of the variables in the constraint. If there
+    // are fewer values in the union of the domain than there are variables, then there is a
+    // conflict and the inference is valid.
+
+    let Constraint::AllDifferent(all_different) = constraint else {
+        return Err(InvalidInference::ConstraintLabelMismatch);
+    };
+
+    let variable_state = VariableState::prepare_for_conflict_check(fact)
+        .ok_or(InvalidInference::InconsistentPremises)?;
+
+    // Collect all values present in at least one of the domains.
+    let union_of_domains = all_different
+        .variables
+        .iter()
+        .filter_map(|variable| variable_state.iter_domain(variable))
+        .flatten()
+        .collect::<HashSet<_>>();
+
+    // Collect the variables mentioned in the fact. Here we ignore variables with a domain
+    // equal to all integers, as they are not mentioned in the fact. Therefore they do not
+    // contribute in the hall-set reasoning.
+    let num_variables = all_different
+        .variables
+        .iter()
+        .filter(|variable| variable_state.iter_domain(variable).is_some())
+        .count();
+
+    if union_of_domains.len() < num_variables {
+        Ok(())
+    } else {
+        Err(InvalidInference::Unsound)
+    }
+}