From bd96f287b5c1234ddeafadc7ea24b9ce96d8f138 Mon Sep 17 00:00:00 2001 From: Allen Zhong Date: Tue, 19 Nov 2024 13:42:52 +1100 Subject: [PATCH] add deactivate-after option --- crates/fzn-huub/src/lib.rs | 8 ++++++++ crates/fzn-huub/src/main.rs | 1 + crates/huub/src/model.rs | 1 + crates/huub/src/solver.rs | 4 +++- crates/huub/src/solver/engine.rs | 25 +++++++++++++++++-------- 5 files changed, 30 insertions(+), 9 deletions(-) diff --git a/crates/fzn-huub/src/lib.rs b/crates/fzn-huub/src/lib.rs index 03d6cd4e..b1a7cf0d 100644 --- a/crates/fzn-huub/src/lib.rs +++ b/crates/fzn-huub/src/lib.rs @@ -79,6 +79,8 @@ pub struct Cli { vsids_after: Option, /// Only use the SAT VSIDS heuristic for search vsids_only: bool, + /// Deactivate propagators after a certain number of conflicts + deactivate_after: Option, /// 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 for Cli 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)) diff --git a/crates/fzn-huub/src/main.rs b/crates/fzn-huub/src/main.rs index 2624738d..aab9c6eb 100644 --- a/crates/fzn-huub/src/main.rs +++ b/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 Deactivate propagators after a certain number of conflicts. --additive-factor Additive factor for increasing the activity scores of propagators. --multiplicative-factor Multiplicative factor for decaying the activity scores of propagators. --propagator-threshold The threshold of activity score for propagators to be activated in diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index 1691261d..89ecc904 100644 --- a/crates/huub/src/model.rs +++ b/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"); } diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index 08d3c2c5..9753470d 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -84,6 +84,8 @@ pub(crate) struct SolverConfiguration { vsids_after: Option, /// 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, /// 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> Solver { pub fn set_vsids_after(&mut self, conflicts: Option); 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); + pub fn set_propagator_activity_factors(&mut self, deactivate_after: Option, threshold: f64, additive: f64, multiplicative: f64, trace_propagations: Option); pub fn set_check_multiple_conflicts(&mut self, enable: bool); pub fn set_enqueue_functional(&mut self, enable: bool); } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 20e2f356..c446ef7d 100644 --- a/crates/huub/src/solver/engine.rs +++ b/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, threshold: f64, additive: f64, multiplicative: f64, trace_propagations: Option, ) { + self.config.deactivate_after = deactivate_after; self.config.propagator_activity_threshold = threshold; self.config.propagtor_additive_factor = additive; self.config.propagtor_multiplicative_factor = multiplicative;