From 36a1ace123f4996edaf2deaf1de8949a717ea685 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 22 Apr 2024 11:31:58 +1000 Subject: [PATCH] Add IntView::Const as initial way to deal with constants in constraints --- crates/fzn-huub/src/tracing.rs | 8 +- crates/huub/src/model.rs | 19 +-- crates/huub/src/propagator.rs | 25 ++-- crates/huub/src/propagator/all_different.rs | 37 +++-- crates/huub/src/propagator/init_action.rs | 1 + .../huub/src/propagator/propagation_action.rs | 130 ++++++++++++++++-- crates/huub/src/propagator/reason.rs | 1 + crates/huub/src/solver.rs | 8 +- crates/huub/src/solver/engine.rs | 74 ++++++---- crates/huub/src/solver/engine/trail.rs | 11 +- crates/huub/src/solver/value.rs | 3 +- crates/huub/src/solver/view.rs | 5 +- 12 files changed, 251 insertions(+), 71 deletions(-) diff --git a/crates/fzn-huub/src/tracing.rs b/crates/fzn-huub/src/tracing.rs index 09a101ac..61f5c2a7 100644 --- a/crates/fzn-huub/src/tracing.rs +++ b/crates/fzn-huub/src/tracing.rs @@ -129,7 +129,7 @@ impl<'a, V: Visit> LitNames<'a, V> { #[inline] fn check_clause(&mut self, field: &Field, value: &dyn fmt::Debug) -> bool { - if matches!(field.name(), "clause") { + if matches!(field.name(), "clause" | "lits") { let res: Result, _> = serde_json::from_str(&format!("{:?}", value)); if let Ok(clause) = res { let mut v: Vec = Vec::with_capacity(clause.len()); @@ -140,7 +140,11 @@ impl<'a, V: Visit> LitNames<'a, V> { v.push(format!("Lit({})", i)); } } - self.inner.record_str(field, &v.join(" ∨ ")); + if field.name() == "clause" { + self.inner.record_str(field, &v.join(" ∨ ")); + } else { + self.inner.record_str(field, &v.join(", ")); + } return true; } } diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index ad356342..0681b93c 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -16,8 +16,8 @@ pub use self::{ use crate::{ model::int::IntVarDef, propagator::all_different::AllDifferentValue, - solver::{engine::int_var::IntVar as SlvIntVar, BoolView, SatSolver}, - Solver, + solver::{engine::int_var::IntVar as SlvIntVar, view::IntViewInner, BoolView, SatSolver}, + IntView, Solver, }; #[derive(Debug, Default)] @@ -108,18 +108,13 @@ impl Constraint { } } Constraint::AllDifferent(v) => { - let (vars, vals): (Vec<_>, _) = v + let vars: Vec<_> = v .iter() .map(|v| v.to_arg(ReifContext::Mixed, slv, map)) - .partition(|x| matches!(x, SimplifiedInt::Var(_))); - if !vals.is_empty() { - todo!() - } - slv.add_propagator(AllDifferentValue::new(vars.into_iter().map(|v| { - let SimplifiedInt::Var(v) = v else { - unreachable!() - }; - v + .collect(); + slv.add_propagator(AllDifferentValue::new(vars.into_iter().map(|v| match v { + SimplifiedInt::Val(i) => IntView(IntViewInner::Const(i)), + SimplifiedInt::Var(v) => v, }))) } } diff --git a/crates/huub/src/propagator.rs b/crates/huub/src/propagator.rs index 7a1be48f..f6203ed8 100644 --- a/crates/huub/src/propagator.rs +++ b/crates/huub/src/propagator.rs @@ -19,14 +19,20 @@ use crate::{ pub trait Propagator: Debug { /// The method called by the solver to notify the propagator of a variable - /// event to which it has subscribed. The propagator can choose a priority - /// level if it wants to be placed in the propagation queue. + /// event to which it has subscribed. The method returns true if the + /// propagator should be placed in the propagation queue. /// /// The [`data`] argument will contain the data that the propagater has set /// when subscribing to an event. - fn notify_event(&mut self, data: u32) -> Option { + fn notify_event(&mut self, data: u32) -> bool { let _ = data; - Some(PriorityLevel::Medium) + false + } + + /// The method called by the solver to request at what priority level the + /// propagator should be placed in the propagation queue.œ + fn queue_priority_level(&self) -> PriorityLevel { + PriorityLevel::Medium } /// This method is called when the solver backtracks to a previous decision @@ -59,10 +65,13 @@ pub trait Propagator: Debug { } pub trait Initialize { - /// The method called when registering a propagator with the solver. This - /// method is generally used to register variable event subscriptions with the - /// solver. - fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) { + /// The method called when registering a propagator with the solver, the method + /// returns true when the propagator needs to be enqued immediately.œ + /// + /// This method is generally used to register variable event + /// subscriptions with the solver. + fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool { let _ = actions; + false } } diff --git a/crates/huub/src/propagator/all_different.rs b/crates/huub/src/propagator/all_different.rs index d93b1343..03b15d71 100644 --- a/crates/huub/src/propagator/all_different.rs +++ b/crates/huub/src/propagator/all_different.rs @@ -5,6 +5,7 @@ use crate::{ }, solver::{ engine::{int_var::LitMeaning, queue::PriorityLevel}, + view::IntViewInner, IntView, SatSolver, }, }; @@ -17,17 +18,30 @@ pub struct AllDifferentValue { impl AllDifferentValue { pub fn new, I: IntoIterator>(vars: I) -> Self { - Self { - vars: vars.into_iter().map(Into::into).collect(), - action_list: Vec::new(), - } + let vars: Vec = vars.into_iter().map(Into::into).collect(); + let action_list = vars + .iter() + .enumerate() + .filter_map(|(i, v)| { + if matches!(v.0, IntViewInner::Const(_)) { + Some(i as u32) + } else { + None + } + }) + .collect(); + Self { vars, action_list } } } impl Propagator for AllDifferentValue { - fn notify_event(&mut self, data: u32) -> Option { + fn notify_event(&mut self, data: u32) -> bool { self.action_list.push(data); - Some(PriorityLevel::Low) + true + } + + fn queue_priority_level(&self) -> PriorityLevel { + PriorityLevel::Low } fn notify_backtrack(&mut self, _new_level: usize) { @@ -38,11 +52,13 @@ impl Propagator for AllDifferentValue { while let Some(i) = self.action_list.pop() { let var = self.vars[i as usize]; let val = actions.get_int_val(var).unwrap(); - let lit = actions.get_int_lit(var, LitMeaning::Eq(val)); + let r = actions + .get_int_lit(var, LitMeaning::Eq(val)) + .map(Reason::Simple); for (j, &v) in self.vars.iter().enumerate() { let j_val = actions.get_int_val(v); if (j as u32) != i && (j_val.is_none() || j_val.unwrap() == val) { - actions.set_int_not_eq(v, val, Reason::Simple(lit))? + actions.set_int_not_eq(v, val, r.clone())? } } } @@ -51,10 +67,11 @@ impl Propagator for AllDifferentValue { } impl Initialize for AllDifferentValue { - fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) { + fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool { for (i, v) in self.vars.iter().enumerate() { actions.subscribe_int(*v, IntEvent::Fixed, i as u32) } + !self.action_list.is_empty() } } @@ -95,6 +112,6 @@ mod tests { let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true); slv.add_propagator(AllDifferentValue::new(vec![a, b, c])); - assert_eq!(slv.solve(|_| { assert!(false) }), SolveResult::Unsat) + assert_eq!(slv.solve(|_| { unreachable!() }), SolveResult::Unsat) } } diff --git a/crates/huub/src/propagator/init_action.rs b/crates/huub/src/propagator/init_action.rs index 90f5bd3b..17dd9e4c 100644 --- a/crates/huub/src/propagator/init_action.rs +++ b/crates/huub/src/propagator/init_action.rs @@ -35,6 +35,7 @@ impl InitializationActions<'_, Sat> { .entry(var) .or_default() .push((self.prop_ref, event, data)), + Const(_) => {} } } } diff --git a/crates/huub/src/propagator/propagation_action.rs b/crates/huub/src/propagator/propagation_action.rs index c2802126..16353c96 100644 --- a/crates/huub/src/propagator/propagation_action.rs +++ b/crates/huub/src/propagator/propagation_action.rs @@ -30,27 +30,27 @@ pub struct PropagationActions<'a> { impl PropagationActions<'_> { #[allow(dead_code)] // TODO pub fn get_bool_val(&self, lit: RawLit) -> Option { - let is_neg = lit.is_negated(); - self.sat_trail - .get(lit.var()) - .map(|v| if is_neg { !v } else { v }) + self.sat_trail.get(lit) } - pub fn get_int_lit(&mut self, var: IntView, bv: LitMeaning) -> RawLit { + pub fn get_int_lit(&mut self, var: IntView, bv: LitMeaning) -> Option { match var.0 { - IntViewInner::VarRef(iv) => self.int_vars[iv].get_bool_var(bv), + IntViewInner::VarRef(iv) => Some(self.int_vars[iv].get_bool_var(bv)), + IntViewInner::Const(_) => None, } } pub fn get_int_lower_bound(&self, var: IntView) -> IntVal { match var.0 { IntViewInner::VarRef(iv) => self.int_trail[self.int_vars[iv].lower_bound], + IntViewInner::Const(i) => i, } } pub fn get_int_upper_bound(&self, var: IntView) -> IntVal { match var.0 { IntViewInner::VarRef(iv) => self.int_trail[self.int_vars[iv].upper_bound], + IntViewInner::Const(i) => i, } } @@ -64,15 +64,129 @@ impl PropagationActions<'_> { } } - pub fn set_int_not_eq(&mut self, var: IntView, val: i64, r: Reason) -> Result<(), Conflict> { + pub fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool { match var.0 { IntViewInner::VarRef(iv) => { + let lb = self.get_int_lower_bound(var); + let ub = self.get_int_upper_bound(var); + if (lb..=ub).contains(&val) { + let lit = self.int_vars[iv].get_bool_var(LitMeaning::Eq(val)); + self.sat_trail.get(lit).unwrap_or(true) + } else { + false + } + } + IntViewInner::Const(i) => i == val, + } + } + + #[allow(dead_code)] + pub fn set_int_lower_bound( + &mut self, + var: IntView, + val: IntVal, + r: Option, + ) -> Result<(), Conflict> { + match var.0 { + IntViewInner::VarRef(iv) => { + if self.get_int_lower_bound(var) >= val { + return Ok(()); + } + let lit = self.int_vars[iv].get_bool_var(LitMeaning::GreaterEq(val)); + if let Some(r) = r { + self.reason_map.insert(lit, r); + } + self.lit_queue.push(lit); + } + IntViewInner::Const(i) => { + if i < val { + todo!() + } + } + } + Ok(()) + } + + #[allow(dead_code)] + pub fn set_int_upper_bound( + &mut self, + var: IntView, + val: IntVal, + r: Option, + ) -> Result<(), Conflict> { + match var.0 { + IntViewInner::VarRef(iv) => { + if self.get_int_upper_bound(var) <= val { + return Ok(()); + } + let lit = self.int_vars[iv].get_bool_var(LitMeaning::Less(val + 1)); + if let Some(r) = r { + self.reason_map.insert(lit, r); + } + self.lit_queue.push(lit); + } + IntViewInner::Const(i) => { + if i > val { + todo!() + } + } + } + Ok(()) + } + + #[allow(dead_code)] + pub fn set_int_val( + &mut self, + var: IntView, + val: IntVal, + r: Option, + ) -> Result<(), Conflict> { + match var.0 { + IntViewInner::VarRef(iv) => { + if self.get_int_val(var) == Some(val) { + return Ok(()); + } + let lit = self.int_vars[iv].get_bool_var(LitMeaning::Eq(val)); + if let Some(r) = r { + self.reason_map.insert(lit, r); + } + self.lit_queue.push(lit); + // TODO: Should this trigger notify? + // TODO: Check conflict + } + IntViewInner::Const(i) => { + if i != val { + todo!() + } + } + }; + Ok(()) + } + + pub fn set_int_not_eq( + &mut self, + var: IntView, + val: IntVal, + r: Option, + ) -> Result<(), Conflict> { + match var.0 { + IntViewInner::VarRef(iv) => { + if !self.check_int_in_domain(var, val) { + return Ok(()); + } let lit = self.int_vars[iv].get_bool_var(LitMeaning::NotEq(val)); - self.reason_map.insert(lit, r); + if let Some(r) = r { + self.reason_map.insert(lit, r); + } self.lit_queue.push(lit); // TODO: Should this trigger notify? // TODO: Check conflict } + IntViewInner::Const(i) => { + if i == val { + todo!() + } + } }; Ok(()) } diff --git a/crates/huub/src/propagator/reason.rs b/crates/huub/src/propagator/reason.rs index de4807e9..2812fef2 100644 --- a/crates/huub/src/propagator/reason.rs +++ b/crates/huub/src/propagator/reason.rs @@ -2,6 +2,7 @@ use pindakaas::Lit; use crate::solver::engine::PropRef; +#[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Reason { /// A promise that a given propagator will compute a causation of the change /// when given the attached data diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index da1c6ec1..acb81751 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -47,6 +47,7 @@ impl Solver { SolverView::Bool(lit) => sat_value(lit.0).map(Value::Bool), SolverView::Int(var) => match var.0 { IntViewInner::VarRef(iv) => Some(Value::Int(int_vars[iv].get_value(sat_value))), + IntViewInner::Const(i) => Some(Value::Int(i)), }, }; on_sol(wrapper); @@ -78,8 +79,13 @@ impl Solver { prop_ref, slv: self, }; - prop.initialize(&mut actions); + let enqueue = prop.initialize(&mut actions); + if enqueue { + let level = prop.queue_priority_level(); + self.engine_mut().prop_queue.insert(level, prop_ref); + } self.engine_mut().propagators.push(Box::new(prop)); + self.engine_mut().enqueued.push(enqueue); } } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 884ba6eb..a08a2b74 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -38,12 +38,14 @@ pub struct Engine { pub(crate) bool_to_int: BoolToIntMap, /// Queue of propagators awaiting action - prop_queue: PriorityQueue, + pub(crate) prop_queue: PriorityQueue, pub(crate) reason_map: HashMap, - /// Storage for the propagators used by the + /// Storage of the propagators pub(crate) propagators: IndexVec>, + /// Flag for whether a propagator is enqueued + pub(crate) enqueued: IndexVec, /// Storage for the integer variables pub(crate) int_vars: IndexVec, /// Trailed integers @@ -70,15 +72,20 @@ impl IpasirPropagator for Engine { persistent, "assignment" ); - if persistent { + + // Process Boolean assignment + if persistent && self.int_trail.decision_level() != 0 { self.persistent.push((var, val)) } self.bool_trail.assign(var, val); - for (prop, data) in self.bool_subscribers.get(&var).into_iter().flatten() { - if let Some(l) = self.propagators[*prop].notify_event(*data) { - self.prop_queue.insert(l, *prop); + for &(prop, data) in self.bool_subscribers.get(&var).into_iter().flatten() { + if self.propagators[prop].notify_event(data) && !self.enqueued[prop] { + let level = self.propagators[prop].queue_priority_level(); + self.prop_queue.insert(level, prop); } } + + // Process Integer consequences if let Some(iv) = self.bool_to_int.get(var) { let lb = self.int_trail[self.int_vars[iv].lower_bound]; let ub = self.int_trail[self.int_vars[iv].upper_bound]; @@ -141,10 +148,12 @@ impl IpasirPropagator for Engine { }; for (prop, level, data) in self.int_subscribers.get(&iv).into_iter().flatten() { - if level.is_activated_by(&event) { - if let Some(l) = self.propagators[*prop].notify_event(*data) { - self.prop_queue.insert(l, *prop) - } + if level.is_activated_by(&event) + && self.propagators[*prop].notify_event(*data) + && !self.enqueued[*prop] + { + let level = self.propagators[*prop].queue_priority_level(); + self.prop_queue.insert(level, *prop); } } } @@ -193,7 +202,16 @@ impl IpasirPropagator for Engine { }; while let Some(p) = self.prop_queue.pop() { let prop = self.propagators[p].as_mut(); - if prop.propagate(&mut context).is_err() { + let _ = prop.propagate(&mut context); + if !context.lit_queue.is_empty() { + trace!( + lits = ?context + .lit_queue + .iter() + .map(|&x| i32::from(x)) + .collect::>(), + "propagate" + ); break; } } @@ -201,21 +219,26 @@ impl IpasirPropagator for Engine { } fn add_reason_clause(&mut self, propagated_lit: pindakaas::Lit) -> Vec { - let reason = match &self.reason_map[&propagated_lit] { - Reason::Lazy(prop, data) => { - let reason = self.propagators[*prop].explain(*data); - once(propagated_lit) - .chain(reason.iter().map(|l| !l)) - .collect() - } - Reason::Eager(v) => once(propagated_lit).chain(v.iter().map(|l| !l)).collect(), - Reason::Simple(l) => vec![propagated_lit, !l], - }; + let reason = self + .reason_map + .get(&propagated_lit) + .map(|r| match r { + Reason::Lazy(prop, data) => { + let reason = self.propagators[*prop].explain(*data); + once(propagated_lit) + .chain(reason.iter().map(|l| !l)) + .collect() + } + Reason::Eager(v) => once(propagated_lit).chain(v.iter().map(|l| !l)).collect(), + Reason::Simple(l) => vec![propagated_lit, !l], + }) + .unwrap_or_else(|| vec![propagated_lit]); trace!(clause = ?reason.iter().map(|&x| i32::from(x)).collect::>(), "give reason clause"); reason } fn check_model(&mut self, sat_value: &dyn pindakaas::Valuation) -> bool { + trace!("check model"); for (r, iv) in self.int_vars.iter_mut().enumerate() { let r = IntVarRef::new(r); let lb = self.int_trail[iv.lower_bound]; @@ -226,10 +249,11 @@ impl IpasirPropagator for Engine { self.int_trail.assign(iv.upper_bound, val); for (prop, level, data) in self.int_subscribers.get(&r).into_iter().flatten() { - if level.is_activated_by(&IntEvent::Fixed) { - if let Some(l) = self.propagators[*prop].notify_event(*data) { - self.prop_queue.insert(l, *prop) - } + if level.is_activated_by(&IntEvent::Fixed) + && self.propagators[*prop].notify_event(*data) + { + let l = self.propagators[*prop].queue_priority_level(); + self.prop_queue.insert(l, *prop) } } } diff --git a/crates/huub/src/solver/engine/trail.rs b/crates/huub/src/solver/engine/trail.rs index 25d87872..7f61e329 100644 --- a/crates/huub/src/solver/engine/trail.rs +++ b/crates/huub/src/solver/engine/trail.rs @@ -1,7 +1,7 @@ use std::{collections::HashMap, mem, ops::Index}; use index_vec::{Idx, IndexVec}; -use pindakaas::Var as RawVar; +use pindakaas::{Lit as RawLit, Var as RawVar}; #[derive(Debug)] pub struct Trail { @@ -36,6 +36,10 @@ impl Trail { self.value[i] = val; } } + + pub fn decision_level(&self) -> usize { + self.prev_len.len() + } } impl Trail { @@ -88,7 +92,8 @@ impl SatTrail { } } - pub fn get(&self, var: RawVar) -> Option { - self.value.get(&var).copied() + pub fn get>(&self, lit: L) -> Option { + let lit = lit.into(); + self.value.get(&lit.var()).copied().map(|x| !x) } } diff --git a/crates/huub/src/solver/value.rs b/crates/huub/src/solver/value.rs index 94266290..d6932f40 100644 --- a/crates/huub/src/solver/value.rs +++ b/crates/huub/src/solver/value.rs @@ -1,9 +1,10 @@ +use super::engine::int_var::IntVal; use crate::solver::SolverView; #[derive(Debug, PartialEq, Eq, Hash)] pub enum Value { Bool(bool), - Int(i64), + Int(IntVal), } pub trait Valuation: Fn(SolverView) -> Option {} diff --git a/crates/huub/src/solver/view.rs b/crates/huub/src/solver/view.rs index c40167c1..b759afc6 100644 --- a/crates/huub/src/solver/view.rs +++ b/crates/huub/src/solver/view.rs @@ -2,7 +2,7 @@ use std::num::NonZeroI32; use pindakaas::Lit as RawLit; -use super::engine::int_var::LitMeaning; +use super::engine::int_var::{IntVal, LitMeaning}; use crate::{ solver::{engine::int_var::IntVarRef, SatSolver}, Solver, @@ -90,6 +90,7 @@ impl IntView { debug_assert!(var_iter.next().is_none()); } + IntViewInner::Const(_) => {} } } @@ -99,6 +100,7 @@ impl IntView { let pos: usize = v.into(); map[pos] = name; } + IntViewInner::Const(_) => {} } } } @@ -106,4 +108,5 @@ impl IntView { #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] pub(crate) enum IntViewInner { VarRef(IntVarRef), + Const(IntVal), }