Skip to content

perf: track active requirement parents #187

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
baszalmstra wants to merge 1 commit into
base: main
Choose a base branch
from
Open

perf: track active requirement parents #187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions src/solver/encoding.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand Down Expand Up @@ -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,
);
}
},
|| {
Expand Down Expand Up @@ -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,
);
}
}

Expand Down
127 changes: 101 additions & 26 deletions src/solver/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -196,6 +196,11 @@ pub(crate) struct SolverState {

/// Activity score per package.
name_activity: Vec<f32>,

/// 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<VariableId, ahash::RandomState>,
}

impl<D: DependencyProvider> Solver<D, NowOrNeverRuntime> {
Expand Down Expand Up @@ -429,19 +434,23 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
"╤══ 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(
Expand Down Expand Up @@ -607,19 +616,23 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
))
} 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)
}
}
Expand Down Expand Up @@ -710,20 +723,33 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}

let mut best_decision: Option<PossibleDecision> = 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(());
Expand Down Expand Up @@ -871,6 +897,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}
}

i += 1;
}

if let Some(PossibleDecision {
Expand Down Expand Up @@ -926,6 +954,12 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
.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)
}
Expand Down Expand Up @@ -1018,19 +1052,24 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {

// 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}");
Expand Down Expand Up @@ -1132,6 +1171,12 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
})?;

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(..) => {}
Expand Down Expand Up @@ -1170,6 +1215,12 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
.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()),
Expand Down Expand Up @@ -1210,6 +1261,12 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
.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
Expand Down Expand Up @@ -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<VariableId, Vec<RequiresClause>, ahash::RandomState>,
active_requires_parents: &mut IndexSet<VariableId, ahash::RandomState>,
) {
if value && requires_clauses.contains_key(&variable) {
active_requires_parents.insert(variable);
}
}