diff --git a/src/encodings/card.rs b/src/encodings/card.rs index 5d15301b..bef047a5 100644 --- a/src/encodings/card.rs +++ b/src/encodings/card.rs @@ -308,7 +308,7 @@ pub fn encode_cardinality_constraint( } if constr.is_clause() { let mut cnf = Cnf::new(); - cnf.add_clause(constr.into_clause().unwrap()); + cnf.add_clause(constr.as_clause().unwrap()); return cnf; } CE::encode_constr(constr, var_manager).unwrap() diff --git a/src/encodings/pb.rs b/src/encodings/pb.rs index 5f84d526..b6b99844 100644 --- a/src/encodings/pb.rs +++ b/src/encodings/pb.rs @@ -320,6 +320,11 @@ pub fn encode_pb_constraint( lits.into_iter().for_each(|(l, _)| cnf.add_unit(l)); return cnf; } + if constr.is_clause() { + let mut cnf = Cnf::new(); + cnf.add_clause(constr.as_clause().unwrap()); + return cnf; + } if constr.is_card() { let card = constr.as_card_constr().unwrap(); return card::default_encode_cardinality_constraint(card, var_manager); diff --git a/src/instances/sat.rs b/src/instances/sat.rs index 47cbc44c..8dc3954e 100644 --- a/src/instances/sat.rs +++ b/src/instances/sat.rs @@ -555,6 +555,10 @@ impl SatInstance { .for_each(|(l, _)| cnf.add_unit(l)); return None; } + if pb.is_clause() { + cnf.add_clause(pb.as_clause().unwrap()); + return None; + } if pb.is_card() { cards.push(pb.as_card_constr().unwrap()); return None; @@ -578,7 +582,7 @@ impl SatInstance { return None; } if card.is_clause() { - cnf.add_clause(card.into_clause().unwrap()); + cnf.add_clause(card.as_clause().unwrap()); return None; } return Some(card); diff --git a/src/types/constraints.rs b/src/types/constraints.rs index 0073390e..9fa9985f 100644 --- a/src/types/constraints.rs +++ b/src/types/constraints.rs @@ -9,7 +9,7 @@ use std::{ ops::{self, Not}, }; -use super::{Assignment, IWLitIter, Lit, LitIter, TernaryVal, WLitIter, RsHashSet}; +use super::{Assignment, IWLitIter, Lit, LitIter, RsHashSet, TernaryVal, WLitIter}; /// Type representing a clause. /// Wrapper around a std collection to allow for changing the data structure. @@ -133,7 +133,7 @@ impl Clause { } Some(self) } - + /// Sanitizes the clause. This includes removing duplicates and removing the /// entire clause if it is a tautology. This preserves the order of the /// literals in the clause. @@ -156,7 +156,7 @@ impl Clause { idx += 1; } } - return Some(self) + return Some(self); } } @@ -375,7 +375,7 @@ impl CardConstraint { } /// Converts the constraint into a clause, if possible - pub fn into_clause(self) -> Option { + pub fn as_clause(self) -> Option { if !self.is_clause() { return None; } @@ -620,6 +620,15 @@ impl PBConstraint { } } + /// Checks if the constraint is a clause + pub fn is_clause(&self) -> bool { + match self { + PBConstraint::UB(constr) => constr.is_clause(), + PBConstraint::LB(constr) => constr.is_clause(), + PBConstraint::EQ(_) => false, + } + } + /// Normalizes the constraint. This sorts the literal and merges duplicates. /// Comparing two normalized constraints checks their logical equivalence. pub fn normalize(self) -> Self { @@ -712,6 +721,22 @@ impl PBConstraint { }) } + /// Converts the constraint into a clause, if possible + pub fn as_clause(self) -> Option { + if !self.is_clause() { + return None; + } + match self { + PBConstraint::UB(constr) => Some(Clause::from_iter( + constr.lits.into_iter().map(|(lit, _)| !lit), + )), + PBConstraint::LB(constr) => Some(Clause::from_iter( + constr.lits.into_iter().map(|(lit, _)| lit), + )), + PBConstraint::EQ(_) => panic!(), + } + } + /// Gets the (positively) weighted literals that are in the constraint pub fn into_lits(self) -> impl WLitIter { match self { @@ -784,6 +809,21 @@ impl PBUBConstr { } unit_weight } + + /// Checks if the constraint is a clause + pub fn is_clause(&self) -> bool { + if self.is_tautology() { + return false; + } + if self.is_unsat() { + return false; + } + let min_coeff: usize = self + .lits + .iter() + .fold(usize::MAX, |min, (_, coeff)| std::cmp::min(min, *coeff)); + self.weight_sum <= self.b as usize + min_coeff && self.weight_sum > self.b as usize + } } /// A lower bound pseudo-boolean constraint (`weighted sum of lits >= b`) @@ -837,6 +877,21 @@ impl PBLBConstr { } unit_weight } + + /// Checks if the constraint is a clause + pub fn is_clause(&self) -> bool { + if self.is_tautology() { + return false; + } + if self.is_unsat() { + return false; + } + let min_coeff: usize = self + .lits + .iter() + .fold(usize::MAX, |min, (_, coeff)| std::cmp::min(min, *coeff)); + (self.b as usize) <= min_coeff + } } /// An equality pseudo-boolean constraint (`weighted sum of lits = b`) @@ -1014,4 +1069,15 @@ mod tests { assert!(!PBConstraint::new_lb(lits.clone(), 3).is_card()); assert!(!PBConstraint::new_eq(lits.clone(), 2).is_card()); } + + #[test] + fn pb_is_clause() { + let lits = vec![(lit![0], 2), (lit![1], 3), (lit![2], 2)]; + assert!(PBConstraint::new_ub(lits.clone(), 6).is_clause()); + assert!(PBConstraint::new_lb(lits.clone(), 2).is_clause()); + assert!(!PBConstraint::new_ub(lits.clone(), 7).is_clause()); + assert!(!PBConstraint::new_ub(lits.clone(), 4).is_clause()); + assert!(!PBConstraint::new_lb(lits.clone(), 3).is_clause()); + assert!(!PBConstraint::new_eq(lits.clone(), 2).is_card()); + } } diff --git a/tests/constraints.rs b/tests/constraints.rs index 0a52e130..c58b79a7 100644 --- a/tests/constraints.rs +++ b/tests/constraints.rs @@ -173,6 +173,34 @@ fn pb_eq() { } #[test] -fn card_is_clause() { - assert!(CardConstraint::new_lb(vec![lit![0], lit![1]], 1).is_clause()); +fn card_clause() { + let lits = vec![lit![0], lit![1], lit![2]]; + test_card!( + CardConstraint::new_lb(lits.clone(), 1), + vec![lit![0], lit![1], !lit![2]], + vec![!lit![0], !lit![1], !lit![2]] + ); + test_card!( + CardConstraint::new_ub(lits.clone(), 2), + vec![!lit![0], lit![1], lit![2]], + vec![lit![0], lit![1], lit![2]] + ); +} + +#[test] +fn pb_clause() { + let mut lits = RsHashMap::default(); + lits.insert(lit![0], 2); + lits.insert(lit![1], 3); + lits.insert(lit![2], 2); + test_pb!( + PBConstraint::new_ub(lits.clone(), 6), + vec![lit![0], !lit![1], !lit![2]], + vec![lit![0], lit![1], lit![2]] + ); + test_pb!( + PBConstraint::new_lb(lits.clone(), 2), + vec![lit![0], lit![1], !lit![2]], + vec![!lit![0], !lit![1], !lit![2]] + ); }