[WIP] add configurations to deactivate propagations of CP propagators

crates/fzn-huub/src/lib.rs

@@ -79,6 +79,21 @@ pub struct Cli<Stdout, Stderr> {
 	vsids_after: Option<u32>,
 	/// Only use the SAT VSIDS heuristic for search
 	vsids_only: bool,
+	/// Deactivate propagators after a certain number of conflicts
+	deactivate_after: Option<u32>,
+	/// 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,
+	/// Enable multiple conflict in checking
+	check_multiple_conflicts: bool,
+	/// Always allow functional constraints to be enqueued.
+	enqueue_functional: bool,
+
+	/// Interval in milliseconds to trace propagator activities
+	trace_propagations: Option<u128>,
 
 	// --- Output configuration ---
 	/// Output stream for (intermediate) solutions and statistics
@@ -188,6 +203,7 @@ where
 				&[
 					("intVariables", &stats.int_vars()),
 					("propagators", &stats.propagators()),
+					("functional_propagators", &stats.functional_propagators()),
 					("unifiedVariables", &fzn_stats.unified_variables()),
 					("extractedViews", &fzn_stats.extracted_views()),
 					(
@@ -254,6 +270,17 @@ where
 			slv.set_vsids_after(self.vsids_after);
 		}
 
+		slv.set_propagator_activity_factors(
+			self.deactivate_after,
+			self.propagator_activity_threshold,
+			self.propagator_additive_factor,
+			self.propagator_multiplicative_factor,
+			self.trace_propagations,
+		);
+
+		slv.set_check_multiple_conflicts(self.check_multiple_conflicts);
+		slv.set_enqueue_functional(self.enqueue_functional);
+
 		// Determine Goal and Objective
 		let start_solve = Instant::now();
 		let goal = if fzn.solve.method != Method::Satisfy {
@@ -498,6 +525,13 @@ where
 			vivification: self.vivification,
 			vsids_after: self.vsids_after,
 			vsids_only: self.vsids_only,
+			deactivate_after: self.deactivate_after,
+			propagator_additive_factor: self.propagator_additive_factor,
+			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
+			propagator_activity_threshold: self.propagator_activity_threshold,
+			trace_propagations: self.trace_propagations,
+			check_multiple_conflicts: self.check_multiple_conflicts,
+			enqueue_functional: self.enqueue_functional,
 			stdout: self.stdout,
 		}
 	}
@@ -520,6 +554,13 @@ where
 			vivification: self.vivification,
 			vsids_after: self.vsids_after,
 			vsids_only: self.vsids_only,
+			deactivate_after: self.deactivate_after,
+			propagator_additive_factor: self.propagator_additive_factor,
+			propagator_multiplicative_factor: self.propagator_multiplicative_factor,
+			propagator_activity_threshold: self.propagator_activity_threshold,
+			trace_propagations: self.trace_propagations,
+			check_multiple_conflicts: self.check_multiple_conflicts,
+			enqueue_functional: self.enqueue_functional,
 			stderr: self.stderr,
 			ansi_color: self.ansi_color,
 		}
@@ -543,6 +584,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"]),
 			all_optimal: args.contains("--all-optimal"),
@@ -570,6 +616,26 @@ 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())?,
+			deactivate_after: args
+				.opt_value_from_str("--deactivate-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())?,
+			trace_propagations: args
+				.opt_value_from_str("--trace-propagations")
+				.map_err(|e| e.to_string())?,
+			check_multiple_conflicts: args.contains("--check-multiple-conflicts"),
+			enqueue_functional: args.contains("--enqueue-functional"),
 
 			verbose,
 			path: args
@@ -579,7 +645,7 @@ impl TryFrom<Arguments> for Cli<io::Stdout, fn() -> io::Stderr> {
 			stdout: io::stdout(),
 			#[expect(trivial_casts, reason = "doesn't compile without the case")]
 			stderr: io::stderr as fn() -> io::Stderr,
-			ansi_color: true,
+			ansi_color: args.contains("--ansi-color"),
 		};
 
 		let remaining = args.finish();

crates/fzn-huub/src/main.rs

@@ -44,7 +44,11 @@ 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.
-
+  --deactivate-after <value>      Deactivate propagators after a certain number of conflicts.
+  --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/actions/initialization.rs

@@ -9,11 +9,24 @@ pub(crate) trait InitializationActions: DecisionActions {
 		&mut self,
 		clause: I,
 	) -> Result<(), ReformulationError>;
+
 	/// Create a new trailed integer value with the given initial value.
 	fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt;
+
 	/// Enqueue a propagator to be enqueued when a boolean variable is assigned.
 	fn enqueue_on_bool_change(&mut self, var: BoolView);
+
 	/// Enqueue a propagator to be enqueued when an integer variable is changed
 	/// according to the given propagation condition.
 	fn enqueue_on_int_change(&mut self, var: IntView, condition: IntPropCond);
+
+	/// Enqueue the propagator when at least "n" of the given variables are fixed,
+	/// and whenever a subsequent variable is fixed.
+	///
+	/// # Warning
+	/// This function will panic
+	/// - if it is called when initiliazing a brancher,
+	/// - if it is called multiple times for the same propagator,
+	/// - or if the number of variables is lower than `n`.
+	fn enqueue_when_n_fixed(&mut self, n: usize, bool_vars: &[BoolView], int_vars: &[IntView]);
 }

crates/huub/src/helpers/opt_field.rs

@@ -10,6 +10,9 @@ impl<const B: usize, T> OptField<B, T> {
 	pub(crate) fn get(&self) -> Option<&T> {
 		self.value.first()
 	}
+	pub(crate) fn is_some(&self) -> bool {
+		!self.value.is_empty()
+	}
 }
 impl<T> OptField<1, T> {
 	pub(crate) fn new(value: T) -> Self {

crates/huub/src/model.rs

@@ -38,6 +38,7 @@ pub struct Model {
 	pub(crate) cnf: Cnf,
 	branchings: Vec<Branching>,
 	constraints: Vec<Constraint>,
+	functional: Vec<bool>,
 	int_vars: Vec<IntVarDef>,
 	prop_queue: VecDeque<usize>,
 	enqueued: Vec<bool>,
@@ -84,6 +85,8 @@ impl Model {
 		if let Some(r) = any_slv.downcast_mut::<Cadical>() {
 			r.set_option("restart", config.restart() as i32);
 			r.set_option("vivify", config.vivification() as i32);
+			r.set_option("chrono", false as i32);
+			r.set_option("phase", 0);
 		} else {
 			warn!("unknown solver: vivification and restart options are ignored");
 		}
@@ -139,8 +142,8 @@ impl Model {
 		}
 
 		// Create constraint data structures within the solver
-		for c in self.constraints.iter() {
-			c.to_solver(&mut slv, &mut map)?;
+		for (i, c) in self.constraints.iter().enumerate() {
+			c.to_solver(&mut slv, &mut map, self.functional[i])?;
 		}
 		// Add branching data structures to the solver
 		for b in self.branchings.iter() {
@@ -162,6 +165,7 @@ impl AddAssign<Constraint> for Model {
 	fn add_assign(&mut self, rhs: Constraint) {
 		self.constraints.push(rhs);
 		self.enqueued.push(false);
+		self.functional.push(false);
 		self.enqueue(self.constraints.len() - 1);
 		self.subscribe(self.constraints.len() - 1);
 	}