Merge pull request #136 from plaans/fix/135

fix(sat): derived clause were incorretly too strong in some corner cases

Author: arbimo

ci/scheduling.py

@@ -12,10 +12,12 @@
 solver_cmd = solver + " {kind} {instance} --expected-makespan {makespan}"
 
 instances = [
-    ("jobshop", "examples/scheduling/instances/jobshop/ft06.jsp", 55),
-    ("jobshop", "examples/scheduling/instances/jobshop/la01.jsp", 666),
-    ("openshop", "examples/scheduling/instances/openshop/taillard/tai04_04_01.osp", 193),
-]
+                ("jobshop", "examples/scheduling/instances/jobshop/ft06.jsp", 55),
+                ("jobshop", "examples/scheduling/instances/jobshop/la01.jsp", 666),
+                ("openshop", "examples/scheduling/instances/openshop/taillard/tai04_04_01.osp", 193),
+            ] + [
+                ("jobshop", "examples/scheduling/instances/jobshop/orb05.jsp", 887),
+            ] * 30
 
 for (kind, instance, makespan) in instances:
     cmd = solver_cmd.format(kind=kind, instance=instance, makespan=makespan).split(" ")
@@ -24,5 +26,3 @@
     if solver_run.returncode != 0:
         print("Solver did not return expected result")
         exit(1)
-
-

solver/src/core/literals/disjunction.rs

@@ -1,5 +1,7 @@
 use crate::core::*;
+use itertools::Itertools;
 use std::borrow::Borrow;
+use std::collections::HashMap;
 use std::fmt::{Debug, Formatter};
 
 /// A set of literals representing a disjunction.
@@ -145,9 +147,57 @@ impl AsRef<[Lit]> for Disjunction {
     }
 }
 
+/// A builder for a disjunction that avoids duplicated literals
+#[derive(Default, Clone)]
+pub struct DisjunctionBuilder {
+    upper_bounds: HashMap<SignedVar, IntCst>,
+}
+
+impl DisjunctionBuilder {
+    pub fn new() -> Self {
+        Default::default()
+    }
+
+    pub fn with_capacity(n: usize) -> Self {
+        Self {
+            upper_bounds: HashMap::with_capacity(n),
+        }
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.upper_bounds.is_empty()
+    }
+
+    pub fn push(&mut self, lit: Lit) {
+        let sv = lit.svar();
+        let ub = lit.bound_value().as_int();
+        let new_ub = if let Some(prev) = self.upper_bounds.get(&sv) {
+            // (sv <= ub) || (sv <= prev)  <=> (sv <= max(ub, prev))
+            ub.max(*prev)
+        } else {
+            ub
+        };
+        self.upper_bounds.insert(sv, new_ub);
+    }
+
+    pub fn literals(&self) -> impl Iterator<Item = Lit> + '_ {
+        self.upper_bounds
+            .iter()
+            .map(|(k, v)| Lit::from_parts(*k, UpperBound::ub(*v)))
+    }
+}
+
+impl From<DisjunctionBuilder> for Disjunction {
+    fn from(value: DisjunctionBuilder) -> Self {
+        Disjunction::new(value.literals().collect_vec())
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
+    use rand::seq::SliceRandom;
+    use rand::thread_rng;
 
     fn leq(var: VarRef, val: IntCst) -> Lit {
         Lit::leq(var, val)
@@ -213,4 +263,33 @@ mod tests {
         assert!(Disjunction::new(vec![leq(a, 0), geq(a, 1)]).is_tautology());
         assert!(Disjunction::new(vec![leq(a, 0), leq(b, 0), geq(b, 2), !leq(a, 0)]).is_tautology());
     }
+
+    #[test]
+    fn test_builder() {
+        let vars = (0..10).map(VarRef::from_u32);
+
+        let vals = 0..10;
+
+        // create a large set of literals from which to generate disjunction
+        let mut lits = Vec::new();
+        for var in vars {
+            for val in vals.clone() {
+                lits.push(Lit::geq(var, val));
+                lits.push(Lit::leq(var, val));
+            }
+        }
+
+        // select many subsets of the literals and test if going through the builder yields the correct output
+        for _ in 0..100 {
+            lits.shuffle(&mut thread_rng());
+            let subset = &lits[0..30];
+            let disj = Disjunction::new(subset.to_vec());
+            let mut builder = DisjunctionBuilder::new();
+            for l in subset {
+                builder.push(*l);
+            }
+            let built: Disjunction = builder.into();
+            assert_eq!(disj, built);
+        }
+    }
 }

solver/src/core/state/domains.rs

@@ -1,6 +1,6 @@
 use crate::backtrack::{Backtrack, DecLvl, DecisionLevelClass, EventIndex, ObsTrail};
 use crate::collections::ref_store::RefMap;
-use crate::core::literals::{Disjunction, ImplicationGraph, LitSet};
+use crate::core::literals::{Disjunction, DisjunctionBuilder, ImplicationGraph, LitSet};
 use crate::core::state::cause::{DirectOrigin, Origin};
 use crate::core::state::event::Event;
 use crate::core::state::int_domains::IntDomains;
@@ -446,7 +446,7 @@ impl Domains {
         // literals falsified at the current decision level, we need to proceed until there is a single one left (1UIP)
         self.queue.clear();
         // literals that are beyond the current decision level and will be part of the final clause
-        let mut result: LitSet = LitSet::with_capacity(128);
+        let mut result: DisjunctionBuilder = DisjunctionBuilder::with_capacity(32);
 
         let decision_level = self.current_decision_level();
         let mut resolved = LitSet::new();
@@ -466,15 +466,15 @@ impl Domains {
                             }
                             DecisionLevelClass::Intermediate => {
                                 // implied before the current decision level, the negation of the literal will appear in the final clause (1UIP)
-                                result.insert(!l)
+                                result.push(!l)
                             }
                         }
                     }
                 } else {
                     // the event is not entailed, must be part of an eager propagation
                     // Even if it was not necessary for this propagation to occur, it must be part of
                     // the clause for correctness
-                    result.insert(!l)
+                    result.push(!l)
                 }
             }
             debug_assert!(explanation.lits.is_empty());
@@ -487,7 +487,7 @@ impl Domains {
                 // if we were at the root decision level, we should have derived the empty clause
                 debug_assert!(decision_level != DecLvl::ROOT || result.is_empty());
                 return Conflict {
-                    clause: Disjunction::new(result.into()),
+                    clause: result.into(),
                     resolved,
                 };
             }
@@ -526,9 +526,9 @@ impl Domains {
                 // the content of result is a conjunction of literal that imply `!l`
                 // build the conflict clause and exit
                 debug_assert!(self.queue.is_empty());
-                result.insert(!l.lit);
+                result.push(!l.lit);
                 return Conflict {
-                    clause: Disjunction::new(result.into()),
+                    clause: result.into(),
                     resolved,
                 };
             }