aboutsummaryrefslogtreecommitdiffhomepage
path: root/crates/mozart-sat-resolver/src/solver.rs
AgeCommit message (Collapse)Author
2026-02-24fix(solver): iterate live watch chain to prevent infinite loop in propagationnsfisis
The watch graph's propagateLiteral used a cloned chain for iteration while checking the live chain for bounds. After move_watch removed a node, the stale clone kept re-reading the same node index, causing an infinite loop on large dependency sets (e.g. laravel/laravel). Now re-fetch the live chain each iteration, matching Composer's SplDoublyLinkedList semantics where remove() advances the iterator. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-22feat(resolver): replace pubgrub with Composer-ported SAT solvernsfisis
Add mozart-sat-resolver crate implementing a CDCL SAT-based dependency resolver ported from Composer's DependencyResolver. This replaces the pubgrub library to ensure identical resolution behavior with Composer. The new crate includes: pool (package storage with integer IDs), rule/rule_set/rule_set_generator (constraint encoding), decisions (assignment tracking), rule_watch_graph (2-watched literal BCP), solver (CDCL loop with conflict analysis and clause learning), policy (version preference), problem (Composer-style error messages), and transaction (install/update/uninstall operation computation). The registry resolver is rewritten to use PoolBuilder → RuleSetGenerator → Solver pipeline instead of pubgrub's DependencyProvider trait. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>