feat(search): Support phase saving in the conflict-based brancher.

examples/scheduling/src/main.rs

@@ -85,7 +85,7 @@ fn solve(kind: ProblemKind, instance: &str, opt: &Opt) {
     let makespan: IVar = IVar::new(model.shape.get_variable(&Var::Makespan).unwrap());
 
     let solver = Solver::new(model);
-    let mut solver = search::get_solver(solver, opt.search, &encoding);
+    let mut solver = search::get_solver(solver, &opt.search, &encoding);
 
     let result = solver.minimize_with(
         makespan,

examples/scheduling/src/search.rs

@@ -2,11 +2,12 @@ mod greedy;
 
 use crate::problem::{Encoding, OperationId};
 use crate::search::greedy::EstBrancher;
+use crate::search::SearchStrategy::Custom;
 use aries::core::*;
 use aries::model::extensions::Shaped;
 use aries::solver::search::activity::Heuristic;
 use aries::solver::search::combinators::{CombinatorExt, UntilFirstConflict};
-use aries::solver::search::conflicts::{ActiveLiterals, ConflictBasedBrancher, Params, ValueSelection};
+use aries::solver::search::conflicts::{ConflictBasedBrancher, Params};
 use aries::solver::search::lexical::LexicalMinValue;
 use aries::solver::search::{conflicts, Brancher};
 use std::str::FromStr;
@@ -34,25 +35,23 @@ pub type Solver = aries::solver::Solver<Var>;
 pub type ParSolver = aries::solver::parallel::ParSolver<Var>;
 
 /// Variants of the search strategy
-#[derive(Eq, PartialEq, Debug, Copy, Clone)]
+#[derive(Eq, PartialEq, Debug, Clone)]
 pub enum SearchStrategy {
     /// greedy earliest-starting-time then VSIDS with solution guidance
     Activity,
     /// greedy earliest-starting-time then LRB with solution guidance
-    /// Boolean parameter indicates whether we should prefer the value of the last solution or the opposite
-    LearningRate(bool),
-    Parallel,
+    LearningRate,
+    /// Custom strategy, parsed from the command line arguments.
+    Custom(String),
 }
 impl FromStr for SearchStrategy {
     type Err = String;
 
     fn from_str(s: &str) -> Result<Self, Self::Err> {
         match s {
-            "lrb" | "lrb+" | "learning-rate" => Ok(SearchStrategy::LearningRate(true)),
-            "lrb-" | "learning-rate-neg" => Ok(SearchStrategy::LearningRate(false)),
+            "lrb" | "lrb+" | "learning-rate" => Ok(SearchStrategy::LearningRate),
             "vsids" | "activity" => Ok(SearchStrategy::Activity),
-            "par" | "parallel" => Ok(SearchStrategy::Parallel),
-            e => Err(format!("Unrecognized option: '{e}'")),
+            _ => Ok(Custom(s.to_string())),
         }
     }
 }
@@ -70,7 +69,7 @@ impl Heuristic<Var> for ResourceOrderingFirst {
 }
 
 /// Builds a solver for the given strategy.
-pub fn get_solver(base: Solver, strategy: SearchStrategy, pb: &Encoding) -> ParSolver {
+pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding) -> ParSolver {
     let first_est: Brancher<Var> = Box::new(UntilFirstConflict::new(Box::new(EstBrancher::new(pb))));
 
     let base_solver = Box::new(base);
@@ -95,27 +94,38 @@ pub fn get_solver(base: Solver, strategy: SearchStrategy, pb: &Encoding) -> ParS
         s.set_brancher_boxed(strat);
     };
 
-    let vsids = conflicts::Params {
-        heuristic: conflicts::Heuristic::Vsids,
-        active: ActiveLiterals::Reasoned,
-        value_selection: ValueSelection::Sol,
-    };
-    let lrb_sol = conflicts::Params {
-        heuristic: conflicts::Heuristic::LearningRate,
-        active: ActiveLiterals::Reasoned,
-        value_selection: ValueSelection::Sol,
-    };
-    let lrb_not_sol = conflicts::Params {
-        heuristic: conflicts::Heuristic::LearningRate,
-        active: ActiveLiterals::Reasoned,
-        value_selection: ValueSelection::NotSol,
+    let load_conf = |conf: &str| -> conflicts::Params {
+        let mut params = conflicts::Params::default();
+        params.heuristic = conflicts::Heuristic::LearningRate;
+        params.active = conflicts::ActiveLiterals::Reasoned;
+        for opt in conf.split(':') {
+            match opt {
+                "+phase" | "+p" => params.value_selection.phase_saving = true,
+                "-phase" | "-p" => params.value_selection.phase_saving = false,
+                "+sol" | "+s" => params.value_selection.solution_guidance = true,
+                "-sol" | "-s" => params.value_selection.solution_guidance = false,
+                "+neg" => params.value_selection.take_opposite = true,
+                "-neg" => params.value_selection.take_opposite = false,
+                "+longest" => params.value_selection.save_phase_on_longest = true,
+                "-longest" => params.value_selection.save_phase_on_longest = false,
+                "+lrb" => {
+                    params.heuristic = conflicts::Heuristic::LearningRate;
+                    params.active = conflicts::ActiveLiterals::Reasoned;
+                }
+                "+vsids" => {
+                    params.heuristic = conflicts::Heuristic::Vsids;
+                }
+                "" => {} // ignore
+                _ => panic!("Unsupported option: {opt}"),
+            }
+        }
+        params
     };
 
     let strats: &[Params] = match strategy {
-        SearchStrategy::Activity => &[vsids],
-        SearchStrategy::LearningRate(true) => &[lrb_sol],
-        SearchStrategy::LearningRate(false) => &[lrb_not_sol],
-        SearchStrategy::Parallel => &[lrb_sol, lrb_not_sol],
+        SearchStrategy::Activity => &[load_conf("+vsids")],
+        SearchStrategy::LearningRate => &[load_conf("+lrb")],
+        SearchStrategy::Custom(conf) => &[load_conf(&conf)],
     };
 
     ParSolver::new(base_solver, strats.len(), |i, s| make_solver(s, strats[i]))

solver/src/backtrack/queues.rs

@@ -274,6 +274,14 @@ impl<V> ObsTrail<V> {
         }
     }
 
+    /// Returns an iterator over all events after the indicated decision level,
+    /// starting from the most recent.
+    pub fn events_after(&self, dec_lvl: DecLvl) -> impl Iterator<Item = &V> + '_ {
+        let last = self.backtrack_points[dec_lvl + 1];
+        let last = usize::from(last);
+        self.events[last..].iter().rev()
+    }
+
     pub fn get_event(&self, id: EventIndex) -> &V {
         &self.events[id]
     }

solver/src/collections/heap.rs

@@ -70,6 +70,11 @@ impl<K: Ref, P: PartialOrd + Copy> IdxHeap<K, P> {
         self.heap.len()
     }
 
+    /// Returns all variables currently in the heap.
+    pub fn enqueued_variables(&self) -> impl Iterator<Item = K> + '_ {
+        self.heap.iter().map(|e| e.key)
+    }
+
     /// Record a new element that is NOT added in the queue.
     /// The element is assigned the given priority.
     pub fn declare_element(&mut self, key: K, priority: P)

solver/src/core/state/explanation.rs

@@ -69,10 +69,6 @@ pub(crate) struct ExplanationQueue {
 }
 
 impl ExplanationQueue {
-    pub fn new() -> Self {
-        Self::default()
-    }
-
     pub fn is_empty(&self) -> bool {
         self.heap.is_empty()
     }

solver/src/solver/search.rs

@@ -4,7 +4,7 @@ pub mod conflicts;
 pub mod lexical;
 pub mod random;
 
-use crate::backtrack::Backtrack;
+use crate::backtrack::{Backtrack, DecLvl};
 use crate::core::state::{Conflict, Explainer};
 use crate::core::*;
 use crate::model::extensions::SavedAssignment;
@@ -45,8 +45,16 @@ pub trait SearchControl<Lbl>: Backtrack {
     /// In particular, it is invoked before analysing the confilct, which might partially undo the trail.
     fn pre_conflict_analysis(&mut self, _model: &Model<Lbl>) {}
 
-    /// Invoked by search when facing a conflict in the search
-    fn conflict(&mut self, clause: &Conflict, model: &Model<Lbl>, explainer: &mut dyn Explainer) {}
+    /// Invoked by search when facing a conflict in the search.
+    /// Also indicate the level at which the search would backtrack as a result fo this conflict.
+    fn conflict(
+        &mut self,
+        clause: &Conflict,
+        model: &Model<Lbl>,
+        explainer: &mut dyn Explainer,
+        backtrack_level: DecLvl,
+    ) {
+    }
 
     /// Invoked by the search when an asserting clause is added to the database. `lit` is the literal that would be asserted.
     fn asserted_after_conflict(&mut self, lit: Lit, model: &Model<Lbl>) {}

solver/src/solver/search/activity.rs

@@ -482,7 +482,13 @@ impl<Lbl: Label> SearchControl<Lbl> for ActivityBrancher<Lbl> {
         }
     }
 
-    fn conflict(&mut self, clause: &Conflict, model: &Model<Lbl>, _explainer: &mut dyn Explainer) {
+    fn conflict(
+        &mut self,
+        clause: &Conflict,
+        model: &Model<Lbl>,
+        _explainer: &mut dyn Explainer,
+        _backtrack_level: DecLvl,
+    ) {
         // bump activity of all variables of the clause
         self.heap.decay_activities();
         for b in clause.literals() {

solver/src/solver/search/combinators.rs

@@ -73,9 +73,15 @@ impl<L: 'static> SearchControl<L> for AndThen<L> {
         self.second.new_assignment_found(objective_value, assignment);
     }
 
-    fn conflict(&mut self, clause: &Conflict, model: &Model<L>, explainer: &mut dyn Explainer) {
-        self.first.conflict(clause, model, explainer);
-        self.second.conflict(clause, model, explainer);
+    fn conflict(
+        &mut self,
+        clause: &Conflict,
+        model: &Model<L>,
+        explainer: &mut dyn Explainer,
+        backtrack_level: DecLvl,
+    ) {
+        self.first.conflict(clause, model, explainer, backtrack_level);
+        self.second.conflict(clause, model, explainer, backtrack_level);
     }
 
     fn asserted_after_conflict(&mut self, lit: Lit, model: &Model<L>) {
@@ -148,7 +154,13 @@ impl<L: 'static> SearchControl<L> for UntilFirstConflict<L> {
         }
     }
 
-    fn conflict(&mut self, _clause: &Conflict, _model: &Model<L>, _explainer: &mut dyn Explainer) {
+    fn conflict(
+        &mut self,
+        _clause: &Conflict,
+        _model: &Model<L>,
+        _explainer: &mut dyn Explainer,
+        _backtrack_level: DecLvl,
+    ) {
         self.active = false;
     }
 
@@ -232,8 +244,14 @@ impl<L: 'static> SearchControl<L> for WithGeomRestart<L> {
         self.brancher.new_assignment_found(objective_value, assignment)
     }
 
-    fn conflict(&mut self, clause: &Conflict, model: &Model<L>, explainer: &mut dyn Explainer) {
-        self.brancher.conflict(clause, model, explainer)
+    fn conflict(
+        &mut self,
+        clause: &Conflict,
+        model: &Model<L>,
+        explainer: &mut dyn Explainer,
+        backtrack_level: DecLvl,
+    ) {
+        self.brancher.conflict(clause, model, explainer, backtrack_level)
     }
 
     fn asserted_after_conflict(&mut self, lit: Lit, model: &Model<L>) {