From 6df2b6f4b1626a97666b084fb7630afac509f1fc Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Fri, 30 Aug 2024 15:57:33 +0200 Subject: [PATCH] feat(search): Add an option to drive search away from last solution in LRB. This tends to prove better result that searching towards the last solution when trying to prove optimality. --- examples/scheduling/src/main.rs | 14 +++++-- examples/scheduling/src/search.rs | 54 +++++++++++++++------------ solver/src/solver/search/conflicts.rs | 19 +++++++++- 3 files changed, 60 insertions(+), 27 deletions(-) diff --git a/examples/scheduling/src/main.rs b/examples/scheduling/src/main.rs index 2b89ee9c..76872f07 100644 --- a/examples/scheduling/src/main.rs +++ b/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,7 +31,7 @@ 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")] @@ -40,6 +39,15 @@ pub struct Opt { } 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), diff --git a/examples/scheduling/src/search.rs b/examples/scheduling/src/search.rs index 91b7c3e2..88c54d4e 100644 --- a/examples/scheduling/src/search.rs +++ b/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 { 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])) } diff --git a/solver/src/solver/search/conflicts.rs b/solver/src/solver/search/conflicts.rs index c4012ef2..c9bbb730 100644 --- a/solver/src/solver/search/conflicts.rs +++ b/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,6 +76,17 @@ 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 { @@ -82,6 +94,7 @@ impl Default for Params { // 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