From ee5c7ba39daaf4a7fa63cd1b18482f565f643b61 Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Tue, 6 Aug 2024 14:52:33 +0200 Subject: [PATCH 1/6] feat: decide on an explicit requirements first --- src/solver/mod.rs | 114 +++++++++++++++++++++++++++------------------- 1 file changed, 67 insertions(+), 47 deletions(-) diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 66bed80..69c9e9a 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -1,11 +1,14 @@ +use std::{ + any::Any, cell::RefCell, collections::HashSet, fmt::Display, future::ready, ops::ControlFlow, +}; + +use ahash::AHashSet; pub use cache::SolverCache; use clause::{Clause, ClauseState, Literal}; use decision::Decision; use decision_tracker::DecisionTracker; use futures::{stream::FuturesUnordered, FutureExt, StreamExt}; use itertools::Itertools; -use std::fmt::Display; -use std::{any::Any, cell::RefCell, collections::HashSet, future::ready, ops::ControlFlow}; use watch_map::WatchMap; use crate::{ @@ -37,23 +40,24 @@ struct AddClauseOutput { /// Describes the problem that is to be solved by the solver. #[derive(Default)] pub struct Problem { - /// The requirements that _must_ have one candidate solvable be included in the - /// solution. + /// The requirements that _must_ have one candidate solvable be included in + /// the solution. pub requirements: Vec, - /// Additional constraints imposed on individual packages that the solvable (if any) - /// chosen for that package _must_ adhere to. + /// Additional constraints imposed on individual packages that the solvable + /// (if any) chosen for that package _must_ adhere to. pub constraints: Vec, - /// A set of additional requirements that the solver should _try_ and fulfill once it has - /// found a solution to the main problem. + /// A set of additional requirements that the solver should _try_ and + /// fulfill once it has found a solution to the main problem. /// - /// An unsatisfiable soft requirement does not cause a conflict; the solver will try - /// and fulfill as many soft requirements as possible and skip the unsatisfiable ones. + /// An unsatisfiable soft requirement does not cause a conflict; the solver + /// will try and fulfill as many soft requirements as possible and skip + /// the unsatisfiable ones. /// - /// Soft requirements are currently only specified as individual solvables to be - /// included in the solution, however in the future they will be able to be specified - /// as version sets. + /// Soft requirements are currently only specified as individual solvables + /// to be included in the solution, however in the future they will be + /// able to be specified as version sets. pub soft_requirements: Vec, } @@ -180,27 +184,32 @@ impl Solver { /// Solves the given [`Problem`]. /// - /// The solver first solves for the root requirements and constraints, and then - /// tries to include in the solution as many of the soft requirements as it can. - /// Each soft requirement is subject to all the clauses and decisions introduced - /// for all the previously decided solvables in the solution. + /// The solver first solves for the root requirements and constraints, and + /// then tries to include in the solution as many of the soft + /// requirements as it can. Each soft requirement is subject to all the + /// clauses and decisions introduced for all the previously decided + /// solvables in the solution. /// - /// Unless the corresponding package has been requested by a version set in another - /// solvable's clauses, each soft requirement is _not_ subject to the - /// package-level clauses introduced in [`DependencyProvider::get_candidates`] since the - /// solvables have been requested specifically (not through a version set) in the solution. + /// Unless the corresponding package has been requested by a version set in + /// another solvable's clauses, each soft requirement is _not_ subject + /// to the package-level clauses introduced in + /// [`DependencyProvider::get_candidates`] since the solvables have been + /// requested specifically (not through a version set) in the solution. /// /// # Returns /// - /// If a solution was found, returns a [`Vec`] of the solvables included in the solution. + /// If a solution was found, returns a [`Vec`] of the solvables included in + /// the solution. /// - /// If no solution to the _root_ requirements and constraints was found, returns a - /// [`Conflict`] wrapped in a [`UnsolvableOrCancelled::Unsolvable`], which provides ways to - /// inspect the causes and report them to the user. If a soft requirement is unsolvable, - /// it is simply not included in the solution. + /// If no solution to the _root_ requirements and constraints was found, + /// returns a [`Conflict`] wrapped in a + /// [`UnsolvableOrCancelled::Unsolvable`], which provides ways to + /// inspect the causes and report them to the user. If a soft requirement is + /// unsolvable, it is simply not included in the solution. /// - /// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]), - /// returns an [`UnsolvableOrCancelled::Cancelled`] containing the cancellation value. + /// If the solution process is cancelled (see + /// [`DependencyProvider::should_cancel_with_value`]), returns an + /// [`UnsolvableOrCancelled::Cancelled`] containing the cancellation value. pub fn solve(&mut self, problem: Problem) -> Result, UnsolvableOrCancelled> { self.decision_tracker.clear(); self.negative_assertions.clear(); @@ -232,7 +241,8 @@ impl Solver { Ok(self.chosen_solvables().collect()) } - /// Returns the solvables that the solver has chosen to include in the solution so far. + /// Returns the solvables that the solver has chosen to include in the + /// solution so far. fn chosen_solvables(&self) -> impl Iterator + '_ { self.decision_tracker.stack().filter_map(|d| { if d.value { @@ -609,12 +619,14 @@ impl Solver { /// /// The solver loop can be found in [`Solver::resolve_dependencies`]. /// - /// Returns `Ok(true)` if a solution was found for `solvable`. If a solution was not - /// found, returns `Ok(false)` if some decisions have already been made by the solver - /// (i.e. the decision tracker stack is not empty). Otherwise, returns - /// [`UnsolvableOrCancelled::Unsolvable`] as an `Err` on no solution. + /// Returns `Ok(true)` if a solution was found for `solvable`. If a solution + /// was not found, returns `Ok(false)` if some decisions have already + /// been made by the solver (i.e. the decision tracker stack is not + /// empty). Otherwise, returns [`UnsolvableOrCancelled::Unsolvable`] as + /// an `Err` on no solution. /// - /// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]), + /// If the solution process is cancelled (see + /// [`DependencyProvider::should_cancel_with_value`]), /// returns [`UnsolvableOrCancelled::Cancelled`] as an `Err`. fn run_sat(&mut self, solvable: InternalSolvableId) -> Result { let starting_level = self @@ -765,12 +777,13 @@ impl Solver { } } - /// Decides how to terminate the solver algorithm when the given `solvable` was - /// deemed unsolvable by [`Solver::run_sat`]. + /// Decides how to terminate the solver algorithm when the given `solvable` + /// was deemed unsolvable by [`Solver::run_sat`]. /// - /// Returns an `Err` value of [`UnsolvableOrCancelled::Unsolvable`] only if `solvable` is - /// the very first solvable we are solving for. Otherwise, undoes all the decisions made - /// when trying to solve for `solvable`, sets it to `false` and returns `Ok(false)`. + /// Returns an `Err` value of [`UnsolvableOrCancelled::Unsolvable`] only if + /// `solvable` is the very first solvable we are solving for. Otherwise, + /// undoes all the decisions made when trying to solve for `solvable`, + /// sets it to `false` and returns `Ok(false)`. fn run_sat_process_unsolvable( &mut self, solvable: InternalSolvableId, @@ -853,7 +866,9 @@ impl Solver { /// ensures that if there are conflicts they are delt with as early as /// possible. fn decide(&mut self) -> Option<(InternalSolvableId, InternalSolvableId, ClauseId)> { - let mut best_decision = None; + let explicit_requirements: AHashSet<_> = self.root_requirements.iter().collect(); + let mut best_decision: Option<(bool, i32, (SolvableId, InternalSolvableId, ClauseId))> = + None; for &(solvable_id, deps, clause_id) in &self.requires_clauses { // Consider only clauses in which we have decided to install the solvable if self.decision_tracker.assigned_value(solvable_id) != Some(true) { @@ -884,13 +899,14 @@ impl Solver { }, ); + let is_explicit_requirement = explicit_requirements.contains(&deps); match candidate { ControlFlow::Continue((Some(candidate), count)) => { let possible_decision = (candidate, solvable_id, clause_id); best_decision = Some(match best_decision { - None => (count, possible_decision), - Some((best_count, _)) if count < best_count => { - (count, possible_decision) + None => (is_explicit_requirement, count, possible_decision), + Some((was_explicit_requirement, best_count, _)) if (is_explicit_requirement && !was_explicit_requirement) || (count < best_count && was_explicit_requirement == is_explicit_requirement) => { + (is_explicit_requirement, count, possible_decision) } Some(best_decision) => best_decision, }) @@ -900,7 +916,9 @@ impl Solver { } } - if let Some((count, (candidate, _solvable_id, clause_id))) = best_decision { + if let Some((_is_explicit_requirement, count, (candidate, _solvable_id, clause_id))) = + best_decision + { tracing::trace!( "deciding to assign {}, ({}, {} possible candidates)", self.provider().display_solvable(candidate), @@ -910,9 +928,11 @@ impl Solver { } // Could not find a requirement that needs satisfying. - best_decision.map(|(_best_count, (candidate, required_by, via))| { - (candidate.into(), required_by, via) - }) + best_decision.map( + |(_is_explicit_dependency, _best_count, (candidate, required_by, via))| { + (candidate.into(), required_by, via) + }, + ) } /// Executes one iteration of the CDCL loop From 19f8d9ef664ca00cf1f4230d2fb33f0544f336cc Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Tue, 6 Aug 2024 15:04:04 +0200 Subject: [PATCH 2/6] test: add a test that shows the result --- src/solver/mod.rs | 4 +--- tests/.solver.rs.pending-snap | 5 +++++ tests/solver.rs | 31 +++++++++++++++++++++++++++++++ 3 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 tests/.solver.rs.pending-snap diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 69c9e9a..d617e6e 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -2,7 +2,6 @@ use std::{ any::Any, cell::RefCell, collections::HashSet, fmt::Display, future::ready, ops::ControlFlow, }; -use ahash::AHashSet; pub use cache::SolverCache; use clause::{Clause, ClauseState, Literal}; use decision::Decision; @@ -866,7 +865,6 @@ impl Solver { /// ensures that if there are conflicts they are delt with as early as /// possible. fn decide(&mut self) -> Option<(InternalSolvableId, InternalSolvableId, ClauseId)> { - let explicit_requirements: AHashSet<_> = self.root_requirements.iter().collect(); let mut best_decision: Option<(bool, i32, (SolvableId, InternalSolvableId, ClauseId))> = None; for &(solvable_id, deps, clause_id) in &self.requires_clauses { @@ -899,7 +897,7 @@ impl Solver { }, ); - let is_explicit_requirement = explicit_requirements.contains(&deps); + let is_explicit_requirement = solvable_id == InternalSolvableId::root(); match candidate { ControlFlow::Continue((Some(candidate), count)) => { let possible_decision = (candidate, solvable_id, clause_id); diff --git a/tests/.solver.rs.pending-snap b/tests/.solver.rs.pending-snap new file mode 100644 index 0000000..f76c8d4 --- /dev/null +++ b/tests/.solver.rs.pending-snap @@ -0,0 +1,5 @@ +{"run_id":"1722949163-45203500","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=2\nb=1\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":"\""}} +{"run_id":"1722949217-541136000","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=2\nb=1\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} +{"run_id":"1722949276-272630500","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=1\nb=2\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} +{"run_id":"1722949296-280282400","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=1\nb=1\nc=5\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} +{"run_id":"1722949417-460194000","line":1427,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1427,"expression":"result"},"snapshot":"a=1\nb=1\nc=5\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} diff --git a/tests/solver.rs b/tests/solver.rs index 6aa1cea..c0e286f 100644 --- a/tests/solver.rs +++ b/tests/solver.rs @@ -1396,6 +1396,37 @@ fn test_snapshot_union_requirements() { )); } +#[test] +fn test_explicit_root_requirements() { + let provider = BundleBoxProvider::from_packages(&[ + // `a` depends transitively on `b` + ("a", 1, vec!["b"]), + // `b` depends on `c`, but the highest version of `b` constrains `c` to `<2`. + ("b", 1, vec!["c"]), + ("b", 2, vec!["c 1..2"]), + // `c` has more versions than `b`, so the heuristic will most likely pick `b` first. + ("c", 1, vec![]), + ("c", 2, vec![]), + ("c", 3, vec![]), + ("c", 4, vec![]), + ("c", 5, vec![]), + ]); + + // We require both `a` and `c` explicitly. The expected outcome will be that we + // get the highest versions of `a` and `c` and a lower version of `b`. + let requirements = provider.requirements(&["a", "c"]); + + let mut solver = Solver::new(provider); + let problem = Problem { + requirements, + ..Problem::default() + }; + let solved = solver.solve(problem).unwrap(); + + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r###""###); +} + #[cfg(feature = "serde")] fn serialize_snapshot(snapshot: &DependencySnapshot, destination: impl AsRef) { let file = std::io::BufWriter::new(std::fs::File::create(destination.as_ref()).unwrap()); From 56e52067f3574a3b5dfd54457b7d137fc290a34c Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Tue, 6 Aug 2024 15:06:07 +0200 Subject: [PATCH 3/6] remove unused file --- tests/.solver.rs.pending-snap | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 tests/.solver.rs.pending-snap diff --git a/tests/.solver.rs.pending-snap b/tests/.solver.rs.pending-snap deleted file mode 100644 index f76c8d4..0000000 --- a/tests/.solver.rs.pending-snap +++ /dev/null @@ -1,5 +0,0 @@ -{"run_id":"1722949163-45203500","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=2\nb=1\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":"\""}} -{"run_id":"1722949217-541136000","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=2\nb=1\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} -{"run_id":"1722949276-272630500","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=1\nb=2\nc=1\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} -{"run_id":"1722949296-280282400","line":1422,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1422,"expression":"result"},"snapshot":"a=1\nb=1\nc=5\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} -{"run_id":"1722949417-460194000","line":1427,"new":{"module_name":"solver","snapshot_name":"explicit_root_requirements","metadata":{"source":"tests/solver.rs","assertion_line":1427,"expression":"result"},"snapshot":"a=1\nb=1\nc=5\n"},"old":{"module_name":"solver","metadata":{},"snapshot":""}} From ea19b825936ce5cb93b4a8659991e75de8e9be04 Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Tue, 6 Aug 2024 15:07:33 +0200 Subject: [PATCH 4/6] include snapshot --- tests/solver.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/solver.rs b/tests/solver.rs index c0e286f..d8e3054 100644 --- a/tests/solver.rs +++ b/tests/solver.rs @@ -1424,7 +1424,11 @@ fn test_explicit_root_requirements() { let solved = solver.solve(problem).unwrap(); let result = transaction_to_string(solver.provider(), &solved); - assert_snapshot!(result, @r###""###); + assert_snapshot!(result, @r###" + a=1 + b=1 + c=5 + "###); } #[cfg(feature = "serde")] From 51e0cc65a9cfdb8bd4f4b327c448bf6c449dfede Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Tue, 6 Aug 2024 17:38:17 +0200 Subject: [PATCH 5/6] small performance optimizations --- src/solver/mod.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/solver/mod.rs b/src/solver/mod.rs index d617e6e..0192f20 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -868,6 +868,13 @@ impl Solver { let mut best_decision: Option<(bool, i32, (SolvableId, InternalSolvableId, ClauseId))> = None; for &(solvable_id, deps, clause_id) in &self.requires_clauses { + let is_explicit_requirement = solvable_id == InternalSolvableId::root(); + if !is_explicit_requirement && matches!(best_decision, Some((true, _, _))) { + // If we already have an explicit requirement, there is no need to evaluate + // non-explicit requirements. + continue; + } + // Consider only clauses in which we have decided to install the solvable if self.decision_tracker.assigned_value(solvable_id) != Some(true) { continue; @@ -897,13 +904,13 @@ impl Solver { }, ); - let is_explicit_requirement = solvable_id == InternalSolvableId::root(); match candidate { ControlFlow::Continue((Some(candidate), count)) => { let possible_decision = (candidate, solvable_id, clause_id); best_decision = Some(match best_decision { None => (is_explicit_requirement, count, possible_decision), - Some((was_explicit_requirement, best_count, _)) if (is_explicit_requirement && !was_explicit_requirement) || (count < best_count && was_explicit_requirement == is_explicit_requirement) => { + Some((false, _, _)) if is_explicit_requirement => (is_explicit_requirement, count, possible_decision), + Some((_, best_count, _)) if count < best_count => { (is_explicit_requirement, count, possible_decision) } Some(best_decision) => best_decision, From b44502c56edbda4d34ee118f57caf8c2ceb1f883 Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Mon, 9 Sep 2024 16:36:40 +0200 Subject: [PATCH 6/6] fix: clippy --- tools/solve-snapshot/src/main.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/solve-snapshot/src/main.rs b/tools/solve-snapshot/src/main.rs index 67692f6..be7f732 100644 --- a/tools/solve-snapshot/src/main.rs +++ b/tools/solve-snapshot/src/main.rs @@ -58,14 +58,14 @@ fn main() { // Generate a range of problems. let mut rng = StdRng::seed_from_u64(0); - let requirement_dist = WeightedIndex::new(&[ + let requirement_dist = WeightedIndex::new([ 10, // 10 times more likely to pick a package - if snapshot.version_sets.len() > 0 { + if !snapshot.version_sets.is_empty() { 1 } else { 0 }, - if snapshot.version_set_unions.len() > 0 { + if !snapshot.version_set_unions.is_empty() { 1 } else { 0