From f45ff2147444c725b3b2e541ebe5c99b258248a5 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 29 Oct 2024 07:56:57 +0100 Subject: [PATCH 01/15] chore(sum): better display --- solver/src/model/lang/linear.rs | 113 ++++++++++++++++++++++++++++---- 1 file changed, 100 insertions(+), 13 deletions(-) diff --git a/solver/src/model/lang/linear.rs b/solver/src/model/lang/linear.rs index 2127b182..fb967890 100644 --- a/solver/src/model/lang/linear.rs +++ b/solver/src/model/lang/linear.rs @@ -9,12 +9,9 @@ use std::collections::BTreeMap; /* LinearTerm */ /* ========================================================================== */ -/// A linear term of the form `a/b * X * P` where: +/// A linear term of the form `a/b * X` where: /// - `a` and `b` are integer constants /// - `X` is an integer variable. -/// - `P` is a non-optional literal interpreted as 0 if False and 1 if true. -/// -/// If `P` is true, it **required** that the expression is defined, meaning that both `X` and `P` are present. #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub struct LinearTerm { factor: IntCst, @@ -25,15 +22,19 @@ pub struct LinearTerm { impl std::fmt::Display for LinearTerm { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { if self.factor != 1 { - if self.factor < 0 { - write!(f, "({})", self.factor)?; + if self.factor == -1 { + write!(f, "-")?; } else { write!(f, "{}", self.factor)?; } + } + if self.factor.abs() != 1 && self.var != IVar::ONE { write!(f, "*")?; } if self.var != IVar::ONE { write!(f, "{:?}", self.var)?; + } else if self.factor.abs() == 1 { + write!(f, "1")?; } Ok(()) } @@ -123,10 +124,26 @@ pub struct LinearSum { impl std::fmt::Display for LinearSum { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { for (i, e) in self.terms.iter().enumerate() { - if i != 0 { + if e.factor < 0 { + if i != 0 { + write!(f, " - ")?; + } else { + write!(f, "-")?; + } + } else if i > 0 { write!(f, " + ")?; } - write!(f, "{e}")?; + if e.factor.abs() != 1 { + write!(f, "{}", e.factor.abs())?; + } + if e.factor.abs() != 1 && e.var != IVar::ONE { + write!(f, "*")?; + } + if e.var != IVar::ONE { + write!(f, "{:?}", e.var)?; + } else if e.factor.abs() == 1 { + write!(f, "1")?; + } } if self.constant != 0 { if !self.terms.is_empty() { @@ -247,7 +264,7 @@ impl LinearSum { terms: term_map .into_iter() .filter(|(v, f)| *f != 0 && *v != IVar::ZERO) - .filter(|(v, _)| !(*v == IVar::ONE)) // Has been grouped into the constant + .filter(|(v, _)| *v != IVar::ONE) // Has been grouped into the constant .map(|(v, f)| LinearTerm { factor: f, var: v, @@ -429,15 +446,19 @@ pub struct NFLinearSumItem { impl std::fmt::Display for NFLinearSumItem { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { if self.factor != 1 { - if self.factor < 0 { - write!(f, "({})", self.factor)?; + if self.factor == -1 { + write!(f, "-")?; } else { write!(f, "{}", self.factor)?; } + } + if self.factor.abs() != 1 && self.var != VarRef::ONE { write!(f, "*")?; } if self.var != VarRef::ONE { write!(f, "{:?}", self.var)?; + } else if self.factor.abs() == 1 { + write!(f, "1")?; } Ok(()) } @@ -468,12 +489,19 @@ impl std::fmt::Display for NFLinearLeq { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { for (i, e) in self.sum.iter().enumerate() { if e.factor < 0 { - write!(f, " - ")?; + if i != 0 { + write!(f, " - ")?; + } else { + write!(f, "-")?; + } } else if i > 0 { write!(f, " + ")?; } if e.factor.abs() != 1 { - write!(f, "{} * ", e.factor.abs())?; + write!(f, "{}", e.factor.abs())?; + } + if e.factor.abs() != 1 && e.var != VarRef::ONE { + write!(f, "*")?; } if e.var != VarRef::ONE { write!(f, "{:?}", e.var)?; @@ -705,6 +733,38 @@ mod tests { } } + #[test] + fn test_term_display() { + let var = IVar::new(VarRef::from_u32(5)); + // Constant terms + assert_eq!(format!("{}", LinearTerm::constant_int(1)), "1"); + assert_eq!(format!("{}", LinearTerm::constant_int(-1)), "-1"); + assert_eq!(format!("{}", LinearTerm::constant_int(5)), "5"); + assert_eq!(format!("{}", LinearTerm::constant_int(-5)), "-5"); + assert_eq!(format!("{}", LinearTerm::constant_rational(1, 10)), "1"); + assert_eq!(format!("{}", LinearTerm::constant_rational(-1, 10)), "-1"); + assert_eq!(format!("{}", LinearTerm::constant_rational(5, 10)), "5"); + assert_eq!(format!("{}", LinearTerm::constant_rational(-5, 10)), "-5"); + // Pseudo-constant terms + assert_eq!(format!("{}", LinearTerm::int(1, IVar::ONE)), "1"); + assert_eq!(format!("{}", LinearTerm::int(-1, IVar::ONE)), "-1"); + assert_eq!(format!("{}", LinearTerm::int(5, IVar::ONE)), "5"); + assert_eq!(format!("{}", LinearTerm::int(-5, IVar::ONE)), "-5"); + assert_eq!(format!("{}", LinearTerm::rational(1, IVar::ONE, 10)), "1"); + assert_eq!(format!("{}", LinearTerm::rational(-1, IVar::ONE, 10)), "-1"); + assert_eq!(format!("{}", LinearTerm::rational(5, IVar::ONE, 10)), "5"); + assert_eq!(format!("{}", LinearTerm::rational(-5, IVar::ONE, 10)), "-5"); + // Variable terms + assert_eq!(format!("{}", LinearTerm::int(1, var)), "var5"); + assert_eq!(format!("{}", LinearTerm::int(-1, var)), "-var5"); + assert_eq!(format!("{}", LinearTerm::int(5, var)), "5*var5"); + assert_eq!(format!("{}", LinearTerm::int(-5, var)), "-5*var5"); + assert_eq!(format!("{}", LinearTerm::rational(1, var, 10)), "var5"); + assert_eq!(format!("{}", LinearTerm::rational(-1, var, 10)), "-var5"); + assert_eq!(format!("{}", LinearTerm::rational(5, var, 10)), "5*var5"); + assert_eq!(format!("{}", LinearTerm::rational(-5, var, 10)), "-5*var5"); + } + /* =========================== LinearSum Tests ========================== */ #[test] @@ -1029,6 +1089,33 @@ mod tests { } } + #[test] + fn test_sum_display() { + let var = IVar::new(VarRef::from_u32(5)); + // Simple addition + let sum = LinearSum::of(vec![ + LinearTerm::rational(1, var, 10), + LinearTerm::constant_rational(5, 10), + LinearTerm::rational(5, var, 10), + LinearTerm::constant_rational(1, 10), + ]); + assert_eq!(format!("{}", sum), "var5 + 5 + 5*var5 + 1"); + // Simple subtraction + let sum = LinearSum::of(vec![ + LinearTerm::rational(1, var, 10), + LinearTerm::constant_rational(-5, 10), + LinearTerm::rational(-5, var, 10), + LinearTerm::constant_rational(-1, 10), + ]); + assert_eq!(format!("{}", sum), "var5 - 5 - 5*var5 - 1"); + // Complete subtraction + let sum = LinearSum::of(vec![ + LinearTerm::rational(-1, var, 10), + LinearTerm::constant_rational(-5, 10), + ]); + assert_eq!(format!("{}", sum), "-var5 - 5"); + } + /* ================================ Utils =============================== */ #[test] From 60fe545bc5288abe8ca50d3ace68b89f2d4d27c6 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 29 Oct 2024 07:56:57 +0100 Subject: [PATCH 02/15] chore(planning): repercussion of linear sum update & prepare redesign of numeric support constraints --- planning/planners/src/encode.rs | 415 +------------------ planning/planning/src/chronicles/concrete.rs | 8 +- planning/unified/plugin/up_aries/solver.py | 2 +- 3 files changed, 15 insertions(+), 410 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index f3a4f581..bfa5e30a 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -11,28 +11,14 @@ use aries::core::state::Conflict; use aries::core::*; use aries::model::extensions::{AssignmentExt, Shaped}; use aries::model::lang::linear::{LinearSum, LinearTerm}; -use aries::model::lang::{expr::*, Kind, Type}; +use aries::model::lang::{expr::*, Kind}; use aries::model::lang::{FAtom, FVar, IAtom, Variable}; -use aries::solver::Solver; use aries_planning::chronicles::constraints::encode_constraint; -use aries_planning::chronicles::printer::Printer; use aries_planning::chronicles::*; use env_param::EnvParam; use std::collections::{HashMap, HashSet}; -use std::convert::TryFrom; use std::ptr; -/// Parameter that activates the debug view of the resource constraints. -/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_DEBUG`. -/// Possible values are `false`(default) and `true`. -pub static RESOURCE_CONSTRAINT_DEBUG: EnvParam = EnvParam::new("ARIES_RESOURCE_CONSTRAINT_DEBUG", "false"); - -/// Parameter that activates the usage of timepoints to encode the increase's literals. -/// The parameter is loaded from the environment variable `ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS`. -/// Possible values are `false` and `true` (default). -pub static RESOURCE_CONSTRAINT_TIMEPOINTS: EnvParam = - EnvParam::new("ARIES_RESOURCE_CONSTRAINT_TIMEPOINTS", "true"); - /// Parameter that activates the temporal relaxation of temporal constraints of a task's /// interval and the its methods intervals. The temporal relaxation can be used when /// using an acting system to allow the interval of a method to be included in the interval @@ -410,9 +396,12 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto let action_costs: Vec = action_presence .iter() .map(|(ch_id, p)| { - model - .new_optional_ivar(1, 1, *p, Container::Instance(*ch_id).var(VarType::Cost)) - .or_zero(*p) + let var = model.new_ivar(0, 1, Container::Instance(*ch_id).var(VarType::Cost)); + let eq_0 = model.reify(eq(var, 0)); + let eq_1 = model.reify(eq(var, 1)); + model.enforce(implies(*p, eq_1), []); + model.enforce(implies(!*p, eq_0), []); + var.into() }) .collect(); let action_costs = LinearSum::of(action_costs); @@ -438,9 +427,12 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto let action_costs: Vec = costs .iter() .map(|&(ch_id, p, cost)| { - model - .new_optional_ivar(cost, cost, p, Container::Instance(ch_id).var(VarType::Cost)) - .or_zero(p) + let var = model.new_ivar(0, cost, Container::Instance(ch_id).var(VarType::Cost)); + let eq_0 = model.reify(eq(var, 0)); + let eq_cost = model.reify(eq(var, cost)); + model.enforce(implies(p, eq_cost), []); + model.enforce(implies(!p, eq_0), []); + var.into() }) .collect(); let action_costs = LinearSum::of(action_costs); @@ -478,11 +470,6 @@ fn is_assignment(eff: &Effect) -> bool { matches!(eff.operation, EffectOp::Assign(_)) } -/// Returns whether the effect is an increase. -fn is_increase(eff: &Effect) -> bool { - matches!(eff.operation, EffectOp::Increase(_)) -} - /// Returns whether the state variable is numeric. fn is_integer(sv: &StateVar) -> bool { matches!(sv.fluent.return_type().into(), Kind::Int) @@ -789,30 +776,6 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result solver.propagate()?; } - { - // Resource constraints - encode_resource_constraints(&mut solver, &effs, &conds, &eff_mutex_ends); - - if RESOURCE_CONSTRAINT_DEBUG.get() { - println!("\n=============================== Constraints =============================="); - Printer::print_reif_constraints(&solver.get_shape().constraints, &solver.model); - - println!("\n=========================== Before Propagation ==========================="); - solver.model.print_state(); - - let after = |solver: &Solver| { - println!("\n============================ After Propagation ==========================="); - solver.model.print_state(); - }; - - let propagation = solver.propagate(); - after(&solver); - propagation?; - } else { - solver.propagate()?; - } - } - let metric = metric.map(|metric| add_metric(pb, &mut solver.model, metric)); symmetry::add_symmetry_breaking(pb, &mut solver.model, &encoding); @@ -824,355 +787,3 @@ pub fn encode(pb: &FiniteProblem, metric: Option) -> std::result::Result encoding, }) } - -/* ========================================================================== */ -/* Resource Constraints */ -/* ========================================================================== */ - -fn encode_resource_constraints( - solver: &mut Box>, - effs: &[(EffID, Lit, &Effect)], - conds: &[(CondID, Lit, &Condition)], - eff_mutex_ends: &HashMap, -) { - /* ============================= Variables setup ============================ */ - - let span = tracing::span!(tracing::Level::TRACE, "resources"); - let _span = span.enter(); - let mut num_resource_constraints = 0; - - // Get the effects and the conditions on numeric state variables. - // Filter those who are not present. - let assignments: Vec<_> = effs - .iter() - .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_assignment(eff) && is_integer(&eff.state_var)) - .collect(); - let increases: Vec<_> = effs - .iter() - .filter(|(_, prez, eff)| !solver.model.entails(!*prez) && is_increase(eff) && is_integer(&eff.state_var)) - .collect(); - let mut conditions: Vec<_> = conds - .iter() - .filter(|(_, prez, cond)| !solver.model.entails(!*prez) && is_integer(&cond.state_var)) - .map(|&(_, prez, cond)| (prez, cond.clone())) - .collect(); - - /* =============================== Assignments ============================== */ - - tracing::trace_span!("assignments").in_scope(|| { - // Force the new assigned values to be in the state variable domain. - for &&(_, prez, eff) in &assignments { - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { - unreachable!() - }; - let EffectOp::Assign(val) = eff.operation else { - unreachable!() - }; - let val: IAtom = val.try_into().expect("Not integer assignment to an int state variable"); - solver.enforce(geq(val, lb), [prez]); - solver.enforce(leq(val, ub), [prez]); - num_resource_constraints += 1; - } - }); - - /* ================================ Increases =============================== */ - - // Convert the increase effects into conditions in order to check that the new value is in the state variable domain. - tracing::trace_span!("increases").in_scope(|| { - for &&(eff_id, prez, eff) in &increases { - assert!( - eff.transition_start + FAtom::EPSILON == eff.transition_end && eff.min_mutex_end.is_empty(), - "Only instantaneous effects are supported" - ); - // Get the bounds of the state variable. - let Type::Int { lb, ub } = eff.state_var.fluent.return_type() else { - unreachable!() - }; - // Create a new variable with those bounds. - let var = solver - .model - .new_ivar(lb, ub, Container::Instance(eff_id.instance_id) / VarType::Reification); - // Check that the state variable value is equals to that new variable. - // It will force the state variable value to be in the bounds of the new variable. - conditions.push(( - prez, - Condition { - start: eff.transition_end, - end: eff.transition_end, - state_var: eff.state_var.clone(), - value: var.into(), - }, - )); - } - }); - - /* =============================== Conditions =============================== */ - - /* - * For each condition `R == z`, a set of linear sum constraints of the form - * `la_j*ca_j + li_jk*ci_jk + ... + li_jm*ci_jm - la_j*z == 0` are created. - * - * The `la_j` literal is true if and only if the associated assignment effect `e_j` is the last one for the condition. - * A disjunctive clause will force to have at least one `la_j`. - * The `ca_j` value is the value of the assignment effect `e_j`. - * The `li_j*` literals are true if and only if: - * - `la_j` is true - * - the associated increase effect `e_*` is between `e_j` and the condition - * The `ci_j*` values are the value of the increase effects `e_*`. - * The `z` variable is the value of the condition. - * - * With all these literals, only one constraint will be taken into account: the one associated with the last assignment. - */ - tracing::trace_span!("conditions").in_scope(|| { - for (prez_cond, cond) in conditions { - assert_eq!(cond.start, cond.end, "Only the instantaneous conditions are supported"); - - // Returns false if the effect can never support the condition. - let eff_compatible_with_cond = |solver: &Solver, prez_eff: Lit, eff: &Effect| { - !solver.model.state.exclusive(prez_eff, prez_cond) - && unifiable_sv(&solver.model, &cond.state_var, &eff.state_var) - }; - - let compatible_assignments = assignments - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) - .collect::>(); - let compatible_increases = increases - .iter() - .filter(|(_, prez, eff)| eff_compatible_with_cond(solver, *prez, eff)) - .collect::>(); - - // Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j`. - let la_ca_ta_pa = if RESOURCE_CONSTRAINT_TIMEPOINTS.get() { - create_la_vector_with_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) - } else { - create_la_vector_without_timepoints(compatible_assignments, &cond, prez_cond, eff_mutex_ends, solver) - }; - - // Force to have at least one assignment. - let la_disjuncts = la_ca_ta_pa.iter().map(|(la, _, _, _)| *la).collect::>(); - solver.enforce(or(la_disjuncts), [prez_cond]); - - /* - * Matrix to store the `li_j*` literals and `ci_j*` values. - * - * `li_j*` is true if and only if the associated increase effect `e_*`: - * - is present - * - is before the condition - * - is after the assignment effect `e_j` - * - has the same state variable as the condition - * - `la_j` is true - * - the assignment effect associated to `la_j` is present - * - the condition is present - */ - let m_li_ci = la_ca_ta_pa - .iter() - .map(|(la, _, ta, pa)| { - compatible_increases - .iter() - .map(|(_, prez_eff, eff)| { - let mut li_conjunction: Vec = Vec::with_capacity(12); - // `la_j` is true - li_conjunction.push(*la); - // the assignment effect assiciated to `la_j` is present - li_conjunction.push(*pa); - // the condition is present - li_conjunction.push(prez_cond); - // is present - li_conjunction.push(*prez_eff); - // is before the condition - li_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - // is after the assignment effect `e_j` - li_conjunction.push(solver.reify(f_lt(*ta, eff.transition_end))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - li_conjunction.push(solver.reify(eq(a, b))); - } - // Create the `li_j*` literal. - let li_lit = solver.reify(and(li_conjunction)); - debug_assert!(solver.model.entails(solver.model.presence_literal(li_lit.variable()))); - - // Get the `ci_j*` value. - let EffectOp::Increase(eff_val) = eff.operation.clone() else { - unreachable!() - }; - (li_lit, eff_val) - }) - .collect::>() - }) - .collect::>(); - - // Create the linear sum constraints. - for (&(la, ca, _, _), li_ci) in la_ca_ta_pa.iter().zip(m_li_ci) { - // Create the sum. - let mut sum = LinearSum::zero(); - sum += LinearSum::with_lit( - ca, - solver.reify(and([la, solver.model.presence_literal(ca.var.into())])), - ); - for (li, ci) in li_ci.iter() { - sum += ci.map_with_lit(|t| { - solver.reify(and([t.lit(), *li, solver.model.presence_literal(t.var().into())])) - }); - } - let cond_val = - IAtom::try_from(cond.value).expect("Condition value is not numeric for a numeric fluent"); - sum -= LinearSum::with_lit( - cond_val, - solver.reify(and([la, solver.model.presence_literal(cond_val.var.into())])), - ); - sum = sum.simplify(); - - // Check that all the literals of the sum are always defined. - // It is wrapped in a `debug_assert!` for performance in release mode. - debug_assert!({ - for term in sum.terms() { - let prez = solver.model.presence_literal(term.lit().variable()); - debug_assert!(solver.model.entails(prez)); - } - true - }); - - // Force the sum to be equals to 0. - solver.enforce(sum.clone().geq(0), [prez_cond]); - solver.enforce(sum.leq(0), [prez_cond]); - num_resource_constraints += 1; - } - } - }); - tracing::debug!(%num_resource_constraints); -} - -/** -Vector to store the `la_j` literals, `ca_j` values, the end of the transition time point of the effect `e_j` -and the presence of the assignment effect. - -`la_j` is true if and only if the associated assignment effect `e_j`: - - is present - - is before the condition - - has the same state variable as the condition - - for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - - the condition is present -**/ -fn create_la_vector_without_timepoints( - assignments: Vec<&&(EffID, Lit, &Effect)>, - cond: &Condition, - prez_cond: Lit, - eff_mutex_ends: &HashMap, - solver: &mut Solver, -) -> Vec<(Lit, IAtom, FAtom, Lit)> { - assignments - .iter() - .map(|(eff_id, prez_eff, eff)| { - let mut la_conjunction: Vec = Vec::with_capacity(32); - // is present - la_conjunction.push(*prez_eff); - // is before the condition - la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - la_conjunction.push(solver.reify(eq(a, b))); - } - // for each other assignment effect `e_k` meeting the above conditions, `e_k` is before `e_j` - // This implies constraint is expressed as a disjunction. - for (other_eff_id, prez_other_eff, other_eff) in assignments.iter() { - // same effect: continue - if eff_id == other_eff_id { - continue; - } - let mut disjunction: Vec = Vec::with_capacity(12); - // is not present - disjunction.push(!*prez_other_eff); - // is after the condition - disjunction.push(solver.reify(f_lt(cond.end, other_eff.transition_end))); - // has a state variable different from the condition - debug_assert_eq!(cond.state_var.fluent, other_eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = other_eff.state_var.args[idx]; - disjunction.push(solver.reify(neq(a, b))); - } - // is before the effect `e_j` - disjunction.push(solver.reify(f_lt(eff_mutex_ends[other_eff_id], eff.transition_end))); - - let disjunction_lit = solver.reify(or(disjunction.clone())); - la_conjunction.push(disjunction_lit); - } - // the condition is present - la_conjunction.push(prez_cond); - - // Create the `la_j` literal. - let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); - - // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { - unreachable!() - }; - let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - - // Get the end of the transition time point of the effect `e_j`. - let ta = eff.transition_end; - (la_lit, ca, ta, *prez_eff) - }) - .collect::>() -} - -/** -Vector to store the `la_j` literals, `ca_j` values and the end of the transition time point of the effect `e_j` -and the presence of the assignment effect. - -`la_j` is true if and only if the associated assignment effect `e_j`: - - is present - - has the same state variable as the condition - - the condition is between the end of the transition and the mutex end - - the condition is present -**/ -fn create_la_vector_with_timepoints( - assignments: Vec<&&(EffID, Lit, &Effect)>, - cond: &Condition, - prez_cond: Lit, - eff_mutex_ends: &HashMap, - solver: &mut Solver, -) -> Vec<(Lit, IAtom, FAtom, Lit)> { - assignments - .iter() - .map(|(eff_id, prez_eff, eff)| { - let mut la_conjunction: Vec = Vec::with_capacity(32); - // is present - la_conjunction.push(*prez_eff); - // has the same state variable as the condition - debug_assert_eq!(cond.state_var.fluent, eff.state_var.fluent); - for idx in 0..cond.state_var.args.len() { - let a = cond.state_var.args[idx]; - let b = eff.state_var.args[idx]; - la_conjunction.push(solver.reify(eq(a, b))); - } - // the condition is between the start and the end of the effect - la_conjunction.push(solver.reify(f_leq(eff.transition_end, cond.start))); - la_conjunction.push(solver.reify(f_leq(cond.end, eff_mutex_ends[eff_id]))); - // the condition is present - la_conjunction.push(prez_cond); - - // Create the `la_j` literal. - let la_lit = solver.reify(and(la_conjunction.clone())); - debug_assert!(solver.model.entails(solver.model.presence_literal(la_lit.variable()))); - - // Get the `ca_j` variable. - let EffectOp::Assign(eff_val) = eff.operation else { - unreachable!() - }; - let ca = IAtom::try_from(eff_val).expect("Try to assign a non-numeric value to a numeric fluent"); - - // Get the end of the transition time point of the effect `e_j`. - let ta = eff.transition_end; - (la_lit, ca, ta, *prez_eff) - }) - .collect::>() -} diff --git a/planning/planning/src/chronicles/concrete.rs b/planning/planning/src/chronicles/concrete.rs index a23b79b3..4d70cb51 100644 --- a/planning/planning/src/chronicles/concrete.rs +++ b/planning/planning/src/chronicles/concrete.rs @@ -60,12 +60,7 @@ pub trait Substitution { } fn sub_linear_term(&self, term: &LinearTerm) -> LinearTerm { - LinearTerm::new( - term.factor(), - self.sub_ivar(term.var()), - self.sub_lit(term.lit()), - term.denom(), - ) + LinearTerm::new(term.factor(), self.sub_ivar(term.var()), term.denom()) } fn sub_linear_sum(&self, sum: &LinearSum) -> LinearSum { @@ -536,7 +531,6 @@ impl VarSet { self.add_atom(term.var()); self.add_atom(term.factor()); self.add_atom(term.denom()); - self.add_lit(term.lit()); } fn add_linear_sum(&mut self, sum: &LinearSum) { diff --git a/planning/unified/plugin/up_aries/solver.py b/planning/unified/plugin/up_aries/solver.py index 42f12e3d..7d52d068 100644 --- a/planning/unified/plugin/up_aries/solver.py +++ b/planning/unified/plugin/up_aries/solver.py @@ -50,7 +50,7 @@ "SCHEDULING", # "CONTINGENT", "ACTION_BASED_MULTI_AGENT", "TAMP", # PROBLEM_TYPE - "SIMPLE_NUMERIC_PLANNING", + # "SIMPLE_NUMERIC_PLANNING", # TODO # "GENERAL_NUMERIC_PLANNING", # TIME "CONTINUOUS_TIME", From 00d77b5d2a66295e2c5ce9eca6b86a2fac1c890b Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 29 Oct 2024 07:58:45 +0100 Subject: [PATCH 03/15] style: cargo clippy --- examples/knapsack/main.rs | 2 +- solver/src/reasoners/eq/dense.rs | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/examples/knapsack/main.rs b/examples/knapsack/main.rs index f3cc19f9..8c3f3c08 100644 --- a/examples/knapsack/main.rs +++ b/examples/knapsack/main.rs @@ -1,6 +1,6 @@ #![allow(clippy::needless_range_loop)] -use aries::core::{IntCst, Lit, INT_CST_MAX}; +use aries::core::{IntCst, INT_CST_MAX}; use aries::model::extensions::AssignmentExt; use aries::model::lang::linear::LinearSum; use aries::model::lang::IVar; diff --git a/solver/src/reasoners/eq/dense.rs b/solver/src/reasoners/eq/dense.rs index d4adcb48..96226a33 100644 --- a/solver/src/reasoners/eq/dense.rs +++ b/solver/src/reasoners/eq/dense.rs @@ -1213,7 +1213,7 @@ mod tests { fn random_model(seed: u64) -> Model { let mut rng = SmallRng::seed_from_u64(seed); - let objects = vec!["alice", "bob", "chloe", "donald", "elon"]; + let objects = ["alice", "bob", "chloe", "donald", "elon"]; let num_objects = rng.gen_range(1..5); let objects = objects[0..num_objects].to_vec(); let symbols = SymbolTable::from(vec![("obj", objects.clone())]); @@ -1225,7 +1225,6 @@ mod tests { let num_scopes = rng.gen_range(0..3); let scopes = (0..=num_scopes) - .into_iter() .map(|i| { if i == 0 { Lit::TRUE From c899ab5fa86856eae5ae458bf5e736431eeea427 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 29 Oct 2024 07:58:45 +0100 Subject: [PATCH 04/15] chore(planning): generalize the reify_or_zero mechanism --- planning/planners/src/encode.rs | 60 +++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 26 deletions(-) diff --git a/planning/planners/src/encode.rs b/planning/planners/src/encode.rs index bfa5e30a..da605470 100644 --- a/planning/planners/src/encode.rs +++ b/planning/planners/src/encode.rs @@ -10,12 +10,13 @@ use anyhow::{Context, Result}; use aries::core::state::Conflict; use aries::core::*; use aries::model::extensions::{AssignmentExt, Shaped}; -use aries::model::lang::linear::{LinearSum, LinearTerm}; -use aries::model::lang::{expr::*, Kind}; +use aries::model::lang::linear::LinearSum; +use aries::model::lang::{expr::*, IVar, Kind}; use aries::model::lang::{FAtom, FVar, IAtom, Variable}; use aries_planning::chronicles::constraints::encode_constraint; use aries_planning::chronicles::*; use env_param::EnvParam; +use std::cmp::{max, min}; use std::collections::{HashMap, HashSet}; use std::ptr; @@ -376,6 +377,31 @@ fn enforce_refinement(t: TaskRef, supporters: Vec, model: &mut Model) { } } +/// Reify an integer atom to a linear sum evaluated to zero if not present. +fn reify_or_zero(model: &mut Model, atom: IAtom, lit: Lit) -> LinearSum { + if atom.var == IVar::ZERO { + // Constant variable + if atom.shift == 0 { + LinearSum::zero() + } else { + let prez = IVar::new(lit.variable()); + LinearSum::of(vec![prez * atom.shift]) + } + } else { + // Real variable + let prez = model.reify(and([lit, model.presence_literal(atom.var.into())])); + let lb = model.lower_bound(atom.var); + let ub = model.upper_bound(atom.var); + let lbl = model.get_label(atom.var).unwrap().clone(); + let var = model.new_ivar(min(lb, 0), max(ub, 0), lbl); + let eq_0 = model.reify(eq(var, 0)); + let eq_atom = model.reify(eq(var, atom.var)); + model.enforce(implies(prez, eq_atom), []); + model.enforce(implies(!prez, eq_0), []); + reify_or_zero(model, atom.shift.into(), prez) + var + } +} + /// Encode a metric in the problem and returns an integer that should minimized in order to optimize the metric. pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAtom { match metric { @@ -393,18 +419,9 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto } // for each action, create an optional variable that evaluate to 1 if the action is present and 0 otherwise - let action_costs: Vec = action_presence - .iter() - .map(|(ch_id, p)| { - let var = model.new_ivar(0, 1, Container::Instance(*ch_id).var(VarType::Cost)); - let eq_0 = model.reify(eq(var, 0)); - let eq_1 = model.reify(eq(var, 1)); - model.enforce(implies(*p, eq_1), []); - model.enforce(implies(!*p, eq_0), []); - var.into() - }) - .collect(); - let action_costs = LinearSum::of(action_costs); + let action_costs: LinearSum = action_presence.iter().fold(LinearSum::zero(), |acc, (_ch_id, p)| { + acc + reify_or_zero(model, 1.into(), *p) + }); // make the sum of the action costs equal a `plan_length` variable. let plan_length = model.new_ivar(0, INT_CST_MAX, VarLabel(Container::Base, VarType::Cost)); @@ -424,18 +441,9 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto } // for each action, create an optional variable that evaluate to the cost if the action is present and 0 otherwise - let action_costs: Vec = costs - .iter() - .map(|&(ch_id, p, cost)| { - let var = model.new_ivar(0, cost, Container::Instance(ch_id).var(VarType::Cost)); - let eq_0 = model.reify(eq(var, 0)); - let eq_cost = model.reify(eq(var, cost)); - model.enforce(implies(p, eq_cost), []); - model.enforce(implies(!p, eq_0), []); - var.into() - }) - .collect(); - let action_costs = LinearSum::of(action_costs); + let action_costs: LinearSum = costs.iter().fold(LinearSum::zero(), |acc, (_ch_id, p, cost)| { + acc + reify_or_zero(model, (*cost).into(), *p) + }); // make the sum of the action costs equal a `plan_cost` variable. let plan_cost = model.new_ivar(0, INT_CST_MAX, VarLabel(Container::Base, VarType::Cost)); From f4bf06b02b96da32eb46c82bac0c86b3b620e536 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Tue, 29 Oct 2024 07:58:45 +0100 Subject: [PATCH 05/15] chore(model): generalize f_domain for linear sums --- solver/src/model/extensions/assignments.rs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/solver/src/model/extensions/assignments.rs b/solver/src/model/extensions/assignments.rs index 7019674e..b3973faf 100644 --- a/solver/src/model/extensions/assignments.rs +++ b/solver/src/model/extensions/assignments.rs @@ -1,7 +1,8 @@ use crate::core::state::{FixedDomain, IntDomain, OptDomain}; use crate::core::*; use crate::model::extensions::SavedAssignment; -use crate::model::lang::{Atom, Cst, FAtom, IAtom, IVar, SAtom}; +use crate::model::lang::linear::LinearSum; +use crate::model::lang::{Atom, Cst, IAtom, IVar, SAtom}; use crate::model::symbols::SymId; use crate::model::symbols::{ContiguousSymbols, TypedSym}; use num_rational::Rational32; @@ -41,10 +42,18 @@ pub trait AssignmentExt { } } - /// Returns the fixed-point domain of the atom. - fn f_domain(&self, fixed: impl Into) -> FixedDomain { - let fixed = fixed.into(); - FixedDomain::new(self.var_domain(fixed.num), fixed.denom) + /// Returns the fixed-point domain of the linear sum. + /// Can also be used with a FAtom. + fn f_domain(&self, sum: impl Into) -> FixedDomain { + let sum: LinearSum = sum.into(); + let (lb, ub) = sum + .terms() + .iter() + .fold((sum.constant(), sum.constant()), |(lb, ub), t| { + let (l, u) = self.domain_of(t.var()); + (lb + l * t.factor(), ub + u * t.factor()) + }); + FixedDomain::new(IntDomain::new(lb, ub), sum.denom()) } fn domain_of(&self, atom: impl Into) -> (IntCst, IntCst) { From a399d6352f1dbfd839ef6506ddc2eca4378b61dd Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Thu, 31 Oct 2024 08:06:10 +0100 Subject: [PATCH 06/15] feat(cp): add VarEqVarMulLit propagator --- solver/src/core/state/domains.rs | 2 +- solver/src/reasoners/cp/linear.rs | 4 +- solver/src/reasoners/cp/mod.rs | 1 + solver/src/reasoners/cp/mul.rs | 475 ++++++++++++++++++++++++++++++ 4 files changed, 479 insertions(+), 3 deletions(-) create mode 100644 solver/src/reasoners/cp/mul.rs diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index e366d9b6..04af8174 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -78,7 +78,7 @@ impl Domains { } #[cfg(test)] - fn new_presence_literal(&mut self, scope: Lit) -> Lit { + pub fn new_presence_literal(&mut self, scope: Lit) -> Lit { let lit = self.new_var(0, 1).geq(1); self.add_implication(lit, scope); lit diff --git a/solver/src/reasoners/cp/linear.rs b/solver/src/reasoners/cp/linear.rs index 9420623e..b781a9dc 100644 --- a/solver/src/reasoners/cp/linear.rs +++ b/solver/src/reasoners/cp/linear.rs @@ -262,7 +262,7 @@ impl Propagator for LinearSumLeq { // this is the element to explain // move its upper bound to the RHS let a_ub = (literal.bound_value().as_int() as i64).saturating_mul(factor); - // the inference is: factor * a.var <= a_ub + // the inference is: factor * e.var <= a_ub // e.var <= a_ub / factor // because e.var is integral, we can increase a_ub until its is immediately before the next multiple of factor // without changing the result @@ -593,7 +593,7 @@ mod tests { // propagate match s.propagate(&mut d, INFERENCE_CAUSE) { Ok(()) => { - // propagation successfull, check that all inferences have correct explanations + // propagation successful, check that all inferences have correct explanations check_events(&d, &mut s); } Err(contradiction) => { diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 20c574f6..fac8e4bf 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -2,6 +2,7 @@ pub mod linear; pub mod max; +pub mod mul; use crate::backtrack::{Backtrack, DecLvl, ObsTrailCursor}; use crate::collections::ref_store::RefVec; diff --git a/solver/src/reasoners/cp/mul.rs b/solver/src/reasoners/cp/mul.rs new file mode 100644 index 00000000..6b7dbfda --- /dev/null +++ b/solver/src/reasoners/cp/mul.rs @@ -0,0 +1,475 @@ +use std::cmp::{max, min}; + +use crate::{ + core::{ + state::{Explanation, Term}, + Lit, Relation, VarRef, + }, + model::extensions::AssignmentExt, + reasoners::Contradiction, + reif, +}; + +use super::Propagator; + +#[derive(Clone, Debug)] +/// Propagator for the constraint `reified <=> original * lit` +pub(super) struct VarEqVarMulLit { + pub reified: VarRef, + pub original: VarRef, + pub lit: Lit, +} + +impl std::fmt::Display for VarEqVarMulLit { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?} <=> {:?} * {:?}", self.reified, self.original, self.lit) + } +} + +impl Propagator for VarEqVarMulLit { + fn setup(&self, id: super::PropagatorId, context: &mut super::Watches) { + context.add_watch(self.reified, id); + context.add_watch(self.original, id); + context.add_watch(self.lit.variable(), id); + } + + fn propagate( + &self, + domains: &mut crate::core::state::Domains, + cause: crate::core::state::Cause, + ) -> Result<(), crate::reasoners::Contradiction> { + let n = domains.trail().len(); + + let orig_prez = domains.presence_literal(self.original); + debug_assert!(domains.implies(self.lit, orig_prez)); + + if domains.entails(self.lit) { + // lit is true, so reified = original + let (orig_lb, orig_ub) = domains.bounds(self.original); + let (reif_lb, reif_ub) = domains.bounds(self.reified); + + domains.set_lb(self.reified, orig_lb, cause)?; + domains.set_ub(self.reified, orig_ub, cause)?; + domains.set_lb(self.original, reif_lb, cause)?; + domains.set_ub(self.original, reif_ub, cause)?; + } else if domains.entails(!self.lit) { + // lit is false, so reified = 0 + domains.set_lb(self.reified, 0, cause)?; + domains.set_ub(self.reified, 0, cause)?; + } else { + // lit is not fixed + let (orig_lb, orig_ub) = domains.bounds(self.original); + let (reif_lb, reif_ub) = domains.bounds(self.reified); + + if reif_lb > orig_ub || reif_ub < orig_lb { + // intersection(dom(reif), dom(orig)) is empty, so lit = false and reified = 0 + domains.set(!self.lit, cause)?; + domains.set_lb(self.reified, 0, cause)?; + domains.set_ub(self.reified, 0, cause)?; + } else if reif_lb > 0 || reif_ub < 0 { + // reified != 0, so lit = true + domains.set(self.lit, cause)?; + } else if domains.entails(orig_prez) { + // original is present, can reduce the bounds of reified while keeping 0 in the domain + domains.set_lb(self.reified, min(0, orig_lb), cause)?; + domains.set_ub(self.reified, max(0, orig_ub), cause)?; + } + } + + if n != domains.trail().len() { + // At least one domain has been modified + self.propagate(domains, cause) + } else { + Ok(()) + } + } + + fn explain( + &self, + literal: Lit, + state: &crate::core::state::Domains, + out_explanation: &mut crate::core::state::Explanation, + ) { + // At least one element of the constraint must be the subject of the explanation + debug_assert!([self.reified, self.original, self.lit.variable()] + .iter() + .any(|&v| v == literal.variable())); + + let (reif_lb, reif_ub) = state.bounds(self.reified); + let (orig_lb, orig_ub) = state.bounds(self.original); + let orig_prez = state.presence_literal(self.original); + + if literal == self.lit { + // Explain why lit is true + // reified != 0, so lit = true + if reif_lb > 0 { + out_explanation.push(self.reified.geq(reif_lb)); + } else if reif_ub < 0 { + out_explanation.push(self.reified.leq(reif_ub)); + } + } else if literal == !self.lit { + // Explain why lit is false + // intersection(dom(reif), dom(orig)) is empty, so lit = false + if reif_lb > orig_ub { + out_explanation.push(self.original.leq(orig_ub)); + out_explanation.push(self.reified.geq(reif_lb)); + } + if reif_ub < orig_lb { + out_explanation.push(self.original.geq(orig_lb)); + out_explanation.push(self.reified.leq(reif_ub)); + } + } else { + let (var, rel, val) = literal.unpack(); + if var == self.reified { + // Explain the bounds of reified + match rel { + Relation::Gt => { + if val < 0 { + if state.entails(!orig_prez) { + out_explanation.push(!orig_prez); + } else if state.entails(!self.lit) { + out_explanation.push(!self.lit); + } else if state.entails(orig_prez) { + out_explanation.push(orig_prez); + out_explanation.push(self.original.gt(val)); + } + } else if state.entails(self.lit) { + out_explanation.push(self.lit); + out_explanation.push(self.original.gt(val)); + } + } + Relation::Leq => { + if val >= 0 { + if state.entails(!orig_prez) { + out_explanation.push(!orig_prez); + } else if state.entails(!self.lit) { + out_explanation.push(!self.lit); + } else if state.entails(orig_prez) { + out_explanation.push(orig_prez); + out_explanation.push(self.original.leq(val)); + } + } else if state.entails(self.lit) { + out_explanation.push(self.lit); + out_explanation.push(self.original.leq(val)); + } + } + }; + } else if var == self.original && state.entails(self.lit) { + // Explain the bounds of original + out_explanation.push(self.lit); + match rel { + Relation::Gt => out_explanation.push(self.reified.gt(val)), + Relation::Leq => out_explanation.push(self.reified.leq(val)), + }; + } + } + } + + fn clone_box(&self) -> Box { + Box::new(self.clone()) + } +} + +#[cfg(test)] +mod tests { + use itertools::Itertools; + use rand::prelude::SmallRng; + use rand::seq::SliceRandom; + use rand::{Rng, SeedableRng}; + + use crate::backtrack::Backtrack; + use crate::core::literals::Disjunction; + use crate::core::state::{Event, Origin}; + use crate::core::{IntCst, Relation}; + use crate::{ + core::state::{Cause, Domains, Explainer, Explanation, InferenceCause, InvalidUpdate}, + reasoners::{Contradiction, ReasonerId}, + }; + + use super::*; + + fn mul(reif: VarRef, orig: VarRef, lit: Lit) -> VarEqVarMulLit { + VarEqVarMulLit { + reified: reif, + original: orig, + lit, + } + } + + fn check_bounds(v: VarRef, d: &Domains, lb: IntCst, ub: IntCst) { + assert_eq!(d.lb(v), lb); + assert_eq!(d.ub(v), ub); + } + + #[test] + fn test_propagation_with_true_lit() { + let mut d = Domains::new(); + let r = d.new_var(-5, 10); + let o = d.new_var(-10, 5); + let c = mul(r, o, Lit::TRUE); + + // Check initial bounds + check_bounds(r, &d, -5, 10); + check_bounds(o, &d, -10, 5); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, -5, 5); + check_bounds(o, &d, -5, 5); + } + + #[test] + fn test_propagation_with_false_lit() { + let mut d = Domains::new(); + let r = d.new_var(-5, 10); + let o = d.new_var(-10, 5); + let c = mul(r, o, Lit::FALSE); + + // Check initial bounds + check_bounds(r, &d, -5, 10); + check_bounds(o, &d, -10, 5); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 0, 0); + check_bounds(o, &d, -10, 5); + } + + #[test] + fn test_propagation_with_non_zero_reif() { + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let r = d.new_var(1, 10); + let o = d.new_optional_var(-10, 5, p); + let l = d.new_presence_literal(p); + let c = mul(r, o, l); + + // Check initial bounds + check_bounds(r, &d, 1, 10); + check_bounds(o, &d, -10, 5); + check_bounds(l.variable(), &d, 0, 1); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 1, 5); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 1, 1); + } + + #[test] + fn test_propagation_with_exclusive_bounds() { + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let r = d.new_var(-5, 0); + let o = d.new_optional_var(1, 5, p); + let l = d.new_presence_literal(p); + let c = mul(r, o, l); + + // Check initial bounds + check_bounds(r, &d, -5, 0); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 0, 1); + + // Check propagation + assert!(c.propagate(&mut d, Cause::Decision).is_ok()); + check_bounds(r, &d, 0, 0); + check_bounds(o, &d, 1, 5); + check_bounds(l.variable(), &d, 0, 0); + } + + static INFERENCE_CAUSE: Cause = Cause::Inference(InferenceCause { + writer: ReasonerId::Cp, + payload: 0, + }); + + /// Test that triggers propagation of random decisions and checks that the explanations are minimal + #[test] + fn test_explanations() { + let mut rng = SmallRng::seed_from_u64(0); + // function that returns a given number of decisions to be applied later + // it use the RNG above to drive its random choices + let mut pick_decisions = |d: &Domains, min: usize, max: usize| -> Vec { + let num_decisions = rng.gen_range(min..=max); + let vars = d.variables().filter(|v| !d.is_bound(*v)).collect_vec(); + let mut lits = Vec::with_capacity(num_decisions); + for _ in 0..num_decisions { + let var_id = rng.gen_range(0..vars.len()); + let var = vars[var_id]; + let (lb, ub) = d.bounds(var); + let below: bool = rng.gen(); + let lit = if below { + let ub = rng.gen_range(lb..ub); + Lit::leq(var, ub) + } else { + let lb = rng.gen_range((lb + 1)..=ub); + Lit::geq(var, lb) + }; + lits.push(lit); + } + lits + }; + // new rng for local use + let mut rng = SmallRng::seed_from_u64(0); + + // repeat a large number of random tests + let mut skipped_tests = 0; + let mut run_tests = 0; + let mut idx = 0; + while run_tests < 1000 { + idx += 1; + + // create the constraint + let mut d = Domains::new(); + let p = d.new_presence_literal(Lit::TRUE); + let lit = d.new_presence_literal(p); + let original = d.new_optional_var(-10, 10, p); + let reified = d.new_var(-10, 10); + let mut c = VarEqVarMulLit { reified, original, lit }; + println!("\n[{idx}] Constraint: {c:?} with prez(original) = {p:?}"); + + // pick a random set of decisions + let decisions = pick_decisions(&d, 1, 10); + println!("Decisions: {decisions:?}"); + + // get a copy of the domain on which to apply all decisions + let mut d = d.clone(); + d.save_state(); + + // apply all decisions + let mut valid_decisions = true; + for dec in decisions { + if d.entails(!dec) { + // a previous decision already implies the negation of the current one + valid_decisions = false; + break; + } + d.set(dec, Cause::Decision); + } + if !valid_decisions { + println!("Invalid decisions: Skipping..."); + skipped_tests += 1; + continue; + } + + // propagate + match c.propagate(&mut d, INFERENCE_CAUSE) { + Ok(()) => { + // propagation successful, check that all inferences have correct explanations + check_events(&d, &mut c); + } + Err(contradiction) => { + // propagation failure, check that the contradiction is a valid one + let explanation = match contradiction { + Contradiction::InvalidUpdate(InvalidUpdate(lit, cause)) => { + let mut expl = Explanation::with_capacity(16); + expl.push(!lit); + d.add_implying_literals_to_explanation(lit, cause, &mut expl, &mut c); + expl + } + Contradiction::Explanation(expl) => expl, + }; + let mut d = d.clone(); + d.reset(); + // get the conjunction and shuffle it + // note that we do not check minimality here + let mut conjuncts = explanation.lits; + conjuncts.shuffle(&mut rng); + for &conjunct in &conjuncts { + let ret = d.set(conjunct, Cause::Decision); + if ret.is_err() { + println!("Invalid update: {conjunct:?}"); + } + } + + assert!( + c.propagate(&mut d, INFERENCE_CAUSE).is_err(), + "Explanation: {conjuncts:?}\n {c:?}" + ); + } + } + + run_tests += 1; + } + println!("\nSkipped tests: {skipped_tests}"); + } + + /// Check that all events since the last decision have a minimal explanation + pub fn check_events(d: &Domains, explainer: &mut (impl Propagator + Explainer)) { + let events = d + .trail() + .events() + .iter() + .rev() + .take_while(|ev| ev.cause != Origin::DECISION) + .cloned() + .collect_vec(); + // check that all events have minimal explanations + for ev in &events { + check_event_explanation(d, ev, explainer); + } + } + + /// Checks that the event has a minimal explanation + pub fn check_event_explanation(d: &Domains, ev: &Event, explainer: &mut (impl Propagator + Explainer)) { + let implied = ev.new_literal(); + // generate explanation + let implicants = d.implying_literals(implied, explainer).unwrap(); + let clause = Disjunction::new(implicants.iter().map(|l| !*l).collect_vec()); + // check minimality + check_explanation_minimality(d, implied, clause, explainer); + } + + pub fn check_explanation_minimality( + domains: &Domains, + implied: Lit, + clause: Disjunction, + propagator: &dyn Propagator, + ) { + let mut domains = domains.clone(); + // println!("=== original trail ==="); + // domains.trail().print(); + domains.reset(); + assert!(!domains.entails(implied)); + + // gather all decisions not already entailed at root level + let mut decisions = clause + .literals() + .iter() + .copied() + .filter(|&l| !domains.entails(l)) + .map(|l| !l) + .collect_vec(); + + for _rotation_id in 0..decisions.len() { + // println!("Clause: {implied:?} <- {decisions:?}"); + for i in 0..decisions.len() { + let l = decisions[i]; + if domains.entails(l) { + continue; + } + // println!("Decide {l:?}"); + domains.decide(l); + propagator + .propagate(&mut domains, INFERENCE_CAUSE) + .expect("failed prop"); + + let decisions_left = decisions[i + 1..] + .iter() + .filter(|&l| !domains.entails(*l)) + .collect_vec(); + + if !decisions_left.is_empty() { + assert!(!domains.entails(implied), "Not minimal, useless: {:?}", &decisions_left) + } + } + + // println!("=== Post trail ==="); + // solver.trail().print(); + assert!( + domains.entails(implied), + "Literal {implied:?} not implied after all implicants ({decisions:?}) enforced" + ); + decisions.rotate_left(1); + } + } +} From 3617a6bfc0f24fe3c79124544b3f4c2ca3178e5d Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Thu, 31 Oct 2024 08:36:47 +0100 Subject: [PATCH 07/15] feat(cp): add EqVarMulLit to ReifExpr --- solver/src/model/lang.rs | 1 + solver/src/model/lang/max.rs | 4 ++-- solver/src/model/lang/mul.rs | 15 +++++++++++++++ solver/src/reasoners/cp/mod.rs | 11 +++++++++++ solver/src/reif/mod.rs | 13 +++++++++++++ solver/src/solver/solver_impl.rs | 4 ++++ 6 files changed, 46 insertions(+), 2 deletions(-) create mode 100644 solver/src/model/lang/mul.rs diff --git a/solver/src/model/lang.rs b/solver/src/model/lang.rs index 0c961893..64bc4dd8 100644 --- a/solver/src/model/lang.rs +++ b/solver/src/model/lang.rs @@ -7,6 +7,7 @@ mod fixed; mod int; pub mod linear; pub mod max; +pub mod mul; pub mod reification; mod sym; mod validity_scope; diff --git a/solver/src/model/lang/max.rs b/solver/src/model/lang/max.rs index c5d21504..a296ab4e 100644 --- a/solver/src/model/lang/max.rs +++ b/solver/src/model/lang/max.rs @@ -5,7 +5,7 @@ use crate::reif::ReifExpr; use itertools::Itertools; use std::fmt::{Debug, Formatter}; -/// Constraint equivalent to `lhs = max { e | e \in rhs } +/// Constraint equivalent to `lhs = max { e | e \in rhs }` pub struct EqMax { lhs: IAtom, rhs: Vec, @@ -20,7 +20,7 @@ impl EqMax { } } -/// Constraint equivalent to `lhs = min { e | e \in rhs } +/// Constraint equivalent to `lhs = min { e | e \in rhs }` pub struct EqMin { lhs: IAtom, rhs: Vec, diff --git a/solver/src/model/lang/mul.rs b/solver/src/model/lang/mul.rs new file mode 100644 index 00000000..4784f7ad --- /dev/null +++ b/solver/src/model/lang/mul.rs @@ -0,0 +1,15 @@ +use crate::core::{Lit, VarRef}; +use std::fmt::{Debug, Formatter}; + +#[derive(Eq, PartialEq, Hash, Clone)] +pub struct NFEqVarMulLit { + pub lhs: VarRef, + pub rhs: VarRef, + pub lit: Lit, +} + +impl Debug for NFEqVarMulLit { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?} = {:?} * {:?}", self.lhs, self.lit, self.rhs) + } +} diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index fac8e4bf..2a5eeb25 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -12,8 +12,10 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef, INT_CST_MAX, INT_CST_MIN}; use crate::create_ref_type; use crate::model::extensions::AssignmentExt; use crate::model::lang::linear::NFLinearLeq; +use crate::model::lang::mul::NFEqVarMulLit; use crate::reasoners::{Contradiction, ReasonerId, Theory}; use anyhow::Context; +use mul::VarEqVarMulLit; use crate::reasoners::cp::linear::{LinearSumLeq, SumElem}; use crate::reasoners::cp::max::AtLeastOneGeq; @@ -121,6 +123,15 @@ impl Cp { self.add_propagator(propagator); } + pub fn add_eq_var_mul_lit_constraint(&mut self, mul: &NFEqVarMulLit) { + let propagator = VarEqVarMulLit { + reified: mul.lhs, + original: mul.rhs, + lit: mul.lit, + }; + self.add_propagator(propagator); + } + pub fn add_propagator(&mut self, propagator: impl Into) { // TODO: handle validity scopes let propagator = propagator.into(); diff --git a/solver/src/reif/mod.rs b/solver/src/reif/mod.rs index 41ba5017..e442d12f 100644 --- a/solver/src/reif/mod.rs +++ b/solver/src/reif/mod.rs @@ -4,6 +4,7 @@ use crate::core::{IntCst, Lit, SignedVar, VarRef}; use crate::model::lang::alternative::NFAlternative; use crate::model::lang::linear::NFLinearLeq; use crate::model::lang::max::NFEqMax; +use crate::model::lang::mul::NFEqVarMulLit; use crate::model::lang::ValidityScope; use crate::model::{Label, Model}; use std::fmt::{Debug, Formatter}; @@ -32,6 +33,7 @@ pub enum ReifExpr { Linear(NFLinearLeq), Alternative(NFAlternative), EqMax(NFEqMax), + EqVarMulLit(NFEqVarMulLit), } impl std::fmt::Display for ReifExpr { @@ -48,6 +50,7 @@ impl std::fmt::Display for ReifExpr { ReifExpr::Linear(l) => write!(f, "{l}"), ReifExpr::EqMax(em) => write!(f, "{em:?}"), ReifExpr::Alternative(alt) => write!(f, "{alt:?}"), + ReifExpr::EqVarMulLit(em) => write!(f, "{em:?}"), } } } @@ -75,6 +78,7 @@ impl ReifExpr { ReifExpr::Linear(lin) => lin.validity_scope(presence), ReifExpr::Alternative(alt) => ValidityScope::new([presence(alt.main)], []), ReifExpr::EqMax(eq_max) => ValidityScope::new([presence(eq_max.lhs.variable())], []), + ReifExpr::EqVarMulLit(em) => ValidityScope::new([presence(em.lhs)], []), } } @@ -89,6 +93,7 @@ impl ReifExpr { OptDomain::Present(lb, ub) if lb == ub => lb, _ => panic!(), }; + let lvalue = |lit: Lit| assignment.value(lit).unwrap(); let sprez = |svar: SignedVar| prez(svar.variable()); let svalue = |svar: SignedVar| { if svar.is_plus() { @@ -202,6 +207,13 @@ impl ReifExpr { Some(true) } } + ReifExpr::EqVarMulLit(NFEqVarMulLit { lhs, rhs, lit }) => { + if prez(*lhs) && prez(*rhs) { + Some(value(*lhs) == (lvalue(*lit) as i32) * value(*rhs)) + } else { + None + } + } } } } @@ -254,6 +266,7 @@ impl Not for ReifExpr { ReifExpr::Linear(lin) => ReifExpr::Linear(!lin), ReifExpr::Alternative(_) => panic!("Alternative is a constraint and cannot be negated"), ReifExpr::EqMax(_) => panic!("EqMax is a constraint and cannot be negated"), + ReifExpr::EqVarMulLit(_) => panic!("EqVarMulLit is a constraint and cannot be negated"), } } } diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 7d1af33d..11dd7eed 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -403,6 +403,10 @@ impl Solver { Ok(()) } + ReifExpr::EqVarMulLit(mul) => { + self.reasoners.cp.add_eq_var_mul_lit_constraint(mul); + Ok(()) + } } } From 18404ea6bd912231eb7074b0fe11486c9ba83ae5 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Thu, 31 Oct 2024 08:41:18 +0100 Subject: [PATCH 08/15] style: cargo clippy --- examples/sat/main.rs | 8 ++++---- examples/scheduling/src/search.rs | 19 ++++++++++--------- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/examples/sat/main.rs b/examples/sat/main.rs index 6721b397..c3e046d0 100644 --- a/examples/sat/main.rs +++ b/examples/sat/main.rs @@ -104,12 +104,12 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option) -> Re let choices: Vec<_> = model.state.variables().map(|v| Lit::geq(v, 1)).collect(); let solver = Box::new(Solver::new(model)); - let search_params: Vec<_> = opt.search.split(",").collect(); + let search_params: Vec<_> = opt.search.split(',').collect(); let num_threads = search_params.len(); let conflict_params = |conf: &str| { let mut params = Params::default(); - for opt in conf.split(":") { + for opt in conf.split(':') { let handled = params.configure(opt); if !handled { panic!("UNSUPPORTED OPTION: {opt}") @@ -119,8 +119,8 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option) -> Re }; let mut par_solver = ParSolver::new(solver, num_threads, |id, solver| { - let search_params: Vec<_> = search_params[id].split("/").collect(); - let stable_params = if search_params.len() > 0 { + let search_params: Vec<_> = search_params[id].split('/').collect(); + let stable_params = if !search_params.is_empty() { search_params[0] } else { "+lrb:+p+l:-neg" diff --git a/examples/scheduling/src/search.rs b/examples/scheduling/src/search.rs index e2c25da2..daa5caa0 100644 --- a/examples/scheduling/src/search.rs +++ b/examples/scheduling/src/search.rs @@ -82,12 +82,14 @@ struct Strat { pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_threads: usize) -> ParSolver { let mut base_solver = Box::new(base); - let mut load_conf = |conf: &str| -> Strat { + let load_conf = |conf: &str| -> Strat { let mut mode = Mode::Stable; - let mut params = conflicts::Params::default(); - params.heuristic = conflicts::Heuristic::LearningRate; - params.active = conflicts::ActiveLiterals::Reasoned; - params.impact_measure = ImpactMeasure::LBD; + let mut params = conflicts::Params { + heuristic: conflicts::Heuristic::LearningRate, + active: conflicts::ActiveLiterals::Reasoned, + impact_measure: ImpactMeasure::LBD, + ..Default::default() + }; for opt in conf.split(':') { if params.configure(opt) { // handled @@ -111,7 +113,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th SearchStrategy::Default => "stable:+sol", SearchStrategy::Custom(conf) => conf.as_str(), }; - let all_strats = conf.split("/").map(|s| load_conf(s)).collect_vec(); + let all_strats = conf.split('/').map(load_conf).collect_vec(); let decision_lits: Vec = base_solver .model @@ -131,8 +133,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th Mode::Stable => (2000, 1.2), // stable: few restarts Mode::Focused => (800, 1.0), // focused: always aggressive restarts }; - let brancher = brancher.with_restarts(restart_period, restart_update); - brancher + brancher.with_restarts(restart_period, restart_update) }; // build a brancher that alternates between the proposed strategies @@ -160,7 +161,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th .collect_vec(); // conflict based search, possibly alternating between several strategies - let branchers = strats.into_iter().map(|strat| build_brancher(strat)).collect_vec(); + let branchers = strats.into_iter().map(build_brancher).collect_vec(); let brancher = round_robin(branchers); // search strategy. For the first one simply add a greedy EST strategy to bootstrap the search From 3b6b38ea325b3764a2e22baed704cdc55462b02f Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 4 Nov 2024 11:14:50 +0100 Subject: [PATCH 09/15] fix(search): set default value for conflict based brancher --- solver/src/solver/search/conflicts.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/solver/src/solver/search/conflicts.rs b/solver/src/solver/search/conflicts.rs index d2108000..e697de11 100644 --- a/solver/src/solver/search/conflicts.rs +++ b/solver/src/solver/search/conflicts.rs @@ -346,9 +346,8 @@ impl ConflictBasedBrancher { } } - pub fn set_default_value(&mut self, _var: VarRef, _val: IntCst) { - todo!() - // self.default_assignment.values.insert(var, val); + pub fn set_default_value(&mut self, var: VarRef, val: IntCst) { + self.default_assignment.set_from_phase(var, val) } /// Increase the activity of the variable and perform an reordering in the queue. From 1009b7eab68c7ddc1f7c052fed0832add5c24b47 Mon Sep 17 00:00:00 2001 From: Roland Godet Date: Mon, 4 Nov 2024 11:24:13 +0100 Subject: [PATCH 10/15] fix(domains): implying literals for decision leading to empty domain --- solver/src/core/state/domains.rs | 4 +++- solver/src/reasoners/cp/mul.rs | 23 ++--------------------- 2 files changed, 5 insertions(+), 22 deletions(-) diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs index 04af8174..3aeeeefe 100644 --- a/solver/src/core/state/domains.rs +++ b/solver/src/core/state/domains.rs @@ -608,7 +608,9 @@ impl Domains { debug_assert!(self.entails(!invalid_lit)); explanation.push(!invalid_lit); match cause { - DirectOrigin::Decision | DirectOrigin::Encoding => {} + DirectOrigin::Decision | DirectOrigin::Encoding => { + explanation.push(invalid_lit); + } DirectOrigin::ExternalInference(cause) => { // print!("[ext {:?}] ", cause.writer); // ask for a clause (l1 & l2 & ... & ln) => lit diff --git a/solver/src/reasoners/cp/mul.rs b/solver/src/reasoners/cp/mul.rs index 6b7dbfda..5c536cab 100644 --- a/solver/src/reasoners/cp/mul.rs +++ b/solver/src/reasoners/cp/mul.rs @@ -312,12 +312,7 @@ mod tests { let mut rng = SmallRng::seed_from_u64(0); // repeat a large number of random tests - let mut skipped_tests = 0; - let mut run_tests = 0; - let mut idx = 0; - while run_tests < 1000 { - idx += 1; - + for _ in 0..1000 { // create the constraint let mut d = Domains::new(); let p = d.new_presence_literal(Lit::TRUE); @@ -325,7 +320,7 @@ mod tests { let original = d.new_optional_var(-10, 10, p); let reified = d.new_var(-10, 10); let mut c = VarEqVarMulLit { reified, original, lit }; - println!("\n[{idx}] Constraint: {c:?} with prez(original) = {p:?}"); + println!("\nConstraint: {c:?} with prez(original) = {p:?}"); // pick a random set of decisions let decisions = pick_decisions(&d, 1, 10); @@ -336,20 +331,9 @@ mod tests { d.save_state(); // apply all decisions - let mut valid_decisions = true; for dec in decisions { - if d.entails(!dec) { - // a previous decision already implies the negation of the current one - valid_decisions = false; - break; - } d.set(dec, Cause::Decision); } - if !valid_decisions { - println!("Invalid decisions: Skipping..."); - skipped_tests += 1; - continue; - } // propagate match c.propagate(&mut d, INFERENCE_CAUSE) { @@ -387,10 +371,7 @@ mod tests { ); } } - - run_tests += 1; } - println!("\nSkipped tests: {skipped_tests}"); } /// Check that all events since the last decision have a minimal explanation From 45b1cc691fd5bfd9c882628de2566f711c5fea3b Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 4 Nov 2024 14:36:45 +0100 Subject: [PATCH 11/15] fix(ci): Update sat solver command line arguments --- ci/sat.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ci/sat.py b/ci/sat.py index 0b026118..d042cd93 100755 --- a/ci/sat.py +++ b/ci/sat.py @@ -9,7 +9,7 @@ import time os.system("cargo build --profile ci --bin aries-sat") -solver = "target/ci/aries-sat --threads 1" +solver = "target/ci/aries-sat" solver_cmd = solver + " {params} --source {archive} {instance}" @@ -42,4 +42,3 @@ def run_all(archive, sat): run_all("examples/sat/instances/test-sat.zip", sat=True) run_all("examples/sat/instances/test-unsat.zip", sat=False) - From cbed9007c5f443999aec9bfbda13cdc2f6f9b893 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 4 Nov 2024 16:41:45 +0100 Subject: [PATCH 12/15] chore(lcp): Kill planner if a thread panics. --- planning/planners/src/bin/lcp.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/planning/planners/src/bin/lcp.rs b/planning/planners/src/bin/lcp.rs index 71b5610a..e2dde851 100644 --- a/planning/planners/src/bin/lcp.rs +++ b/planning/planners/src/bin/lcp.rs @@ -65,6 +65,15 @@ pub struct Opt { } fn main() -> Result<()> { + // Terminate the process if a thread panics. + // take_hook() returns the default hook in case when a custom one is not set + let orig_hook = std::panic::take_hook(); + std::panic::set_hook(Box::new(move |panic_info| { + // invoke the default handler and exit the process + orig_hook(panic_info); + std::process::exit(1); + })); + let opt: Opt = Opt::from_args(); // set up logger From 3101e9b5920e8e849253c1341829b29a00f87665 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 4 Nov 2024 16:42:39 +0100 Subject: [PATCH 13/15] fix(sat): Keep watches on true literals if clause is satisfied. --- solver/src/reasoners/sat/clauses/mod.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/solver/src/reasoners/sat/clauses/mod.rs b/solver/src/reasoners/sat/clauses/mod.rs index 6d0782ea..16d10964 100644 --- a/solver/src/reasoners/sat/clauses/mod.rs +++ b/solver/src/reasoners/sat/clauses/mod.rs @@ -188,6 +188,13 @@ impl Clause { debug_assert!(lvl0 >= lvl1); debug_assert!(self.unwatched.iter().all(|l| lvl1 >= priority(*l))); + if value_of(self.watch1) == Some(true) { + // clause is satisfied, leave the watches untouched (true literals would be the watches) + return; + } + debug_assert_ne!(value_of(self.watch1), Some(true)); + debug_assert_ne!(value_of(self.watch2), Some(true)); + if self.watch1 == !presence(self.watch2) { self.swap_watches() } else if self.watch2 == !presence(self.watch1) { From 472b56ffe3b205a85582063780eac16f042f6a36 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 4 Nov 2024 16:43:51 +0100 Subject: [PATCH 14/15] perf(sat): Limit clause sharing two clauses of size 3 Larger number seem to arm the performance as some threads would spend there time processing learned clauses. --- solver/src/solver/parallel/signals.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solver/src/solver/parallel/signals.rs b/solver/src/solver/parallel/signals.rs index 586a4ff0..dd723036 100644 --- a/solver/src/solver/parallel/signals.rs +++ b/solver/src/solver/parallel/signals.rs @@ -7,7 +7,7 @@ use std::sync::atomic::{AtomicUsize, Ordering}; use std::sync::Arc; /// The maximum size of a clause that can be shared with other threads. -static MAX_CLAUSE_SHARING_SIZE: EnvParam = EnvParam::new("ARIES_MAX_CLAUSE_SHARING_SIZE", "6"); +static MAX_CLAUSE_SHARING_SIZE: EnvParam = EnvParam::new("ARIES_MAX_CLAUSE_SHARING_SIZE", "3"); static THREAD_ID_COUNTER: AtomicUsize = AtomicUsize::new(0); pub type ThreadID = usize; From ccfabc9576c065491f41415e54eb3714d33d537e Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Mon, 4 Nov 2024 16:45:17 +0100 Subject: [PATCH 15/15] fix(sat): provide stronger explanation in STN theory propagation. The previous version was unnecessarily careful now that we have eager sat propagation. --- solver/src/reasoners/stn/theory.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/solver/src/reasoners/stn/theory.rs b/solver/src/reasoners/stn/theory.rs index b7bd7289..2a4f0e1b 100644 --- a/solver/src/reasoners/stn/theory.rs +++ b/solver/src/reasoners/stn/theory.rs @@ -478,7 +478,6 @@ impl StnTheory { for edge in path { let enabler = self.constraints[edge].enabler.expect("inactive constraint"); out_explanation.push(enabler.active); - out_explanation.push(model.presence(enabler.active.variable())); } } TheoryPropagationCause::Bounds { source, target } => {