From beb6d57d26e87d87ce5276cf4f2b2e0cbe461aa3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 26 Nov 2025 19:18:32 +0000 Subject: [PATCH] Optimize decide() by tracking active requirement parents Instead of iterating over all requires_clauses in decide(), maintain an IndexSet of variables that are assigned true and have requires clauses. This reduces the iteration scope to only relevant variables. Key changes: - Add active_requires_parents field to SolverState - Add track_decision_for_requires() free function for split borrows - Update decide() to iterate over active_requires_parents with lazy cleanup - Use index-based iteration with in-place swap_remove for stale entries --- src/solver/encoding.rs | 21 +++++++ src/solver/mod.rs | 127 ++++++++++++++++++++++++++++++++--------- 2 files changed, 122 insertions(+), 26 deletions(-) diff --git a/src/solver/encoding.rs b/src/solver/encoding.rs index 9daab6b..44f8a6b 100644 --- a/src/solver/encoding.rs +++ b/src/solver/encoding.rs @@ -370,6 +370,15 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { .or_default() .push((requirement.requirement, condition, clause_id)); + // If the variable is already assigned true, add it to active_requires_parents + // so that decide() will consider its requirements + super::track_decision_for_requires( + variable, + self.state.decision_tracker.assigned_value(variable) == Some(true), + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); + if conflict { self.conflicting_clauses.push(clause_id); } else if no_candidates && condition.is_none() { @@ -676,6 +685,12 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { self.level, ) .expect("we checked that there is no value yet"); + super::track_decision_for_requires( + literal.variable(), + literal.satisfying_value(), + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); } }, || { @@ -749,6 +764,12 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { self.level, ) .expect("the at least one variable must be undecided"); + super::track_decision_for_requires( + at_least_one_variable, + true, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 8e0e25e..40e1e64 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -8,7 +8,7 @@ use decision::Decision; use decision_tracker::DecisionTracker; use elsa::FrozenMap; use encoding::Encoder; -use indexmap::IndexMap; +use indexmap::{IndexMap, IndexSet}; use itertools::Itertools; use variable_map::VariableMap; use watch_map::WatchMap; @@ -196,6 +196,11 @@ pub(crate) struct SolverState { /// Activity score per package. name_activity: Vec, + + /// Variables that are assigned true and have requires clauses. + /// Used to speed up `decide()` by only iterating over relevant variables. + /// May contain stale entries which are cleaned up lazily during `decide()`. + active_requires_parents: IndexSet, } impl Solver { @@ -429,19 +434,23 @@ impl Solver { "╤══ Install {} at level {level}", root_solvable.display(self.provider()) ); + let root_variable = self + .state + .variable_map + .intern_solvable_or_root(root_solvable); self.state .decision_tracker .try_add_decision( - Decision::new( - self.state - .variable_map - .intern_solvable_or_root(root_solvable), - true, - ClauseId::install_root(), - ), + Decision::new(root_variable, true, ClauseId::install_root()), level, ) .expect("already decided"); + track_decision_for_requires( + root_variable, + true, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); // Add the clauses for the root solvable. let conflicting_clauses = self.async_runtime.block_on( @@ -607,19 +616,23 @@ impl Solver { )) } else { self.state.decision_tracker.undo_until(starting_level); + let variable = self + .state + .variable_map + .intern_solvable_or_root(solvable_or_root); self.state .decision_tracker .try_add_decision( - Decision::new( - self.state - .variable_map - .intern_solvable_or_root(solvable_or_root), - false, - ClauseId::install_root(), - ), + Decision::new(variable, false, ClauseId::install_root()), starting_level + 1, ) .expect("bug: already decided - decision should have been undone"); + track_decision_for_requires( + variable, + false, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); Ok(false) } } @@ -710,20 +723,33 @@ impl Solver { } let mut best_decision: Option = None; - for (&solvable_id, requirements) in self.state.requires_clauses.iter() { + + // Use index-based iteration to allow in-place removal of stale entries + let mut i = 0; + while i < self.state.active_requires_parents.len() { + let solvable_id = *self.state.active_requires_parents.get_index(i).unwrap(); + + // Lazy cleanup: if no longer assigned true, remove in-place and skip + if self.state.decision_tracker.assigned_value(solvable_id) != Some(true) { + self.state.active_requires_parents.swap_remove_index(i); + continue; // Don't increment, check swapped-in element + } + let is_explicit_requirement = solvable_id == VariableId::root(); if let Some(best_decision) = &best_decision { // If we already have an explicit requirement, there is no need to evaluate // non-explicit requirements. if best_decision.is_explicit_requirement && !is_explicit_requirement { + i += 1; continue; } } - // Consider only clauses in which we have decided to install the solvable - if self.state.decision_tracker.assigned_value(solvable_id) != Some(true) { - continue; - } + let Some(requirements) = self.state.requires_clauses.get(&solvable_id) else { + // No requirements for this variable (shouldn't happen but handle gracefully) + self.state.active_requires_parents.swap_remove_index(i); + continue; // Don't increment, check swapped-in element + }; for (deps, condition, clause_id) in requirements.iter() { let mut candidate = ControlFlow::Break(()); @@ -871,6 +897,8 @@ impl Solver { } } } + + i += 1; } if let Some(PossibleDecision { @@ -926,6 +954,12 @@ impl Solver { .decision_tracker .try_add_decision(Decision::new(solvable, true, clause_id), level) .expect("bug: solvable was already decided!"); + track_decision_for_requires( + solvable, + true, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); self.propagate_and_learn(level) } @@ -1018,19 +1052,24 @@ impl Solver { // Optimization: propagate right now, since we know that the clause is a unit // clause - let decision = literal.satisfying_value(); + let decision_value = literal.satisfying_value(); + let decision_variable = literal.variable(); self.state .decision_tracker .try_add_decision( - Decision::new(literal.variable(), decision, learned_clause_id), + Decision::new(decision_variable, decision_value, learned_clause_id), level, ) .expect("bug: solvable was already decided!"); + track_decision_for_requires( + decision_variable, + decision_value, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); tracing::trace!( - "│├ Propagate after learn: {} = {decision}", - literal - .variable() - .display(&self.state.variable_map, self.provider()), + "│├ Propagate after learn: {} = {decision_value}", + decision_variable.display(&self.state.variable_map, self.provider()), ); tracing::debug!("│└ Backtracked from {old_level} -> {level}"); @@ -1132,6 +1171,12 @@ impl Solver { })?; if decided { + track_decision_for_requires( + other_watched_literal.variable(), + other_watched_literal.satisfying_value(), + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); match clause { // Skip logging for ForbidMultipleInstances, which is so noisy Clause::ForbidMultipleInstances(..) => {} @@ -1170,6 +1215,12 @@ impl Solver { .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?; if decided { + track_decision_for_requires( + solvable_id, + value, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); tracing::trace!( "Negative assertions derived from other rules: Propagate assertion {} = {}", solvable_id.display(&self.state.variable_map, self.provider()), @@ -1210,6 +1261,12 @@ impl Solver { .map_err(|_| PropagationError::Conflict(literal.variable(), decision, clause_id))?; if decided { + track_decision_for_requires( + literal.variable(), + decision, + &self.state.requires_clauses, + &mut self.state.active_requires_parents, + ); tracing::trace!( "├─ Propagate assertion {} = {}", literal @@ -1482,3 +1539,21 @@ impl SolverState { }) } } + +/// Called after a decision is successfully added to the decision tracker. +/// If the variable is assigned true and has requires clauses, it is added +/// to `active_requires_parents` to speed up the `decide()` function. +/// +/// This is a free function to enable split borrows - callers may hold borrows +/// to other SolverState fields while calling this. +#[inline] +fn track_decision_for_requires( + variable: VariableId, + value: bool, + requires_clauses: &IndexMap, ahash::RandomState>, + active_requires_parents: &mut IndexSet, +) { + if value && requires_clauses.contains_key(&variable) { + active_requires_parents.insert(variable); + } +}