pubsat

SAT-based dependency resolution for semver-shaped constraint problems — the kind that show up in npm, Cargo, Composer, pip, and every other package ecosystem with caret / tilde / hyphen / range syntax.

pubsat is backend-agnostic (defaults to Varisat) and ecosystem-agnostic: callers implement PackageRegistry for their package source, hand the resolver a starting set of dependencies, and get back a concrete (name, version) selection or a structured conflict report.

When to reach for this

• You're writing a dependency resolver (private artifact registry, build tool, alternative package manager) and want to skip the semver-range parsing, SAT encoding, and version-preference logic.
• You need an npm-flavour range parser (caret, tilde, hyphen, x-ranges, dist tags) that's stricter than semver but more permissive than node-semver parsers that reject the punctuation drift real registries contain.
• You want a resolver whose preference policy (newest-wins, conservative, custom) is expressible as SAT assumptions rather than baked into the search strategy.

End-to-end example

use std::sync::Arc;

use pubsat::builder::DependencyGraphBuilder;
use pubsat::registry::{MockRegistry, VersionMetadata};
use pubsat::resolver::DependencyResolver;
use pubsat::version::VersionSet;
use semver::Version;

# #[tokio::main(flavor = "current_thread")]
# async fn main() {
let vs = |s: &str| -> VersionSet { s.parse().unwrap() };

// Stand up a registry. Real implementations wrap an HTTP client
// or an on-disk index; `MockRegistry` is the in-process version
// used in tests and examples.
let registry = Arc::new(
    MockRegistry::new()
        .with_versions("chalk", &["4.1.0", "5.0.0"])
        .with_versions("ansi-styles", &["4.3.0", "6.2.1"])
        .with_dependency("chalk", "4.1.0", "ansi-styles", vs("^4.0.0"))
        .with_dependency("chalk", "5.0.0", "ansi-styles", vs("^6.0.0")),
);

// Describe what we want — a synthetic root that depends on chalk ^5.
let root = VersionMetadata::new("my-app", Version::new(1, 0, 0))
    .with_dependency("chalk", vs("^5.0.0"));

// Walk the registry into a dependency graph.
let graph = DependencyGraphBuilder::new(registry.clone())
    .build(root)
    .await
    .unwrap();

// Resolve to a concrete selection.
let resolution = DependencyResolver::new(registry)
    .resolve(graph)
    .await
    .unwrap();

for pkg in &resolution.packages {
    println!("{} {}", pkg.name, pkg.version);
}
// chalk 5.0.0
// ansi-styles 6.2.1
# }

A runnable version lives in examples/resolve_mock.rs. Run it with cargo run --example resolve_mock.

What's in the crate

94 unit tests (including 17 proptest-driven property tests covering VersionSet algebra, the encoder's CNF semantics, and resolver output invariants — ~2,300 case executions per cargo test invocation) plus 3 doctests; fmt + clippy (-D warnings) + cargo-doc (RUSTDOCFLAGS=-Dwarnings) all clean in CI.

Algorithm

pubsat encodes each (package, version) pair as a SAT variable, adds clauses for dependency edges and version-set membership, and asks a SAT solver for a model. Version-preference ("newest wins") is expressed as a set of assumptions on the solver rather than as part of the algorithm's branching strategy. On UNSAT with all preferences, the resolver drops preferences one at a time in deterministic order — a greedy fallback that keeps a maximal compatible subset rather than collapsing to "any satisfying version everywhere".

Hot paths the implementation cares about:

• Single-flighted registry cache. Concurrent callers for the same package share one upstream round-trip (OnceCell per key, intercepted at all three reads).
• Encoder primes its local version map from the resolver's cache before encoding, so it filters in-process rather than asking the registry once per (package, version, dep_edge) tuple. Without this, encoding express-sized graphs makes ~7000 redundant fetches.
• Sequential at-most-one cardinality encoding. Pairwise is O(n²) clauses — a package with 20 candidates would generate 190 binary clauses. The sequential/ladder encoding emits O(n) with auxiliary variables.
• Deterministic iteration. HashMaps are sorted before SAT variable allocation so resolutions don't flap between runs (Varisat's branching is order-sensitive).

See docs/design/architecture.md for the full design discussion (why SAT and not PubGrub, the trade-offs accepted, the comparison with prior art, and the "intentionally out of scope" boundary).

Stability

0.1.x: public API may evolve between minor versions until 1.0. Breaking changes will be called out in CHANGELOG.md with migration notes. The CNF representation (literal/clause shapes) is the most stable; the higher-level PackageRegistry trait and Constraint vocabulary are the layers most likely to grow.

Features

• varisat-solver (default) — pure-Rust Varisat CDCL backend
• cadical-solver — placeholder; no CaDiCaL Rust binding currently exposes the surface this crate needs. The feature flag and trait abstraction are in place so adding it later is a small change.

License

MIT — see LICENSE.