use explanation events to adjust activity score

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()),
 					(

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<Clause: FromIterator<RawLit>>(
 		&self,
-		props: &mut IndexVec<PropRef, BoxedPropagator>,
+		prop: &mut BoxedPropagator,
 		actions: &mut State,
 		lit: Option<RawLit>,
 	) -> 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<A: ExplanationActions> ReasonBuilder<A> for LazyReason {
 	fn build_reason(self, _: &mut A) -> Result<Reason, bool> {
-		Ok(Reason::Lazy(self.0, self.1))
+		Ok(Reason::Lazy(self.1))
 	}
 }
 

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<Sol, Sat> Solver<Sat>
@@ -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(),
 		}
 	}
 

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<RawLit, Reason>,
+	/// Reasons and Propagators for setting values of literals
+	pub(crate) reason_map: HashMap<RawLit, (PropRef, Reason)>,
 	/// Whether conflict has (already) been detected
 	pub(crate) conflict: Option<Clause>,
 
@@ -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::<Vec<i32>>(), "add reason clause");
 		clause
 	}
@@ -545,8 +549,8 @@ impl State {
 	fn ensure_clause_changes(&mut self, propagators: &mut IndexVec<PropRef, BoxedPropagator>) {
 		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<Reason, bool>) {
+	fn register_reason(&mut self, lit: RawLit, prop: PropRef, built_reason: Result<Reason, bool>) {
 		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

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::<Vec<i32>>(), "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(())
 				}