From b7d841553899914ad248d0f81c759c888ab71d2d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 3 Sep 2024 17:27:01 +1000 Subject: [PATCH] Add int_abs bounds consistent propagator --- crates/huub/src/model/constraint.rs | 33 +++++ crates/huub/src/propagator.rs | 1 + crates/huub/src/propagator/int_abs.rs | 179 ++++++++++++++++++++++++++ share/minizinc/huub/redefinitions.mzn | 2 - 4 files changed, 213 insertions(+), 2 deletions(-) create mode 100644 crates/huub/src/propagator/int_abs.rs diff --git a/crates/huub/src/model/constraint.rs b/crates/huub/src/model/constraint.rs index 06d2464d..4e9c9b62 100644 --- a/crates/huub/src/model/constraint.rs +++ b/crates/huub/src/model/constraint.rs @@ -16,6 +16,7 @@ use crate::{ array_int_minimum::ArrayIntMinimumBounds, array_var_int_element::ArrayVarIntElementBounds, disjunctive_stict::DisjunctiveStrictEdgeFinding, + int_abs::IntAbsBounds, int_div::IntDivBounds, int_lin_le::{IntLinearLessEqBounds, IntLinearLessEqImpBounds}, int_lin_ne::{IntLinearNotEqImpValue, IntLinearNotEqValue}, @@ -38,6 +39,7 @@ pub enum Constraint { ArrayVarBoolElement(Vec, IntView, BoolExpr), ArrayVarIntElement(Vec, IntView, IntView), DisjunctiveStrict(Vec, Vec), + IntAbs(IntView, IntView), IntDiv(IntView, IntView, IntView), IntLinEq(Vec, IntVal), IntLinEqImp(Vec, IntVal, BoolExpr), @@ -182,6 +184,12 @@ impl Constraint { ))?; Ok(()) } + Constraint::IntAbs(origin, abs) => { + let origin = origin.to_arg(slv, map); + let abs = abs.to_arg(slv, map); + slv.add_propagator(IntAbsBounds::prepare(origin, abs))?; + Ok(()) + } Constraint::IntDiv(numerator, denominator, result) => { let numerator = numerator.to_arg(slv, map); let denominator = denominator.to_arg(slv, map); @@ -485,6 +493,31 @@ impl Model { } Some(Constraint::DisjunctiveStrict(starts, durations)) } + Constraint::IntAbs(origin, abs) => { + let lb = self.get_int_lower_bound(&origin); + let ub = self.get_int_upper_bound(&origin); + if ub < 0 { + self.set_int_lower_bound(&abs, -ub, con)?; + self.set_int_upper_bound(&abs, -lb, con)?; + } else if lb >= 0 { + self.set_int_lower_bound(&abs, lb, con)?; + self.set_int_upper_bound(&abs, ub, con)?; + } else { + self.set_int_lower_bound(&abs, 0, con)?; + let abs_max = ub.max(-lb); + self.set_int_upper_bound(&abs, abs_max, con)?; + } + let abs_ub = ub.abs(); + debug_assert!(abs_ub >= 0); + self.set_int_lower_bound(&origin, -abs_ub, con)?; + self.set_int_upper_bound(&abs, abs_ub, con)?; + if lb >= 0 { + // TODO: Unify + Some(Constraint::IntLinEq(vec![origin, -abs], 0)) + } else { + Some(Constraint::IntAbs(origin, abs)) + } + } Constraint::IntDiv(num, denom, res) => { self.diff_int_domain(&denom, &RangeList::from(0..=0), con)?; Some(Constraint::IntDiv(num, denom, res)) diff --git a/crates/huub/src/propagator.rs b/crates/huub/src/propagator.rs index 4ac74fb6..c695229a 100644 --- a/crates/huub/src/propagator.rs +++ b/crates/huub/src/propagator.rs @@ -3,6 +3,7 @@ pub(crate) mod array_int_minimum; pub(crate) mod array_var_int_element; pub(crate) mod conflict; pub(crate) mod disjunctive_stict; +pub(crate) mod int_abs; pub(crate) mod int_div; pub(crate) mod int_event; pub(crate) mod int_lin_le; diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs new file mode 100644 index 00000000..f5d9907f --- /dev/null +++ b/crates/huub/src/propagator/int_abs.rs @@ -0,0 +1,179 @@ +use std::iter::once; + +use crate::{ + actions::{ + explanation::ExplanationActions, initialization::InitializationActions, + trailing::TrailingActions, + }, + propagator::{conflict::Conflict, int_event::IntEvent, PropagationActions, Propagator}, + solver::{ + engine::queue::PriorityLevel, + poster::{BoxedPropagator, Poster, QueuePreferences}, + }, + IntView, LitMeaning, ReformulationError, +}; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Bounds propagator for one integer variable being the absolute value of another +pub(crate) struct IntAbsBounds { + /// The integer variable whose absolute value is being taken + origin: IntView, + /// Whether the bounds of the origin variable have changed since the last propagation + orig_changed: bool, + /// The integer variable representing the absolute value + abs: IntView, + /// Whether the upper bound of the absolute value has changed since the last propagation + abs_changed: bool, +} + +struct IntAbsBoundsPoster { + origin: IntView, + abs: IntView, +} + +impl IntAbsBounds { + pub(crate) fn prepare(origin: IntView, abs: IntView) -> impl Poster { + IntAbsBoundsPoster { origin, abs } + } +} + +impl Propagator for IntAbsBounds +where + P: PropagationActions, + E: ExplanationActions, + T: TrailingActions, +{ + fn notify_event(&mut self, data: u32, _: &IntEvent, _: &mut T) -> bool { + match data { + 1 => self.orig_changed = true, + 2 => self.abs_changed = true, + _ => unreachable!("unexpected event data"), + }; + true + } + + fn notify_backtrack(&mut self, _new_level: usize) { + self.orig_changed = false; + self.abs_changed = false; + } + + #[tracing::instrument(name = "int_abs", level = "trace", skip(self, actions))] + fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { + let (lb, ub) = actions.get_int_bounds(self.origin); + + if self.orig_changed { + self.orig_changed = false; + // If we know that the origin is negative, then just negate the bounds + if ub < 0 { + actions.set_int_upper_bound(self.abs, -lb, |a: &mut P| { + vec![ + a.get_int_lower_bound_lit(self.origin), + a.get_int_lit(self.origin, LitMeaning::Less(0)), + ] + })?; + actions.set_int_lower_bound(self.abs, -ub, |a: &mut P| { + once(a.get_int_upper_bound_lit(self.origin)) + })?; + } else if lb >= 0 { + // If we know that the origin is positive, then the bounds are the same + actions.set_int_lower_bound(self.abs, lb, |a: &mut P| { + once(a.get_int_lower_bound_lit(self.origin)) + })?; + actions.set_int_upper_bound(self.abs, ub, |a: &mut P| { + vec![ + a.get_int_upper_bound_lit(self.origin), + a.get_int_lit(self.origin, LitMeaning::GreaterEq(0)), + ] + })?; + } else { + // If the origin can be either positive or negative, then the bounds are the maximum of the absolute values + let abs_max = ub.max(-lb); + actions.set_int_upper_bound(self.abs, abs_max, |a: &mut P| { + vec![ + a.get_int_lit(self.origin, LitMeaning::GreaterEq(-abs_max)), + a.get_int_lit(self.origin, LitMeaning::Less(abs_max + 1)), + ] + })?; + } + } + + if self.abs_changed { + self.abs_changed = false; + let ub = actions.get_int_upper_bound(self.abs); + let ub_lit = actions.get_int_upper_bound_lit(self.abs); + actions.set_int_lower_bound(self.origin, -ub, ub_lit)?; + actions.set_int_upper_bound(self.origin, ub, ub_lit)?; + } + + Ok(()) + } +} + +impl Poster for IntAbsBoundsPoster { + fn post( + self, + actions: &mut I, + ) -> Result<(BoxedPropagator, QueuePreferences), ReformulationError> { + // Subscribe to both bounds of the origin variable + actions.subscribe_int(self.origin, IntEvent::Bounds, 1); + // Subscribe only to the upper bound of the absolute value variable + actions.subscribe_int(self.abs, IntEvent::UpperBound, 2); + + Ok(( + Box::new(IntAbsBounds { + origin: self.origin, + orig_changed: false, + abs: self.abs, + abs_changed: false, + }), + QueuePreferences { + enqueue_on_post: false, + priority: PriorityLevel::Highest, + }, + )) + } +} + +#[cfg(test)] +mod tests { + use expect_test::expect; + use pindakaas::{solver::cadical::Cadical, Cnf}; + use rangelist::RangeList; + use tracing_test::traced_test; + + use crate::{ + propagator::int_abs::IntAbsBounds, + solver::engine::int_var::{EncodingType, IntVar}, + Solver, + }; + + #[test] + #[traced_test] + fn test_int_abs_sat() { + let mut slv: Solver = Cnf::default().into(); + let a = IntVar::new_in( + &mut slv, + (-3..=3).into(), + EncodingType::Eager, + EncodingType::Lazy, + ); + let b = IntVar::new_in( + &mut slv, + RangeList::from_iter([-3..=3]), + EncodingType::Eager, + EncodingType::Lazy, + ); + slv.add_propagator(IntAbsBounds::prepare(a, b)).unwrap(); + slv.expect_solutions( + &[a, b], + expect![[r#" + -3, 3 + -2, 2 + -1, 1 + 0, 0 + 1, 1 + 2, 2 + 3, 3"#]], + ); + } +} diff --git a/share/minizinc/huub/redefinitions.mzn b/share/minizinc/huub/redefinitions.mzn index dee74344..ca0978f7 100644 --- a/share/minizinc/huub/redefinitions.mzn +++ b/share/minizinc/huub/redefinitions.mzn @@ -4,8 +4,6 @@ predicate bool_lt(var bool: a, var bool: b) = not a /\ b; predicate bool_lt_imp(var bool: a, var bool: b, var bool: r) = r -> (not a /\ b); predicate bool_lt_reif(var bool: a, var bool: b, var bool: r) = r = (not a /\ b); -predicate int_abs(var int: a, var int: b) = b = [a,-a][1 + (a < 0)]; - predicate int_eq_imp(var int: a, var int: b, var bool: r); predicate int_le_imp(var int: a, var int: b, var bool: r); predicate int_ne_imp(var int: a, var int: b, var bool: r);