add deactivate-after option

crates/fzn-huub/src/lib.rs

@@ -79,6 +79,8 @@ 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
@@ -269,6 +271,7 @@ where
 		}
 
 		slv.set_propagator_activity_factors(
+			self.deactivate_after,
 			self.propagator_activity_threshold,
 			self.propagator_additive_factor,
 			self.propagator_multiplicative_factor,
@@ -522,6 +525,7 @@ 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,
@@ -550,6 +554,7 @@ 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,
@@ -611,6 +616,9 @@ 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))

crates/fzn-huub/src/main.rs

@@ -44,6 +44,7 @@ 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

crates/huub/src/model.rs

@@ -86,6 +86,7 @@ impl Model {
 			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");
 		}

crates/huub/src/solver.rs

@@ -84,6 +84,8 @@ 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,
+	/// Deactivate propagators after the given number of conflicts.
+	deactivate_after: Option<u32>,
 	/// Additive constant for the activity-based activation of propagators.
 	propagtor_additive_factor: f64,
 	/// Multiplicative constant for the activity-based activation of propagators.
@@ -408,7 +410,7 @@ impl<Oracle: PropagatingSolver<Engine>> Solver<Oracle> {
 			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, trace_propagations: Option<u128>);
+			pub fn set_propagator_activity_factors(&mut self, deactivate_after: Option<u32>, threshold: f64, additive: f64, multiplicative: f64, trace_propagations: Option<u128>);
 			pub fn set_check_multiple_conflicts(&mut self, enable: bool);
 			pub fn set_enqueue_functional(&mut self, enable: bool);
 		}

crates/huub/src/solver/engine.rs

@@ -664,17 +664,16 @@ impl State {
 				if Some(prop) != skip {
 					if count == 0 {
 						force_enqueue.push(prop);
-					} 
+					}
 				}
 			}
-		} 
-		
+		}
+
 		for prop in self.int_activation[int_var].activated_by(event) {
 			if Some(prop) != skip {
 				possible_enqueue.push(prop);
 			}
 		}
-
 
 		for prop in force_enqueue {
 			if !self.enqueued[prop] {
@@ -688,8 +687,12 @@ impl State {
 			if self.enqueued[prop] || self.enqueued_inactive[prop] {
 				continue;
 			}
-			if (!self.vsids
-				|| self.activity_scores[prop] >= self.config.propagator_activity_threshold)
+			if self
+				.config
+				.deactivate_after
+				.map_or(false, |conflicts| (self.conflicts <= conflicts as usize))
+				|| (!self.vsids
+					|| self.activity_scores[prop] >= self.config.propagator_activity_threshold)
 				|| (self.config.enqueue_functional && self.functional[prop])
 			{
 				self.propagator_queue
@@ -761,8 +764,12 @@ impl State {
 				if self.enqueued[prop] || self.enqueued_inactive[prop] {
 					continue;
 				}
-				if (!self.vsids
-					|| self.activity_scores[prop] >= self.config.propagator_activity_threshold)
+				if self
+					.config
+					.deactivate_after
+					.map_or(false, |conflicts| (self.conflicts <= conflicts as usize))
+					|| (!self.vsids
+						|| self.activity_scores[prop] >= self.config.propagator_activity_threshold)
 					|| (self.config.enqueue_functional && self.functional[prop])
 				{
 					self.propagator_queue
@@ -840,11 +847,13 @@ impl State {
 
 	pub(crate) fn set_propagator_activity_factors(
 		&mut self,
+		deactivate_after: Option<u32>,
 		threshold: f64,
 		additive: f64,
 		multiplicative: f64,
 		trace_propagations: Option<u128>,
 	) {
+		self.config.deactivate_after = deactivate_after;
 		self.config.propagator_activity_threshold = threshold;
 		self.config.propagtor_additive_factor = additive;
 		self.config.propagtor_multiplicative_factor = multiplicative;