feat(search): Add an option to drive search away from last solution i…

…n LRB.

This tends to prove better result that searching towards the last solution when trying to prove optimality.

examples/scheduling/src/main.rs

@@ -9,7 +9,6 @@ use aries::model::extensions::AssignmentExt;
 use aries::model::lang::IVar;
 use aries::solver::parallel::SolverResult;
 use std::fmt::Write;
-use std::fs;
 use std::time::{Duration, Instant};
 use structopt::StructOpt;
 use walkdir::WalkDir;
@@ -32,14 +31,23 @@ pub struct Opt {
     #[structopt(long = "upper-bound", default_value = "100000")]
     upper_bound: u32,
     /// Search strategy to use in {activity, est, parallel}
-    #[structopt(long = "search", default_value = "learning-rate")]
+    #[structopt(long = "search", default_value = "parallel")]
     search: SearchStrategy,
     /// maximum runtime, in seconds.
     #[structopt(long = "timeout", short = "t")]
     timeout: Option<u32>,
 }
 
 fn main() -> Result<()> {
+    // Terminate the process if a thread panics.
+    // take_hook() returns the default hook in case when a custom one is not set
+    let orig_hook = std::panic::take_hook();
+    std::panic::set_hook(Box::new(move |panic_info| {
+        // invoke the default handler and exit the process
+        orig_hook(panic_info);
+        std::process::exit(1);
+    }));
+    // read command line arguments
     let opt = Opt::from_args();
 
     let file = &opt.file;
@@ -61,7 +69,7 @@ fn main() -> Result<()> {
 fn solve(kind: ProblemKind, instance: &str, opt: &Opt) {
     let deadline = opt.timeout.map(|dur| Instant::now() + Duration::from_secs(dur as u64));
     let start_time = std::time::Instant::now();
-    let filecontent = fs::read_to_string(instance).expect("Cannot read file");
+    let filecontent = std::fs::read_to_string(instance).expect("Cannot read file");
     let pb = match kind {
         ProblemKind::OpenShop => parser::openshop(&filecontent),
         ProblemKind::JobShop => parser::jobshop(&filecontent),

examples/scheduling/src/search.rs

@@ -6,7 +6,7 @@ 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};
+use aries::solver::search::conflicts::{ActiveLiterals, ConflictBasedBrancher, Params, ValueSelection};
 use aries::solver::search::lexical::LexicalMinValue;
 use aries::solver::search::{conflicts, Brancher};
 use std::str::FromStr;
@@ -39,15 +39,19 @@ pub enum SearchStrategy {
     /// greedy earliest-starting-time then VSIDS with solution guidance
     Activity,
     /// greedy earliest-starting-time then LRB with solution guidance
-    LearningRate,
+    /// Boolean parameter indicates whether we should prefer the value of the last solution or the opposite
+    LearningRate(bool),
+    Parallel,
 }
 impl FromStr for SearchStrategy {
     type Err = String;
 
     fn from_str(s: &str) -> Result<Self, Self::Err> {
         match s {
-            "lrb" | "learning-rate" => Ok(SearchStrategy::LearningRate),
+            "lrb" | "lrb+" | "learning-rate" => Ok(SearchStrategy::LearningRate(true)),
+            "lrb-" | "learning-rate-neg" => Ok(SearchStrategy::LearningRate(false)),
             "vsids" | "activity" => Ok(SearchStrategy::Activity),
+            "par" | "parallel" => Ok(SearchStrategy::Parallel),
             e => Err(format!("Unrecognized option: '{e}'")),
         }
     }
@@ -91,24 +95,28 @@ pub fn get_solver(base: Solver, strategy: SearchStrategy, pb: &Encoding) -> ParS
         s.set_brancher_boxed(strat);
     };
 
-    match strategy {
-        SearchStrategy::Activity => ParSolver::new(base_solver, 1, |_, s| {
-            make_solver(
-                s,
-                conflicts::Params {
-                    heuristic: conflicts::Heuristic::Vsids,
-                    active: ActiveLiterals::Reasoned,
-                },
-            )
-        }),
-        SearchStrategy::LearningRate => ParSolver::new(base_solver, 1, |_, s| {
-            make_solver(
-                s,
-                conflicts::Params {
-                    heuristic: conflicts::Heuristic::LearningRate,
-                    active: ActiveLiterals::Reasoned,
-                },
-            )
-        }),
-    }
+    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 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],
+    };
+
+    ParSolver::new(base_solver, strats.len(), |i, s| make_solver(s, strats[i]))
 }

solver/src/solver/search/conflicts.rs

@@ -50,6 +50,7 @@ pub struct Params {
     pub heuristic: Heuristic,
     /// How do we determine that a variable participates in a conflict.
     pub active: ActiveLiterals,
+    pub value_selection: ValueSelection,
 }
 
 #[derive(PartialEq, Copy, Clone, Debug)]
@@ -75,13 +76,25 @@ pub enum ActiveLiterals {
     Reasoned,
 }
 
+/// Configuration of the value selection heuristic
+#[derive(PartialEq, Copy, Clone, Debug)]
+pub enum ValueSelection {
+    /// Prefer the value of the last solution.
+    /// Typically preferred when optimizing.
+    Sol,
+    /// Prefer a value that is not in the last solution.
+    /// Typically preferred when proving the optimality of the current solution
+    NotSol,
+}
+
 impl Default for Params {
     fn default() -> Self {
         Params {
             // Reasoned is normally the most efficient but our implementation for explanation is
             // not always supporting it.
             active: ActiveLiterals::Resolved,
             heuristic: Heuristic::LearningRate,
+            value_selection: ValueSelection::Sol,
         }
     }
 }
@@ -190,7 +203,11 @@ impl ConflictBasedBrancher {
                 Lit::leq(v, value)
             };
             // println!("dec: {literal:?}   {}", self.heap.activity(literal));
-            Some(Decision::SetLiteral(literal))
+            let decision = match self.params.value_selection {
+                ValueSelection::Sol => literal,
+                ValueSelection::NotSol => !literal,
+            };
+            Some(Decision::SetLiteral(decision))
         } else {
             // all variables are set, no decision left
             None