Skip to content

feat(pumpkin-solver): Support checking of derived nogoods during search #373

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maartenflippo wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat(pumpkin-solver): Support checking of derived nogoods during search #373

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
89318e8
Move inference checker to its own file
maartenflippo Feb 25, 2026
c9d3a74
Move the deduction checker to `pumpkin_checking`
maartenflippo Feb 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

278 changes: 76 additions & 202 deletions pumpkin-checker/src/deductions.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -46,212 +46,86 @@ 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(
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<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.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::<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,
});
// 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::<Result<Vec<_>, _>>()?;

// 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<Atomic>,
facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
) -> 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<Atomic>,
facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
) -> 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<str>` everywhere, which
// does not implement `Send`.
name: String::from(int_atomic.name.as_ref()),
comparison: int_atomic.comparison,
value: int_atomic.value,
},
})
.collect(),
}
}
12 changes: 11 additions & 1 deletion pumpkin-checker/src/inferences/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<Atomic>,
pub consequent: Option<Atomic>,
}

impl From<SupportingInference<Atomic>> for Fact {
fn from(value: SupportingInference<Atomic>) -> Self {
Fact {
premises: value.premises,
consequent: value.consequent,
}
}
}

impl Fact {
/// Create a fact `premises -> false`.
pub fn nogood(premises: Vec<Atomic>) -> Self {
Expand Down
17 changes: 0 additions & 17 deletions pumpkin-checker/src/test_utils.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
///
Expand Down Expand Up @@ -90,18 +88,3 @@ macro_rules! fact {
}
};
}

pub(crate) fn deduction(
id: u32,
premises: impl Into<Vec<IntAtomic<Rc<str>, i32>>>,
sequence: impl IntoIterator<Item = u32>,
) -> drcp_format::Deduction<Rc<str>, 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(),
}
}
1 change: 1 addition & 0 deletions pumpkin-crates/checking/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ authors.workspace = true
[dependencies]
dyn-clone = "1.0.20"
fnv = "1.0.7"
thiserror = "2.0.18"

[lints]
workspace = true
Loading