diff --git a/ci/scheduling.py b/ci/scheduling.py index 23ad7f05..fb90c8ff 100755 --- a/ci/scheduling.py +++ b/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) - - diff --git a/solver/src/core/literals/disjunction.rs b/solver/src/core/literals/disjunction.rs index a610730b..926c8605 100644 --- a/solver/src/core/literals/disjunction.rs +++ b/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, +} + +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 + '_ { + self.upper_bounds + .iter() + .map(|(k, v)| Lit::from_parts(*k, UpperBound::ub(*v))) + } +} + +impl From 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); + } + } } diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index b9e21777..2cb886cc 100644 --- a/solver/src/core/state/domains.rs +++ b/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,7 +466,7 @@ 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) } } } @@ -474,7 +474,7 @@ impl Domains { // 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, }; }