improved assignment detection

src/encodings/card.rs

@@ -300,12 +300,18 @@ pub fn encode_cardinality_constraint<CE: BoundBoth>(
         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());

src/encodings/pb.rs

@@ -314,7 +314,13 @@ pub fn encode_pb_constraint<PBE: BoundBoth>(
         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));

src/instances/sat.rs

@@ -548,13 +548,20 @@ impl<VM: ManageVars> SatInstance<VM> {
                     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<VM: ManageVars> SatInstance<VM> {
                     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;

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,17 +812,28 @@ 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
     pub fn is_unsat(&self) -> bool {
         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<usize> {
         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]