# pubsat
[](https://github.com/cygnus-io/pubsat/actions/workflows/ci.yml)
[](https://codecov.io/gh/cygnus-io/pubsat)
[](https://opensource.org/licenses/MIT)
[](https://www.rust-lang.org)
**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](https://crates.io/crates/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
```rust,no_run
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() {
// 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`](examples/resolve_mock.rs).
Run it with `cargo run --example resolve_mock`.
## What's in the crate
| `version` | Node-semver-compatible range parser. Caret, tilde, hyphen, partial versions, `>=`/`<=`/`>`/`<` with optional whitespace, x-ranges, unions, dist tags. Plus `VersionSet` operations (intersection, union, satisfaction). |
| `constraint` | Ecosystem-independent `Constraint` vocabulary: `Dependency`, `Conflict`, `AtMostOne`, `AtLeastOne`, `Exactly`, `Exclude`, `Implies`, `OptionalDependency`, `ConditionalDependency`. |
| `registry` | `PackageRegistry` trait, single-flighted `CachedRegistry` wrapper, and in-process `MockRegistry` for tests and examples. |
| `graph` | `DependencyGraph` (petgraph-backed), `DependencyNode`, `DependencyEdge`, cycle detection, topological sort, DOT export. |
| `encoding` | `ConstraintEncoder` — lowers `Constraint`s to CNF clauses with sequential at-most-one encoding for cardinality and a primable version cache for the hot path. |
| `builder` | `DependencyGraphBuilder` — walks a registry concurrently (configurable in-flight cap) to build a graph from a root `VersionMetadata`. |
| `resolver` | `DependencyResolver` — orchestrates `graph → encoder → SAT problem → solver → resolution` with greedy "prefer newest" SAT assumptions and per-package fallback on UNSAT. |
| `sat` | Backend-agnostic SAT types (`SatProblem`, `Clause`, `Literal`, `SatModel`, `SatSolution`) and the `SatSolver` trait. A `VarisatSolver` impl ships behind the default `varisat-solver` feature. |
| `error` | `ResolutionError`, `SatError`, `EncodingResult`, `ConflictDetail`, `ConflictReason`. |
94 unit tests (including 17 [`proptest`][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.
[proptest]: https://crates.io/crates/proptest
## 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.** `HashMap`s are sorted before SAT
variable allocation so resolutions don't flap between runs
(Varisat's branching is order-sensitive).
See [`docs/design/architecture.md`](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](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.
[Varisat]: https://crates.io/crates/varisat
[`PackageRegistry`]: https://docs.rs/pubsat/latest/pubsat/registry/trait.PackageRegistry.html
## License
MIT — see [LICENSE](LICENSE).