add configurations to deactivate propagations of CP propagators

crates/fzn-huub/src/lib.rs

@@ -77,6 +77,12 @@ pub struct Cli<Stdout, Stderr> {
 	vsids_after: Option<u32>,
 	/// Only use the SAT VSIDS heuristic for search
 	vsids_only: bool,
+	/// Additive factor for propagator activation
+	propagator_additive_factor: f64,
+	/// Multiplicative factor for propagator activation
+	propagator_multiplicative_factor: f64,
+	/// Threshold for propagator activation
+	propagator_activity_threshold: f64,
 
 	// --- Output configuration ---
 	/// Output stream for (intermediate) solutions and statistics
@@ -252,6 +258,12 @@ where
 			slv.set_vsids_after(self.vsids_after);
 		}
 
+		slv.set_propagator_activity_factors(
+			self.propagator_activity_threshold,
+			self.propagator_additive_factor,
+			self.propagator_multiplicative_factor,
+		);
+
 		// Determine Goal and Objective
 		let start_solve = Instant::now();
 		let goal = if fzn.solve.method != Method::Satisfy {
@@ -449,6 +461,9 @@ where
 			vivification: self.vivification,
 			vsids_after: self.vsids_after,
 			vsids_only: self.vsids_only,
+			propagator_additive_factor: self.propagator_additive_factor,
+			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
+			propagator_activity_threshold: self.propagator_activity_threshold,
 			stdout: self.stdout,
 		}
 	}
@@ -470,6 +485,9 @@ where
 			vivification: self.vivification,
 			vsids_after: self.vsids_after,
 			vsids_only: self.vsids_only,
+			propagator_additive_factor: self.propagator_additive_factor,
+			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
+			propagator_activity_threshold: self.propagator_activity_threshold,
 			stderr: self.stderr,
 			ansi_color: self.ansi_color,
 		}
@@ -493,6 +511,11 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 			)),
 		};
 
+		let parse_float_arg = |s: &str| match s.parse::<f64>() {
+			Ok(v) => Ok(v),
+			Err(_) => Err(format!("expected a floating point number, found '{}'", s)),
+		};
+
 		let cli = Cli {
 			all_solutions: args.contains(["-a", "--all-solutions"]),
 			intermediate_solutions: args.contains(["-i", "--intermediate-solutions"]),
@@ -519,6 +542,18 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 			vsids_after: args
 				.opt_value_from_str("--vsids-after")
 				.map_err(|e| e.to_string())?,
+			propagator_additive_factor: args
+				.opt_value_from_fn("--additive-factor", parse_float_arg)
+				.map(|x| x.unwrap_or(0.0))
+				.map_err(|e| e.to_string())?,
+			propagator_multiplicative_factor: args
+				.opt_value_from_fn("--multiplicative-factor", parse_float_arg)
+				.map(|x| x.unwrap_or(1.0))
+				.map_err(|e| e.to_string())?,
+			propagator_activity_threshold: args
+				.opt_value_from_fn("--propagator-threshold", parse_float_arg)
+				.map(|x| x.unwrap_or(0.5))
+				.map_err(|e| e.to_string())?,
 
 			verbose,
 			path: args

crates/fzn-huub/src/main.rs

@@ -43,7 +43,10 @@ FLAGS
                                   (overwritten by --vsids-only)
   --vsids-only                    Only use the activity-based search heuristic provided by the SAT
                                   solver. Ignore the user-specific search heuristic.
-
+  --additive-factor <value>       Additive factor for increasing the activity scores of propagators.
+  --multiplicative-factor <value> Multiplicative factor for decaying the activity scores of propagators.
+  --propagator-threshold <value>  The threshold of activity score for propagators to be activated in
+                                  the propagation phase.
 
                       === BEHAVIOUR OPTIONS ===
   --log-file <FILE>	              Output log messages from the solver to a file, instead of stderr.

crates/huub/src/solver.rs

@@ -39,7 +39,7 @@ use crate::{
 	BoolView, IntVal, LitMeaning, ReformulationError,
 };
 
-#[derive(Clone, Debug, Default, PartialEq, Eq)]
+#[derive(Clone, Debug, Default)]
 pub(crate) struct SolverConfiguration {
 	/// Switch between the activity-based search heuristic and the user-specific search heuristic after each restart.
 	///
@@ -51,6 +51,12 @@ pub(crate) struct SolverConfiguration {
 	vsids_after: Option<u32>,
 	/// Only use the activity-based search heuristic provided by the SAT solver. Ignore the user-specific search heuristic.
 	vsids_only: bool,
+	/// Additive constant for the activity-based activation of propagators.
+	propagtor_additive_factor: f64,
+	/// Multiplicative constant for the activity-based activation of propagators.
+	propagtor_multiplicative_factor: f64,
+	/// The threshold for the activity-based activation of propagators.
+	propagator_activity_threshold: f64,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -158,6 +164,8 @@ where
 		debug_assert_eq!(prop_ref, p);
 		let p = self.engine_mut().state.enqueued.push(false);
 		debug_assert_eq!(prop_ref, p);
+		let p = self.engine_mut().state.activity_scores.push(1.0);
+		debug_assert_eq!(prop_ref, p);
 		if queue_pref.enqueue_on_post {
 			let state = &mut self.engine_mut().state;
 			state
@@ -378,6 +386,7 @@ where
 			pub fn set_vsids_after(&mut self, conflicts: Option<u32>);
 			pub fn set_vsids_only(&mut self, enable: bool);
 			pub fn set_toggle_vsids(&mut self, enable: bool);
+			pub fn set_propagator_activity_factors(&mut self, threshold: f64, additive: f64, multiplicative: f64);
 		}
 	}
 

crates/huub/src/solver/engine.rs

@@ -136,6 +136,8 @@ pub(crate) struct State {
 	pub(crate) propagator_priority: IndexVec<PropRef, PriorityLevel>,
 	/// Flag for whether a propagator is enqueued
 	pub(crate) enqueued: IndexVec<PropRef, bool>,
+	/// Activity scores for propagators to determine whether they are active or not
+	pub(crate) activity_scores: IndexVec<PropRef, f64>,
 }
 
 impl IpasirPropagator for Engine {
@@ -223,7 +225,8 @@ impl IpasirPropagator for Engine {
 		}
 		if self.state.propagation_queue.is_empty() && self.state.conflict.is_none() {
 			// If there are no previous changes, run propagators
-			SolvingContext::new(slv, &mut self.state).run_propagators(&mut self.propagators);
+			SolvingContext::new(slv, &mut self.state)
+				.run_propagators::<true>(&mut self.propagators);
 		}
 		// Check whether there are new clauses that need to be communicated first
 		if !self.state.clauses.is_empty() {
@@ -342,7 +345,7 @@ impl IpasirPropagator for Engine {
 		}
 
 		// Run propgagators to find any conflicts
-		ctx.run_propagators(&mut self.propagators);
+		ctx.run_propagators::<false>(&mut self.propagators);
 		// No propagation can be triggered (all variables are fixed, so only
 		// conflicts are possible)
 		debug_assert!(self.state.propagation_queue.is_empty());
@@ -529,7 +532,7 @@ impl State {
 		// Backtrack trail
 		self.trail.notify_backtrack(level);
 		// Empty propagation queue
-		while let Some(p) = self.propagator_queue.pop() {
+		while let Some(p) = self.propagator_queue.pop::<true>() {
 			self.enqueued[p] = false;
 		}
 		if ARTIFICIAL {
@@ -581,19 +584,29 @@ impl State {
 	) {
 		for prop in self.int_activation[int_var].activated_by(event) {
 			if Some(prop) != skip && !self.enqueued[prop] {
-				self.propagator_queue
-					.insert(self.propagator_priority[prop], prop);
-				self.enqueued[prop] = true;
+				let priority =
+					if self.activity_scores[prop] < self.config.propagator_activity_threshold {
+						trace!(propagator = usize::from(prop), "deactivate propagator");
+						PriorityLevel::Inactive
+					} else {
+						self.propagator_priority[prop]
+					};
+				self.propagator_queue.insert(priority, prop);
 			}
 		}
 	}
 
 	fn enqueue_propagators(&mut self, lit: RawLit, skip: Option<PropRef>) {
 		for &prop in self.bool_activation.get(&lit.var()).into_iter().flatten() {
 			if Some(prop) != skip && !self.enqueued[prop] {
-				self.propagator_queue
-					.insert(self.propagator_priority[prop], prop);
-				self.enqueued[prop] = true;
+				let priority =
+					if self.activity_scores[prop] < self.config.propagator_activity_threshold {
+						trace!(propagator = usize::from(prop), "deactivate propagator");
+						PriorityLevel::Inactive
+					} else {
+						self.propagator_priority[prop]
+					};
+				self.propagator_queue.insert(priority, prop);
 			}
 		}
 
@@ -629,6 +642,17 @@ impl State {
 		self.config.vsids_only = enable;
 		self.vsids = enable;
 	}
+
+	pub(crate) fn set_propagator_activity_factors(
+		&mut self,
+		threshold: f64,
+		additive: f64,
+		multiplicative: f64,
+	) {
+		self.config.propagator_activity_threshold = threshold;
+		self.config.propagtor_additive_factor = additive;
+		self.config.propagtor_multiplicative_factor = multiplicative;
+	}
 }
 
 impl ExplanationActions for State {

crates/huub/src/solver/engine/queue.rs

@@ -1,6 +1,8 @@
+const PRIORITY_LEVEL_COUNT: usize = PriorityLevel::Immediate as usize + 1;
+
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct PriorityQueue<E> {
-	storage: [Vec<E>; 6],
+	storage: [Vec<E>; PRIORITY_LEVEL_COUNT],
 }
 
 impl<E> Default for PriorityQueue<E> {
@@ -13,6 +15,7 @@ impl<E> Default for PriorityQueue<E> {
 				Vec::new(),
 				Vec::new(),
 				Vec::new(),
+				Vec::new(),
 			],
 		}
 	}
@@ -21,12 +24,12 @@ impl<E> Default for PriorityQueue<E> {
 impl<E> PriorityQueue<E> {
 	pub(crate) fn insert(&mut self, priority: PriorityLevel, elem: E) {
 		let i = priority as usize;
-		debug_assert!((0..=5).contains(&i));
+		debug_assert!((0..=PRIORITY_LEVEL_COUNT - 1).contains(&i));
 		self.storage[i].push(elem);
 	}
 
-	pub(crate) fn pop(&mut self) -> Option<E> {
-		for queue in self.storage.iter_mut().rev() {
+	pub(crate) fn pop<const SKIP_INACTIVE: bool>(&mut self) -> Option<E> {
+		for queue in self.storage.iter_mut().skip(SKIP_INACTIVE as usize).rev() {
 			if !queue.is_empty() {
 				return queue.pop();
 			}
@@ -38,6 +41,8 @@ impl<E> PriorityQueue<E> {
 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
 #[repr(u8)]
 pub(crate) enum PriorityLevel {
+	/// The inactive priority level, only triggered in check model
+	Inactive,
 	#[allow(
 		dead_code,
 		reason = "TODO: no current propagators are this priority level"

crates/huub/src/solver/engine/solving_context.rs

@@ -53,25 +53,38 @@ impl<'a> SolvingContext<'a> {
 
 	/// Run the propagators in the queue until a propagator detects a conflict,
 	/// returns literals to be propagated by the SAT oracle, or the queue is empty.
-	pub(crate) fn run_propagators(&mut self, propagators: &mut IndexVec<PropRef, BoxedPropagator>) {
-		while let Some(p) = self.state.propagator_queue.pop() {
+	/// The generic artugment `SKIP_INACTIVE` is used to skip the inactive propagators in the queue.
+	pub(crate) fn run_propagators<const SKIP_INACTIVE: bool>(
+		&mut self,
+		propagators: &mut IndexVec<PropRef, BoxedPropagator>,
+	) {
+		while let Some(p) = self.state.propagator_queue.pop::<SKIP_INACTIVE>() {
 			debug_assert!(self.state.conflict.is_none());
+			let propagation_before = self.state.propagation_queue.len();
 			self.state.enqueued[p] = false;
 			self.current_prop = p;
 			let prop = propagators[p].as_mut();
 			let res = prop.propagate(self);
 			self.state.statistics.propagations += 1;
 			self.current_prop = PropRef::new(u32::MAX as usize);
+			// 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);
-				trace!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::<Vec<i32>>(), "conflict detected");
+				trace!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::<Vec<i32>>(), prop =? p, "conflict detected");
 				debug_assert!(!clause.is_empty());
 				debug_assert!(self.state.conflict.is_none());
 				self.state.conflict = Some(clause);
+				self.state.activity_scores[p] += self.state.config.propagtor_additive_factor;
+			} else if propagation_before != self.state.propagation_queue.len() {
+				trace!(prop =? p, "literal propagated");
+				self.state.activity_scores[p] += self.state.config.propagtor_additive_factor;
 			}
 			if self.state.conflict.is_some() || !self.state.propagation_queue.is_empty() {
 				return;
 			}
+			// After wake-up, multiplicatively decay the activity score of the propagator
+			self.state.activity_scores[p] *= self.state.config.propagtor_multiplicative_factor;
 		}
 	}
 

share/minizinc/solvers/huub.msc

@@ -13,6 +13,9 @@
     ["--toggle-vsids", "Alternate between the activity-based search heuristic and the user-specific search heuristic after every restart.", "bool", "false"],
     ["--vivify","whether to enable vivification","bool:false:true","false"],
     ["--vsids-after", "Switch to activity-based search heuristic provided by the SAT solver after the given number of conflicts.", "int", "0"],
-    ["--vsids-only", "Only use the activity-based search provided by the SAT solver", "bool", "false"]
+    ["--vsids-only", "Only use the activity-based search provided by the SAT solver", "bool", "false"], 
+    ["--additive-factor", "Additive factor for increasing the activity scores of propagators.", "float", "0.0"],
+    ["--multiplicative-factor", "Multiplicative factor for decaying the activity scores of propagators.", "float", "1.0"],
+    ["--propagator-threshold", "The threshold of activity score for propagators to be activated in the propagation phase.", "float", "0.5"],
   ]
 }