diff --git a/crates/fzn-huub/src/lib.rs b/crates/fzn-huub/src/lib.rs index 8abda39f..b1a7cf0d 100644 --- a/crates/fzn-huub/src/lib.rs +++ b/crates/fzn-huub/src/lib.rs @@ -79,6 +79,21 @@ 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 + 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, // --- 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 for Cli io::Stderr> { )), }; + let parse_float_arg = |s: &str| match s.parse::() { + 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 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)) + .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 for Cli 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(); diff --git a/crates/fzn-huub/src/main.rs b/crates/fzn-huub/src/main.rs index f3e08853..aab9c6eb 100644 --- a/crates/fzn-huub/src/main.rs +++ b/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 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 + the propagation phase. === BEHAVIOUR OPTIONS === --log-file Output log messages from the solver to a file, instead of stderr. diff --git a/crates/huub/src/actions/initialization.rs b/crates/huub/src/actions/initialization.rs index 8c753628..cebde36e 100644 --- a/crates/huub/src/actions/initialization.rs +++ b/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]); } diff --git a/crates/huub/src/helpers/opt_field.rs b/crates/huub/src/helpers/opt_field.rs index eed4f806..044ac8bc 100644 --- a/crates/huub/src/helpers/opt_field.rs +++ b/crates/huub/src/helpers/opt_field.rs @@ -10,6 +10,9 @@ impl OptField { pub(crate) fn get(&self) -> Option<&T> { self.value.first() } + pub(crate) fn is_some(&self) -> bool { + !self.value.is_empty() + } } impl OptField<1, T> { pub(crate) fn new(value: T) -> Self { diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index 20049c16..89ecc904 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -38,6 +38,7 @@ pub struct Model { pub(crate) cnf: Cnf, branchings: Vec, constraints: Vec, + functional: Vec, int_vars: Vec, prop_queue: VecDeque, enqueued: Vec, @@ -84,6 +85,8 @@ impl Model { if let Some(r) = any_slv.downcast_mut::() { 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 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); } diff --git a/crates/huub/src/model/constraint.rs b/crates/huub/src/model/constraint.rs index 5e860154..2d77ad96 100644 --- a/crates/huub/src/model/constraint.rs +++ b/crates/huub/src/model/constraint.rs @@ -58,11 +58,12 @@ impl Constraint { &self, slv: &mut Solver, map: &mut VariableMap, + functional: bool, ) -> Result<(), ReformulationError> { match self { Constraint::AllDifferentInt(v) => { let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect(); - slv.add_propagator(AllDifferentIntValue::prepare(vars))?; + slv.add_propagator(AllDifferentIntValue::prepare(vars), functional)?; Ok(()) } Constraint::ArrayIntElement(arr, idx, y) => { @@ -94,13 +95,13 @@ impl Constraint { Constraint::ArrayIntMinimum(vars, y) => { let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); let y = y.to_arg(slv, map); - slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y))?; + slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y), functional)?; Ok(()) } Constraint::ArrayIntMaximum(vars, y) => { let vars: Vec<_> = vars.iter().map(|v| -v.to_arg(slv, map)).collect(); let y = -y.to_arg(slv, map); - slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y))?; + slv.add_propagator(ArrayIntMinimumBounds::prepare(vars, y), functional)?; Ok(()) } Constraint::ArrayVarIntElement(vars, idx, y) => { @@ -108,7 +109,10 @@ impl Constraint { let y = y.to_arg(slv, map); let idx = idx.to_arg(slv, map); // tranform 1-based index into 0-based index array - slv.add_propagator(ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)))?; + slv.add_propagator( + ArrayVarIntElementBounds::prepare(vars, y, idx + (-1)), + functional, + )?; Ok(()) } Constraint::ArrayVarBoolElement(vars, idx, y) => { @@ -155,10 +159,10 @@ impl Constraint { }) .collect_vec(); // Add propagator for lower bound propagation - slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare( - vars.clone(), - durs.clone(), - ))?; + slv.add_propagator( + DisjunctiveStrictEdgeFinding::prepare(vars.clone(), durs.clone()), + functional, + )?; // Add symmetric propagator for upper bound propagation let horizon = vars @@ -171,34 +175,37 @@ impl Constraint { .iter() .zip(durs.iter()) .map(|(v, d)| -*v + (horizon - d)); - slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare( - symmetric_vars, - durs.clone(), - ))?; + slv.add_propagator( + DisjunctiveStrictEdgeFinding::prepare(symmetric_vars, durs.clone()), + functional, + )?; Ok(()) } Constraint::IntAbs(origin, abs) => { let origin = origin.to_arg(slv, map); let abs = abs.to_arg(slv, map); - slv.add_propagator(IntAbsBounds::prepare(origin, abs))?; + slv.add_propagator(IntAbsBounds::prepare(origin, abs), functional)?; Ok(()) } Constraint::IntDiv(numerator, denominator, result) => { let numerator = numerator.to_arg(slv, map); let denominator = denominator.to_arg(slv, map); let result = result.to_arg(slv, map); - slv.add_propagator(IntDivBounds::prepare(numerator, denominator, result))?; + slv.add_propagator( + IntDivBounds::prepare(numerator, denominator, result), + functional, + )?; Ok(()) } Constraint::IntLinEq(vars, c) => { let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); // coeffs * vars <= c - slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?; + slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c), functional)?; // coeffs * vars >= c <=> -coeffs * vars <= -c - slv.add_propagator(IntLinearLessEqBounds::prepare( - vars.into_iter().map(|v| -v), - -c, - ))?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c), + functional, + )?; Ok(()) } Constraint::IntLinEqImp(vars, c, r) => { @@ -206,20 +213,25 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?; - slv.add_propagator(IntLinearLessEqBounds::prepare( - vars.into_iter().map(|v| -v), - -c, - ))?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.clone(), *c), + functional, + )?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c), + functional, + )?; } BoolViewInner::Const(false) => {} BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?; - slv.add_propagator(IntLinearLessEqImpBounds::prepare( - vars.into_iter().map(|v| -v), - -c, - r, - ))?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), + functional, + )?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.into_iter().map(|v| -v), -c, r), + functional, + )?; } } Ok(()) @@ -229,30 +241,38 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?; - slv.add_propagator(IntLinearLessEqBounds::prepare( - vars.into_iter().map(|v| -v), - -c, - ))?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.clone(), *c), + functional, + )?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c), + functional, + )?; } BoolViewInner::Const(false) => { - slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?; + slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?; } BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?; - slv.add_propagator(IntLinearLessEqImpBounds::prepare( - vars.iter().map(|v| -(*v)), - -c, - r, - ))?; - slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, !r))?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), + functional, + )?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.iter().map(|v| -(*v)), -c, r), + functional, + )?; + slv.add_propagator( + IntLinearNotEqImpValue::prepare(vars, *c, !r), + functional, + )?; } } Ok(()) } Constraint::IntLinLessEq(vars, c) => { let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?; + slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?; Ok(()) } Constraint::IntLinLessEqImp(vars, c, r) => { @@ -260,11 +280,14 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?; + slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?; } BoolViewInner::Const(false) => {} BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars, *c, r))?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars, *c, r), + functional, + )?; } } Ok(()) @@ -274,28 +297,34 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c))?; + slv.add_propagator(IntLinearLessEqBounds::prepare(vars, *c), functional)?; } BoolViewInner::Const(false) => { - slv.add_propagator(IntLinearLessEqBounds::prepare( - vars.into_iter().map(|v| -v), - -(c + 1), - ))?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -(c + 1)), + functional, + )?; } BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r))?; - slv.add_propagator(IntLinearLessEqImpBounds::prepare( - vars.into_iter().map(|v| -v), - -(c + 1), - !r, - ))?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.clone(), *c, r), + functional, + )?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare( + vars.into_iter().map(|v| -v), + -(c + 1), + !r, + ), + functional, + )?; } } Ok(()) } Constraint::IntLinNotEq(vars, c) => { let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?; + slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?; Ok(()) } Constraint::IntLinNotEqImp(vars, c, r) => { @@ -303,11 +332,14 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?; + slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?; } BoolViewInner::Const(false) => {} BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearNotEqImpValue::prepare(vars, *c, r))?; + slv.add_propagator( + IntLinearNotEqImpValue::prepare(vars, *c, r), + functional, + )?; } } Ok(()) @@ -317,27 +349,31 @@ impl Constraint { let r = r.to_arg(slv, map, None)?; match r.0 { BoolViewInner::Const(true) => { - slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c))?; + slv.add_propagator(IntLinearNotEqValue::prepare(vars, *c), functional)?; } BoolViewInner::Const(false) => { - slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c))?; - slv.add_propagator(IntLinearLessEqBounds::prepare( - vars.into_iter().map(|v| -v), - -c, - ))?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.clone(), *c), + functional, + )?; + slv.add_propagator( + IntLinearLessEqBounds::prepare(vars.into_iter().map(|v| -v), -c), + functional, + )?; } BoolViewInner::Lit(r) => { - slv.add_propagator(IntLinearNotEqImpValue::prepare(vars.clone(), *c, r))?; - slv.add_propagator(IntLinearLessEqImpBounds::prepare( - vars.clone(), - *c, - !r, - ))?; - slv.add_propagator(IntLinearLessEqImpBounds::prepare( - vars.iter().map(|v| -(*v)), - -c, - !r, - ))?; + slv.add_propagator( + IntLinearNotEqImpValue::prepare(vars.clone(), *c, r), + functional, + )?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.clone(), *c, !r), + functional, + )?; + slv.add_propagator( + IntLinearLessEqImpBounds::prepare(vars.iter().map(|v| -(*v)), -c, !r), + functional, + )?; } } Ok(()) @@ -346,14 +382,14 @@ impl Constraint { let base = base.to_arg(slv, map); let exponent = exponent.to_arg(slv, map); let result = res.to_arg(slv, map); - slv.add_propagator(IntPowBounds::prepare(base, exponent, result))?; + slv.add_propagator(IntPowBounds::prepare(base, exponent, result), functional)?; Ok(()) } Constraint::IntTimes(x, y, z) => { let x = x.to_arg(slv, map); let y = y.to_arg(slv, map); let z = z.to_arg(slv, map); - slv.add_propagator(IntTimesBounds::prepare(x, y, z))?; + slv.add_propagator(IntTimesBounds::prepare(x, y, z), functional)?; Ok(()) } Constraint::PropLogic(exp) => exp.constrain(slv, map), diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index 3ae78971..708b37de 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -1025,6 +1025,9 @@ where } _ => return Err(FlatZincError::UnknownConstraint(c.id.to_string())), } + + let n = self.prb.functional.len() - 1; + self.prb.functional[n] = c.defines.is_some(); } Ok(()) diff --git a/crates/huub/src/propagator/all_different_int.rs b/crates/huub/src/propagator/all_different_int.rs index 7f9c29ac..74346b99 100644 --- a/crates/huub/src/propagator/all_different_int.rs +++ b/crates/huub/src/propagator/all_different_int.rs @@ -71,6 +71,7 @@ impl Poster for AllDifferentIntValuePoster { for &v in prop.vars.iter() { actions.enqueue_on_int_change(v, IntPropCond::Fixed); } + actions.enqueue_when_n_fixed(prop.vars.len(), &[], &prop.vars); Ok(( Box::new(prop), QueuePreferences { @@ -79,6 +80,10 @@ impl Poster for AllDifferentIntValuePoster { }, )) } + + fn name(&self) -> &'static str { + "AllDifferentIntValue" + } } #[cfg(test)] @@ -117,7 +122,7 @@ mod tests { EncodingType::Eager, ); - slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c])) + slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]), false) .unwrap(); slv.assert_all_solutions(&[a, b, c], |sol| sol.iter().all_unique()); } @@ -145,7 +150,7 @@ mod tests { EncodingType::Eager, ); - slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c])) + slv.add_propagator(AllDifferentIntValue::prepare(vec![a, b, c]), false) .unwrap(); slv.assert_unsatisfiable(); } @@ -169,14 +174,14 @@ mod tests { )); } } - slv.add_propagator(AllDifferentIntValue::prepare(vars.clone())) + slv.add_propagator(AllDifferentIntValue::prepare(vars.clone()), false) .unwrap(); all_vars.push(vars); }); // add all different propagator for each column for i in 0..9 { let col_vars: Vec = (0..9).map(|j| all_vars[j][i]).collect(); - slv.add_propagator(AllDifferentIntValue::prepare(col_vars)) + slv.add_propagator(AllDifferentIntValue::prepare(col_vars), false) .unwrap(); } // add all different propagator for each 3 by 3 grid @@ -188,7 +193,7 @@ mod tests { block_vars.push(all_vars[3 * i + x][3 * j + y]); } } - slv.add_propagator(AllDifferentIntValue::prepare(block_vars)) + slv.add_propagator(AllDifferentIntValue::prepare(block_vars), false) .unwrap(); } } diff --git a/crates/huub/src/propagator/array_int_minimum.rs b/crates/huub/src/propagator/array_int_minimum.rs index dab5f811..a81945bb 100644 --- a/crates/huub/src/propagator/array_int_minimum.rs +++ b/crates/huub/src/propagator/array_int_minimum.rs @@ -94,6 +94,12 @@ impl Poster for ArrayIntMinimumBoundsPoster { actions.enqueue_on_int_change(v, IntPropCond::Bounds); } actions.enqueue_on_int_change(prop.min, IntPropCond::LowerBound); + + actions.enqueue_when_n_fixed( + prop.vars.len() + 1, + &[], + &[prop.vars.as_slice(), &[prop.min]].concat(), + ); Ok(( Box::new(prop), QueuePreferences { @@ -102,6 +108,10 @@ impl Poster for ArrayIntMinimumBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "ArrayIntMinimumBounds" + } } #[cfg(test)] diff --git a/crates/huub/src/propagator/array_var_int_element.rs b/crates/huub/src/propagator/array_var_int_element.rs index 00069996..0f073c9c 100644 --- a/crates/huub/src/propagator/array_var_int_element.rs +++ b/crates/huub/src/propagator/array_var_int_element.rs @@ -226,6 +226,12 @@ impl Poster for ArrayVarIntElementBoundsPoster { }; actions.enqueue_on_int_change(prop.result, IntPropCond::Bounds); actions.enqueue_on_int_change(prop.index, IntPropCond::Domain); + + actions.enqueue_when_n_fixed( + prop.vars.len() + 1, + &[], + &[prop.vars.as_slice(), &[prop.result, prop.index]].concat(), + ); Ok(( Box::new(prop), QueuePreferences { @@ -234,6 +240,10 @@ impl Poster for ArrayVarIntElementBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "ArrayVarIntElementBounds" + } } #[cfg(test)] @@ -284,8 +294,11 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index)) - .unwrap(); + slv.add_propagator( + ArrayVarIntElementBounds::prepare(vec![a, b, c], y, index), + false, + ) + .unwrap(); slv.expect_solutions( &[index, y, a, b, c], expect![[r#" @@ -351,8 +364,11 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(ArrayVarIntElementBounds::prepare(vec![a, b], y, index)) - .unwrap(); + slv.add_propagator( + ArrayVarIntElementBounds::prepare(vec![a, b], y, index), + false, + ) + .unwrap(); slv.expect_solutions( &[index, y, a, b], expect![[r#" diff --git a/crates/huub/src/propagator/disjunctive_strict.rs b/crates/huub/src/propagator/disjunctive_strict.rs index 9607f295..8bfc3a44 100644 --- a/crates/huub/src/propagator/disjunctive_strict.rs +++ b/crates/huub/src/propagator/disjunctive_strict.rs @@ -556,6 +556,8 @@ impl Poster for DisjunctiveEdgeFindingPoster { actions.enqueue_on_int_change(v, IntPropCond::Bounds); } + actions.enqueue_when_n_fixed(prop.start_times.len(), &[], &prop.start_times); + Ok(( Box::new(prop), QueuePreferences { @@ -564,6 +566,10 @@ impl Poster for DisjunctiveEdgeFindingPoster { }, )) } + + fn name(&self) -> &'static str { + "DisjunctiveStrictEdgeFinding" + } } #[cfg(test)] @@ -602,18 +608,21 @@ mod tests { EncodingType::Lazy, ); let durations = vec![2, 3, 1]; - slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare( - [a, b, c], - durations.clone(), - )) + slv.add_propagator( + DisjunctiveStrictEdgeFinding::prepare([a, b, c], durations.clone()), + false, + ) .unwrap(); - slv.add_propagator(DisjunctiveStrictEdgeFinding::prepare( - [a, b, c] - .iter() - .zip(durations.iter()) - .map(|(v, d)| -*v + (7 - d)), - durations.clone(), - )) + slv.add_propagator( + DisjunctiveStrictEdgeFinding::prepare( + [a, b, c] + .iter() + .zip(durations.iter()) + .map(|(v, d)| -*v + (7 - d)), + durations.clone(), + ), + false, + ) .unwrap(); slv.expect_solutions( diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs index b2071348..3fb18fa1 100644 --- a/crates/huub/src/propagator/int_abs.rs +++ b/crates/huub/src/propagator/int_abs.rs @@ -94,6 +94,8 @@ impl Poster for IntAbsBoundsPoster { // Subscribe only to the upper bound of the absolute value variable actions.enqueue_on_int_change(self.abs, IntPropCond::UpperBound); + actions.enqueue_when_n_fixed(2, &[], &[self.origin, self.abs]); + Ok(( Box::new(IntAbsBounds { origin: self.origin, @@ -105,6 +107,10 @@ impl Poster for IntAbsBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "IntAbsBounds" + } } #[cfg(test)] @@ -136,7 +142,8 @@ mod tests { EncodingType::Eager, EncodingType::Lazy, ); - slv.add_propagator(IntAbsBounds::prepare(a, b)).unwrap(); + slv.add_propagator(IntAbsBounds::prepare(a, b), false) + .unwrap(); slv.expect_solutions( &[a, b], expect![[r#" diff --git a/crates/huub/src/propagator/int_div.rs b/crates/huub/src/propagator/int_div.rs index 95a5ec10..db9c8357 100644 --- a/crates/huub/src/propagator/int_div.rs +++ b/crates/huub/src/propagator/int_div.rs @@ -213,6 +213,8 @@ impl Poster for IntDivBoundsPoster { actions.enqueue_on_int_change(self.denominator, IntPropCond::Bounds); actions.enqueue_on_int_change(self.result, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.numerator, self.denominator, self.result]); + // Ensure the consistency of the signs of the three variables using the following clauses. if actions.get_int_lower_bound(self.numerator) < 0 || actions.get_int_lower_bound(self.denominator) < 0 @@ -247,6 +249,10 @@ impl Poster for IntDivBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "IntDivBounds" + } } #[cfg(test)] @@ -285,7 +291,8 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(IntDivBounds::prepare(a, b, c)).unwrap(); + slv.add_propagator(IntDivBounds::prepare(a, b, c), false) + .unwrap(); slv.expect_solutions( &[a, b, c], expect![[r#" diff --git a/crates/huub/src/propagator/int_lin_le.rs b/crates/huub/src/propagator/int_lin_le.rs index 44399733..a60a97b3 100644 --- a/crates/huub/src/propagator/int_lin_le.rs +++ b/crates/huub/src/propagator/int_lin_le.rs @@ -171,6 +171,19 @@ impl Poster for IntLinearLessEqBoundsPoster { if let Some(r) = prop.reification.get() { actions.enqueue_on_bool_change(BoolView(BoolViewInner::Lit(*r))); } + + let bool_vec: Vec = prop + .reification + .get() + .map(|&l| BoolView(BoolViewInner::Lit(l))) + .into_iter() + .collect(); + actions.enqueue_when_n_fixed( + prop.vars.len() + if prop.reification.is_some() { 1 } else { 0 }, + &bool_vec, + &prop.vars, + ); + Ok(( Box::new(prop), QueuePreferences { @@ -179,6 +192,10 @@ impl Poster for IntLinearLessEqBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "IntLinearLessEqBounds" + } } #[cfg(test)] @@ -217,10 +234,10 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(IntLinearLessEqBounds::prepare( - vec![a * NonZeroIntVal::new(2).unwrap(), b, c], - 6, - )) + slv.add_propagator( + IntLinearLessEqBounds::prepare(vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6), + false, + ) .unwrap(); slv.expect_solutions( @@ -269,10 +286,10 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(IntLinearLessEqBounds::prepare( - vec![a * NonZeroIntVal::new(-2).unwrap(), -b, -c], - -6, - )) + slv.add_propagator( + IntLinearLessEqBounds::prepare(vec![a * NonZeroIntVal::new(-2).unwrap(), -b, -c], -6), + false, + ) .unwrap(); slv.expect_solutions( &[a, b, c], diff --git a/crates/huub/src/propagator/int_lin_ne.rs b/crates/huub/src/propagator/int_lin_ne.rs index b2b3761f..44eb9152 100644 --- a/crates/huub/src/propagator/int_lin_ne.rs +++ b/crates/huub/src/propagator/int_lin_ne.rs @@ -8,7 +8,7 @@ use crate::{ Propagator, }, solver::{ - engine::{activation_list::IntPropCond, queue::PriorityLevel, trail::TrailedInt}, + engine::{queue::PriorityLevel, trail::TrailedInt}, poster::{BoxedPropagator, Poster, QueuePreferences}, value::IntVal, view::{BoolViewInner, IntView, IntViewInner}, @@ -163,12 +163,17 @@ impl Poster for IntLinearNotEqValuePoster { reification: self.reification, num_fixed: actions.new_trailed_int(0), }; - for &v in prop.vars.iter() { - actions.enqueue_on_int_change(v, IntPropCond::Fixed); - } - if let Some(r) = prop.reification.get() { - actions.enqueue_on_bool_change(BoolView(BoolViewInner::Lit(*r))); - } + let bool_vec: Vec = prop + .reification + .get() + .map(|&l| BoolView(BoolViewInner::Lit(l))) + .into_iter() + .collect(); + actions.enqueue_when_n_fixed( + prop.vars.len() + if prop.reification.is_some() { 1 } else { 0 } - 1, + &bool_vec, + &prop.vars, + ); Ok(( Box::new(prop), QueuePreferences { @@ -177,6 +182,10 @@ impl Poster for IntLinearNotEqValuePoster { }, )) } + + fn name(&self) -> &'static str { + "IntLinearNotEqValue" + } } #[cfg(test)] @@ -215,10 +224,10 @@ mod tests { EncodingType::Eager, ); - slv.add_propagator(IntLinearNotEqValue::prepare( - vec![a * NonZeroIntVal::new(2).unwrap(), b, c], - 6, - )) + slv.add_propagator( + IntLinearNotEqValue::prepare(vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6), + false, + ) .unwrap(); slv.expect_solutions( diff --git a/crates/huub/src/propagator/int_pow.rs b/crates/huub/src/propagator/int_pow.rs index b3453d34..bc24809e 100644 --- a/crates/huub/src/propagator/int_pow.rs +++ b/crates/huub/src/propagator/int_pow.rs @@ -255,6 +255,8 @@ impl Poster for IntPowBoundsPoster { actions.enqueue_on_int_change(self.exponent, IntPropCond::Bounds); actions.enqueue_on_int_change(self.result, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.base, self.exponent, self.result]); + // Ensure that if the base is negative, then the exponent cannot be zero let (exp_lb, exp_ub) = actions.get_int_bounds(self.exponent); let (base_lb, base_ub) = actions.get_int_bounds(self.base); @@ -289,6 +291,10 @@ impl Poster for IntPowBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "IntPowBounds" + } } fn pow(base: IntVal, exponent: IntVal) -> Option { @@ -347,7 +353,8 @@ mod tests { EncodingType::Eager, ); - slv.add_propagator(IntPowBounds::prepare(a, b, c)).unwrap(); + slv.add_propagator(IntPowBounds::prepare(a, b, c), false) + .unwrap(); slv.expect_solutions( &[a, b, c], expect![[r#" diff --git a/crates/huub/src/propagator/int_times.rs b/crates/huub/src/propagator/int_times.rs index 3342504f..f612f5d6 100644 --- a/crates/huub/src/propagator/int_times.rs +++ b/crates/huub/src/propagator/int_times.rs @@ -126,6 +126,7 @@ impl Poster for IntTimesBoundsPoster { actions.enqueue_on_int_change(self.x, IntPropCond::Bounds); actions.enqueue_on_int_change(self.y, IntPropCond::Bounds); actions.enqueue_on_int_change(self.z, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.x, self.y, self.z]); Ok(( Box::new(IntTimesBounds { x: self.x, @@ -138,6 +139,10 @@ impl Poster for IntTimesBoundsPoster { }, )) } + + fn name(&self) -> &'static str { + "IntTimesBounds" + } } #[cfg(test)] @@ -175,7 +180,7 @@ mod tests { EncodingType::Lazy, ); - slv.add_propagator(IntTimesBounds::prepare(a, b, c)) + slv.add_propagator(IntTimesBounds::prepare(a, b, c), false) .unwrap(); slv.expect_solutions( &[a, b, c], diff --git a/crates/huub/src/propagator/reason.rs b/crates/huub/src/propagator/reason.rs index d488dd5d..13d05476 100644 --- a/crates/huub/src/propagator/reason.rs +++ b/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>( &self, - props: &mut IndexVec, + prop: &mut BoxedPropagator, actions: &mut State, lit: Option, ) -> 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 ReasonBuilder for LazyReason { fn build_reason(self, _: &mut A) -> Result { - Ok(Reason::Lazy(self.0, self.1)) + Ok(Reason::Lazy(self.1)) } } diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index 66c18ac3..9753470d 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -55,6 +55,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, } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -70,7 +72,7 @@ pub struct Solver> { pub(crate) oracle: Oracle, } -#[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. /// @@ -82,6 +84,20 @@ 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. + propagtor_multiplicative_factor: f64, + /// The threshold for the activity-based activation of propagators. + propagator_activity_threshold: f64, + /// Interval in milliseconds to trace propagator activities. + trace_propagations: Option, + /// Allow the solver to return multiple conflicts in a single call to `check_model`. + check_multiple_conflicts: bool, + /// Always allow functional constraints to be enqueued. + enqueue_functional: bool, } fn trace_learned_clause(clause: &mut dyn Iterator) { @@ -95,29 +111,8 @@ impl InitStatistics { pub fn propagators(&self) -> usize { self.propagators } -} - -impl Solver -where - Oracle: PropagatingSolver, - Oracle::Slv: LearnCallback, -{ - pub fn set_learn_callback) + 'static>( - &mut self, - cb: Option, - ) { - if let Some(mut f) = cb { - self.oracle.solver_mut().set_learn_callback(Some( - move |clause: &mut dyn Iterator| { - trace_learned_clause(clause); - f(clause); - }, - )); - } else { - self.oracle - .solver_mut() - .set_learn_callback(Some(trace_learned_clause)); - } + pub fn functional_propagators(&self) -> usize { + self.functional_propagators } } @@ -197,8 +192,11 @@ impl> Solver { pub(crate) fn add_propagator( &mut self, poster: P, + functional: bool, ) -> Result<(), ReformulationError> { let prop_ref = PropRef::from(self.engine().propagators.len()); + let p = self.engine_mut().state.propagator_types.push(poster.name()); + debug_assert_eq!(prop_ref, p); let mut actions = InitializationContext { slv: self, init_ref: InitRef::Propagator(prop_ref), @@ -211,12 +209,19 @@ impl> Solver { 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.enqueued_inactive.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); + let p = self.engine_mut().state.functional.push(functional); + debug_assert_eq!(prop_ref, p); if queue_pref.enqueue_on_post { let state = &mut self.engine_mut().state; state .propagator_queue .insert(state.propagator_priority[prop_ref], prop_ref); state.enqueued[prop_ref] = true; + state.enqueued_inactive[prop_ref] = true; } Ok(()) } @@ -381,6 +386,13 @@ impl> Solver { 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(), } } @@ -393,6 +405,17 @@ impl> Solver { &self.engine().state.statistics } + delegate! { + to self.engine_mut().state { + 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, 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); + } + } + /// Try and find a solution to the problem for which the Solver was initialized. pub fn solve(&mut self, on_sol: impl FnMut(&dyn Valuation)) -> SolveResult { self.solve_assuming([], on_sol, |_| {}) @@ -459,14 +482,6 @@ impl> Solver { SatSolveResult::Unknown => SolveResult::Unknown, } } - - delegate! { - to self.engine_mut().state { - pub fn set_toggle_vsids(&mut self, enable: bool); - pub fn set_vsids_after(&mut self, conflicts: Option); - pub fn set_vsids_only(&mut self, enable: bool); - } - } } impl> DecisionActions for Solver { diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 1a37a908..c446ef7d 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -8,6 +8,7 @@ pub(crate) mod trail; use std::{ collections::{HashMap, VecDeque}, mem, + time::Instant, }; use delegate::delegate; @@ -29,7 +30,7 @@ use crate::{ propagator::reason::Reason, solver::{ engine::{ - activation_list::{ActivationList, IntEvent}, + activation_list::{BoolActivationList, IntActivationList, IntEvent}, bool_to_int::BoolToIntMap, int_var::{IntVar, IntVarRef, LitMeaning, OrderStorage}, queue::{PriorityLevel, PriorityQueue}, @@ -92,8 +93,19 @@ pub struct SearchStatistics { user_decisions: u64, } -#[derive(Clone, Debug, Default)] +#[derive(Clone, Debug)] pub(crate) struct State { + // ---- Propagator Tracing Value Infrastructure (e.g., timer) ---- + /// Timer + pub(crate) timer: Instant, + /// Propagator activity statistics in the last time slot + pub(crate) explanations: usize, + pub(crate) propagations: usize, + pub(crate) conflicts: usize, + pub(crate) no_propagations: usize, + /// Last time slot for propagator tracing + pub(crate) time_slot: usize, + // Solver confifguration pub(crate) config: SolverConfiguration, @@ -107,10 +119,10 @@ 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, + /// Reasons and Propagators for setting values of literals + pub(crate) reason_map: HashMap, /// Whether conflict has (already) been detected - pub(crate) conflict: Option, + pub(crate) conflict: VecDeque, // ---- Non-Trailed Infrastructure ---- /// Storage for clauses to be communicated to the solver @@ -122,15 +134,61 @@ pub(crate) struct State { // ---- Queueing Infrastructure ---- /// Boolean variable enqueueing information - pub(crate) bool_activation: HashMap>, + pub(crate) bool_activation: HashMap, /// Integer variable enqueueing information - pub(crate) int_activation: IndexVec, + pub(crate) int_activation: IndexVec, + /// Fixed Deamons + /// + /// These are propagators that are enqueued when set number of values have been + /// assigned. + pub(crate) fixed_daemons: HashMap, /// Queue of propagators awaiting action pub(crate) propagator_queue: PriorityQueue, /// Priority within the queue for each propagator pub(crate) propagator_priority: IndexVec, /// Flag for whether a propagator is enqueued pub(crate) enqueued: IndexVec, + /// Flag for whether a propagator is enqueued into inactive level (i.e., not active) + pub(crate) enqueued_inactive: IndexVec, + /// Activity scores for propagators to determine whether they are active or not + pub(crate) activity_scores: IndexVec, + /// Whether the propagator is functional + pub(crate) functional: IndexVec, + /// Name of the propagator + pub(crate) propagator_types: IndexVec, +} + +impl Default for State { + fn default() -> Self { + Self { + timer: Instant::now(), + explanations: Default::default(), + propagations: Default::default(), + conflicts: Default::default(), + no_propagations: Default::default(), + time_slot: Default::default(), + config: Default::default(), + int_vars: Default::default(), + bool_to_int: Default::default(), + trail: Default::default(), + propagation_queue: Default::default(), + reason_map: Default::default(), + conflict: Default::default(), + clauses: Default::default(), + statistics: Default::default(), + vsids: false, + bool_activation: Default::default(), + int_activation: Default::default(), + fixed_daemons: Default::default(), + propagator_queue: Default::default(), + propagator_priority: Default::default(), + enqueued: Default::default(), + enqueued_inactive: Default::default(), + activity_scores: Default::default(), + functional: Default::default(), + propagator_types: Default::default(), + } + } } impl PropagatorExtension for Engine { @@ -146,14 +204,14 @@ impl PropagatorExtension for Engine { continue; } // Enqueue propagators, if no conflict has been found - if self.state.conflict.is_none() { + if self.state.conflict.is_empty() { self.state.enqueue_propagators(lit, None); } } } fn notify_new_decision_level(&mut self) { - debug_assert!(self.state.conflict.is_none()); + debug_assert!(self.state.conflict.is_empty()); trace!("new decision level"); self.state.notify_new_decision_level(); } @@ -204,9 +262,13 @@ impl PropagatorExtension for Engine { if !self.state.clauses.is_empty() { return Vec::new(); } - if self.state.propagation_queue.is_empty() && self.state.conflict.is_none() { + if self.state.propagation_queue.is_empty() + && self.state.conflict.is_empty() + && !self.state.propagator_queue.is_empty() + { // 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::(&mut self.propagators); } // Check whether there are new clauses that need to be communicated first if !self.state.clauses.is_empty() { @@ -233,9 +295,9 @@ impl PropagatorExtension 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; @@ -263,12 +325,19 @@ impl PropagatorExtension 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] }; @@ -283,9 +352,10 @@ impl PropagatorExtension for Engine { slv: &mut dyn SolvingActions, _sol: &dyn pindakaas::Valuation, ) -> bool { - debug_assert!(self.state.conflict.is_none()); + debug_assert!(self.state.conflict.is_empty()); + let check_multiple_conflicts = self.state.config.check_multiple_conflicts; // If there is a known conflict, return false - if !self.state.propagation_queue.is_empty() || self.state.conflict.is_some() { + if !self.state.propagation_queue.is_empty() || !self.state.conflict.is_empty() { self.state.ensure_clause_changes(&mut self.propagators); debug!(accept = false, "check model"); return false; @@ -324,19 +394,23 @@ impl PropagatorExtension for Engine { } // Run propgagators to find any conflicts - ctx.run_propagators(&mut self.propagators); + if !ctx.state.propagator_queue.is_empty() { + if check_multiple_conflicts { + ctx.check_propagators(&mut self.propagators); + } else { + ctx.run_propagators::(&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()); // Process propagation results, and accept model if no conflict is detected - let accept = if let Some(conflict) = self.state.conflict.clone() { - // Move conflict to clauses before backtrack + let mut accept = true; + while let Some(conflict) = self.state.conflict.pop_front() { self.state.clauses.push_back(conflict); - false - } else { - true - }; + accept = false; + } // Revert to real decision level self.state.notify_backtrack::(level as usize, false); @@ -355,7 +429,7 @@ impl PropagatorExtension for Engine { clause.map(|c| (c, ClausePersistence::Irreduntant)) } else if !self.state.propagation_queue.is_empty() { None // Require that the solver first applies the remaining propagation - } else if let Some(conflict) = self.state.conflict.clone() { + } else if let Some(conflict) = self.state.conflict.pop_front() { debug!(clause = ?conflict.iter().map(|&x| i32::from(x)).collect::>(), "add conflict clause"); Some((conflict, ClausePersistence::Forgettable)) } else { @@ -407,7 +481,7 @@ impl State { return None; } if i < lb || i > ub { - // Notified of invalid assignment, do nothing. + // TODO: Notification of an invalid assignment, do nothing. // // Although we do not expect this to happen, it seems that Cadical // chronological backtracking might send notifications before @@ -431,6 +505,11 @@ impl State { if new_lb <= lb { return None; } + if new_lb > ub { + // TODO: Notification of an invalid assignment, do nothing. + trace!(lit = i32::from(lit), lb, ub, "invalid geq notification"); + return None; + } let prev = self.int_vars[iv].notify_lower_bound(&mut self.trail, new_lb); debug_assert!(prev < new_lb); if new_lb == ub { @@ -444,6 +523,11 @@ impl State { if new_ub >= ub { return None; } + if new_ub < lb { + // TODO: Notification of an invalid assignment, do nothing. + trace!(lit = i32::from(lit), lb, ub, "invalid less notification"); + return None; + } let prev = self.int_vars[iv].notify_upper_bound(&mut self.trail, new_ub); debug_assert!(new_ub < prev); if new_ub == lb { @@ -470,8 +554,8 @@ impl State { fn ensure_clause_changes(&mut self, propagators: &mut IndexVec) { 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] }; @@ -501,14 +585,15 @@ impl State { debug_assert!(!ARTIFICIAL || level as u32 == self.trail.decision_level() - 1); debug_assert!(!ARTIFICIAL || !restart); // Resolve the conflict status - self.conflict = None; + self.conflict.clear(); // Remove (now invalid) propagations (but leave clauses in place) self.propagation_queue.clear(); // 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::() { self.enqueued[p] = false; + self.enqueued_inactive[p] = false; } if ARTIFICIAL { return; @@ -551,28 +636,180 @@ impl State { } } + // Three types of events: + // 1. Not fixed event Or fixed event but not the last variable: + // - propogator enqueued in normal level: no actions + // - propogator enqueued in inactive level: no actions + // - propogator not enqueued: enqueue according to the activity score + // 2. Fixed event and the last variable: + // - propogator enqueued in normal level: no actions + // - propogator enqueued in inactive level: enqueue to the normal level + // - propogator not enqueued: enqueue to the normal level + // Assume that there is a copy for every PropRef in both `self.int_activation[int_var].fixed_daemons` + // and `self.int_activation[int_var].activations` fn enqueue_int_propagators( &mut self, int_var: IntVarRef, event: IntEvent, skip: Option, ) { + let mut force_enqueue = Vec::new(); + let mut possible_enqueue = Vec::new(); + if event == IntEvent::Fixed { + // Decrement the variable counter for fixed events + for prop in self.int_activation[int_var].fixed_daemons() { + let counter = self.fixed_daemons[&prop]; + let count = self.trail.get_trailed_int(counter) - 1; + let _ = self.trail.set_trailed_int(counter, count); + 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 && !self.enqueued[prop] { + if Some(prop) != skip { + possible_enqueue.push(prop); + } + } + + for prop in force_enqueue { + if !self.enqueued[prop] { self.propagator_queue .insert(self.propagator_priority[prop], prop); self.enqueued[prop] = true; } } - } - fn enqueue_propagators(&mut self, lit: RawLit, skip: Option) { - for &prop in self.bool_activation.get(&lit.var()).into_iter().flatten() { - if Some(prop) != skip && !self.enqueued[prop] { + for prop in possible_enqueue { + if self.enqueued[prop] || self.enqueued_inactive[prop] { + continue; + } + 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 .insert(self.propagator_priority[prop], prop); self.enqueued[prop] = true; + } else { + self.propagator_queue.insert(PriorityLevel::Inactive, prop); + self.enqueued_inactive[prop] = false; + } + } + + // for prop in self.int_activation[int_var].activated_by(event) { + // if Some(prop) != skip && !self.enqueued[prop] { + // if !self.vsids + // || self.activity_scores[prop] >= self.config.propagator_activity_threshold + // || (self.config.enqueue_functional && self.functional[prop]) + // { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; // Mark as enqueued to the normal level + // } else { + // trace!(propagator = usize::from(prop), "deactivate propagator"); + // self.propagator_queue.insert(PriorityLevel::Inactive, prop); + // self.enqueued_deactivate[prop] = true; // Mark as enqueued to the inactive level + // } + // } + // } + // if event == IntEvent::Fixed { + // for prop in self.int_activation[int_var].fixed_daemons() { + // let counter = self.fixed_daemons[&prop]; + // let count = self.trail.get_trailed_int(counter) - 1; + // let _ = self.trail.set_trailed_int(counter, count); + // if count == 0 && !self.enqueued[prop] { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; + // } + // } + // } + } + + fn enqueue_propagators(&mut self, lit: RawLit, skip: Option) { + if let Some(activator) = self.bool_activation.get(&lit.var()) { + let mut force_enqueue = Vec::new(); + let mut possible_enqueue = Vec::new(); + // Decrement the variable counter for fixed events + for prop in activator.fixed_daemons() { + let counter = self.fixed_daemons[&prop]; + let count = self.trail.get_trailed_int(counter) - 1; + let _ = self.trail.set_trailed_int(counter, count); + if Some(prop) != skip { + if count == 0 { + force_enqueue.push(prop); + } else { + possible_enqueue.push(prop); + } + } + } + + for prop in force_enqueue { + if !self.enqueued[prop] { + self.propagator_queue + .insert(self.propagator_priority[prop], prop); + self.enqueued[prop] = true; + } } + + for prop in possible_enqueue { + if self.enqueued[prop] || self.enqueued_inactive[prop] { + continue; + } + 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 + .insert(self.propagator_priority[prop], prop); + self.enqueued[prop] = true; + } else { + self.propagator_queue.insert(PriorityLevel::Inactive, prop); + self.enqueued_inactive[prop] = false; + } + } + + // // Enqueue all propagators that are directly activated by the given literal + // for prop in activator.activations() { + // if Some(prop) != skip && !self.enqueued[prop] { + // if !self.vsids + // || self.activity_scores[prop] >= self.config.propagator_activity_threshold + // || (self.config.enqueue_functional && self.functional[prop]) + // { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // } else { + // trace!(propagator = usize::from(prop), "deactivate propagator"); + // self.propagator_queue.insert(PriorityLevel::Inactive, prop); + // } + // self.enqueued[prop] = true; + // } + // } + + // // Decrease all fixed daemons that are associated with the given literal and + // // activate them if they are now zero + // for prop in activator.fixed_daemons() { + // let counter = self.fixed_daemons[&prop]; + // let count = self.trail.get_trailed_int(counter) - 1; + // let _ = self.trail.set_trailed_int(counter, count); + // if count == 0 && !self.enqueued[prop] { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; + // } + // } } // Process Integer consequences @@ -581,11 +818,11 @@ impl State { } } - fn register_reason(&mut self, lit: RawLit, built_reason: Result) { + fn register_reason(&mut self, lit: RawLit, prop: PropRef, built_reason: Result) { 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 @@ -607,6 +844,29 @@ impl State { self.config.vsids_only = enable; self.vsids = enable; } + + 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; + self.config.trace_propagations = trace_propagations; + } + + pub(crate) fn set_check_multiple_conflicts(&mut self, enable: bool) { + self.config.check_multiple_conflicts = enable; + } + + pub(crate) fn set_enqueue_functional(&mut self, enable: bool) { + self.config.enqueue_functional = enable; + } } impl ExplanationActions for State { diff --git a/crates/huub/src/solver/engine/activation_list.rs b/crates/huub/src/solver/engine/activation_list.rs index 78fe770e..de9c2911 100644 --- a/crates/huub/src/solver/engine/activation_list.rs +++ b/crates/huub/src/solver/engine/activation_list.rs @@ -2,6 +2,14 @@ use std::{mem, ops::Add}; use crate::solver::engine::PropRef; +#[derive(Clone, Debug, Default, Eq, PartialEq)] +/// A data structure that store a list of propagators to be enqueued based on +/// different propagation conditions. +pub(crate) struct BoolActivationList { + activations: Vec, + fixed_daemons: Vec, +} + #[derive(Clone, Debug, Default, Eq, PartialEq)] /// A data structure that store a list of propagators to be enqueued based on /// different propagation conditions. @@ -15,12 +23,13 @@ use crate::solver::engine::PropRef; /// index of the LowerBound condition, enqueue all propagators untill the /// beginning of the UpperBound condition, and then continue from the beginning /// of the Bound condition to the end of the list. -pub(crate) struct ActivationList { +pub(crate) struct IntActivationList { activations: Vec, lower_bound_idx: u32, upper_bound_idx: u32, bounds_idx: u32, domain_idx: u32, + fixed_daemons: Vec, } #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -61,7 +70,30 @@ pub(crate) enum IntPropCond { Domain, } -impl ActivationList { +impl BoolActivationList { + /// Add a propagator to the list of propagators to be enqueued when the boolean + /// variable is assigned. + pub(crate) fn add(&mut self, prop: PropRef) { + self.activations.push(prop); + } + + /// Add propagator whose fixed daemon should be decreased when the boolean is + /// assigned. + pub(crate) fn add_fixed_daemon(&mut self, prop: PropRef) { + self.fixed_daemons.push(prop); + } + + #[allow(dead_code, reason = "TODO: testing demon with normal propagator")] + pub(crate) fn activations(&self) -> impl Iterator + '_ { + self.activations.iter().copied() + } + + pub(crate) fn fixed_daemons(&self) -> impl Iterator + '_ { + self.fixed_daemons.iter().copied() + } +} + +impl IntActivationList { /// Add a propagator to the list of propagators to be enqueued based on the /// given condition. pub(crate) fn add(&mut self, mut prop: PropRef, condition: IntPropCond) { @@ -121,6 +153,10 @@ impl ActivationList { }; } + pub(crate) fn add_fixed_daemon(&mut self, prop: PropRef) { + self.fixed_daemons.push(prop); + } + /// Get an iterator over the list of propagators to be enqueued. pub(crate) fn activated_by(&self, event: IntEvent) -> impl Iterator + '_ { let r1 = if event == IntEvent::LowerBound { @@ -141,6 +177,12 @@ impl ActivationList { .copied() .chain(self.activations[r2].iter().copied()) } + + /// Add a propagator whose fixed daemon should be decreased when the variable + /// is fixed to a single value. + pub(crate) fn fixed_daemons(&self) -> impl Iterator + '_ { + self.fixed_daemons.iter().copied() + } } impl Add for IntEvent { @@ -166,7 +208,7 @@ mod tests { use itertools::Itertools; use crate::solver::engine::{ - activation_list::{ActivationList, IntEvent, IntPropCond}, + activation_list::{IntActivationList, IntEvent, IntPropCond}, PropRef, }; @@ -181,7 +223,7 @@ mod tests { ]; for list in props.iter().permutations(5) { - let mut activation_list = ActivationList::default(); + let mut activation_list = IntActivationList::default(); for (prop, cond) in list.iter() { activation_list.add(*prop, *cond); } diff --git a/crates/huub/src/solver/engine/queue.rs b/crates/huub/src/solver/engine/queue.rs index 0730aa5c..4672c372 100644 --- a/crates/huub/src/solver/engine/queue.rs +++ b/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 { - storage: [Vec; 6], + storage: [Vec; PRIORITY_LEVEL_COUNT], } impl Default for PriorityQueue { @@ -13,6 +15,7 @@ impl Default for PriorityQueue { Vec::new(), Vec::new(), Vec::new(), + Vec::new(), ], } } @@ -21,23 +24,29 @@ impl Default for PriorityQueue { impl PriorityQueue { 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 { - for queue in self.storage.iter_mut().rev() { + pub(crate) fn pop(&mut self) -> Option { + for queue in self.storage.iter_mut().skip(SKIP_INACTIVE as usize).rev() { if !queue.is_empty() { return queue.pop(); } } None } + + pub(crate) fn is_empty(&self) -> bool { + self.storage.iter().all(Vec::is_empty) + } } #[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" diff --git a/crates/huub/src/solver/engine/solving_context.rs b/crates/huub/src/solver/engine/solving_context.rs index 5f55d4c8..aab3aa09 100644 --- a/crates/huub/src/solver/engine/solving_context.rs +++ b/crates/huub/src/solver/engine/solving_context.rs @@ -1,7 +1,7 @@ use delegate::delegate; use index_vec::IndexVec; use pindakaas::{solver::propagation::SolvingActions, Lit as RawLit}; -use tracing::trace; +use tracing::{info, trace}; use crate::{ actions::{ @@ -53,28 +53,100 @@ 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) { - while let Some(p) = self.state.propagator_queue.pop() { - debug_assert!(self.state.conflict.is_none()); + /// The generic artugment `SKIP_INACTIVE` is used to skip the inactive propagators in the queue. + pub(crate) fn run_propagators( + &mut self, + propagators: &mut IndexVec, + ) { + // Update tracing statistics on new decision level + if self.state.config.trace_propagations.is_some() + && self.state.timer.elapsed().as_millis() + / self.state.config.trace_propagations.unwrap() + - self.state.time_slot as u128 + > 0 + { + info!( + "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, + 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; + self.state.conflicts = 0; + self.state.propagations = 0; + self.state.no_propagations = 0; + self.state.explanations = 0; + } + + while let Some(p) = self.state.propagator_queue.pop::() { + debug_assert!(self.state.conflict.is_empty()); + let propagation_before = self.state.propagation_queue.len(); self.state.enqueued[p] = false; + self.state.enqueued_inactive[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); + let clause: Clause = reason.explain(&mut propagators[p], self.state, subject); trace!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::>(), "conflict detected"); debug_assert!(!clause.is_empty()); - debug_assert!(self.state.conflict.is_none()); - self.state.conflict = Some(clause); + debug_assert!(self.state.conflict.is_empty()); + self.state.conflict.push_back(clause); + self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; + self.state.conflicts += 1; + } else if propagation_before != self.state.propagation_queue.len() { + self.state.propagations += 1; + } 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; } - if self.state.conflict.is_some() || !self.state.propagation_queue.is_empty() { - return; + + if !self.state.conflict.is_empty() || !self.state.propagation_queue.is_empty() { + break; } } } + pub(crate) fn check_propagators( + &mut self, + propagators: &mut IndexVec, + ) { + let checking_before = self.state.propagation_queue.len(); + while let Some(p) = self.state.propagator_queue.pop::() { + self.state.enqueued[p] = false; + self.state.enqueued_inactive[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(&mut propagators[p], self.state, subject); + trace!(clause = ?clause.iter().map(|&x| i32::from(x)).collect::>(), "conflict detected"); + debug_assert!(!clause.is_empty()); + self.state.conflict.push_back(clause); + self.state.activity_scores[p] += self.state.config.propagtor_additive_factor; + self.state.conflicts += 1; + } else { + // Ensure no propagation happened since all variables are assigned + debug_assert!(self.state.propagation_queue.len() == checking_before); + // 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; + } + } + } #[inline] /// Check whether a change is redundant, conflicting, or new with respect to /// the bounds of an integer variable @@ -211,7 +283,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(()) } diff --git a/crates/huub/src/solver/initialization_context.rs b/crates/huub/src/solver/initialization_context.rs index d2b72b2d..25112288 100644 --- a/crates/huub/src/solver/initialization_context.rs +++ b/crates/huub/src/solver/initialization_context.rs @@ -54,7 +54,7 @@ impl<'a, Oracle: PropagatingSolver> InitializationActions .bool_activation .entry(lit.var()) .or_default() - .push(prop); + .add(prop); } } BoolViewInner::Const(_) => {} @@ -88,6 +88,69 @@ impl<'a, Oracle: PropagatingSolver> InitializationActions (InitRef::Brancher, _) => {} // ignore: branchers don't receive notifications, and contained literals are already observed. } } + + fn enqueue_when_n_fixed(&mut self, mut n: usize, bool_vars: &[BoolView], int_vars: &[IntView]) { + let InitRef::Propagator(prop) = self.init_ref else { + panic!("enqueue_when_n_fixed can only be called for propagators") + }; + assert!( + n <= bool_vars.len() + int_vars.len(), + "waiting on more fixed events than there are variables" + ); + assert!( + !self + .slv + .engine_mut() + .state + .fixed_daemons + .contains_key(&prop), + "propagator is already waiting on fixed events" + ); + + // Filter constants and extract variable references + let mut lits = Vec::new(); + let mut ints = Vec::new(); + for bv in bool_vars { + match bv.0 { + BoolViewInner::Lit(lit) => lits.push(lit), + BoolViewInner::Const(_) => n -= 1, + } + } + for iv in int_vars { + match iv.0 { + IntViewInner::Bool { lit, .. } => lits.push(lit), + IntViewInner::Const(_) => n -= 1, + IntViewInner::Linear { var, .. } | IntViewInner::VarRef(var) => ints.push(var), + } + } + + // if n <= 0 { + // todo!("immediately enqueue the propagator") + // } + + for lit in lits { + self.slv.engine_mut().state.trail.grow_to_boolvar(lit.var()); + self.slv.oracle.add_observed_var(lit.var()); + self.slv + .engine_mut() + .state + .bool_activation + .entry(lit.var()) + .or_default() + .add_fixed_daemon(prop); + } + for var in ints { + self.slv.engine_mut().state.int_activation[var].add_fixed_daemon(prop); + } + + let count = self.slv.engine_mut().state.trail.track_int(n as i64); + let _ = self + .slv + .engine_mut() + .state + .fixed_daemons + .insert(prop, count); + } } impl<'a, Oracle: PropagatingSolver> TrailingActions for InitializationContext<'a, Oracle> { diff --git a/crates/huub/src/solver/poster.rs b/crates/huub/src/solver/poster.rs index e0e3c36f..0d606f6b 100644 --- a/crates/huub/src/solver/poster.rs +++ b/crates/huub/src/solver/poster.rs @@ -24,6 +24,8 @@ pub(crate) trait Poster { self, actions: &mut I, ) -> Result<(BoxedPropagator, QueuePreferences), ReformulationError>; + + fn name(&self) -> &'static str; } pub(crate) struct QueuePreferences { diff --git a/share/minizinc/solvers/huub.msc b/share/minizinc/solvers/huub.msc index b4811be5..94130dcc 100644 --- a/share/minizinc/solvers/huub.msc +++ b/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"], ] }