From b69336774991543543f23a0135112c71f8772cef Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 22 Nov 2023 17:23:11 +0100 Subject: [PATCH 1/7] feat(cp): Reactivate watch-based propagation of linear constraints. --- solver/src/reasoners/cp/mod.rs | 36 ++++++++++++++++------------------ 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 58b149ae..a34a3915 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -141,14 +141,12 @@ impl Propagator for LinearSumLeq { for e in &self.elements { if !e.is_constant() { - match e.factor.cmp(&0) { - Ordering::Less => context.add_watch(SignedVar::plus(e.var), id), - Ordering::Equal => {} - Ordering::Greater => context.add_watch(SignedVar::minus(e.var), id), - } + context.add_watch(SignedVar::plus(e.var), id); + context.add_watch(SignedVar::minus(e.var), id); } if e.lit != Lit::TRUE { context.add_watch(e.lit.svar(), id); + context.add_watch(e.lit.svar().neg(), id); } } } @@ -355,21 +353,21 @@ impl Theory for Cp { } fn propagate(&mut self, domains: &mut Domains) -> Result<(), Contradiction> { - // TODO: at this point, all propagators are invoked regardless of watches - // if self.saved == DecLvl::ROOT { - for (id, p) in self.constraints.entries() { - let cause = self.id.cause(id); - p.constraint.propagate(domains, cause)?; + if self.saved == DecLvl::ROOT { + // in first propagation, propagate everyone + for (id, p) in self.constraints.entries() { + let cause = self.id.cause(id); + p.constraint.propagate(domains, cause)?; + } + } + while let Some(event) = self.model_events.pop(domains.trail()).copied() { + let watchers = self.watches.get(event.affected_bound); + for &watcher in watchers { + let constraint = self.constraints[watcher].constraint.as_ref(); + let cause = self.id.cause(watcher); + constraint.propagate(domains, cause)?; + } } - // } - // while let Some(event) = self.model_events.pop(domains.trail()).copied() { - // let watchers = self.watches.get(event.affected_bound); - // for &watcher in watchers { - // let constraint = self.constraints[watcher].constraint.as_ref(); - // let cause = self.id.cause(watcher); - // constraint.propagate(&event, domains, cause)?; - // } - // } Ok(()) } From fa525cd8bd64f57c8099f34a27532bea9bcb3c2e Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 22 Nov 2023 17:25:58 +0100 Subject: [PATCH 2/7] chore(cp): Make watches on VarRef (less error prone than SVar) --- solver/src/reasoners/cp/mod.rs | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index a34a3915..3bf1b2b0 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -141,12 +141,10 @@ impl Propagator for LinearSumLeq { for e in &self.elements { if !e.is_constant() { - context.add_watch(SignedVar::plus(e.var), id); - context.add_watch(SignedVar::minus(e.var), id); + context.add_watch(e.var, id); } if e.lit != Lit::TRUE { - context.add_watch(e.lit.svar(), id); - context.add_watch(e.lit.svar().neg(), id); + context.add_watch(e.lit.svar().variable(), id); } } } @@ -275,19 +273,19 @@ impl From for DynPropagator { #[derive(Clone, Default)] pub struct Watches { - propagations: HashMap>, + propagations: HashMap>, empty: [PropagatorId; 0], } impl Watches { - fn add_watch(&mut self, watched: SignedVar, propagator_id: PropagatorId) { + fn add_watch(&mut self, watched: VarRef, propagator_id: PropagatorId) { self.propagations .entry(watched) .or_insert_with(|| Vec::with_capacity(4)) .push(propagator_id) } - fn get(&self, var_bound: SignedVar) -> &[PropagatorId] { + fn get(&self, var_bound: VarRef) -> &[PropagatorId] { self.propagations .get(&var_bound) .map(|v| v.as_slice()) @@ -361,7 +359,7 @@ impl Theory for Cp { } } while let Some(event) = self.model_events.pop(domains.trail()).copied() { - let watchers = self.watches.get(event.affected_bound); + let watchers = self.watches.get(event.affected_bound.variable()); for &watcher in watchers { let constraint = self.constraints[watcher].constraint.as_ref(); let cause = self.id.cause(watcher); From 22771d96788c742f257c92d1a0cf7954808f66ae Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 22 Nov 2023 17:34:49 +0100 Subject: [PATCH 3/7] feat(cp): Only trigger propagation once per constraint. --- solver/src/reasoners/cp/mod.rs | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 3bf1b2b0..464e8253 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -11,7 +11,7 @@ use crate::reasoners::{Contradiction, ReasonerId, Theory}; use anyhow::Context; use num_integer::{div_ceil, div_floor}; use std::cmp::Ordering; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; // =========== Sum =========== @@ -351,21 +351,29 @@ impl Theory for Cp { } fn propagate(&mut self, domains: &mut Domains) -> Result<(), Contradiction> { + // list of all propagators to trigger + let mut to_propagate = HashSet::with_capacity(64); + + // in first propagation, propagate everyone if self.saved == DecLvl::ROOT { - // in first propagation, propagate everyone for (id, p) in self.constraints.entries() { - let cause = self.id.cause(id); - p.constraint.propagate(domains, cause)?; + to_propagate.insert(id); } } + + // add any propagator that watched a changed variable since last propagation while let Some(event) = self.model_events.pop(domains.trail()).copied() { let watchers = self.watches.get(event.affected_bound.variable()); for &watcher in watchers { - let constraint = self.constraints[watcher].constraint.as_ref(); - let cause = self.id.cause(watcher); - constraint.propagate(domains, cause)?; + to_propagate.insert(watcher); } } + + for propagator in to_propagate { + let constraint = self.constraints[propagator].constraint.as_ref(); + let cause = self.id.cause(propagator); + constraint.propagate(domains, cause)?; + } Ok(()) } From 174473fc4dc5e0c0dba32afc795f4b707813b3f2 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 22 Nov 2023 17:43:27 +0100 Subject: [PATCH 4/7] chore(cp): Clean up internal conversions from/to i64. --- solver/src/reasoners/cp/mod.rs | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 464e8253..342eab18 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -68,17 +68,16 @@ impl std::fmt::Display for LinearSumLeq { } impl LinearSumLeq { - fn get_lower_bound(&self, elem: SumElem, domains: &Domains) -> IntCst { + fn get_lower_bound(&self, elem: SumElem, domains: &Domains) -> i64 { let var_is_present = domains.present(elem.var) == Some(true); debug_assert!(!domains.entails(elem.lit) || var_is_present); let int_part = match elem.factor.cmp(&0) { - Ordering::Less => domains.ub(elem.var), + Ordering::Less => domains.ub(elem.var) as i64, Ordering::Equal => 0, - Ordering::Greater => domains.lb(elem.var), + Ordering::Greater => domains.lb(elem.var) as i64, } - .saturating_mul(elem.factor) - .clamp(INT_CST_MIN, INT_CST_MAX); + .saturating_mul(elem.factor as i64); match domains.value(elem.lit) { Some(true) => int_part, @@ -86,17 +85,16 @@ impl LinearSumLeq { None => 0.min(int_part), } } - fn get_upper_bound(&self, elem: SumElem, domains: &Domains) -> IntCst { + fn get_upper_bound(&self, elem: SumElem, domains: &Domains) -> i64 { let var_is_present = domains.present(elem.var) == Some(true); debug_assert!(!domains.entails(elem.lit) || var_is_present); let int_part = match elem.factor.cmp(&0) { - Ordering::Less => domains.lb(elem.var), + Ordering::Less => domains.lb(elem.var) as i64, Ordering::Equal => 0, - Ordering::Greater => domains.ub(elem.var), + Ordering::Greater => domains.ub(elem.var) as i64, } - .saturating_mul(elem.factor) - .clamp(INT_CST_MIN, INT_CST_MAX); + .saturating_mul(elem.factor as i64); match domains.value(elem.lit) { Some(true) => int_part, @@ -104,7 +102,9 @@ impl LinearSumLeq { None => 0.max(int_part), } } - fn set_ub(&self, elem: SumElem, ub: IntCst, domains: &mut Domains, cause: Cause) -> Result { + fn set_ub(&self, elem: SumElem, ub: i64, domains: &mut Domains, cause: Cause) -> Result { + // convert back to i32 (which is used for domains). Clamping should prevent any conversion error. + let ub = ub.clamp(INT_CST_MIN as i64, INT_CST_MAX as i64) as i32; debug_assert!(!domains.entails(elem.lit) || domains.present(elem.var) == Some(true)); // println!( // " {:?} : [{}, {}] ub: {ub} -> {}", @@ -156,7 +156,7 @@ impl Propagator for LinearSumLeq { .iter() .copied() .filter(|e| !domains.entails(!e.lit)) - .map(|e| self.get_lower_bound(e, domains) as i64) + .map(|e| self.get_lower_bound(e, domains)) .sum(); let f = (self.ub as i64) - sum_lb; // println!("Propagation : {} <= {}", sum_lb, self.ub); @@ -168,13 +168,12 @@ impl Propagator for LinearSumLeq { return Err(Contradiction::Explanation(expl)); } for &e in &self.elements { - let lb = self.get_lower_bound(e, domains) as i64; - let ub = self.get_upper_bound(e, domains) as i64; + let lb = self.get_lower_bound(e, domains); + let ub = self.get_upper_bound(e, domains); debug_assert!(lb <= ub); if ub - lb > f { // println!(" problem on: {e:?} {lb} {ub}"); - // NOTE: Conversion from i64 to i32 should not fail due to the clamp between two i32 values. - let new_ub = (f + lb).clamp(INT_CST_MIN as i64, INT_CST_MAX as i64) as i32; + let new_ub = (f + lb); match self.set_ub(e, new_ub, domains, cause) { Ok(true) => {} // println!(" propagated: {e:?} <= {}", f + lb), Ok(false) => {} From a4c362680c939a8fd494b21336ec749a66dc6d8f Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Wed, 22 Nov 2023 17:51:54 +0100 Subject: [PATCH 5/7] chore(cp): fix compilation errors in tests --- solver/src/reasoners/cp/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 342eab18..d9d347ab 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -472,8 +472,8 @@ mod tests { /* =============================== Helpers ============================== */ fn check_bounds(s: &LinearSumLeq, e: SumElem, d: &Domains, lb: IntCst, ub: IntCst) { - assert_eq!(s.get_lower_bound(e, d), lb); - assert_eq!(s.get_upper_bound(e, d), ub); + assert_eq!(s.get_lower_bound(e, d), lb.into()); + assert_eq!(s.get_upper_bound(e, d), ub.into()); } fn check_bounds_var(v: VarRef, d: &Domains, lb: IntCst, ub: IntCst) { From b24c79cdb726c3de4eb6d34cc3fa61608e22ebad Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 24 Nov 2023 11:31:04 +0100 Subject: [PATCH 6/7] chore(cp): Remove old code. --- solver/src/reasoners/cp/mod.rs | 62 ++++------------------------------ 1 file changed, 7 insertions(+), 55 deletions(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index d9d347ab..4a0df437 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -106,13 +106,7 @@ impl LinearSumLeq { // convert back to i32 (which is used for domains). Clamping should prevent any conversion error. let ub = ub.clamp(INT_CST_MIN as i64, INT_CST_MAX as i64) as i32; debug_assert!(!domains.entails(elem.lit) || domains.present(elem.var) == Some(true)); - // println!( - // " {:?} : [{}, {}] ub: {ub} -> {}", - // var, - // domains.lb(var), - // domains.ub(var), - // ub / elem.factor, - // ); + match elem.factor.cmp(&0) { Ordering::Less => domains.set_lb(elem.var, div_ceil(ub, elem.factor), cause), Ordering::Equal => unreachable!(), @@ -137,8 +131,6 @@ impl LinearSumLeq { impl Propagator for LinearSumLeq { fn setup(&self, id: PropagatorId, context: &mut Watches) { - // println!("SET UP"); - for e in &self.elements { if !e.is_constant() { context.add_watch(e.var, id); @@ -159,10 +151,9 @@ impl Propagator for LinearSumLeq { .map(|e| self.get_lower_bound(e, domains)) .sum(); let f = (self.ub as i64) - sum_lb; - // println!("Propagation : {} <= {}", sum_lb, self.ub); - // self.print(domains); + if f < 0 { - // println!("INCONSISTENT"); + // INCONSISTENT let mut expl = Explanation::new(); self.explain(Lit::FALSE, domains, &mut expl); return Err(Contradiction::Explanation(expl)); @@ -172,11 +163,10 @@ impl Propagator for LinearSumLeq { let ub = self.get_upper_bound(e, domains); debug_assert!(lb <= ub); if ub - lb > f { - // println!(" problem on: {e:?} {lb} {ub}"); let new_ub = (f + lb); match self.set_ub(e, new_ub, domains, cause) { - Ok(true) => {} // println!(" propagated: {e:?} <= {}", f + lb), - Ok(false) => {} + Ok(true) => {} // domain updated + Ok(false) => {} // no-op Err(err) => { // If the update is invalid, a solution could be to force the element to not be present. if !domains.entails(e.lit) { @@ -194,9 +184,6 @@ impl Propagator for LinearSumLeq { } } } - // println!("AFTER PROP"); - // self.print(domains); - // println!(); Ok(()) } @@ -223,8 +210,6 @@ impl Propagator for LinearSumLeq { } } } - // dbg!(&self); - // dbg!(&out_explanation.lits); } fn clone_box(&self) -> Box { @@ -353,7 +338,8 @@ impl Theory for Cp { // list of all propagators to trigger let mut to_propagate = HashSet::with_capacity(64); - // in first propagation, propagate everyone + // in first propagation, mark everything for propagation + // NOte: this is might actually be trigger multiple times when going back to the root if self.saved == DecLvl::ROOT { for (id, p) in self.constraints.entries() { to_propagate.insert(id); @@ -406,40 +392,6 @@ impl Backtrack for Cp { } } -// impl BindSplit for Cp { -// fn enforce_true(&mut self, expr: &Expr, _doms: &mut Domains) -> BindingResult { -// if let Some(leq) = downcast::(expr) { -// let elements = leq -// .sum -// .iter() -// .map(|e| SumElem { -// factor: e.factor, -// var: e.var, -// or_zero: e.or_zero, -// }) -// .collect(); -// let propagator = LinearSumLeq { -// elements, -// ub: leq.upper_bound, -// }; -// self.add_propagator(propagator); -// BindingResult::Enforced -// } else { -// BindingResult::Unsupported -// } -// } -// -// fn enforce_false(&mut self, _expr: &Expr, _doms: &mut Domains) -> BindingResult { -// // TODO -// BindingResult::Unsupported -// } -// -// fn enforce_eq(&mut self, _literal: Lit, _expr: &Expr, _doms: &mut Domains) -> BindingResult { -// // TODO -// BindingResult::Unsupported -// } -// } - /* ========================================================================== */ /* Tests */ /* ========================================================================== */ From ff586edbe2821773d584a88d3796d2d9901af133 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 24 Nov 2023 12:38:31 +0100 Subject: [PATCH 7/7] fix(cp): Add missing watch in linear propagator. --- solver/src/reasoners/cp/mod.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 4a0df437..94517fca 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -131,6 +131,7 @@ impl LinearSumLeq { impl Propagator for LinearSumLeq { fn setup(&self, id: PropagatorId, context: &mut Watches) { + context.add_watch(self.active.variable(), id); for e in &self.elements { if !e.is_constant() { context.add_watch(e.var, id); @@ -163,7 +164,7 @@ impl Propagator for LinearSumLeq { let ub = self.get_upper_bound(e, domains); debug_assert!(lb <= ub); if ub - lb > f { - let new_ub = (f + lb); + let new_ub = f + lb; match self.set_ub(e, new_ub, domains, cause) { Ok(true) => {} // domain updated Ok(false) => {} // no-op