From adc1e2e0529de63dd9af077d99eb4b85ba0b58e8 Mon Sep 17 00:00:00 2001 From: Allen Zhong Date: Thu, 17 Oct 2024 18:07:11 +1100 Subject: [PATCH] use explanation events to adjust activity score --- crates/fzn-huub/src/lib.rs | 1 + crates/huub/src/propagator/reason.rs | 11 +++--- crates/huub/src/solver.rs | 12 +++++++ crates/huub/src/solver/engine.rs | 34 +++++++++++-------- .../huub/src/solver/engine/solving_context.rs | 19 ++++------- 5 files changed, 43 insertions(+), 34 deletions(-) diff --git a/crates/fzn-huub/src/lib.rs b/crates/fzn-huub/src/lib.rs index c9c84433..cd7bf98e 100644 --- a/crates/fzn-huub/src/lib.rs +++ b/crates/fzn-huub/src/lib.rs @@ -197,6 +197,7 @@ where &[ ("intVariables", &stats.int_vars()), ("propagators", &stats.propagators()), + ("functional_propagators", &stats.functional_propagators()), ("unifiedVariables", &fzn_stats.unified_variables()), ("extractedViews", &fzn_stats.extracted_views()), ( diff --git a/crates/huub/src/propagator/reason.rs b/crates/huub/src/propagator/reason.rs index d488dd5d..13d05476 100644 --- a/crates/huub/src/propagator/reason.rs +++ b/crates/huub/src/propagator/reason.rs @@ -1,6 +1,5 @@ use std::{iter::once, marker::PhantomData, mem}; -use index_vec::IndexVec; use pindakaas::Lit as RawLit; use crate::{ @@ -30,7 +29,7 @@ pub(crate) struct LazyReason(pub(crate) PropRef, pub(crate) u64); pub(crate) enum Reason { /// A promise that a given propagator will compute a causation of the change /// when given the attached data - Lazy(PropRef, u64), + Lazy(u64), /// A conjunction of literals forming the causation of the change Eager(Box<[RawLit]>), Simple(RawLit), @@ -55,13 +54,13 @@ impl Reason { /// When the `lit` argument is `None`, the reason is explaining `false`. pub(crate) fn explain>( &self, - props: &mut IndexVec, + prop: &mut BoxedPropagator, actions: &mut State, lit: Option, ) -> Clause { match self { - Reason::Lazy(prop, data) => { - let reason = props[*prop].explain(actions, lit, *data); + Reason::Lazy(data) => { + let reason = prop.explain(actions, lit, *data); reason.into_iter().map(|l| !l).chain(lit).collect() } Reason::Eager(v) => v.iter().map(|l| !l).chain(lit).collect(), @@ -134,7 +133,7 @@ where impl ReasonBuilder for LazyReason { fn build_reason(self, _: &mut A) -> Result { - Ok(Reason::Lazy(self.0, self.1)) + Ok(Reason::Lazy(self.1)) } } diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index b7258e87..423ba653 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -77,6 +77,8 @@ pub struct InitStatistics { int_vars: usize, /// Number of propagators in the solver propagators: usize, + /// Number of functional propagators in the solver + functional_propagators: usize, } pub trait SatSolver: @@ -118,6 +120,9 @@ impl InitStatistics { pub fn propagators(&self) -> usize { self.propagators } + pub fn functional_propagators(&self) -> usize { + self.functional_propagators + } } impl Solver @@ -382,6 +387,13 @@ where InitStatistics { int_vars: self.engine().state.int_vars.len(), propagators: self.engine().propagators.len(), + functional_propagators: self + .engine() + .state + .functional + .iter() + .filter(|&&x| x) + .count(), } } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 712b8757..6bf1f6a4 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -118,8 +118,8 @@ pub(crate) struct State { pub(crate) trail: Trail, /// Literals to be propagated by the oracle pub(crate) propagation_queue: Conjunction, - /// Reasons for setting values - pub(crate) reason_map: HashMap, + /// Reasons and Propagators for setting values of literals + pub(crate) reason_map: HashMap, /// Whether conflict has (already) been detected pub(crate) conflict: Option, @@ -285,9 +285,9 @@ impl IpasirPropagator for Engine { if let Some(prev) = prev { self.notify_assignments(&[prev]); } - if let Some(reason) = self.state.reason_map.get(&lit).cloned() { + if let Some((prop, reason)) = self.state.reason_map.get(&lit).cloned() { let clause: Clause = - reason.explain(&mut self.propagators, &mut self.state, Some(lit)); + reason.explain(&mut self.propagators[prop], &mut self.state, Some(lit)); for l in &clause { if l == &lit { continue; @@ -315,19 +315,23 @@ impl IpasirPropagator for Engine { // Find reason let reason = self.state.reason_map.remove(&propagated_lit); // Restore the current state to the state when the propagation happened if explaining lazily - if matches!(reason, Some(Reason::Lazy(_, _))) { + if matches!(reason, Some((_, Reason::Lazy(_)))) { self.state.trail.goto_assign_lit(propagated_lit); } // Create a clause from the reason - let clause = if let Some(reason) = reason { - reason.explain(&mut self.propagators, &mut self.state, Some(propagated_lit)) + let clause = if let Some((p, reason)) = reason { + self.state.explanations += 1; + self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; + + reason.explain( + &mut self.propagators[p], + &mut self.state, + Some(propagated_lit), + ) } else { vec![propagated_lit] }; - // TODO: how to get the propagator for explanations of the propagated literals? - self.state.explanations += 1; - debug!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::>(), "add reason clause"); clause } @@ -545,8 +549,8 @@ impl State { fn ensure_clause_changes(&mut self, propagators: &mut IndexVec) { let queue = mem::take(&mut self.propagation_queue); for lit in queue { - let clause = if let Some(reason) = self.reason_map.remove(&lit) { - reason.explain(propagators, self, Some(lit)) + let clause = if let Some((prop, reason)) = self.reason_map.remove(&lit) { + reason.explain(&mut propagators[prop], self, Some(lit)) } else { vec![lit] }; @@ -652,7 +656,7 @@ impl State { for &prop in self.bool_activation.get(&lit.var()).into_iter().flatten() { if Some(prop) != skip && !self.enqueued[prop] { if !self.vsids - && self.activity_scores[prop] >= self.config.propagator_activity_threshold + || self.activity_scores[prop] >= self.config.propagator_activity_threshold { self.propagator_queue .insert(self.propagator_priority[prop], prop); @@ -670,11 +674,11 @@ impl State { } } - fn register_reason(&mut self, lit: RawLit, built_reason: Result) { + fn register_reason(&mut self, lit: RawLit, prop: PropRef, built_reason: Result) { match built_reason { Ok(reason) => { // Insert new reason, possibly overwriting old one (from previous search attempt) - let _ = self.reason_map.insert(lit, reason); + let _ = self.reason_map.insert(lit, (prop, reason)); } Err(true) => { // No (previous) reason required diff --git a/crates/huub/src/solver/engine/solving_context.rs b/crates/huub/src/solver/engine/solving_context.rs index 2a7d1298..a5fad4e6 100644 --- a/crates/huub/src/solver/engine/solving_context.rs +++ b/crates/huub/src/solver/engine/solving_context.rs @@ -66,13 +66,13 @@ impl<'a> SolvingContext<'a> { > 0 { info!( - "time={time} propagation results conflicts={conflicts}, propagations={propagations}, no_propagations={no_propagations}, explanations={explanations}, trace_interval={interval}", + "time={time} propagation results conflicts={conflicts}, propagations={propagations}, no_propagations={no_propagations}, explanations={explanations}, search={search}", time= self.state.time_slot, conflicts = self.state.conflicts, propagations = self.state.propagations, no_propagations = self.state.no_propagations, explanations = self.state.explanations, - interval = self.state.config.trace_propagations.unwrap() + search = if self.state.vsids { "VSIDS" } else { "User" } ); self.state.time_slot = (self.state.timer.elapsed().as_millis() / self.state.config.trace_propagations.unwrap()) as usize; @@ -94,26 +94,19 @@ impl<'a> SolvingContext<'a> { // If the propagator detected a conflict or add new literals to the propagation queue, // additively increase the activity score of the propagator if let Err(Conflict { subject, reason }) = res { - let clause: Clause = reason.explain(propagators, self.state, subject); + let clause: Clause = reason.explain(&mut propagators[p], self.state, subject); trace!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::>(), "conflict detected"); debug_assert!(!clause.is_empty()); debug_assert!(self.state.conflict.is_none()); self.state.conflict = Some(clause); - if !self.state.functional[p] { - self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; - } + self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; self.state.conflicts += 1; } else if propagation_before != self.state.propagation_queue.len() { - if !self.state.functional[p] { - self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; - } self.state.propagations += 1; - } else if !self.state.functional[p] { + } else { // After wake-up, multiplicatively decay the activity score of the propagator if no propagations self.state.activity_scores[p] *= self.state.config.propagtor_multiplicative_factor; self.state.no_propagations += 1; - } else { - self.state.no_propagations += 1; } if self.state.conflict.is_some() || !self.state.propagation_queue.is_empty() { @@ -259,7 +252,7 @@ impl PropagationActions for SolvingContext<'_> { None => { let reason = reason.build_reason(self); trace!(lit = i32::from(lit), reason = ?reason, "propagate bool"); - self.state.register_reason(lit, reason); + self.state.register_reason(lit, self.current_prop, reason); self.state.propagation_queue.push(lit); Ok(()) }