From 3e8e2c78552d72591025704dbdb89b871694ac21 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Wed, 17 Jul 2024 11:04:09 +0300 Subject: [PATCH] feat!: add `evaluate`, replacing `is_sat` --- solvertests/src/integration.rs | 2 +- src/instances/fio.rs | 6 +- src/instances/multiopt.rs | 4 +- src/instances/opt.rs | 2 +- src/instances/sat.rs | 60 +++++++++---- src/types/constraints.rs | 154 +++++++++++++++++++++++---------- 6 files changed, 161 insertions(+), 67 deletions(-) diff --git a/solvertests/src/integration.rs b/solvertests/src/integration.rs index f2e0afa6..50465ae0 100644 --- a/solvertests/src/integration.rs +++ b/solvertests/src/integration.rs @@ -38,7 +38,7 @@ pub fn base(input: IntegrationInput) -> TokenStream { if $res == rustsat::solvers::SolverResult::Sat { let sol = rustsat::solvers::Solve::solution(&solver, inst.max_var().expect("no variables in instance")) .expect("failed to get solution from solver"); - assert!(inst.is_sat(&sol)); + assert_eq!(inst.evaluate(&sol), rustsat::types::TernaryVal::True); } }}; } diff --git a/src/instances/fio.rs b/src/instances/fio.rs index 6da5e430..a8ef6dcc 100644 --- a/src/instances/fio.rs +++ b/src/instances/fio.rs @@ -277,7 +277,7 @@ mod tests { .unwrap(); let res = parse_sat_solver_output(&mut reader).unwrap(); if let SolverOutput::Sat(sol) = res { - assert!(instance.is_sat(&sol)); + assert_eq!(instance.evaluate(&sol), TernaryVal::True); } else { panic!() } @@ -288,7 +288,7 @@ mod tests { .unwrap(); let res = parse_sat_solver_output(&mut reader).unwrap(); if let SolverOutput::Sat(sol) = res { - assert!(instance.is_sat(&sol)); + assert_eq!(instance.evaluate(&sol), TernaryVal::True); } else { panic!() } @@ -299,7 +299,7 @@ mod tests { .unwrap(); let res = parse_sat_solver_output(&mut reader).unwrap(); if let SolverOutput::Sat(sol) = res { - assert!(instance.is_sat(&sol)); + assert_eq!(instance.evaluate(&sol), TernaryVal::True); } else { panic!() } diff --git a/src/instances/multiopt.rs b/src/instances/multiopt.rs index 7e926f16..37e2155d 100644 --- a/src/instances/multiopt.rs +++ b/src/instances/multiopt.rs @@ -6,7 +6,7 @@ use crate::{ encodings::{card, pb}, types::{ constraints::{CardConstraint, PbConstraint}, - Assignment, Lit, Var, WClsIter, WLitIter, + Assignment, Lit, TernaryVal, Var, WClsIter, WLitIter, }, RequiresClausal, RequiresSoftLits, }; @@ -454,7 +454,7 @@ impl MultiOptInstance { /// Calculates the objective values of an assignment. Returns [`None`] if the /// assignment is not a solution. pub fn cost(&self, assign: &Assignment) -> Option> { - if !self.constrs.is_sat(assign) { + if self.constrs.evaluate(assign) != TernaryVal::True { return None; } Some(self.objs.iter().map(|o| o.evaluate(assign)).collect()) diff --git a/src/instances/opt.rs b/src/instances/opt.rs index dd3a40e7..08b7b7ba 100644 --- a/src/instances/opt.rs +++ b/src/instances/opt.rs @@ -1394,7 +1394,7 @@ impl Instance { /// Calculates the objective value of an assignment. Returns [`None`] if the /// assignment is not a solution. pub fn cost(&self, assign: &Assignment) -> Option { - if !self.constrs.is_sat(assign) { + if self.constrs.evaluate(assign) != TernaryVal::True { return None; } Some(self.obj.evaluate(assign)) diff --git a/src/instances/sat.rs b/src/instances/sat.rs index 7dd604f4..d1704d3d 100644 --- a/src/instances/sat.rs +++ b/src/instances/sat.rs @@ -8,7 +8,7 @@ use crate::{ lit, types::{ constraints::{CardConstraint, PbConstraint}, - Assignment, Clause, Lit, Var, + Assignment, Clause, Lit, TernaryVal, Var, }, utils::{unreachable_err, LimitedIter}, RequiresClausal, @@ -234,15 +234,28 @@ impl Cnf { fio::dimacs::write_cnf_annotated(writer, self, n_vars) } - /// Checks whether the CNF is satisfied by the given assignment + /// Checks the value of the CNF under a given assignment #[must_use] - pub fn is_sat(&self, assign: &Assignment) -> bool { + pub fn evaluate(&self, assign: &Assignment) -> TernaryVal { + let mut val = TernaryVal::True; for clause in &self.clauses { - if !clause.is_sat(assign) { - return false; + match clause.evaluate(assign) { + TernaryVal::True => (), + TernaryVal::False => return TernaryVal::False, + TernaryVal::DontCare => val = TernaryVal::DontCare, } } - true + val + } + + /// Checks whether the CNF is satisfied by the given assignment + #[deprecated( + since = "0.6.0", + note = "use `evaluate` instead and check against `TernaryVal::True`" + )] + #[must_use] + pub fn is_sat(&self, assign: &Assignment) -> bool { + self.evaluate(assign) == TernaryVal::True } } @@ -965,23 +978,40 @@ impl Instance { } } - /// Checks whether the instance is satisfied by the given assignment + /// Computes the value of the instance under a given assignment #[must_use] - pub fn is_sat(&self, assign: &Assignment) -> bool { - if !self.cnf.is_sat(assign) { - return false; + pub fn evaluate(&self, assign: &Assignment) -> TernaryVal { + let mut val = TernaryVal::True; + match self.cnf.evaluate(assign) { + TernaryVal::True => (), + TernaryVal::False => return TernaryVal::False, + TernaryVal::DontCare => val = TernaryVal::DontCare, } for card in &self.cards { - if !card.is_sat(assign) { - return false; + match card.evaluate(assign) { + TernaryVal::True => (), + TernaryVal::False => return TernaryVal::False, + TernaryVal::DontCare => val = TernaryVal::DontCare, } } for pb in &self.pbs { - if !pb.is_sat(assign) { - return false; + match pb.evaluate(assign) { + TernaryVal::True => (), + TernaryVal::False => return TernaryVal::False, + TernaryVal::DontCare => val = TernaryVal::DontCare, } } - true + val + } + + /// Checks whether the instance is satisfied by the given assignment + #[deprecated( + since = "0.6.0", + note = "use `evaluate` instead and check against `TernaryVal::True`" + )] + #[must_use] + pub fn is_sat(&self, assign: &Assignment) -> bool { + self.evaluate(assign) == TernaryVal::True } } diff --git a/src/types/constraints.rs b/src/types/constraints.rs index 114c1016..93a2e22e 100644 --- a/src/types/constraints.rs +++ b/src/types/constraints.rs @@ -376,6 +376,10 @@ impl Cl { /// Checks wheter the clause is satisfied #[must_use] + #[deprecated( + since = "0.6.0", + note = "use `evaluate` instead and check against `TernaryVal::True`" + )] pub fn is_sat(&self, assignment: &Assignment) -> bool { self.evaluate(assignment) == TernaryVal::True } @@ -541,6 +545,16 @@ impl CardConstraint { } } + /// Gets the bound of the constraint + #[must_use] + pub fn bound(&self) -> usize { + match self { + CardConstraint::Ub(CardUbConstr { b, .. }) + | CardConstraint::Lb(CardLbConstr { b, .. }) + | CardConstraint::Eq(CardEqConstr { b, .. }) => *b, + } + } + /// Changes the bound on the constraint pub fn change_bound(&mut self, b: usize) { match self { @@ -677,19 +691,34 @@ impl CardConstraint { /// Checks whether the cardinality constraint is satisfied by the given assignment #[must_use] - pub fn is_sat(&self, assign: &Assignment) -> bool { - let count = self.iter().fold(0, |cnt, lit| { - if assign.lit_value(*lit) == TernaryVal::True { - return cnt + 1; - } - cnt - }); + pub fn evaluate(&self, assign: &Assignment) -> TernaryVal { + #[allow(clippy::range_plus_one)] + let range = self + .iter() + .fold(0..0, |rng, &lit| match assign.lit_value(lit) { + TernaryVal::True => rng.start + 1..rng.end + 1, + TernaryVal::False => rng, + TernaryVal::DontCare => rng.start..rng.end + 1, + }); + if range.contains(&self.bound()) { + return TernaryVal::DontCare; + } match self { - CardConstraint::Ub(constr) => count <= constr.b, - CardConstraint::Lb(constr) => count >= constr.b, - CardConstraint::Eq(constr) => count == constr.b, + CardConstraint::Ub(CardUbConstr { b, .. }) => (range.start <= *b).into(), + CardConstraint::Lb(CardLbConstr { b, .. }) => (range.start >= *b).into(), + CardConstraint::Eq(CardEqConstr { b, .. }) => (range.start == *b).into(), } } + + /// Checks whether the cardinality constraint is satisfied by the given assignment + #[deprecated( + since = "0.6.0", + note = "use `evaluate` instead and check against `TernaryVal::True`" + )] + #[must_use] + pub fn is_sat(&self, assign: &Assignment) -> bool { + self.evaluate(assign) == TernaryVal::True + } } impl<'slf> IntoIterator for &'slf CardConstraint { @@ -958,6 +987,16 @@ impl PbConstraint { *b += b_add; } + /// Gets the bound of the constraint + #[must_use] + pub fn bound(&self) -> isize { + match self { + PbConstraint::Ub(PbUbConstr { b, .. }) + | PbConstraint::Lb(PbLbConstr { b, .. }) + | PbConstraint::Eq(PbEqConstr { b, .. }) => *b, + } + } + /// Checks if the constraint is always satisfied #[must_use] pub fn is_tautology(&self) -> bool { @@ -1187,37 +1226,54 @@ impl PbConstraint { /// Checks whether the PB constraint is satisfied by the given assignment #[must_use] - pub fn is_sat(&self, assign: &Assignment) -> bool { - let sum = self.iter().fold(0, |sum, (lit, coeff)| { - if assign.lit_value(*lit) == TernaryVal::True { - return sum + coeff; - } - sum - }); - match self { - PbConstraint::Ub(constr) => { - if let Ok(sum) = >::try_into(sum) { - sum <= constr.b - } else { - false + pub fn evaluate(&self, assign: &Assignment) -> TernaryVal { + #[allow(clippy::range_plus_one)] + let range = self + .iter() + .fold(0..0, |rng, &(lit, coeff)| match assign.lit_value(lit) { + TernaryVal::True => rng.start + coeff..rng.end + coeff, + TernaryVal::False => rng, + TernaryVal::DontCare => rng.start..rng.end + coeff, + }); + match (isize::try_from(range.start), isize::try_from(range.end)) { + (Ok(start), Ok(end)) => { + if (start..end).contains(&self.bound()) { + return TernaryVal::DontCare; } - } - PbConstraint::Lb(constr) => { - if let Ok(sum) = >::try_into(sum) { - sum >= constr.b - } else { - true + match self { + PBConstraint::Ub(PbUbConstr { b, .. }) => (start <= *b).into(), + PBConstraint::Lb(PbLbConstr { b, .. }) => (start >= *b).into(), + PBConstraint::Eq(PbEqConstr { b, .. }) => (start == *b).into(), } } - PbConstraint::Eq(constr) => { - if let Ok(sum) = >::try_into(sum) { - sum == constr.b - } else { - false + (Ok(start), Err(_)) => match self { + PbConstraint::Ub(PbUbConstr { b, .. }) => { + if (start..).contains(b) { + return TernaryVal::DontCare; + } + TernaryVal::True } - } + PbConstraint::Lb(PbLbConstr { b, .. }) | PbConstraint::Eq(PbEqConstr { b, .. }) => { + if (start..).contains(b) { + return TernaryVal::DontCare; + } + TernaryVal::False + } + }, + (Err(_), Err(_)) => matches!(self, PbConstraint::Lb(_)).into(), + (Err(_), Ok(_)) => unreachable!(), // since end >= start } } + + /// Checks whether the PB constraint is satisfied by the given assignment + #[deprecated( + since = "0.6.0", + note = "use `evaluate` instead and check against `TernaryVal::True`" + )] + #[must_use] + pub fn is_sat(&self, assign: &Assignment) -> bool { + self.evaluate(assign) == TernaryVal::True + } } impl<'slf> IntoIterator for &'slf PbConstraint { @@ -1495,7 +1551,11 @@ impl PbEqConstr { #[cfg(test)] mod tests { use super::{CardConstraint, Cl, PbConstraint}; - use crate::{lit, types::Assignment, var}; + use crate::{ + lit, + types::{Assignment, TernaryVal}, + var, + }; #[test] fn clause_remove() { @@ -1550,16 +1610,20 @@ mod tests { } #[test] - fn clause_is_sat() { + fn clause_evaluate() { let cl = clause![lit![0], lit![1], lit![2]]; - assert!(!cl.is_sat(&assign!(0b000))); - assert!(cl.is_sat(&assign!(0b001))); - assert!(cl.is_sat(&assign!(0b010))); - assert!(cl.is_sat(&assign!(0b011))); - assert!(cl.is_sat(&assign!(0b100))); - assert!(cl.is_sat(&assign!(0b101))); - assert!(cl.is_sat(&assign!(0b110))); - assert!(cl.is_sat(&assign!(0b111))); + assert_eq!(cl.evaluate(&assign!(0b000)), TernaryVal::False); + assert_eq!(cl.evaluate(&assign!(0b001)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b010)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b011)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b100)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b101)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b110)), TernaryVal::True); + assert_eq!(cl.evaluate(&assign!(0b111)), TernaryVal::True); + assert_eq!( + cl.evaluate(&assign!(0b000).truncate(var![1])), + TernaryVal::DontCare + ); } #[test]