From 7320b678e94980edec908006864888ce3e2746db Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Mon, 3 Jul 2023 17:08:51 +0300 Subject: [PATCH] improved assignment detection --- src/encodings/card.rs | 8 +- src/encodings/pb.rs | 8 +- src/instances/sat.rs | 16 +++- src/types/constraints.rs | 156 ++++++++++++++++++++++++++++----------- 4 files changed, 140 insertions(+), 48 deletions(-) diff --git a/src/encodings/card.rs b/src/encodings/card.rs index bef047a5..6d1c8f77 100644 --- a/src/encodings/card.rs +++ b/src/encodings/card.rs @@ -300,12 +300,18 @@ pub fn encode_cardinality_constraint( cnf.add_clause(Clause::new()); return cnf; } - if constr.is_assignment() { + if constr.is_positive_assignment() { let mut cnf = Cnf::new(); let lits = constr.into_lits(); lits.into_iter().for_each(|l| cnf.add_unit(l)); return cnf; } + if constr.is_negative_assignment() { + let mut cnf = Cnf::new(); + let lits = constr.into_lits(); + 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()); diff --git a/src/encodings/pb.rs b/src/encodings/pb.rs index b6b99844..7f3e0c6f 100644 --- a/src/encodings/pb.rs +++ b/src/encodings/pb.rs @@ -314,7 +314,13 @@ pub fn encode_pb_constraint( cnf.add_clause(Clause::new()); return cnf; } - if constr.is_assignment() { + if constr.is_positive_assignment() { + let mut cnf = Cnf::new(); + let lits = constr.into_lits(); + lits.into_iter().for_each(|(l, _)| cnf.add_unit(l)); + return cnf; + } + if constr.is_negative_assignment() { let mut cnf = Cnf::new(); let lits = constr.into_lits(); lits.into_iter().for_each(|(l, _)| cnf.add_unit(l)); diff --git a/src/instances/sat.rs b/src/instances/sat.rs index 8dc3954e..fa29d08b 100644 --- a/src/instances/sat.rs +++ b/src/instances/sat.rs @@ -548,13 +548,20 @@ impl SatInstance { unsat = true; return None; } - if pb.is_assignment() { + if pb.is_positive_assignment() { // Add unit clauses pb.into_lits() .into_iter() .for_each(|(l, _)| cnf.add_unit(l)); return None; } + if pb.is_negative_assignment() { + // Add unit clauses + pb.into_lits() + .into_iter() + .for_each(|(l, _)| cnf.add_unit(!l)); + return None; + } if pb.is_clause() { cnf.add_clause(pb.as_clause().unwrap()); return None; @@ -576,11 +583,16 @@ impl SatInstance { unsat = true; return None; } - if card.is_assignment() { + if card.is_positive_assignment() { // Add unit clauses card.into_lits().into_iter().for_each(|l| cnf.add_unit(l)); return None; } + if card.is_negative_assignment() { + // Add unit clauses + card.into_lits().into_iter().for_each(|l| cnf.add_unit(!l)); + return None; + } if card.is_clause() { cnf.add_clause(card.as_clause().unwrap()); return None; diff --git a/src/types/constraints.rs b/src/types/constraints.rs index 9fa9985f..868ce648 100644 --- a/src/types/constraints.rs +++ b/src/types/constraints.rs @@ -330,12 +330,21 @@ impl CardConstraint { } } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { match self { CardConstraint::UB(_) => false, - CardConstraint::LB(constr) => constr.is_assignment(), - CardConstraint::EQ(constr) => constr.is_assignment(), + CardConstraint::LB(constr) => constr.is_positive_assignment(), + CardConstraint::EQ(constr) => constr.is_positive_assignment(), + } + } + + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { + match self { + CardConstraint::UB(constr) => constr.is_negative_assignment(), + CardConstraint::LB(_) => false, + CardConstraint::EQ(constr) => constr.is_negative_assignment(), } } @@ -427,6 +436,11 @@ impl CardUBConstr { self.b >= self.lits.len() } + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { + self.b == 0 + } + /// Checks if the constraint is a clause pub fn is_clause(&self) -> bool { self.b + 1 == self.lits.len() @@ -456,8 +470,8 @@ impl CardLBConstr { self.b > self.lits.len() } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { self.b == self.lits.len() } @@ -485,10 +499,15 @@ impl CardEQConstr { self.b > self.lits.len() } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { self.b == self.lits.len() } + + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { + self.b == 0 + } } /// Errors when converting pseudo-boolean to cardinality constraints @@ -602,12 +621,21 @@ impl PBConstraint { } } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { match self { PBConstraint::UB(_) => false, - PBConstraint::LB(constr) => constr.is_assignment(), - PBConstraint::EQ(constr) => constr.is_assignment(), + PBConstraint::LB(constr) => constr.is_positive_assignment(), + PBConstraint::EQ(constr) => constr.is_positive_assignment(), + } + } + + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { + match self { + PBConstraint::UB(constr) => constr.is_negative_assignment(), + PBConstraint::LB(_) => false, + PBConstraint::EQ(constr) => constr.is_negative_assignment(), } } @@ -784,10 +812,9 @@ impl PBUBConstr { /// Checks if the constraint is always satisfied pub fn is_tautology(&self) -> bool { if self.b < 0 { - false - } else { - self.b as usize >= self.weight_sum + return false; } + self.b as usize >= self.weight_sum } /// Checks if the constraint is unsatisfiable @@ -795,6 +822,18 @@ impl PBUBConstr { self.b < 0 } + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { + if self.is_unsat() { + return false; + } + let min_coeff: usize = self + .lits + .iter() + .fold(usize::MAX, |min, (_, coeff)| std::cmp::min(min, *coeff)); + min_coeff > self.b as usize + } + /// Gets the unit weight of the constraint, if it exists pub fn find_unit_weight(&self) -> Option { let mut unit_weight = None; @@ -848,19 +887,22 @@ impl PBLBConstr { /// Checks if the constraint is unsatisfiable pub fn is_unsat(&self) -> bool { if self.b < 0 { - false - } else { - self.b as usize > self.weight_sum + return false; } + self.b as usize > self.weight_sum } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { - if self.b < 0 { - false - } else { - self.b as usize == self.weight_sum + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { + if self.b < 0 || self.is_unsat() { + return false; } + let min_coeff: usize = self + .lits + .iter() + .fold(usize::MAX, |min, (_, coeff)| std::cmp::min(min, *coeff)); + // note: self.b <= self.weight_sum is checked in is_unsat + self.b as usize + min_coeff > self.weight_sum } /// Gets the unit weight of the constraint, if it exists @@ -911,19 +953,25 @@ impl PBEQConstr { /// Checks if the constraint is unsatisfiable pub fn is_unsat(&self) -> bool { if self.b < 0 { - true - } else { - self.b as usize > self.weight_sum + return true; + } + self.b as usize > self.weight_sum + } + + /// Checks if the constraint assigns all literals to true + pub fn is_positive_assignment(&self) -> bool { + if self.b < 0 { + return false; } + self.b as usize == self.weight_sum } - /// Checks if the constraint is an assignment - pub fn is_assignment(&self) -> bool { + /// Checks if the constraint assigns all literals to false + pub fn is_negative_assignment(&self) -> bool { if self.b < 0 { - false - } else { - self.b as usize == self.weight_sum + return false; } + self.b as usize == 0 } /// Gets the unit weight of the constraint, if it exists @@ -1010,13 +1058,23 @@ mod tests { } #[test] - fn card_is_assignment() { + fn card_is_positive_assignment() { let lits = vec![lit![0], lit![1], lit![2]]; - assert!(!CardConstraint::new_ub(lits.clone(), 1).is_assignment()); - assert!(CardConstraint::new_lb(lits.clone(), 3).is_assignment()); - assert!(!CardConstraint::new_lb(lits.clone(), 2).is_assignment()); - assert!(CardConstraint::new_eq(lits.clone(), 3).is_assignment()); - assert!(!CardConstraint::new_eq(lits.clone(), 2).is_assignment()); + assert!(!CardConstraint::new_ub(lits.clone(), 1).is_positive_assignment()); + assert!(CardConstraint::new_lb(lits.clone(), 3).is_positive_assignment()); + assert!(!CardConstraint::new_lb(lits.clone(), 2).is_positive_assignment()); + assert!(CardConstraint::new_eq(lits.clone(), 3).is_positive_assignment()); + assert!(!CardConstraint::new_eq(lits.clone(), 2).is_positive_assignment()); + } + + #[test] + fn card_is_negative_assignment() { + let lits = vec![lit![0], lit![1], lit![2]]; + assert!(CardConstraint::new_ub(lits.clone(), 0).is_negative_assignment()); + assert!(!CardConstraint::new_ub(lits.clone(), 1).is_negative_assignment()); + assert!(!CardConstraint::new_lb(lits.clone(), 2).is_negative_assignment()); + assert!(CardConstraint::new_eq(lits.clone(), 0).is_negative_assignment()); + assert!(!CardConstraint::new_eq(lits.clone(), 1).is_negative_assignment()); } #[test] @@ -1049,13 +1107,23 @@ mod tests { } #[test] - fn pb_is_assignment() { + fn pb_is_positive_assignment() { let lits = vec![(lit![0], 1), (lit![1], 2), (lit![2], 3)]; - assert!(!PBConstraint::new_ub(lits.clone(), 1).is_assignment()); - assert!(PBConstraint::new_lb(lits.clone(), 6).is_assignment()); - assert!(!PBConstraint::new_lb(lits.clone(), 2).is_assignment()); - assert!(PBConstraint::new_eq(lits.clone(), 6).is_assignment()); - assert!(!PBConstraint::new_eq(lits.clone(), 2).is_assignment()); + assert!(!PBConstraint::new_ub(lits.clone(), 1).is_positive_assignment()); + assert!(PBConstraint::new_lb(lits.clone(), 6).is_positive_assignment()); + assert!(!PBConstraint::new_lb(lits.clone(), 2).is_positive_assignment()); + assert!(PBConstraint::new_eq(lits.clone(), 6).is_positive_assignment()); + assert!(!PBConstraint::new_eq(lits.clone(), 2).is_positive_assignment()); + } + + #[test] + fn pb_is_negative_assignment() { + let lits = vec![(lit![0], 2), (lit![1], 2), (lit![2], 3)]; + assert!(PBConstraint::new_ub(lits.clone(), 1).is_negative_assignment()); + assert!(!PBConstraint::new_ub(lits.clone(), 2).is_negative_assignment()); + assert!(!PBConstraint::new_lb(lits.clone(), 2).is_negative_assignment()); + assert!(PBConstraint::new_eq(lits.clone(), 0).is_negative_assignment()); + assert!(!PBConstraint::new_eq(lits.clone(), 1).is_negative_assignment()); } #[test]