From de25564ae661522668ba832f67d83a524c06805f Mon Sep 17 00:00:00 2001 From: Daniel Alley Date: Sun, 31 May 2026 21:55:42 -0400 Subject: [PATCH 1/2] Fix assertion failure when a package constrains itself In such a case, the constrains clause would try to forbid the package from coexisting with itself. This caused WatchedLiterals::constrains to panic with "both literals cannot be false" because both watched literals referred to the same variable. There exists a special case in certain packaging ecosystems such as RPM, where a package can both provide and conflict with the same capability (example: in CentOS Stream, the "centos-stream-release" provides "system-release" and also conflicts with "system-release"). This is explicitly permitted and supported by libsolv, which provides the configuration flag "forbidselfconflicts" which can be disabled. Provide an option to skip self-referential constrains entries, so that implementations can configure the resolver such that a package that is already in the solution cannot constrain itself out of it. Assisted-By: Claude Opus 4.6 --- src/lib.rs | 13 +++++++- src/solver/encoding.rs | 34 +++++++++++++++++++- src/solver/mod.rs | 31 ++++++++++++++++++ tests/solver/main.rs | 73 +++++++++++++++++++++++++++++++++++++++++- 4 files changed, 148 insertions(+), 3 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index fbda8fab..b3b3643d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -34,7 +34,9 @@ pub use id::{ }; use itertools::Itertools; pub use requirement::Requirement; -pub use solver::{EmptySolvables, Problem, Solver, SolverCache, UnsolvableOrCancelled}; +pub use solver::{ + EmptySolvables, Problem, Solver, SolverCache, SolverConfig, UnsolvableOrCancelled, +}; pub use solver_id::{DenseId, IdMap, IdSet, SolverId, SparseId}; pub use utils::{IndexedSet, Mapping, MappingIter}; @@ -158,6 +160,15 @@ pub trait DependencyProvider: Sized + Interner { fn should_cancel_with_value(&self) -> Option> { None } + + /// Returns the solver configuration for this dependency provider. + /// + /// Override this to customize solver behavior. The returned config is used + /// by [`Solver::new`] unless explicitly overridden with + /// [`Solver::with_config`]. + fn solver_config(&self) -> SolverConfig { + SolverConfig::default() + } } /// A list of candidate solvables for a specific package. This is returned from diff --git a/src/solver/encoding.rs b/src/solver/encoding.rs index 49fc6b75..5f4de715 100644 --- a/src/solver/encoding.rs +++ b/src/solver/encoding.rs @@ -1,6 +1,10 @@ use std::{any::Any, collections::VecDeque}; -use super::{SolverState, clause::WatchedLiterals, conditions}; +use super::{ + SolverConfig, SolverState, + clause::{Clause, WatchedLiterals}, + conditions, +}; use crate::{ Candidates, ConditionId, ConditionalRequirement, DenseIndex, Dependencies, DependencyProvider, Requirement, SolverCache, StringId, VariableId, VersionSetId, @@ -70,6 +74,7 @@ async fn get_requirement_candidates( pub(crate) struct Encoder<'a, 'cache, D: DependencyProvider> { state: &'a mut SolverState, cache: &'cache SolverCache, + config: &'a SolverConfig, level: u32, /// The dependencies of the root solvable. @@ -192,6 +197,7 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { pub fn new( state: &'a mut SolverState, cache: &'cache SolverCache, + config: &'a SolverConfig, root_dependencies: &'cache Dependencies, level: u32, future_queue_mode: FutureQueueMode, @@ -199,6 +205,7 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { Self { state, cache, + config, root_dependencies, pending_futures: FuturesUnordered::new(), conflicting_clauses: Vec::new(), @@ -697,6 +704,12 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { // Pairwise encoding: one (¬parent ∨ ¬candidate) clause per // excluded candidate. for &forbidden_candidate in candidates { + if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { + if self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); + } + continue; + } let forbidden_candidate_var = self.state.variable_map.intern_solvable(forbidden_candidate); let (watched_literals, conflict, kind) = WatchedLiterals::constrains( @@ -729,6 +742,12 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { .insert(constraint, aux_variable); for &forbidden_candidate in candidates { + if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { + if self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); + } + continue; + } let forbidden_candidate_var = self.state.variable_map.intern_solvable(forbidden_candidate); let (watched_literals, kind) = WatchedLiterals::constrains_excluded( @@ -819,6 +838,19 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { variable } + /// Adds a unary constrains clause that forbids a solvable that conflicts + /// with something it also provides (a self-conflict). + fn add_self_conflict_clause(&mut self, variable: VariableId, constraint: VersionSetId) { + let kind = Clause::Constrains(variable, variable, constraint); + let clause_id = self.state.add_clause(None, kind); + + self.state.negative_assertions.push((variable, clause_id)); + + if self.state.decision_tracker.assigned_value(variable) == Some(true) { + self.conflicting_clauses.push(clause_id); + } + } + /// Enqueues retrieving the dependencies for a solvable. /// /// This method requests the dependencies for the given solvable in an diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 3aace71f..17cee5b3 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -176,6 +176,23 @@ impl Clauses { type RequirementCandidateVariables = Vec>; +/// Configuration options for the solver. +#[derive(Debug, Clone)] +pub struct SolverConfig { + /// When `true`, a package that conflicts with something it also provides + /// (i.e. it conflicts with itself) is marked uninstallable. When `false`, + /// self-conflicts are silently ignored. + pub forbid_self_conflicts: bool, +} + +impl Default for SolverConfig { + fn default() -> Self { + Self { + forbid_self_conflicts: true, + } + } +} + /// Drives the SAT solving process. pub struct Solver { /// The runtime to use for async operations. @@ -191,6 +208,9 @@ pub struct Solver { /// runtime remains pending-capable without extending the public runtime contract. future_queue_mode: FutureQueueMode, + /// Solver configuration options. + config: SolverConfig, + /// The activity add factor. This is a value that is added to the activity /// score of each package that is part of a conflict. activity_add: f32, @@ -372,11 +392,13 @@ impl Solver { /// Creates a single threaded block solver, using the provided /// [`DependencyProvider`]. pub fn new(provider: D) -> Self { + let config = provider.solver_config(); Self { cache: SolverCache::new(provider), async_runtime: NowOrNeverRuntime, state: SolverState::default(), future_queue_mode: FutureQueueMode::Immediate, + config, activity_add: 1.0, activity_decay: 0.95, } @@ -454,6 +476,7 @@ impl Solver { cache: self.cache, state: self.state, future_queue_mode: FutureQueueMode::PendingCapable, + config: self.config, activity_decay: self.activity_decay, activity_add: self.activity_add, } @@ -470,6 +493,12 @@ impl Solver { } } + /// Set the solver configuration. + #[must_use] + pub fn with_config(self, config: SolverConfig) -> Self { + Self { config, ..self } + } + /// Solves the given [`Problem`]. /// /// The solver first solves for the root requirements and constraints, and @@ -643,6 +672,7 @@ impl Solver { Encoder::new( &mut self.state, &self.cache, + &self.config, root_deps, level, self.future_queue_mode, @@ -804,6 +834,7 @@ impl Solver { Encoder::new( &mut self.state, &self.cache, + &self.config, root_deps, level, self.future_queue_mode, diff --git a/tests/solver/main.rs b/tests/solver/main.rs index 6d26355b..8c80c6e6 100644 --- a/tests/solver/main.rs +++ b/tests/solver/main.rs @@ -7,7 +7,7 @@ use insta::assert_snapshot; use itertools::Itertools; use resolvo::{ ConditionalRequirement, DependencyProvider, Interner, Problem, SolvableId, Solver, - UnsolvableOrCancelled, VersionSetId, + SolverConfig, UnsolvableOrCancelled, VersionSetId, }; use tracing_test::traced_test; @@ -2131,6 +2131,77 @@ fn test_constrains_multiple_parents() { x=1 "###); } +mod test_self_conflict { + use super::*; + + /// When `forbid_self_conflicts` is false, a package that constrains itself + /// is silently allowed. Some ecosystems (e.g. RPM) explicitly support this. + /// The real-world examples are structured a bit differently however. + #[test] + fn test_self_conflict_allowed() { + let mut provider = BundleBoxProvider::new(); + // a=1 constrains "a" to [2,100) — version 1 is NOT in that range, + // so a=1 appears as a non-matching candidate for its own constraint + // (i.e. a self-conflict). + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).unwrap(); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r" + a=1 + "); + } + + /// When `forbid_self_conflicts` is true (the default), a package that + /// constrains itself is marked uninstallable. + #[test] + fn test_self_conflict_forbidden() { + let mut provider = BundleBoxProvider::new(); + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + + let requirements = provider.requirements(&["a"]); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + match solver.solve(problem) { + Ok(_) => panic!("expected unsat due to self-conflict"), + Err(UnsolvableOrCancelled::Unsolvable(_)) => {} + Err(UnsolvableOrCancelled::Cancelled(_)) => { + panic!("expected unsolvable, not cancelled") + } + } + } + + /// `allow_self_conflicts` works correctly when the self-conflicting + /// package is a transitive dependency discovered in a later solver pass. + #[test] + fn test_self_conflict_allowed_transitive() { + let mut provider = BundleBoxProvider::new(); + // "a" has a self-conflict and is a transitive dep of "app" via "lib". + provider.add_package("a", 1.into(), &[], &["a 2..100"]); + provider.add_package("lib", 1.into(), &["a"], &[]); + provider.add_package("app", 1.into(), &["lib"], &[]); + + let requirements = provider.requirements(&["app"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).unwrap(); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @r" + a=1 + app=1 + lib=1 + "); + } +} // ============================================================================ // Decide-queue wake-up scenarios From 5974efb5d03951fd7a573919ef54f632d5864f8e Mon Sep 17 00:00:00 2001 From: Daniel Alley Date: Mon, 31 Aug 2026 13:37:36 -0400 Subject: [PATCH 2/2] Fix shared-aux constrains encoding for multiple self-conflicting providers The shared aux-variable constrains encoding (used when a version set has >= CONSTRAINS_AUX_ENCODING_THRESHOLD forbidden candidates) allocates one aux variable per version set, meaning "some forbidden provider of this constraint is installed", shared across all constraining parents. The previous self-conflict handling skipped the self term while *building* that shared aux variable. Because the aux var is memoized per version set and built by whichever parent triggers it first, this left the aux definition incomplete for every other parent: the skipped candidate was no longer forbidden for anyone else, and every other self-conflicting provider that reused the aux became spuriously uninstallable. In the real CentOS case (five centos-stream-release versions each providing and conflicting with system-release) this produced a spurious UNSAT whenever the solver had to fall back off the aux-building provider. Build the shared aux variable over all candidates so its meaning is parent-independent, and handle a self-conflicting parent separately: since it is itself part of the aux definition (parent -> aux), the shared (parent -> not aux) clause would make it uninstallable, so encode it pairwise (forbidding the other providers but not itself), or, when forbid_self_conflicts is set, mark it uninstallable directly. Add regression tests covering multiple self-conflicting providers on both the shared-aux and pairwise paths, including the fallback case that previously went unsat. Assisted-By: Claude Opus 4.8 Co-Authored-By: Claude Opus 4.8 --- src/solver/encoding.rs | 98 +++++++++++++++++++++++++++++------------- tests/solver/main.rs | 97 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 166 insertions(+), 29 deletions(-) diff --git a/src/solver/encoding.rs b/src/solver/encoding.rs index 5f4de715..5e05af3f 100644 --- a/src/solver/encoding.rs +++ b/src/solver/encoding.rs @@ -700,36 +700,33 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { let variable = self.state.variable_map.intern_solvable_or_root(solvable_id); + // Whether the constraining solvable is itself one of the forbidden + // (non-matching) candidates: i.e. it conflicts with a capability it + // also provides (a self-conflict). + let self_conflict = candidates + .iter() + .any(|&c| SolvableIdOrRoot::from(c) == solvable_id); + if candidates.len() < CONSTRAINS_AUX_ENCODING_THRESHOLD { // Pairwise encoding: one (¬parent ∨ ¬candidate) clause per - // excluded candidate. - for &forbidden_candidate in candidates { - if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { - if self.config.forbid_self_conflicts { - self.add_self_conflict_clause(variable, constraint); - } - continue; - } - let forbidden_candidate_var = - self.state.variable_map.intern_solvable(forbidden_candidate); - let (watched_literals, conflict, kind) = WatchedLiterals::constrains( - variable, - forbidden_candidate_var, - constraint, - &self.state.decision_tracker, - ); - - let clause_id = self.state.add_clause(watched_literals, kind); - - if conflict { - self.conflicting_clauses.push(clause_id); - } + // excluded candidate, skipping the parent itself. + self.add_constrains_pairwise_for_parent(variable, solvable_id, constraint, candidates); + if self_conflict && self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); } return; } // Shared encoding: the (¬candidate ∨ aux) clauses are emitted once per - // version set, each parent only adds a single (¬parent ∨ ¬aux) clause. + // version set, each non-self parent only adds a single (¬parent ∨ ¬aux) + // clause. + // + // The aux variable means "some forbidden candidate of this constraint + // is installed" and MUST be defined over *all* candidates, so its + // meaning does not depend on which parent happens to build it. Skipping + // a candidate here (e.g. a self-conflicting parent) would both leave + // that candidate un-forbidden for every *other* parent and make every + // other self-conflicting provider that reuses the aux uninstallable. let aux_variable = match self.state.constrains_aux_vars.get(&constraint) { Some(&aux_variable) => aux_variable, None => { @@ -742,12 +739,6 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { .insert(constraint, aux_variable); for &forbidden_candidate in candidates { - if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { - if self.config.forbid_self_conflicts { - self.add_self_conflict_clause(variable, constraint); - } - continue; - } let forbidden_candidate_var = self.state.variable_map.intern_solvable(forbidden_candidate); let (watched_literals, kind) = WatchedLiterals::constrains_excluded( @@ -780,6 +771,25 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { } }; + // A self-conflicting parent is itself part of the aux definition + // (parent -> aux), so the shared (parent -> ¬aux) clause would make it + // uninstallable. Encode such a parent pairwise instead (forbidding the + // other providers but not itself), or, if self-conflicts are forbidden, + // mark it uninstallable directly. + if self_conflict { + if self.config.forbid_self_conflicts { + self.add_self_conflict_clause(variable, constraint); + } else { + self.add_constrains_pairwise_for_parent( + variable, + solvable_id, + constraint, + candidates, + ); + } + return; + } + let (watched_literals, conflict, kind) = WatchedLiterals::constrains_parent( variable, aux_variable, @@ -792,6 +802,36 @@ impl<'a, 'cache, D: DependencyProvider> Encoder<'a, 'cache, D> { } } + /// Emits the pairwise constrains clauses `(¬parent ∨ ¬candidate)` for a + /// single parent, skipping the parent itself (a self-conflict). + fn add_constrains_pairwise_for_parent( + &mut self, + variable: VariableId, + solvable_id: SolvableIdOrRoot, + constraint: VersionSetId, + candidates: &[D::SolvableId], + ) { + for &forbidden_candidate in candidates { + if SolvableIdOrRoot::from(forbidden_candidate) == solvable_id { + continue; + } + let forbidden_candidate_var = + self.state.variable_map.intern_solvable(forbidden_candidate); + let (watched_literals, conflict, kind) = WatchedLiterals::constrains( + variable, + forbidden_candidate_var, + constraint, + &self.state.decision_tracker, + ); + + let clause_id = self.state.add_clause(watched_literals, kind); + + if conflict { + self.conflicting_clauses.push(clause_id); + } + } + } + /// Adds clauses to forbid any other clauses than the locked solvable to be /// installed. fn add_locked_package_clauses( diff --git a/tests/solver/main.rs b/tests/solver/main.rs index 8c80c6e6..21115cf9 100644 --- a/tests/solver/main.rs +++ b/tests/solver/main.rs @@ -2201,6 +2201,103 @@ mod test_self_conflict { lib=1 "); } + + /// Multiple self-conflicting providers of the SAME capability, enough of + /// them (>= CONSTRAINS_AUX_ENCODING_THRESHOLD == 4) to trigger the shared + /// aux-variable constrains encoding. This mirrors the real CentOS case: + /// several versions of centos-stream-release each provide AND conflict + /// with `system-release`. Installing any one of them should succeed (it + /// just excludes the OTHER providers). The `100..200` range matches none of + /// the existing versions, so every version is a non-matching (forbidden) + /// candidate of its own constraint, i.e. a self-conflict. + #[test] + fn test_self_conflict_multiple_providers() { + let mut provider = BundleBoxProvider::new(); + for v in 1..=5u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should be solvable"); + let result = transaction_to_string(solver.provider(), &solved); + // Exactly one version of "a" should be installed. + assert_snapshot!(result, @"a=5"); + } + + /// Same shape as above (shared aux encoding), but the highest version — + /// which builds the shared aux variable — is unsatisfiable, forcing the + /// solver to fall back to a lower self-conflicting provider that reuses the + /// aux var. Regression test: the shared aux definition must cover *all* + /// candidates so the fallback provider is not spuriously uninstallable. + #[test] + fn test_self_conflict_multiple_providers_fallback() { + let mut provider = BundleBoxProvider::new(); + // a=5 pulls in a missing dependency, so it cannot be installed, but the + // solver considers it first (highest version) and builds the aux var. + provider.add_package("a", 5.into(), &["missing"], &["a 100..200"]); + for v in 1..=4u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should fall back to a=4"); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @"a=4"); + } + + /// Control for the above: identical fallback shape but only 3 providers + /// (< threshold), so the pairwise encoding is used instead of the shared + /// aux variable. This path was already correct; guard against regressions. + #[test] + fn test_self_conflict_pairwise_fallback() { + let mut provider = BundleBoxProvider::new(); + provider.add_package("a", 3.into(), &["missing"], &["a 100..200"]); + for v in 1..=2u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let config = SolverConfig { + forbid_self_conflicts: false, + }; + let mut solver = Solver::new(provider).with_config(config); + let problem = Problem::new().requirements(requirements); + let solved = solver.solve(problem).expect("should fall back to a=2"); + let result = transaction_to_string(solver.provider(), &solved); + assert_snapshot!(result, @"a=2"); + } + + /// With `forbid_self_conflicts` (the default), multiple self-conflicting + /// providers on the shared-aux path are ALL uninstallable, so the whole + /// solve is unsat. + #[test] + fn test_self_conflict_multiple_providers_forbidden() { + let mut provider = BundleBoxProvider::new(); + for v in 1..=5u32 { + provider.add_package("a", v.into(), &[], &["a 100..200"]); + } + + let requirements = provider.requirements(&["a"]); + let mut solver = Solver::new(provider); + let problem = Problem::new().requirements(requirements); + match solver.solve(problem) { + Ok(_) => panic!("expected unsat: all providers self-conflict"), + Err(UnsolvableOrCancelled::Unsolvable(_)) => {} + Err(UnsolvableOrCancelled::Cancelled(_)) => { + panic!("expected unsolvable, not cancelled") + } + } + } } // ============================================================================