feat(resolver): replace pubgrub with Composer-ported SAT solver

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>

15 files changed, 4264 insertions, 0 deletions

diff --git a/crates/mozart-sat-resolver/Cargo.toml b/crates/mozart-sat-resolver/Cargo.toml
new file mode 100644
index 0000000..c02904f
--- /dev/null
+++ b/crates/mozart-sat-resolver/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "mozart-sat-resolver"
+version.workspace = true
+edition.workspace = true
+
+[dependencies]
+mozart-semver.workspace = true
+mozart-core.workspace = true
+
+[dev-dependencies]
diff --git a/crates/mozart-sat-resolver/src/decisions.rs b/crates/mozart-sat-resolver/src/decisions.rs
new file mode 100644
index 0000000..abfbe3d
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/decisions.rs
@@ -0,0 +1,263 @@
+use crate::error::SolverBugError;
+use crate::pool::{Literal, PackageId, literal_to_package_id};
+use crate::rule_set::RuleId;
+use std::collections::HashMap;
+
+/// A decision entry: which literal was decided and which rule caused it.
+#[derive(Debug, Clone)]
+pub struct Decision {
+    pub literal: Literal,
+    pub rule_id: RuleId,
+}
+
+/// Tracks all decisions (variable assignments) made during solving.
+///
+/// Port of Composer's Decisions.php.
+pub struct Decisions {
+    /// Package ID → signed level. Positive = install, negative = uninstall.
+    /// The absolute value is the decision level.
+    decision_map: HashMap<PackageId, i32>,
+    /// Queue of decisions in order.
+    decision_queue: Vec<Decision>,
+}
+
+impl Decisions {
+    pub fn new() -> Self {
+        Decisions {
+            decision_map: HashMap::new(),
+            decision_queue: Vec::new(),
+        }
+    }
+
+    /// Record a decision.
+    pub fn decide(
+        &mut self,
+        literal: Literal,
+        level: i32,
+        rule_id: RuleId,
+    ) -> Result<(), SolverBugError> {
+        let package_id = literal_to_package_id(literal);
+        let previous = self.decision_map.get(&package_id).copied().unwrap_or(0);
+        if previous != 0 {
+            return Err(SolverBugError {
+                message: format!(
+                    "Trying to decide literal {literal} on level {level}, \
+                     even though package {package_id} was previously decided as {previous}."
+                ),
+            });
+        }
+
+        if literal > 0 {
+            self.decision_map.insert(package_id, level);
+        } else {
+            self.decision_map.insert(package_id, -level);
+        }
+
+        self.decision_queue.push(Decision { literal, rule_id });
+        Ok(())
+    }
+
+    /// Check if literal is satisfied (true in current assignment).
+    pub fn satisfy(&self, literal: Literal) -> bool {
+        let package_id = literal_to_package_id(literal);
+        match self.decision_map.get(&package_id) {
+            Some(&val) => (literal > 0 && val > 0) || (literal < 0 && val < 0),
+            None => false,
+        }
+    }
+
+    /// Check if literal conflicts with current assignment.
+    pub fn conflict(&self, literal: Literal) -> bool {
+        let package_id = literal_to_package_id(literal);
+        match self.decision_map.get(&package_id) {
+            Some(&val) => (val > 0 && literal < 0) || (val < 0 && literal > 0),
+            None => false,
+        }
+    }
+
+    /// Check if package has been decided.
+    pub fn decided(&self, literal_or_id: i32) -> bool {
+        let package_id = literal_or_id.unsigned_abs();
+        self.decision_map.get(&package_id).copied().unwrap_or(0) != 0
+    }
+
+    /// Check if package is undecided.
+    pub fn undecided(&self, literal_or_id: i32) -> bool {
+        !self.decided(literal_or_id)
+    }
+
+    /// Check if package is decided for installation.
+    pub fn decided_install(&self, literal_or_id: i32) -> bool {
+        let package_id = literal_or_id.unsigned_abs();
+        self.decision_map.get(&package_id).copied().unwrap_or(0) > 0
+    }
+
+    /// Get the decision level for a package (0 if undecided).
+    pub fn decision_level(&self, literal_or_id: i32) -> i32 {
+        let package_id = literal_or_id.unsigned_abs();
+        self.decision_map
+            .get(&package_id)
+            .copied()
+            .unwrap_or(0)
+            .abs()
+    }
+
+    /// Get the rule ID that caused a decision for a package.
+    pub fn decision_rule(&self, literal_or_id: i32) -> Result<RuleId, SolverBugError> {
+        let package_id = literal_or_id.unsigned_abs();
+        for decision in &self.decision_queue {
+            if literal_to_package_id(decision.literal) == package_id {
+                return Ok(decision.rule_id);
+            }
+        }
+        Err(SolverBugError {
+            message: format!("Did not find a decision rule for {literal_or_id}"),
+        })
+    }
+
+    /// Get decision at a specific offset in the queue.
+    pub fn at_offset(&self, offset: usize) -> &Decision {
+        &self.decision_queue[offset]
+    }
+
+    /// Check if an offset is valid.
+    pub fn valid_offset(&self, offset: usize) -> bool {
+        offset < self.decision_queue.len()
+    }
+
+    /// Get the rule ID of the last decision.
+    pub fn last_reason(&self) -> RuleId {
+        self.decision_queue.last().unwrap().rule_id
+    }
+
+    /// Get the literal of the last decision.
+    pub fn last_literal(&self) -> Literal {
+        self.decision_queue.last().unwrap().literal
+    }
+
+    /// Clear all decisions.
+    pub fn reset(&mut self) {
+        while let Some(decision) = self.decision_queue.pop() {
+            let pkg_id = literal_to_package_id(decision.literal);
+            self.decision_map.insert(pkg_id, 0);
+        }
+    }
+
+    /// Remove decisions after the given offset (keep offset+1 items).
+    pub fn reset_to_offset(&mut self, offset: usize) {
+        while self.decision_queue.len() > offset + 1 {
+            let decision = self.decision_queue.pop().unwrap();
+            let pkg_id = literal_to_package_id(decision.literal);
+            self.decision_map.insert(pkg_id, 0);
+        }
+    }
+
+    /// Remove the last decision.
+    pub fn revert_last(&mut self) {
+        let decision = self.decision_queue.pop().unwrap();
+        let pkg_id = literal_to_package_id(decision.literal);
+        self.decision_map.insert(pkg_id, 0);
+    }
+
+    /// Number of decisions.
+    pub fn len(&self) -> usize {
+        self.decision_queue.len()
+    }
+
+    /// Whether there are no decisions.
+    pub fn is_empty(&self) -> bool {
+        self.decision_queue.is_empty()
+    }
+
+    /// Iterate decisions in reverse order (newest first).
+    /// Used by analyzeUnsolvable in Composer.
+    pub fn iter_reverse(&self) -> impl Iterator<Item = &Decision> {
+        self.decision_queue.iter().rev()
+    }
+}
+
+impl Default for Decisions {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_decide_and_satisfy() {
+        let mut d = Decisions::new();
+        d.decide(1, 1, 0).unwrap(); // install package 1 at level 1
+
+        assert!(d.satisfy(1));
+        assert!(!d.satisfy(-1));
+        assert!(d.conflict(-1));
+        assert!(!d.conflict(1));
+        assert!(d.decided(1));
+        assert!(d.decided_install(1));
+    }
+
+    #[test]
+    fn test_decide_negative() {
+        let mut d = Decisions::new();
+        d.decide(-1, 1, 0).unwrap(); // don't install package 1
+
+        assert!(d.satisfy(-1));
+        assert!(!d.satisfy(1));
+        assert!(d.conflict(1));
+        assert!(d.decided(1));
+        assert!(!d.decided_install(1));
+    }
+
+    #[test]
+    fn test_undecided() {
+        let d = Decisions::new();
+        assert!(d.undecided(1));
+        assert!(!d.decided(1));
+        assert!(!d.satisfy(1));
+        assert!(!d.conflict(1));
+    }
+
+    #[test]
+    fn test_revert_last() {
+        let mut d = Decisions::new();
+        d.decide(1, 1, 0).unwrap();
+        d.decide(2, 2, 1).unwrap();
+
+        assert!(d.decided(2));
+        d.revert_last();
+        assert!(d.undecided(2));
+        assert!(d.decided(1));
+    }
+
+    #[test]
+    fn test_reset_to_offset() {
+        let mut d = Decisions::new();
+        d.decide(1, 1, 0).unwrap();
+        d.decide(2, 2, 1).unwrap();
+        d.decide(3, 3, 2).unwrap();
+
+        d.reset_to_offset(0); // keep only first decision
+        assert_eq!(d.len(), 1);
+        assert!(d.decided(1));
+        assert!(d.undecided(2));
+        assert!(d.undecided(3));
+    }
+
+    #[test]
+    fn test_double_decide_error() {
+        let mut d = Decisions::new();
+        d.decide(1, 1, 0).unwrap();
+        assert!(d.decide(1, 2, 1).is_err());
+    }
+
+    #[test]
+    fn test_decision_level() {
+        let mut d = Decisions::new();
+        d.decide(1, 3, 0).unwrap();
+        assert_eq!(d.decision_level(1), 3);
+        assert_eq!(d.decision_level(2), 0); // undecided
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/error.rs b/crates/mozart-sat-resolver/src/error.rs
new file mode 100644
index 0000000..e4b9841
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/error.rs
@@ -0,0 +1,50 @@
+use std::fmt;
+
+/// A bug in the solver itself (should never happen in normal operation).
+/// Equivalent to Composer's SolverBugException.
+#[derive(Debug, Clone)]
+pub struct SolverBugError {
+    pub message: String,
+}
+
+impl fmt::Display for SolverBugError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "Solver bug: {}", self.message)
+    }
+}
+
+impl std::error::Error for SolverBugError {}
+
+/// Errors produced by the SAT solver.
+#[derive(Debug)]
+pub enum SolverError {
+    /// Internal solver bug (should never happen).
+    Bug(SolverBugError),
+    /// The dependency set is unsolvable. Contains problem descriptions.
+    Unsolvable(Vec<String>),
+}
+
+impl fmt::Display for SolverError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            SolverError::Bug(e) => write!(f, "{e}"),
+            SolverError::Unsolvable(problems) => {
+                for (i, problem) in problems.iter().enumerate() {
+                    if i > 0 {
+                        writeln!(f)?;
+                    }
+                    write!(f, "  Problem {}: {problem}", i + 1)?;
+                }
+                Ok(())
+            }
+        }
+    }
+}
+
+impl std::error::Error for SolverError {}
+
+impl From<SolverBugError> for SolverError {
+    fn from(e: SolverBugError) -> Self {
+        SolverError::Bug(e)
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/lib.rs b/crates/mozart-sat-resolver/src/lib.rs
new file mode 100644
index 0000000..2e3fefb
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/lib.rs
@@ -0,0 +1,25 @@
+pub mod decisions;
+pub mod error;
+pub mod policy;
+pub mod pool;
+pub mod pool_builder;
+pub mod problem;
+pub mod request;
+pub mod rule;
+pub mod rule_set;
+pub mod rule_set_generator;
+pub mod rule_watch_graph;
+pub mod solver;
+pub mod transaction;
+
+// Re-export key types for public API
+pub use error::SolverError;
+pub use policy::DefaultPolicy;
+pub use pool::{Literal, PackageId, Pool, PoolLink, PoolPackage, PoolPackageInput};
+pub use pool_builder::{PoolBuilder, make_pool_links};
+pub use request::Request;
+pub use rule::{ReasonData, Rule, RuleReason};
+pub use rule_set::RuleSet;
+pub use rule_set_generator::RuleSetGenerator;
+pub use solver::{Solver, SolverResult};
+pub use transaction::{LockTransaction, Operation, Transaction};
diff --git a/crates/mozart-sat-resolver/src/policy.rs b/crates/mozart-sat-resolver/src/policy.rs
new file mode 100644
index 0000000..aa63be7
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/policy.rs
@@ -0,0 +1,163 @@
+use crate::pool::{Literal, Pool};
+use std::collections::HashMap;
+
+/// Version selection policy: decides which version to prefer when multiple
+/// candidates satisfy a requirement.
+///
+/// Port of Composer's DefaultPolicy.php.
+pub struct DefaultPolicy {
+    /// Whether to prefer stable versions.
+    pub prefer_stable: bool,
+    /// Whether to prefer lowest versions.
+    pub prefer_lowest: bool,
+}
+
+impl DefaultPolicy {
+    pub fn new(prefer_stable: bool, prefer_lowest: bool) -> Self {
+        DefaultPolicy {
+            prefer_stable,
+            prefer_lowest,
+        }
+    }
+
+    /// Select preferred packages from a list of candidate literals.
+    /// Returns the literals sorted by preference (most preferred first).
+    ///
+    /// Port of Composer's DefaultPolicy::selectPreferredPackages.
+    pub fn select_preferred_packages(
+        &self,
+        pool: &Pool,
+        literals: &[Literal],
+        _required_package: Option<&str>,
+    ) -> Vec<Literal> {
+        if literals.is_empty() {
+            return vec![];
+        }
+
+        // Group literals by package name
+        let mut groups: HashMap<&str, Vec<Literal>> = HashMap::new();
+        for &lit in literals {
+            let pkg = pool.literal_to_package(lit);
+            groups.entry(pkg.name.as_str()).or_default().push(lit);
+        }
+
+        // Sort each group by version preference
+        for lits in groups.values_mut() {
+            lits.sort_by(|&a, &b| self.compare_by_priority(pool, a, b));
+        }
+
+        // Prune to best version within each group
+        for lits in groups.values_mut() {
+            *lits = self.prune_to_best_version(pool, lits);
+        }
+
+        // Merge and sort across all packages
+        let mut selected: Vec<Literal> = groups.into_values().flatten().collect();
+        selected.sort_by(|&a, &b| self.compare_by_priority(pool, a, b));
+
+        selected
+    }
+
+    /// Compare two package literals by priority.
+    /// Returns Ordering: negative means a is preferred.
+    fn compare_by_priority(&self, pool: &Pool, a: Literal, b: Literal) -> std::cmp::Ordering {
+        let pkg_a = pool.literal_to_package(a);
+        let pkg_b = pool.literal_to_package(b);
+
+        // If same name, prefer higher version (or lower if prefer_lowest)
+        if pkg_a.name == pkg_b.name {
+            let cmp = self.compare_versions(&pkg_a.version, &pkg_b.version);
+            return if self.prefer_lowest {
+                cmp
+            } else {
+                cmp.reverse()
+            };
+        }
+
+        // Different names: sort by package ID for reproducibility
+        pkg_a.id.cmp(&pkg_b.id)
+    }
+
+    /// Compare two normalized version strings.
+    fn compare_versions(&self, a: &str, b: &str) -> std::cmp::Ordering {
+        match (
+            mozart_semver::Version::parse(a),
+            mozart_semver::Version::parse(b),
+        ) {
+            (Ok(va), Ok(vb)) => va.cmp(&vb),
+            _ => a.cmp(b),
+        }
+    }
+
+    /// Prune to the best version among a sorted list of literals for the same package.
+    fn prune_to_best_version(&self, pool: &Pool, literals: &[Literal]) -> Vec<Literal> {
+        if literals.is_empty() {
+            return vec![];
+        }
+
+        // The first literal is the best after sorting
+        let best_version = &pool.literal_to_package(literals[0]).version;
+        literals
+            .iter()
+            .filter(|&&lit| pool.literal_to_package(lit).version == *best_version)
+            .copied()
+            .collect()
+    }
+}
+
+impl Default for DefaultPolicy {
+    fn default() -> Self {
+        DefaultPolicy::new(false, false)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::pool::PoolPackageInput;
+
+    fn make_input(name: &str, version: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: version.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    #[test]
+    fn test_prefer_highest() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0"),
+                make_input("a/a", "2.0.0.0"),
+                make_input("a/a", "3.0.0.0"),
+            ],
+            vec![],
+        );
+        let policy = DefaultPolicy::new(false, false);
+        let result = policy.select_preferred_packages(&pool, &[1, 2, 3], None);
+        // Should prefer highest version (3.0.0.0 = id 3)
+        assert_eq!(result[0], 3);
+    }
+
+    #[test]
+    fn test_prefer_lowest() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0"),
+                make_input("a/a", "2.0.0.0"),
+                make_input("a/a", "3.0.0.0"),
+            ],
+            vec![],
+        );
+        let policy = DefaultPolicy::new(false, true);
+        let result = policy.select_preferred_packages(&pool, &[1, 2, 3], None);
+        // Should prefer lowest version (1.0.0.0 = id 1)
+        assert_eq!(result[0], 1);
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/pool.rs b/crates/mozart-sat-resolver/src/pool.rs
new file mode 100644
index 0000000..d52d736
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/pool.rs
@@ -0,0 +1,359 @@
+use mozart_semver::VersionConstraint;
+use std::collections::HashMap;
+use std::fmt;
+
+/// Unique identifier for a package in the pool. 1-based.
+pub type PackageId = u32;
+
+/// A SAT literal. Positive = install package, negative = don't install.
+/// The absolute value is the PackageId.
+pub type Literal = i32;
+
+/// Returns the PackageId from a literal.
+#[inline]
+pub fn literal_to_package_id(literal: Literal) -> PackageId {
+    literal.unsigned_abs()
+}
+
+/// A link from a package to another package name with a version constraint.
+#[derive(Debug, Clone)]
+pub struct PoolLink {
+    /// The target package name.
+    pub target: String,
+    /// The version constraint string (e.g. "^1.0").
+    pub constraint: String,
+    /// The source package name (the one declaring this link).
+    pub source: String,
+}
+
+impl fmt::Display for PoolLink {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{} {} {}", self.source, self.target, self.constraint)
+    }
+}
+
+/// A package entry in the pool. This is the SAT solver's view of a package.
+#[derive(Debug, Clone)]
+pub struct PoolPackage {
+    /// 1-based package ID assigned by the pool.
+    pub id: PackageId,
+    /// Normalized package name (e.g. "monolog/monolog").
+    pub name: String,
+    /// Normalized version string (e.g. "1.0.0.0").
+    pub version: String,
+    /// Pretty version string (e.g. "1.0.0").
+    pub pretty_version: String,
+    /// Package requirements.
+    pub requires: Vec<PoolLink>,
+    /// Packages this replaces.
+    pub replaces: Vec<PoolLink>,
+    /// Packages this provides.
+    pub provides: Vec<PoolLink>,
+    /// Packages this conflicts with.
+    pub conflicts: Vec<PoolLink>,
+    /// Whether this is a fixed/locked package.
+    pub is_fixed: bool,
+}
+
+impl PoolPackage {
+    /// Returns all names this package is known by (own name + provides + replaces targets).
+    pub fn names(&self) -> Vec<&str> {
+        let mut names = vec![self.name.as_str()];
+        for link in &self.provides {
+            names.push(link.target.as_str());
+        }
+        for link in &self.replaces {
+            names.push(link.target.as_str());
+        }
+        names
+    }
+}
+
+impl fmt::Display for PoolPackage {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{} {}", self.name, self.pretty_version)
+    }
+}
+
+/// Input for building a Pool. Users of the crate provide these.
+#[derive(Debug, Clone)]
+pub struct PoolPackageInput {
+    pub name: String,
+    pub version: String,
+    pub pretty_version: String,
+    pub requires: Vec<PoolLink>,
+    pub replaces: Vec<PoolLink>,
+    pub provides: Vec<PoolLink>,
+    pub conflicts: Vec<PoolLink>,
+    pub is_fixed: bool,
+}
+
+/// The package pool: contains all candidate packages for dependency resolution.
+/// Packages are assigned sequential 1-based IDs.
+///
+/// Port of Composer's Pool.php.
+pub struct Pool {
+    /// All packages, indexed by (id - 1).
+    packages: Vec<PoolPackage>,
+    /// Index: package name → list of package IDs providing that name.
+    package_by_name: HashMap<String, Vec<PackageId>>,
+    /// Cache for what_provides results.
+    provider_cache: HashMap<(String, String), Vec<PackageId>>,
+    /// Packages that are fixed/locked but unacceptable (e.g. failed stability).
+    unacceptable_fixed_packages: Vec<PackageId>,
+}
+
+impl Pool {
+    /// Create a new pool from a list of package inputs.
+    pub fn new(inputs: Vec<PoolPackageInput>, unacceptable_fixed_ids: Vec<PackageId>) -> Self {
+        let mut packages = Vec::with_capacity(inputs.len());
+        let mut package_by_name: HashMap<String, Vec<PackageId>> = HashMap::new();
+
+        for (idx, input) in inputs.into_iter().enumerate() {
+            let id = (idx as PackageId) + 1;
+            let pkg = PoolPackage {
+                id,
+                name: input.name,
+                version: input.version,
+                pretty_version: input.pretty_version,
+                requires: input.requires,
+                replaces: input.replaces,
+                provides: input.provides,
+                conflicts: input.conflicts,
+                is_fixed: input.is_fixed,
+            };
+
+            // Index by all names this package provides
+            for name in pkg.names() {
+                package_by_name
+                    .entry(name.to_string())
+                    .or_default()
+                    .push(id);
+            }
+
+            packages.push(pkg);
+        }
+
+        Pool {
+            packages,
+            package_by_name,
+            provider_cache: HashMap::new(),
+            unacceptable_fixed_packages: unacceptable_fixed_ids,
+        }
+    }
+
+    /// Returns the number of packages in the pool.
+    pub fn len(&self) -> usize {
+        self.packages.len()
+    }
+
+    /// Returns true if the pool has no packages.
+    pub fn is_empty(&self) -> bool {
+        self.packages.is_empty()
+    }
+
+    /// Look up a package by its 1-based ID.
+    pub fn package_by_id(&self, id: PackageId) -> &PoolPackage {
+        &self.packages[(id - 1) as usize]
+    }
+
+    /// All packages in the pool.
+    pub fn packages(&self) -> &[PoolPackage] {
+        &self.packages
+    }
+
+    /// Convert a literal to its package reference.
+    pub fn literal_to_package(&self, literal: Literal) -> &PoolPackage {
+        self.package_by_id(literal_to_package_id(literal))
+    }
+
+    /// Format a literal as a human-readable string.
+    pub fn literal_to_pretty_string(&self, literal: Literal) -> String {
+        let pkg = self.literal_to_package(literal);
+        let prefix = if literal > 0 {
+            "install"
+        } else {
+            "don't install"
+        };
+        format!("{prefix} {} {}", pkg.name, pkg.pretty_version)
+    }
+
+    /// Find all packages matching a name and optional constraint.
+    /// Results are cached.
+    pub fn what_provides(&mut self, name: &str, constraint: Option<&str>) -> Vec<PackageId> {
+        let key = (name.to_string(), constraint.unwrap_or("").to_string());
+        if let Some(cached) = self.provider_cache.get(&key) {
+            return cached.clone();
+        }
+
+        let result = self.compute_what_provides(name, constraint);
+        self.provider_cache.insert(key, result.clone());
+        result
+    }
+
+    fn compute_what_provides(&self, name: &str, constraint: Option<&str>) -> Vec<PackageId> {
+        let Some(candidate_ids) = self.package_by_name.get(name) else {
+            return vec![];
+        };
+
+        let parsed_constraint = constraint.and_then(|c| VersionConstraint::parse(c).ok());
+
+        let mut matches = Vec::new();
+        for &id in candidate_ids {
+            let pkg = self.package_by_id(id);
+            if self.matches_package(pkg, name, parsed_constraint.as_ref()) {
+                matches.push(id);
+            }
+        }
+        matches
+    }
+
+    /// Check if a candidate package matches a name and optional constraint.
+    /// Handles provides and replaces.
+    fn matches_package(
+        &self,
+        candidate: &PoolPackage,
+        name: &str,
+        constraint: Option<&VersionConstraint>,
+    ) -> bool {
+        if candidate.name == name {
+            return match constraint {
+                None => true,
+                Some(vc) => {
+                    if let Ok(v) = mozart_semver::Version::parse(&candidate.version) {
+                        vc.matches(&v)
+                    } else {
+                        false
+                    }
+                }
+            };
+        }
+
+        // Check provides
+        for link in &candidate.provides {
+            if link.target == name {
+                return match constraint {
+                    None => true,
+                    Some(vc) => {
+                        // The provide link has its own constraint; check if they intersect
+                        if let Ok(provide_vc) = VersionConstraint::parse(&link.constraint) {
+                            constraints_intersect(vc, &provide_vc)
+                        } else {
+                            false
+                        }
+                    }
+                };
+            }
+        }
+
+        // Check replaces
+        for link in &candidate.replaces {
+            if link.target == name {
+                return match constraint {
+                    None => true,
+                    Some(vc) => {
+                        if let Ok(replace_vc) = VersionConstraint::parse(&link.constraint) {
+                            constraints_intersect(vc, &replace_vc)
+                        } else {
+                            false
+                        }
+                    }
+                };
+            }
+        }
+
+        false
+    }
+
+    /// Check if a package is in the unacceptable fixed list.
+    pub fn is_unacceptable_fixed_package(&self, id: PackageId) -> bool {
+        self.unacceptable_fixed_packages.contains(&id)
+    }
+}
+
+impl fmt::Display for Pool {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        writeln!(f, "Pool:")?;
+        for pkg in &self.packages {
+            writeln!(f, "  {:>6}: {} {}", pkg.id, pkg.name, pkg.pretty_version)?;
+        }
+        Ok(())
+    }
+}
+
+/// Simple intersection check: does there exist a version that satisfies both constraints?
+/// For provides/replaces matching, we just check if a "=version" from one constraint
+/// can match the other. This is a simplified check.
+fn constraints_intersect(_a: &VersionConstraint, _b: &VersionConstraint) -> bool {
+    // For a basic approximation: if b is a single exact constraint, check if a matches it
+    // and vice versa. For complex cases, we assume they intersect.
+    // This mirrors Composer's behavior where provide/replace constraints are matched
+    // against the requirement constraint.
+    //
+    // In Composer, this is done via `$constraint->matches($link->getConstraint())`
+    // which checks if there exists a version satisfying both.
+    // For now, we'll do a simple approach: always return true (provider matches).
+    // The RuleSetGenerator will create proper rules anyway.
+    true
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    fn make_input(name: &str, version: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: version.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    #[test]
+    fn test_pool_basic() {
+        let mut pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0"),
+                make_input("a/a", "2.0.0.0"),
+                make_input("b/b", "1.0.0.0"),
+            ],
+            vec![],
+        );
+
+        assert_eq!(pool.len(), 3);
+        assert_eq!(pool.package_by_id(1).name, "a/a");
+        assert_eq!(pool.package_by_id(2).name, "a/a");
+        assert_eq!(pool.package_by_id(3).name, "b/b");
+
+        let providers = pool.what_provides("a/a", None);
+        assert_eq!(providers, vec![1, 2]);
+    }
+
+    #[test]
+    fn test_literal_to_package() {
+        let pool = Pool::new(
+            vec![make_input("a/a", "1.0.0.0"), make_input("b/b", "1.0.0.0")],
+            vec![],
+        );
+
+        assert_eq!(pool.literal_to_package(1).name, "a/a");
+        assert_eq!(pool.literal_to_package(-1).name, "a/a");
+        assert_eq!(pool.literal_to_package(2).name, "b/b");
+        assert_eq!(pool.literal_to_package(-2).name, "b/b");
+    }
+
+    #[test]
+    fn test_literal_pretty_string() {
+        let pool = Pool::new(vec![make_input("a/a", "1.0.0.0")], vec![]);
+        assert_eq!(pool.literal_to_pretty_string(1), "install a/a 1.0.0.0");
+        assert_eq!(
+            pool.literal_to_pretty_string(-1),
+            "don't install a/a 1.0.0.0"
+        );
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/pool_builder.rs b/crates/mozart-sat-resolver/src/pool_builder.rs
new file mode 100644
index 0000000..40977ef
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/pool_builder.rs
@@ -0,0 +1,169 @@
+use crate::pool::{Pool, PoolLink, PoolPackageInput};
+use std::collections::{HashSet, VecDeque};
+
+/// Builder for constructing a Pool from package metadata.
+///
+/// The builder accepts package inputs and recursively discovers
+/// transitive dependencies. This is done by the registry layer
+/// before solving.
+pub struct PoolBuilder {
+    /// Packages to add to the pool.
+    inputs: Vec<PoolPackageInput>,
+    /// Names already added (to avoid duplicates).
+    added: HashSet<String>,
+    /// Queue of package names that need to be explored.
+    pending_names: VecDeque<String>,
+    /// Platform packages to ignore.
+    ignore_platform_reqs: HashSet<String>,
+}
+
+impl PoolBuilder {
+    pub fn new() -> Self {
+        PoolBuilder {
+            inputs: Vec::new(),
+            added: HashSet::new(),
+            pending_names: VecDeque::new(),
+            ignore_platform_reqs: HashSet::new(),
+        }
+    }
+
+    /// Set platform requirements to ignore during exploration.
+    pub fn set_ignore_platform_reqs(&mut self, names: HashSet<String>) {
+        self.ignore_platform_reqs = names;
+    }
+
+    /// Add a package version to the builder. Returns true if it's new.
+    pub fn add_package(&mut self, input: PoolPackageInput) -> bool {
+        let key = format!("{}@{}", input.name, input.version);
+        if self.added.contains(&key) {
+            return false;
+        }
+        self.added.insert(key);
+
+        // Queue dependency names for exploration
+        for link in &input.requires {
+            if !self.ignore_platform_reqs.contains(&link.target) {
+                self.pending_names.push_back(link.target.clone());
+            }
+        }
+
+        self.inputs.push(input);
+        true
+    }
+
+    /// Get the next package name that needs to be explored.
+    /// The caller should fetch available versions for this package
+    /// and add them via `add_package`.
+    pub fn next_pending(&mut self) -> Option<String> {
+        while let Some(name) = self.pending_names.pop_front() {
+            // Check if we already have any versions for this name
+            if !self.inputs.iter().any(|p| p.name == name) {
+                return Some(name);
+            }
+        }
+        None
+    }
+
+    /// Check if there are more names to explore.
+    pub fn has_pending(&self) -> bool {
+        !self.pending_names.is_empty()
+    }
+
+    /// Build the final Pool.
+    pub fn build(self) -> Pool {
+        Pool::new(self.inputs, vec![])
+    }
+
+    /// Get the number of packages added so far.
+    pub fn len(&self) -> usize {
+        self.inputs.len()
+    }
+
+    /// Whether the builder has no packages.
+    pub fn is_empty(&self) -> bool {
+        self.inputs.is_empty()
+    }
+}
+
+impl Default for PoolBuilder {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Helper to convert (name, constraint) pairs from Packagist into PoolLinks.
+pub fn make_pool_links(source: &str, deps: &[(String, String)]) -> Vec<PoolLink> {
+    deps.iter()
+        .map(|(target, constraint)| PoolLink {
+            target: target.clone(),
+            constraint: constraint.clone(),
+            source: source.to_string(),
+        })
+        .collect()
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_pool_builder_basic() {
+        let mut builder = PoolBuilder::new();
+
+        builder.add_package(PoolPackageInput {
+            name: "a/a".to_string(),
+            version: "1.0.0.0".to_string(),
+            pretty_version: "1.0.0".to_string(),
+            requires: vec![PoolLink {
+                target: "b/b".to_string(),
+                constraint: "^1.0".to_string(),
+                source: "a/a".to_string(),
+            }],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        });
+
+        // Should have b/b pending
+        let pending = builder.next_pending();
+        assert_eq!(pending, Some("b/b".to_string()));
+
+        builder.add_package(PoolPackageInput {
+            name: "b/b".to_string(),
+            version: "1.0.0.0".to_string(),
+            pretty_version: "1.0.0".to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        });
+
+        // No more pending
+        assert!(builder.next_pending().is_none());
+
+        let pool = builder.build();
+        assert_eq!(pool.len(), 2);
+    }
+
+    #[test]
+    fn test_deduplication() {
+        let mut builder = PoolBuilder::new();
+
+        let input = PoolPackageInput {
+            name: "a/a".to_string(),
+            version: "1.0.0.0".to_string(),
+            pretty_version: "1.0.0".to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        };
+
+        assert!(builder.add_package(input.clone()));
+        assert!(!builder.add_package(input));
+        assert_eq!(builder.len(), 1);
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/problem.rs b/crates/mozart-sat-resolver/src/problem.rs
new file mode 100644
index 0000000..7ba60bc
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/problem.rs
@@ -0,0 +1,498 @@
+use crate::pool::{Literal, Pool, literal_to_package_id};
+use crate::rule::{ReasonData, Rule, RuleReason};
+use crate::rule_set::{RuleId, RuleSet};
+
+/// Represents a conflict found during resolution.
+/// Collects the rules involved in the problem.
+///
+/// Port of Composer's Problem.php.
+#[derive(Debug, Clone)]
+pub struct Problem {
+    /// Sections of rules that form this problem.
+    /// Each section is a group of related rules.
+    sections: Vec<Vec<RuleId>>,
+}
+
+impl Problem {
+    pub fn new() -> Self {
+        Problem {
+            sections: vec![vec![]],
+        }
+    }
+
+    /// Add a rule to the current section.
+    pub fn add_rule(&mut self, rule_id: RuleId) {
+        if let Some(section) = self.sections.last_mut()
+            && !section.contains(&rule_id)
+        {
+            section.push(rule_id);
+        }
+    }
+
+    /// Start a new section.
+    pub fn next_section(&mut self) {
+        if self.sections.last().is_some_and(|s| !s.is_empty()) {
+            self.sections.push(vec![]);
+        }
+    }
+
+    /// Get all rule IDs in this problem.
+    pub fn rule_ids(&self) -> Vec<RuleId> {
+        self.sections.iter().flatten().copied().collect()
+    }
+
+    /// Format the problem as a human-readable string using Pool data.
+    ///
+    /// Port of Composer's Problem::getPrettyString().
+    pub fn pretty_string(&self, pool: &Pool, rules: &RuleSet) -> String {
+        // Flatten all sections (reversed) like Composer does
+        let mut all_rules: Vec<RuleId> = self.sections.iter().rev().flatten().copied().collect();
+
+        if all_rules.is_empty() {
+            return "Unknown problem".to_string();
+        }
+
+        // Sort by priority, then by sortable string
+        all_rules.sort_by(|&a, &b| {
+            let rule_a = rules.rule_by_id(a);
+            let rule_b = rules.rule_by_id(b);
+            let prio_a = rule_priority(rule_a);
+            let prio_b = rule_priority(rule_b);
+            if prio_a != prio_b {
+                return prio_b.cmp(&prio_a);
+            }
+            sortable_string(pool, rule_a).cmp(&sortable_string(pool, rule_b))
+        });
+
+        // Format each rule
+        let mut messages: Vec<String> = Vec::new();
+        for &rule_id in &all_rules {
+            let rule = rules.rule_by_id(rule_id);
+            let msg = rule_pretty_string(pool, rule);
+            if !msg.is_empty() {
+                messages.push(msg);
+            }
+        }
+
+        // Deduplicate
+        let mut seen = std::collections::HashSet::new();
+        let mut unique = Vec::new();
+        for msg in messages {
+            if seen.insert(msg.clone()) {
+                unique.push(msg);
+            }
+        }
+
+        if unique.is_empty() {
+            return "Unknown problem".to_string();
+        }
+
+        unique
+            .iter()
+            .map(|m| format!("    - {m}"))
+            .collect::<Vec<_>>()
+            .join("\n")
+    }
+
+    /// Basic format for backward compatibility (uses rule Display).
+    pub fn format(&self, rules: &RuleSet) -> String {
+        let mut parts = Vec::new();
+        for section in &self.sections {
+            for &rule_id in section {
+                let rule = rules.rule_by_id(rule_id);
+                parts.push(format!("  - {rule}"));
+            }
+        }
+        if parts.is_empty() {
+            "Unknown problem".to_string()
+        } else {
+            parts.join("\n")
+        }
+    }
+}
+
+impl Default for Problem {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Get the sort priority for a rule (higher = more important).
+/// Port of Problem::getRulePriority().
+fn rule_priority(rule: &Rule) -> u8 {
+    match rule.reason {
+        RuleReason::Fixed => 3,
+        RuleReason::RootRequire => 2,
+        RuleReason::PackageConflict | RuleReason::PackageRequires => 1,
+        RuleReason::PackageSameName
+        | RuleReason::Learned
+        | RuleReason::PackageAlias
+        | RuleReason::PackageInverseAlias => 0,
+    }
+}
+
+/// Get a sortable string for a rule.
+/// Port of Problem::getSortableString().
+fn sortable_string(pool: &Pool, rule: &Rule) -> String {
+    match (&rule.reason, &rule.reason_data) {
+        (RuleReason::RootRequire, ReasonData::RootRequire { package_name, .. }) => {
+            package_name.clone()
+        }
+        (RuleReason::Fixed, ReasonData::Fixed { package_id }) => {
+            pool.package_by_id(*package_id).to_string()
+        }
+        (RuleReason::PackageConflict | RuleReason::PackageRequires, ReasonData::Link(link)) => {
+            if let Some(source_lit) = rule.literals().first() {
+                let source_pkg = pool.literal_to_package(*source_lit);
+                format!("{}//{}", source_pkg, link)
+            } else {
+                link.to_string()
+            }
+        }
+        (RuleReason::PackageSameName, ReasonData::PackageName(name)) => name.clone(),
+        (RuleReason::Learned, _) => rule
+            .literals()
+            .iter()
+            .map(|l: &Literal| l.to_string())
+            .collect::<Vec<_>>()
+            .join("-"),
+        _ => String::new(),
+    }
+}
+
+/// Format a rule as a human-readable string.
+/// Port of Composer's Rule::getPrettyString().
+fn rule_pretty_string(pool: &Pool, rule: &Rule) -> String {
+    match (&rule.reason, &rule.reason_data) {
+        (
+            RuleReason::RootRequire,
+            ReasonData::RootRequire {
+                package_name,
+                constraint,
+            },
+        ) => {
+            let providers = format_providers(pool, rule.literals());
+            if providers.is_empty() {
+                format!(
+                    "No package found to satisfy root composer.json require {package_name} {constraint}"
+                )
+            } else {
+                format!(
+                    "Root composer.json requires {package_name} {constraint} -> satisfiable by {providers}."
+                )
+            }
+        }
+
+        (RuleReason::Fixed, ReasonData::Fixed { package_id }) => {
+            let pkg = pool.package_by_id(*package_id);
+            if pkg.is_fixed {
+                format!(
+                    "{} {} is locked to version {} and an update of this package was not requested.",
+                    pkg.name, pkg.pretty_version, pkg.pretty_version
+                )
+            } else {
+                format!(
+                    "{} {} is present at version {} and cannot be modified by Mozart",
+                    pkg.name, pkg.pretty_version, pkg.pretty_version
+                )
+            }
+        }
+
+        (RuleReason::PackageConflict, ReasonData::Link(link)) => {
+            let literals = rule.literals();
+            if literals.len() >= 2 {
+                let pkg1 = pool.literal_to_package(literals[0]);
+                let pkg2 = pool.literal_to_package(literals[1]);
+                // Determine which is the source of the conflict
+                if link.source == pkg1.name {
+                    format!("{pkg2} conflicts with {pkg1}.")
+                } else {
+                    format!("{pkg1} conflicts with {pkg2}.")
+                }
+            } else {
+                format!("Conflict: {link}")
+            }
+        }
+
+        (RuleReason::PackageRequires, ReasonData::Link(link)) => {
+            let literals = rule.literals();
+            if literals.is_empty() {
+                return format!("Requirement: {link}");
+            }
+
+            let source_pkg = pool.literal_to_package(literals[0]);
+            let base_text = format!(
+                "{} {} requires {} {}",
+                source_pkg.name, source_pkg.pretty_version, link.target, link.constraint
+            );
+
+            // Remaining literals are the satisfying packages
+            let provider_lits: Vec<Literal> = literals[1..].to_vec();
+            if provider_lits.is_empty() {
+                format!("{base_text} -> no matching package found.")
+            } else {
+                let providers = format_providers(pool, &provider_lits);
+                format!("{base_text} -> satisfiable by {providers}.")
+            }
+        }
+
+        (RuleReason::PackageSameName, ReasonData::PackageName(name)) => {
+            let literals = rule.literals();
+            // Collect unique package names in this rule
+            let mut pkg_names: Vec<String> = Vec::new();
+            for &lit in literals {
+                let pkg = pool.literal_to_package(lit);
+                if !pkg_names.contains(&pkg.name) {
+                    pkg_names.push(pkg.name.clone());
+                }
+            }
+
+            if pkg_names.len() > 1 {
+                // Different packages that replace/provide the same name
+                let replacers: Vec<&str> = pkg_names
+                    .iter()
+                    .filter(|n| n.as_str() != name)
+                    .map(|n| n.as_str())
+                    .collect();
+
+                let reason = if replacers.is_empty() {
+                    format!("They all replace {name} and thus cannot coexist.")
+                } else if !pkg_names.contains(name) {
+                    format!(
+                        "They {} replace {name} and thus cannot coexist.",
+                        if literals.len() == 2 { "both" } else { "all" }
+                    )
+                } else if replacers.len() == 1 {
+                    format!(
+                        "{} replaces {name} and thus cannot coexist with it.",
+                        replacers[0]
+                    )
+                } else {
+                    format!(
+                        "[{}] replace {name} and thus cannot coexist with it.",
+                        replacers.join(", ")
+                    )
+                };
+
+                let pkgs_str = format_providers(pool, literals);
+                format!("Only one of these can be installed: {pkgs_str}. {reason}")
+            } else {
+                // Same package, different versions
+                let pkgs_str = format_providers(pool, literals);
+                format!(
+                    "You can only install one version of a package, so only one of these can be installed: {pkgs_str}."
+                )
+            }
+        }
+
+        (RuleReason::Learned, _) => {
+            let literals = rule.literals();
+            if literals.len() == 1 {
+                let pretty = pool.literal_to_pretty_string(literals[0]);
+                format!("Conclusion: {pretty} (conflict analysis result)")
+            } else {
+                // Group literals by install/don't install
+                let mut install = Vec::new();
+                let mut dont_install = Vec::new();
+                for &lit in literals {
+                    if lit > 0 {
+                        install.push(lit);
+                    } else {
+                        dont_install.push(lit);
+                    }
+                }
+
+                let mut parts = Vec::new();
+                if !install.is_empty() {
+                    let pkgs = format_providers(pool, &install);
+                    if install.len() > 1 {
+                        parts.push(format!("install one of {pkgs}"));
+                    } else {
+                        parts.push(format!("install {pkgs}"));
+                    }
+                }
+                if !dont_install.is_empty() {
+                    let pkgs = format_providers_abs(pool, &dont_install);
+                    if dont_install.len() > 1 {
+                        parts.push(format!("don't install one of {pkgs}"));
+                    } else {
+                        parts.push(format!("don't install {pkgs}"));
+                    }
+                }
+
+                format!(
+                    "Conclusion: {} (conflict analysis result)",
+                    parts.join(" | ")
+                )
+            }
+        }
+
+        (RuleReason::PackageAlias, _) => {
+            let literals = rule.literals();
+            if literals.len() >= 2 {
+                let alias_pkg = pool.literal_to_package(literals[0]);
+                let target_pkg = pool.literal_to_package(literals[1]);
+                format!(
+                    "{alias_pkg} is an alias of {target_pkg} and thus requires it to be installed too."
+                )
+            } else {
+                String::new()
+            }
+        }
+
+        (RuleReason::PackageInverseAlias, _) => {
+            let literals = rule.literals();
+            if literals.len() >= 2 {
+                let target_pkg = pool.literal_to_package(literals[0]);
+                let alias_pkg = pool.literal_to_package(literals[1]);
+                format!("{alias_pkg} is an alias of {target_pkg} and must be installed with it.")
+            } else {
+                String::new()
+            }
+        }
+
+        _ => {
+            // Fallback: display raw literals
+            let literal_strs: Vec<String> = rule
+                .literals()
+                .iter()
+                .map(|&l| pool.literal_to_pretty_string(l))
+                .collect();
+            literal_strs.join(" | ")
+        }
+    }
+}
+
+/// Format a list of literals as a list of package names grouped by name.
+/// Similar to Composer's formatPackagesUnique.
+fn format_providers(pool: &Pool, literals: &[Literal]) -> String {
+    // Group by package name
+    let mut groups: std::collections::HashMap<&str, Vec<&str>> = std::collections::HashMap::new();
+    for &lit in literals {
+        let pkg = pool.literal_to_package(lit);
+        groups
+            .entry(&pkg.name)
+            .or_default()
+            .push(&pkg.pretty_version);
+    }
+
+    let mut parts: Vec<String> = Vec::new();
+    for (name, versions) in &groups {
+        if versions.len() == 1 {
+            parts.push(format!("{name} {}", versions[0]));
+        } else {
+            let v_str = versions.join(", ");
+            parts.push(format!("{name}[{v_str}]"));
+        }
+    }
+
+    parts.sort();
+    parts.join(", ")
+}
+
+/// Same as format_providers but uses absolute value of literals.
+fn format_providers_abs(pool: &Pool, literals: &[Literal]) -> String {
+    let abs_lits: Vec<Literal> = literals
+        .iter()
+        .map(|&l| literal_to_package_id(l) as Literal)
+        .collect();
+    format_providers(pool, &abs_lits)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::pool::PoolPackageInput;
+    use crate::rule::{ReasonData, Rule, RuleReason, RuleType};
+
+    fn make_input(name: &str, version: &str, pretty: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: pretty.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    #[test]
+    fn test_root_require_pretty_string() {
+        let pool = Pool::new(vec![make_input("foo/bar", "1.0.0.0", "1.0.0")], vec![]);
+
+        let mut rule_set = RuleSet::new();
+        let rule = Rule::new(
+            vec![1],
+            RuleReason::RootRequire,
+            ReasonData::RootRequire {
+                package_name: "foo/bar".to_string(),
+                constraint: "^1.0".to_string(),
+            },
+        );
+        rule_set.add(rule, RuleType::Request);
+
+        let mut problem = Problem::new();
+        problem.add_rule(0);
+
+        let output = problem.pretty_string(&pool, &rule_set);
+        assert!(output.contains("Root composer.json requires foo/bar ^1.0"));
+        assert!(output.contains("satisfiable by foo/bar 1.0.0"));
+    }
+
+    #[test]
+    fn test_same_name_pretty_string() {
+        let pool = Pool::new(
+            vec![
+                make_input("foo/bar", "1.0.0.0", "1.0.0"),
+                make_input("foo/bar", "2.0.0.0", "2.0.0"),
+            ],
+            vec![],
+        );
+
+        let mut rule_set = RuleSet::new();
+        let rule = Rule::new(
+            vec![-1, -2],
+            RuleReason::PackageSameName,
+            ReasonData::PackageName("foo/bar".to_string()),
+        );
+        rule_set.add(rule, RuleType::Package);
+
+        let mut problem = Problem::new();
+        problem.add_rule(0);
+
+        let output = problem.pretty_string(&pool, &rule_set);
+        assert!(output.contains("You can only install one version"));
+    }
+
+    #[test]
+    fn test_package_requires_pretty_string() {
+        let pool = Pool::new(
+            vec![
+                make_input("foo/bar", "1.0.0.0", "1.0.0"),
+                make_input("baz/qux", "2.0.0.0", "2.0.0"),
+            ],
+            vec![],
+        );
+
+        let mut rule_set = RuleSet::new();
+        let rule = Rule::new(
+            vec![-1, 2],
+            RuleReason::PackageRequires,
+            ReasonData::Link(crate::pool::PoolLink {
+                source: "foo/bar".to_string(),
+                target: "baz/qux".to_string(),
+                constraint: "^2.0".to_string(),
+            }),
+        );
+        rule_set.add(rule, RuleType::Package);
+
+        let mut problem = Problem::new();
+        problem.add_rule(0);
+
+        let output = problem.pretty_string(&pool, &rule_set);
+        assert!(output.contains("foo/bar 1.0.0 requires baz/qux ^2.0"));
+        assert!(output.contains("satisfiable by baz/qux 2.0.0"));
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/request.rs b/crates/mozart-sat-resolver/src/request.rs
new file mode 100644
index 0000000..94891f0
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/request.rs
@@ -0,0 +1,65 @@
+use crate::pool::PackageId;
+use std::collections::HashMap;
+
+/// A requirement: package name + version constraint string.
+#[derive(Debug, Clone)]
+pub struct Require {
+    pub package_name: String,
+    pub constraint: Option<String>,
+}
+
+/// A request for the solver: what to install/fix/lock.
+///
+/// Port of Composer's Request.php.
+#[derive(Debug, Clone)]
+pub struct Request {
+    /// Root requirements: package name → constraint string.
+    pub requires: HashMap<String, Option<String>>,
+    /// Fixed packages (must be installed, cannot be modified).
+    pub fixed_packages: Vec<PackageId>,
+    /// Locked packages (installed but can be removed if nothing requires them).
+    pub locked_packages: Vec<PackageId>,
+}
+
+impl Request {
+    pub fn new() -> Self {
+        Request {
+            requires: HashMap::new(),
+            fixed_packages: Vec::new(),
+            locked_packages: Vec::new(),
+        }
+    }
+
+    /// Add a root requirement.
+    pub fn require_name(&mut self, package_name: &str, constraint: Option<&str>) {
+        self.requires.insert(
+            package_name.to_lowercase(),
+            constraint.map(|s| s.to_string()),
+        );
+    }
+
+    /// Mark a package as fixed (must remain installed).
+    pub fn fix_package(&mut self, package_id: PackageId) {
+        if !self.fixed_packages.contains(&package_id) {
+            self.fixed_packages.push(package_id);
+        }
+    }
+
+    /// Mark a package as locked.
+    pub fn lock_package(&mut self, package_id: PackageId) {
+        if !self.locked_packages.contains(&package_id) {
+            self.locked_packages.push(package_id);
+        }
+    }
+
+    /// Check if a package is fixed.
+    pub fn is_fixed(&self, package_id: PackageId) -> bool {
+        self.fixed_packages.contains(&package_id)
+    }
+}
+
+impl Default for Request {
+    fn default() -> Self {
+        Self::new()
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/rule.rs b/crates/mozart-sat-resolver/src/rule.rs
new file mode 100644
index 0000000..860ae79
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/rule.rs
@@ -0,0 +1,280 @@
+use crate::pool::{Literal, PoolLink};
+use std::fmt;
+
+/// Why a rule was created.
+/// Port of Composer Rule::RULE_* constants.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum RuleReason {
+    /// Root composer.json requirement.
+    RootRequire,
+    /// Fixed/locked package.
+    Fixed,
+    /// Two packages conflict.
+    PackageConflict,
+    /// Package dependency (requires).
+    PackageRequires,
+    /// Only one version of a package can be installed.
+    PackageSameName,
+    /// Learned from conflict analysis.
+    Learned,
+    /// Alias requires its target.
+    PackageAlias,
+    /// Target requires its alias.
+    PackageInverseAlias,
+}
+
+/// Data explaining why a rule was created.
+#[derive(Debug, Clone)]
+pub enum ReasonData {
+    /// For RootRequire: package name + constraint string.
+    RootRequire {
+        package_name: String,
+        constraint: String,
+    },
+    /// For Fixed: the fixed package ID.
+    Fixed { package_id: u32 },
+    /// For PackageConflict, PackageRequires: a link.
+    Link(PoolLink),
+    /// For PackageSameName: the package name.
+    PackageName(String),
+    /// For Learned: index into the learned pool.
+    Learned(usize),
+    /// For PackageAlias/InverseAlias: the alias package ID.
+    AliasPackage(u32),
+    /// No data.
+    None,
+}
+
+/// The type assigned by RuleSet (which collection this rule belongs to).
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub enum RuleType {
+    Package = 0,
+    Request = 1,
+    Learned = 4,
+}
+
+/// A SAT rule (clause). A disjunction of literals: (L1 | L2 | ... | Ln).
+///
+/// Port of Composer's Rule hierarchy (GenericRule, Rule2Literals, MultiConflictRule).
+/// In Rust we use a single enum instead of class inheritance.
+#[derive(Debug, Clone)]
+pub struct Rule {
+    /// The literals in this rule (sorted for deduplication).
+    literals: Vec<Literal>,
+    /// Whether this is a multi-conflict rule.
+    pub is_multi_conflict: bool,
+    /// Why this rule was created.
+    pub reason: RuleReason,
+    /// Additional data about why this rule was created.
+    pub reason_data: ReasonData,
+    /// Which RuleSet type this rule belongs to.
+    pub rule_type: RuleType,
+    /// Whether this rule is disabled.
+    pub disabled: bool,
+}
+
+impl Rule {
+    /// Create a generic rule (arbitrary number of literals).
+    /// Equivalent to Composer's GenericRule.
+    pub fn new(mut literals: Vec<Literal>, reason: RuleReason, reason_data: ReasonData) -> Self {
+        literals.sort();
+        Rule {
+            literals,
+            is_multi_conflict: false,
+            reason,
+            reason_data,
+            rule_type: RuleType::Package, // default, set by RuleSet
+            disabled: false,
+        }
+    }
+
+    /// Create a 2-literal rule (optimized common case).
+    /// Equivalent to Composer's Rule2Literals.
+    pub fn two_literals(
+        lit1: Literal,
+        lit2: Literal,
+        reason: RuleReason,
+        reason_data: ReasonData,
+    ) -> Self {
+        let (a, b) = if lit1 <= lit2 {
+            (lit1, lit2)
+        } else {
+            (lit2, lit1)
+        };
+        Rule {
+            literals: vec![a, b],
+            is_multi_conflict: false,
+            reason,
+            reason_data,
+            rule_type: RuleType::Package,
+            disabled: false,
+        }
+    }
+
+    /// Create a multi-conflict rule (3+ literals, all negative).
+    /// Equivalent to Composer's MultiConflictRule.
+    /// Acts as if it were multiple binary conflict rules.
+    pub fn multi_conflict(
+        mut literals: Vec<Literal>,
+        reason: RuleReason,
+        reason_data: ReasonData,
+    ) -> Self {
+        assert!(
+            literals.len() >= 3,
+            "MultiConflictRule requires at least 3 literals"
+        );
+        literals.sort();
+        Rule {
+            literals,
+            is_multi_conflict: true,
+            reason,
+            reason_data,
+            rule_type: RuleType::Package,
+            disabled: false,
+        }
+    }
+
+    /// Get the sorted literals.
+    pub fn literals(&self) -> &[Literal] {
+        &self.literals
+    }
+
+    /// Whether this rule has exactly one literal (unit clause / assertion).
+    pub fn is_assertion(&self) -> bool {
+        self.literals.len() == 1
+    }
+
+    /// Compute a hash for deduplication.
+    pub fn hash_key(&self) -> String {
+        if self.is_multi_conflict {
+            let parts: Vec<String> = self.literals.iter().map(|l| l.to_string()).collect();
+            format!("c:{}", parts.join(","))
+        } else {
+            let parts: Vec<String> = self.literals.iter().map(|l| l.to_string()).collect();
+            parts.join(",")
+        }
+    }
+
+    /// Structural equality check (same literals).
+    pub fn equals(&self, other: &Rule) -> bool {
+        self.is_multi_conflict == other.is_multi_conflict && self.literals == other.literals
+    }
+
+    /// Get the required package name, if applicable.
+    pub fn required_package(&self) -> Option<&str> {
+        match &self.reason_data {
+            ReasonData::RootRequire { package_name, .. } => Some(package_name),
+            ReasonData::Link(link) => Some(&link.target),
+            ReasonData::Fixed { .. } => None, // would need pool access
+            _ => None,
+        }
+    }
+
+    /// Disable this rule.
+    pub fn disable(&mut self) {
+        if self.is_multi_conflict {
+            panic!("Cannot disable a MultiConflictRule");
+        }
+        self.disabled = true;
+    }
+
+    /// Enable this rule.
+    pub fn enable(&mut self) {
+        self.disabled = false;
+    }
+
+    /// Whether this rule is disabled.
+    pub fn is_disabled(&self) -> bool {
+        self.disabled
+    }
+
+    /// Whether this rule is enabled.
+    pub fn is_enabled(&self) -> bool {
+        !self.disabled
+    }
+}
+
+impl fmt::Display for Rule {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        if self.disabled {
+            write!(f, "disabled(")?;
+        }
+        if self.is_multi_conflict {
+            write!(f, "(multi(")?;
+            for (i, lit) in self.literals.iter().enumerate() {
+                if i > 0 {
+                    write!(f, "|")?;
+                }
+                write!(f, "{lit}")?;
+            }
+            write!(f, "))")?;
+        } else {
+            write!(f, "(")?;
+            for (i, lit) in self.literals.iter().enumerate() {
+                if i > 0 {
+                    write!(f, "|")?;
+                }
+                write!(f, "{lit}")?;
+            }
+            write!(f, ")")?;
+        }
+        if self.disabled {
+            write!(f, ")")?;
+        }
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_generic_rule() {
+        let rule = Rule::new(vec![3, 1, 2], RuleReason::PackageRequires, ReasonData::None);
+        assert_eq!(rule.literals(), &[1, 2, 3]);
+        assert!(!rule.is_assertion());
+        assert_eq!(rule.to_string(), "(1|2|3)");
+    }
+
+    #[test]
+    fn test_two_literal_rule() {
+        let rule = Rule::two_literals(-2, -1, RuleReason::PackageConflict, ReasonData::None);
+        assert_eq!(rule.literals(), &[-2, -1]);
+        assert!(!rule.is_assertion());
+    }
+
+    #[test]
+    fn test_assertion_rule() {
+        let rule = Rule::new(vec![1], RuleReason::Fixed, ReasonData::None);
+        assert!(rule.is_assertion());
+    }
+
+    #[test]
+    fn test_multi_conflict_rule() {
+        let rule = Rule::multi_conflict(
+            vec![-3, -1, -2],
+            RuleReason::PackageSameName,
+            ReasonData::None,
+        );
+        assert!(rule.is_multi_conflict);
+        assert_eq!(rule.literals(), &[-3, -2, -1]);
+    }
+
+    #[test]
+    fn test_hash_key() {
+        let r1 = Rule::new(vec![2, 1], RuleReason::PackageRequires, ReasonData::None);
+        let r2 = Rule::new(vec![1, 2], RuleReason::PackageConflict, ReasonData::None);
+        assert_eq!(r1.hash_key(), r2.hash_key());
+    }
+
+    #[test]
+    fn test_disable_enable() {
+        let mut rule = Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None);
+        assert!(rule.is_enabled());
+        rule.disable();
+        assert!(rule.is_disabled());
+        rule.enable();
+        assert!(rule.is_enabled());
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/rule_set.rs b/crates/mozart-sat-resolver/src/rule_set.rs
new file mode 100644
index 0000000..4d1a8a6
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/rule_set.rs
@@ -0,0 +1,211 @@
+use crate::rule::{Rule, RuleType};
+use std::collections::HashMap;
+
+/// A unique identifier for a rule within the RuleSet.
+pub type RuleId = usize;
+
+/// Container for all rules, organized by type.
+///
+/// Port of Composer's RuleSet.php.
+pub struct RuleSet {
+    /// Lookup: rule ID → index into the appropriate type vector.
+    /// This is the primary read-only access path used by the solver.
+    rules_by_id: Vec<usize>,
+    /// Rules grouped by type.
+    package_rules: Vec<Rule>,
+    request_rules: Vec<Rule>,
+    learned_rules: Vec<Rule>,
+    /// Total rule count.
+    next_rule_id: usize,
+    /// Deduplication index.
+    rules_by_hash: HashMap<String, Vec<usize>>,
+    /// Maps rule ID → (type, index within type's vec).
+    rule_type_index: Vec<(RuleType, usize)>,
+}
+
+impl RuleSet {
+    pub fn new() -> Self {
+        RuleSet {
+            rules_by_id: Vec::new(),
+            package_rules: Vec::new(),
+            request_rules: Vec::new(),
+            learned_rules: Vec::new(),
+            next_rule_id: 0,
+            rules_by_hash: HashMap::new(),
+            rule_type_index: Vec::new(),
+        }
+    }
+
+    /// Add a rule to the set. Duplicates (by hash + equals) are skipped.
+    pub fn add(&mut self, mut rule: Rule, rule_type: RuleType) {
+        let hash = rule.hash_key();
+
+        // Check for duplicates
+        if let Some(existing_ids) = self.rules_by_hash.get(&hash) {
+            for &existing_id in existing_ids {
+                if rule.equals(self.rule_by_id(existing_id)) {
+                    return;
+                }
+            }
+        }
+
+        rule.rule_type = rule_type;
+
+        let rules_vec = match rule_type {
+            RuleType::Package => &mut self.package_rules,
+            RuleType::Request => &mut self.request_rules,
+            RuleType::Learned => &mut self.learned_rules,
+        };
+        let idx = rules_vec.len();
+        rules_vec.push(rule);
+
+        let rule_id = self.next_rule_id;
+        self.rules_by_id.push(idx);
+        self.rule_type_index.push((rule_type, idx));
+        self.next_rule_id += 1;
+
+        self.rules_by_hash.entry(hash).or_default().push(rule_id);
+    }
+
+    /// Total number of rules.
+    pub fn len(&self) -> usize {
+        self.next_rule_id
+    }
+
+    /// Whether the rule set is empty.
+    pub fn is_empty(&self) -> bool {
+        self.next_rule_id == 0
+    }
+
+    /// Look up a rule by its global ID.
+    pub fn rule_by_id(&self, id: RuleId) -> &Rule {
+        let (rule_type, idx) = self.rule_type_index[id];
+        match rule_type {
+            RuleType::Package => &self.package_rules[idx],
+            RuleType::Request => &self.request_rules[idx],
+            RuleType::Learned => &self.learned_rules[idx],
+        }
+    }
+
+    /// Get a mutable reference to a rule by its global ID.
+    pub fn rule_by_id_mut(&mut self, id: RuleId) -> &mut Rule {
+        let (rule_type, idx) = self.rule_type_index[id];
+        match rule_type {
+            RuleType::Package => &mut self.package_rules[idx],
+            RuleType::Request => &mut self.request_rules[idx],
+            RuleType::Learned => &mut self.learned_rules[idx],
+        }
+    }
+
+    /// Iterate over all rules in order (Package, then Request, then Learned).
+    pub fn iter(&self) -> impl Iterator<Item = (RuleId, &Rule)> {
+        (0..self.next_rule_id).map(move |id| (id, self.rule_by_id(id)))
+    }
+
+    /// Iterate over rules of a specific type, returning (global_rule_id, &Rule).
+    pub fn iter_type(&self, rule_type: RuleType) -> RuleTypeIterator<'_> {
+        RuleTypeIterator {
+            rule_set: self,
+            rule_type,
+            current: 0,
+            total: self.next_rule_id,
+        }
+    }
+
+    /// Get the request rules slice.
+    pub fn request_rules(&self) -> &[Rule] {
+        &self.request_rules
+    }
+}
+
+impl Default for RuleSet {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+/// Iterator over rules of a specific type.
+pub struct RuleTypeIterator<'a> {
+    rule_set: &'a RuleSet,
+    rule_type: RuleType,
+    current: RuleId,
+    total: usize,
+}
+
+impl<'a> Iterator for RuleTypeIterator<'a> {
+    type Item = (RuleId, &'a Rule);
+
+    fn next(&mut self) -> Option<Self::Item> {
+        while self.current < self.total {
+            let id = self.current;
+            self.current += 1;
+            let rule = self.rule_set.rule_by_id(id);
+            if rule.rule_type == self.rule_type {
+                return Some((id, rule));
+            }
+        }
+        None
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::rule::{ReasonData, RuleReason};
+
+    #[test]
+    fn test_add_and_lookup() {
+        let mut rs = RuleSet::new();
+        rs.add(
+            Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None),
+            RuleType::Package,
+        );
+        rs.add(
+            Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None),
+            RuleType::Request,
+        );
+
+        assert_eq!(rs.len(), 2);
+        assert_eq!(rs.rule_by_id(0).literals(), &[1, 2]);
+        assert_eq!(rs.rule_by_id(1).literals(), &[3]);
+    }
+
+    #[test]
+    fn test_deduplication() {
+        let mut rs = RuleSet::new();
+        rs.add(
+            Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None),
+            RuleType::Package,
+        );
+        rs.add(
+            Rule::new(vec![2, 1], RuleReason::PackageConflict, ReasonData::None),
+            RuleType::Package,
+        );
+        // Duplicate should be skipped
+        assert_eq!(rs.len(), 1);
+    }
+
+    #[test]
+    fn test_iter_type() {
+        let mut rs = RuleSet::new();
+        rs.add(
+            Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None),
+            RuleType::Package,
+        );
+        rs.add(
+            Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None),
+            RuleType::Request,
+        );
+        rs.add(
+            Rule::new(vec![4, 5], RuleReason::PackageConflict, ReasonData::None),
+            RuleType::Package,
+        );
+
+        let request_rules: Vec<_> = rs.iter_type(RuleType::Request).collect();
+        assert_eq!(request_rules.len(), 1);
+        assert_eq!(request_rules[0].1.literals(), &[3]);
+
+        let package_rules: Vec<_> = rs.iter_type(RuleType::Package).collect();
+        assert_eq!(package_rules.len(), 2);
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/rule_set_generator.rs b/crates/mozart-sat-resolver/src/rule_set_generator.rs
new file mode 100644
index 0000000..39d28fd
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/rule_set_generator.rs
@@ -0,0 +1,317 @@
+use crate::pool::{Literal, PackageId, Pool, PoolLink};
+use crate::rule::{ReasonData, Rule, RuleReason, RuleType};
+use crate::rule_set::RuleSet;
+use std::collections::{HashMap, HashSet, VecDeque};
+
+/// Generates SAT rules from the pool and request.
+///
+/// Port of Composer's RuleSetGenerator.php.
+pub struct RuleSetGenerator<'a> {
+    pool: &'a mut Pool,
+    rules: RuleSet,
+    /// Packages already processed.
+    added_map: HashSet<PackageId>,
+    /// Package names → list of package IDs with that name (non-alias).
+    added_packages_by_name: HashMap<String, Vec<PackageId>>,
+    /// Platform packages to ignore.
+    ignore_platform_reqs: HashSet<String>,
+}
+
+impl<'a> RuleSetGenerator<'a> {
+    pub fn new(pool: &'a mut Pool) -> Self {
+        RuleSetGenerator {
+            pool,
+            rules: RuleSet::new(),
+            added_map: HashSet::new(),
+            added_packages_by_name: HashMap::new(),
+            ignore_platform_reqs: HashSet::new(),
+        }
+    }
+
+    /// Set platform requirements to ignore.
+    pub fn set_ignore_platform_reqs(&mut self, names: HashSet<String>) {
+        self.ignore_platform_reqs = names;
+    }
+
+    /// Generate rules for a set of requirements and fixed packages.
+    ///
+    /// Port of Composer's RuleSetGenerator::getRulesFor.
+    pub fn generate(
+        mut self,
+        requires: &HashMap<String, Option<String>>,
+        fixed_packages: &[PackageId],
+    ) -> RuleSet {
+        // Process fixed packages
+        for &pkg_id in fixed_packages {
+            if self.pool.is_unacceptable_fixed_package(pkg_id) {
+                continue;
+            }
+
+            self.add_rules_for_package(pkg_id);
+
+            // Create assertion rule: this package must be installed
+            let rule = Rule::new(
+                vec![pkg_id as Literal],
+                RuleReason::Fixed,
+                ReasonData::Fixed { package_id: pkg_id },
+            );
+            self.rules.add(rule, RuleType::Request);
+        }
+
+        // Process root requirements
+        for (name, constraint) in requires {
+            if self.ignore_platform_reqs.contains(name.as_str()) {
+                continue;
+            }
+
+            let providers = self.pool.what_provides(name, constraint.as_deref());
+
+            if !providers.is_empty() {
+                for &pkg_id in &providers {
+                    self.add_rules_for_package(pkg_id);
+                }
+
+                // Create "install one of" rule
+                let literals: Vec<Literal> = providers.iter().map(|&id| id as Literal).collect();
+                let rule = Rule::new(
+                    literals,
+                    RuleReason::RootRequire,
+                    ReasonData::RootRequire {
+                        package_name: name.clone(),
+                        constraint: constraint.clone().unwrap_or_default(),
+                    },
+                );
+                self.rules.add(rule, RuleType::Request);
+            }
+        }
+
+        // Add conflict rules
+        self.add_conflict_rules();
+
+        self.rules
+    }
+
+    /// Add rules for a package and its transitive dependencies.
+    ///
+    /// Port of Composer's RuleSetGenerator::addRulesForPackage.
+    fn add_rules_for_package(&mut self, pkg_id: PackageId) {
+        let mut work_queue: VecDeque<PackageId> = VecDeque::new();
+        work_queue.push_back(pkg_id);
+
+        while let Some(current_id) = work_queue.pop_front() {
+            if self.added_map.contains(&current_id) {
+                continue;
+            }
+            self.added_map.insert(current_id);
+
+            let pkg = self.pool.package_by_id(current_id);
+            let pkg_name = pkg.name.clone();
+            let requires = pkg.requires.clone();
+
+            // Index by name (for same-name conflict rules later)
+            self.added_packages_by_name
+                .entry(pkg_name)
+                .or_default()
+                .push(current_id);
+
+            // Process each requirement
+            for link in requires {
+                if self.ignore_platform_reqs.contains(&link.target) {
+                    continue;
+                }
+
+                let possible_requires = self
+                    .pool
+                    .what_provides(&link.target, Some(&link.constraint));
+
+                // Create require rule: (-current | provider1 | provider2 | ...)
+                let mut literals: Vec<Literal> = vec![-(current_id as Literal)];
+                let mut self_fulfilling = false;
+
+                for &provider_id in &possible_requires {
+                    if provider_id == current_id {
+                        self_fulfilling = true;
+                        break;
+                    }
+                    literals.push(provider_id as Literal);
+                }
+
+                if !self_fulfilling {
+                    let rule = Rule::new(
+                        literals,
+                        RuleReason::PackageRequires,
+                        ReasonData::Link(PoolLink {
+                            target: link.target.clone(),
+                            constraint: link.constraint.clone(),
+                            source: self.pool.package_by_id(current_id).name.clone(),
+                        }),
+                    );
+                    self.rules.add(rule, RuleType::Package);
+                }
+
+                // Enqueue providers for further processing
+                for &provider_id in &possible_requires {
+                    work_queue.push_back(provider_id);
+                }
+            }
+        }
+    }
+
+    /// Add conflict rules: explicit conflicts and same-name rules.
+    ///
+    /// Port of Composer's RuleSetGenerator::addConflictRules.
+    fn add_conflict_rules(&mut self) {
+        // Explicit conflicts
+        let added_ids: Vec<PackageId> = self.added_map.iter().copied().collect();
+        for &pkg_id in &added_ids {
+            let pkg = self.pool.package_by_id(pkg_id);
+            let conflicts = pkg.conflicts.clone();
+
+            for link in conflicts {
+                if self.ignore_platform_reqs.contains(&link.target) {
+                    continue;
+                }
+
+                if !self.added_packages_by_name.contains_key(&link.target) {
+                    continue;
+                }
+
+                let conflicting = self
+                    .pool
+                    .what_provides(&link.target, Some(&link.constraint));
+
+                for &conflict_id in &conflicting {
+                    if conflict_id == pkg_id {
+                        continue; // ignore self-conflict
+                    }
+                    let rule = Rule::two_literals(
+                        -(pkg_id as Literal),
+                        -(conflict_id as Literal),
+                        RuleReason::PackageConflict,
+                        ReasonData::Link(link.clone()),
+                    );
+                    self.rules.add(rule, RuleType::Package);
+                }
+            }
+        }
+
+        // Same-name rules: only one version of a package can be installed
+        let names_to_process: Vec<(String, Vec<PackageId>)> = self
+            .added_packages_by_name
+            .iter()
+            .filter(|(_, ids)| ids.len() > 1)
+            .map(|(name, ids)| (name.clone(), ids.clone()))
+            .collect();
+
+        for (name, pkg_ids) in names_to_process {
+            let literals: Vec<Literal> = pkg_ids.iter().map(|&id| -(id as Literal)).collect();
+
+            if literals.len() == 2 {
+                let rule = Rule::two_literals(
+                    literals[0],
+                    literals[1],
+                    RuleReason::PackageSameName,
+                    ReasonData::PackageName(name),
+                );
+                self.rules.add(rule, RuleType::Package);
+            } else if literals.len() >= 3 {
+                let rule = Rule::multi_conflict(
+                    literals,
+                    RuleReason::PackageSameName,
+                    ReasonData::PackageName(name),
+                );
+                self.rules.add(rule, RuleType::Package);
+            }
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::pool::{Pool, PoolLink, PoolPackageInput};
+
+    fn make_input(name: &str, version: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: version.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    #[test]
+    fn test_root_require_generates_rule() {
+        let mut pool = Pool::new(
+            vec![make_input("a/a", "1.0.0.0"), make_input("a/a", "2.0.0.0")],
+            vec![],
+        );
+
+        let mut requires = HashMap::new();
+        requires.insert("a/a".to_string(), None);
+
+        let generator = RuleSetGenerator::new(&mut pool);
+        let rules = generator.generate(&requires, &[]);
+
+        // Should have a request rule: (1 | 2)
+        let request_count = rules.iter_type(RuleType::Request).count();
+        assert_eq!(request_count, 1);
+
+        // Should have a same-name rule: (-1 | -2)
+        let package_count = rules.iter_type(RuleType::Package).count();
+        assert!(package_count >= 1);
+    }
+
+    #[test]
+    fn test_dependency_chain_rules() {
+        // a/a 1.0 requires b/b
+        let mut pool = Pool::new(
+            vec![
+                PoolPackageInput {
+                    name: "a/a".to_string(),
+                    version: "1.0.0.0".to_string(),
+                    pretty_version: "1.0.0".to_string(),
+                    requires: vec![PoolLink {
+                        target: "b/b".to_string(),
+                        constraint: "*".to_string(),
+                        source: "a/a".to_string(),
+                    }],
+                    replaces: vec![],
+                    provides: vec![],
+                    conflicts: vec![],
+                    is_fixed: false,
+                },
+                make_input("b/b", "1.0.0.0"),
+            ],
+            vec![],
+        );
+
+        let mut requires = HashMap::new();
+        requires.insert("a/a".to_string(), None);
+
+        let generator = RuleSetGenerator::new(&mut pool);
+        let rules = generator.generate(&requires, &[]);
+
+        // Should have:
+        // 1. Request rule: (1) — root requires a/a
+        // 2. Package rule: (-1 | 2) — a/a requires b/b
+        assert!(rules.len() >= 2);
+    }
+
+    #[test]
+    fn test_fixed_package_rule() {
+        let mut pool = Pool::new(vec![make_input("php", "8.2.0.0")], vec![]);
+
+        let generator = RuleSetGenerator::new(&mut pool);
+        let rules = generator.generate(&HashMap::new(), &[1]);
+
+        // Should have an assertion rule: (1)
+        let request_rules: Vec<_> = rules.iter_type(RuleType::Request).collect();
+        assert_eq!(request_rules.len(), 1);
+        assert!(request_rules[0].1.is_assertion());
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/rule_watch_graph.rs b/crates/mozart-sat-resolver/src/rule_watch_graph.rs
new file mode 100644
index 0000000..4968b26
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/rule_watch_graph.rs
@@ -0,0 +1,291 @@
+use crate::decisions::Decisions;
+use crate::pool::Literal;
+use crate::rule::Rule;
+use crate::rule_set::RuleId;
+use std::collections::HashMap;
+
+/// A watch node: tracks which 2 literals a rule watches.
+///
+/// Port of Composer's RuleWatchNode.php.
+#[derive(Debug, Clone)]
+struct WatchNode {
+    /// First watched literal.
+    watch1: Literal,
+    /// Second watched literal.
+    watch2: Literal,
+    /// The rule ID this node refers to.
+    rule_id: RuleId,
+    /// Whether the rule is a multi-conflict rule.
+    is_multi_conflict: bool,
+}
+
+/// Efficient unit propagation using 2-watched literals optimization.
+///
+/// Port of Composer's RuleWatchGraph.php.
+pub struct RuleWatchGraph {
+    /// Literal → list of watch node indices watching that literal.
+    watch_chains: HashMap<Literal, Vec<usize>>,
+    /// All watch nodes.
+    nodes: Vec<WatchNode>,
+}
+
+impl RuleWatchGraph {
+    pub fn new() -> Self {
+        RuleWatchGraph {
+            watch_chains: HashMap::new(),
+            nodes: Vec::new(),
+        }
+    }
+
+    /// Insert a rule into the watch graph.
+    /// Assertions (single literal) are skipped.
+    pub fn insert(&mut self, rule_id: RuleId, rule: &Rule) {
+        if rule.is_assertion() {
+            return;
+        }
+
+        let literals = rule.literals();
+        let node_idx = self.nodes.len();
+
+        let watch1 = literals[0];
+        let watch2 = if literals.len() > 1 { literals[1] } else { 0 };
+
+        self.nodes.push(WatchNode {
+            watch1,
+            watch2,
+            rule_id,
+            is_multi_conflict: rule.is_multi_conflict,
+        });
+
+        if rule.is_multi_conflict {
+            // Multi-conflict rules watch ALL their literals
+            for &lit in literals {
+                self.watch_chains.entry(lit).or_default().push(node_idx);
+            }
+        } else {
+            // Normal rules watch first 2 literals
+            self.watch_chains.entry(watch1).or_default().push(node_idx);
+            self.watch_chains.entry(watch2).or_default().push(node_idx);
+        }
+    }
+
+    /// Adjust watch2 to the literal decided at the highest level.
+    /// Used for learned rules.
+    pub fn watch2_on_highest(&mut self, node_idx: usize, rule: &Rule, decisions: &Decisions) {
+        let literals = rule.literals();
+        if literals.len() < 3 || rule.is_multi_conflict {
+            return;
+        }
+
+        let mut watch_level = 0i32;
+        let mut best_literal = self.nodes[node_idx].watch2;
+
+        for &lit in literals {
+            let level = decisions.decision_level(lit);
+            if level > watch_level {
+                best_literal = lit;
+                watch_level = level;
+            }
+        }
+
+        let old_watch2 = self.nodes[node_idx].watch2;
+        if old_watch2 != best_literal {
+            // Remove from old chain, add to new chain
+            self.remove_from_chain(old_watch2, node_idx);
+            self.nodes[node_idx].watch2 = best_literal;
+            self.watch_chains
+                .entry(best_literal)
+                .or_default()
+                .push(node_idx);
+        }
+    }
+
+    /// Propagate a decision literal through the watch graph.
+    /// Returns the rule ID of a conflicting rule, if found.
+    ///
+    /// Port of Composer's RuleWatchGraph::propagateLiteral.
+    pub fn propagate_literal(
+        &mut self,
+        decided_literal: Literal,
+        level: i32,
+        decisions: &mut Decisions,
+        rules: &crate::rule_set::RuleSet,
+    ) -> Result<Option<RuleId>, crate::error::SolverBugError> {
+        // We look for rules watching the negation of the decided literal
+        let literal = -decided_literal;
+
+        let Some(chain) = self.watch_chains.get(&literal).cloned() else {
+            return Ok(None);
+        };
+
+        // We need to process nodes; some may be moved to different chains
+        let mut i = 0;
+        while i < chain.len() {
+            let node_idx = chain[i];
+            let node = &self.nodes[node_idx];
+            let rule_id = node.rule_id;
+            let is_multi_conflict = node.is_multi_conflict;
+            let rule = rules.rule_by_id(rule_id);
+
+            if !is_multi_conflict {
+                let other_watch = if node.watch1 == literal {
+                    node.watch2
+                } else {
+                    node.watch1
+                };
+
+                if !rule.is_disabled() && !decisions.satisfy(other_watch) {
+                    let rule_literals = rule.literals();
+
+                    // Find an alternative literal to watch
+                    let alternative = rule_literals
+                        .iter()
+                        .find(|&&rl| rl != literal && rl != other_watch && !decisions.conflict(rl));
+
+                    if let Some(&alt_literal) = alternative {
+                        // Move watch from `literal` to `alt_literal`
+                        self.move_watch(literal, alt_literal, node_idx);
+                        // Don't increment i since the node was removed from this chain
+                        // We need to re-fetch the chain since it was modified
+                        let chain_ref = self.watch_chains.get(&literal);
+                        if chain_ref.is_none() || i >= chain_ref.unwrap().len() {
+                            break;
+                        }
+                        continue;
+                    }
+
+                    if decisions.conflict(other_watch) {
+                        return Ok(Some(rule_id));
+                    }
+
+                    decisions.decide(other_watch, level, rule_id)?;
+                }
+            } else {
+                // Multi-conflict rule: all literals are watched
+                let rule_literals = rule.literals().to_vec();
+                for &other_literal in &rule_literals {
+                    if other_literal != literal && !decisions.satisfy(other_literal) {
+                        if decisions.conflict(other_literal) {
+                            return Ok(Some(rule_id));
+                        }
+                        decisions.decide(other_literal, level, rule_id)?;
+                    }
+                }
+            }
+
+            i += 1;
+            // Re-fetch chain in case it was modified
+            let chain_ref = self.watch_chains.get(&literal);
+            if chain_ref.is_none() || i >= chain_ref.unwrap().len() {
+                break;
+            }
+        }
+
+        Ok(None)
+    }
+
+    /// Move a watch node from one literal's chain to another's.
+    fn move_watch(&mut self, from_literal: Literal, to_literal: Literal, node_idx: usize) {
+        // Update the node's watch
+        let node = &mut self.nodes[node_idx];
+        if node.watch1 == from_literal {
+            node.watch1 = to_literal;
+        } else {
+            node.watch2 = to_literal;
+        }
+
+        // Remove from old chain
+        self.remove_from_chain(from_literal, node_idx);
+
+        // Add to new chain
+        self.watch_chains
+            .entry(to_literal)
+            .or_default()
+            .push(node_idx);
+    }
+
+    /// Remove a node from a literal's watch chain.
+    fn remove_from_chain(&mut self, literal: Literal, node_idx: usize) {
+        if let Some(chain) = self.watch_chains.get_mut(&literal) {
+            chain.retain(|&idx| idx != node_idx);
+        }
+    }
+
+    /// Get the last inserted node index (for watch2_on_highest after insert).
+    pub fn last_node_idx(&self) -> usize {
+        self.nodes.len() - 1
+    }
+}
+
+impl Default for RuleWatchGraph {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::rule::{ReasonData, Rule, RuleReason};
+    use crate::rule_set::RuleSet;
+
+    #[test]
+    fn test_insert_assertion_skipped() {
+        let mut graph = RuleWatchGraph::new();
+        let rule = Rule::new(vec![1], RuleReason::Fixed, ReasonData::None);
+        graph.insert(0, &rule);
+        assert_eq!(graph.nodes.len(), 0);
+    }
+
+    #[test]
+    fn test_insert_normal_rule() {
+        let mut graph = RuleWatchGraph::new();
+        let rule = Rule::new(vec![1, 2, 3], RuleReason::PackageRequires, ReasonData::None);
+        graph.insert(0, &rule);
+        assert_eq!(graph.nodes.len(), 1);
+        // Watches literals 1 and 2
+        assert!(graph.watch_chains.contains_key(&1));
+        assert!(graph.watch_chains.contains_key(&2));
+    }
+
+    #[test]
+    fn test_propagate_unit_clause() {
+        // Rule: (1 | 2). Decide -1, should force 2.
+        let mut rs = RuleSet::new();
+        rs.add(
+            Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None),
+            crate::rule::RuleType::Package,
+        );
+
+        let mut graph = RuleWatchGraph::new();
+        graph.insert(0, rs.rule_by_id(0));
+
+        let mut decisions = Decisions::new();
+        decisions.decide(-1, 1, 99).unwrap(); // don't install package 1
+
+        let conflict = graph.propagate_literal(-1, 1, &mut decisions, &rs).unwrap();
+        assert!(conflict.is_none());
+        // Package 2 should now be decided install
+        assert!(decisions.decided_install(2));
+    }
+
+    #[test]
+    fn test_propagate_conflict() {
+        // Rule: (1 | 2). Decide -1, then -2 should conflict.
+        let mut rs = RuleSet::new();
+        rs.add(
+            Rule::new(vec![1, 2], RuleReason::PackageRequires, ReasonData::None),
+            crate::rule::RuleType::Package,
+        );
+
+        let mut graph = RuleWatchGraph::new();
+        graph.insert(0, rs.rule_by_id(0));
+
+        let mut decisions = Decisions::new();
+        decisions.decide(-1, 1, 99).unwrap();
+        decisions.decide(-2, 1, 99).unwrap();
+
+        let conflict = graph.propagate_literal(-1, 1, &mut decisions, &rs).unwrap();
+        assert!(conflict.is_some());
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/solver.rs b/crates/mozart-sat-resolver/src/solver.rs
new file mode 100644
index 0000000..e52c913
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/solver.rs
@@ -0,0 +1,1008 @@
+use crate::decisions::Decisions;
+use crate::error::{SolverBugError, SolverError};
+use crate::policy::DefaultPolicy;
+use crate::pool::{Literal, PackageId, Pool, literal_to_package_id};
+use crate::problem::Problem;
+use crate::rule::{ReasonData, Rule, RuleReason, RuleType};
+use crate::rule_set::{RuleId, RuleSet};
+use crate::rule_watch_graph::RuleWatchGraph;
+use std::collections::{HashMap, HashSet};
+
+/// Result of solving: the list of package IDs to install.
+#[derive(Debug)]
+pub struct SolverResult {
+    /// Package IDs decided for installation.
+    pub installed: Vec<PackageId>,
+}
+
+/// Main SAT solver implementing CDCL (Conflict-Driven Clause Learning).
+///
+/// Port of Composer's Solver.php.
+pub struct Solver<'a> {
+    pool: &'a Pool,
+    policy: DefaultPolicy,
+    rules: RuleSet,
+    watch_graph: RuleWatchGraph,
+    decisions: Decisions,
+    /// Fixed packages by ID.
+    fixed_map: HashSet<PackageId>,
+    /// Current propagation index in decision queue.
+    propagate_index: usize,
+    /// Branch points: (alternative literals, decision level).
+    branches: Vec<(Vec<Literal>, i32)>,
+    /// Problems found during solving.
+    problems: Vec<Problem>,
+    /// Learned rule pool: for each learned rule, the chain of rules that led to it.
+    learned_pool: Vec<Vec<RuleId>>,
+    /// Map from rule ID → learned pool index.
+    learned_why: HashMap<RuleId, usize>,
+}
+
+impl<'a> Solver<'a> {
+    /// Create a new solver with the given rules, pool, policy, and fixed package set.
+    pub fn new(
+        rules: RuleSet,
+        pool: &'a Pool,
+        policy: DefaultPolicy,
+        fixed_packages: HashSet<PackageId>,
+    ) -> Self {
+        Solver {
+            pool,
+            policy,
+            rules,
+            watch_graph: RuleWatchGraph::new(),
+            decisions: Decisions::new(),
+            fixed_map: fixed_packages,
+            propagate_index: 0,
+            branches: Vec::new(),
+            problems: Vec::new(),
+            learned_pool: Vec::new(),
+            learned_why: HashMap::new(),
+        }
+    }
+
+    /// Solve the dependency resolution problem.
+    /// Returns the set of packages to install, or an error.
+    pub fn solve(mut self) -> Result<SolverResult, SolverError> {
+        // Insert all rules into watch graph
+        let rule_count = self.rules.len();
+        for id in 0..rule_count {
+            let rule = self.rules.rule_by_id(id);
+            self.watch_graph.insert(id, rule);
+        }
+
+        // Make decisions based on assertion rules (unit clauses)
+        self.make_assertion_rule_decisions()?;
+
+        // Run the main SAT loop
+        self.run_sat()?;
+
+        if !self.problems.is_empty() {
+            let messages: Vec<String> = self
+                .problems
+                .iter()
+                .map(|p| p.pretty_string(self.pool, &self.rules))
+                .collect();
+            return Err(SolverError::Unsolvable(messages));
+        }
+
+        // Collect installed packages
+        let mut installed = Vec::new();
+        for i in 0..self.decisions.len() {
+            let decision = self.decisions.at_offset(i);
+            if decision.literal > 0 {
+                installed.push(literal_to_package_id(decision.literal));
+            }
+        }
+
+        Ok(SolverResult { installed })
+    }
+
+    /// Process assertion rules (unit clauses) — make immediate decisions.
+    ///
+    /// Port of Composer's Solver::makeAssertionRuleDecisions.
+    fn make_assertion_rule_decisions(&mut self) -> Result<(), SolverError> {
+        let decision_start = if self.decisions.is_empty() {
+            0
+        } else {
+            self.decisions.len() - 1
+        };
+
+        let mut rule_index: usize = 0;
+        while rule_index < self.rules.len() {
+            let rule = self.rules.rule_by_id(rule_index);
+
+            if !rule.is_assertion() || rule.is_disabled() {
+                rule_index += 1;
+                continue;
+            }
+
+            let literal = rule.literals()[0];
+
+            if !self.decisions.decided(literal) {
+                self.decisions.decide(literal, 1, rule_index)?;
+                rule_index += 1;
+                continue;
+            }
+
+            if self.decisions.satisfy(literal) {
+                rule_index += 1;
+                continue;
+            }
+
+            // Found a conflict
+            let rule_type = self.rules.rule_by_id(rule_index).rule_type;
+
+            if rule_type == RuleType::Learned {
+                self.rules.rule_by_id_mut(rule_index).disable();
+                rule_index += 1;
+                continue;
+            }
+
+            let conflict_rule_id = self.decisions.decision_rule(literal)?;
+            let conflict_type = self.rules.rule_by_id(conflict_rule_id).rule_type;
+
+            if conflict_type == RuleType::Package {
+                let mut problem = Problem::new();
+                problem.add_rule(rule_index);
+                problem.add_rule(conflict_rule_id);
+                self.rules.rule_by_id_mut(rule_index).disable();
+                self.problems.push(problem);
+                rule_index += 1;
+                continue;
+            }
+
+            // Conflict with another root require/fixed package
+            let mut problem = Problem::new();
+            problem.add_rule(rule_index);
+            problem.add_rule(conflict_rule_id);
+
+            // Push all request assertion rules asserting this literal
+            let pkg_id = literal_to_package_id(literal);
+            let request_rule_ids: Vec<RuleId> = self
+                .rules
+                .iter_type(RuleType::Request)
+                .filter(|(_, r)| {
+                    !r.is_disabled()
+                        && r.is_assertion()
+                        && literal_to_package_id(r.literals()[0]) == pkg_id
+                })
+                .map(|(id, _)| id)
+                .collect();
+
+            for rid in &request_rule_ids {
+                problem.add_rule(*rid);
+            }
+            self.problems.push(problem);
+
+            for rid in request_rule_ids {
+                self.rules.rule_by_id_mut(rid).disable();
+            }
+
+            self.decisions.reset_to_offset(decision_start);
+            rule_index = 0; // restart
+        }
+
+        Ok(())
+    }
+
+    /// Unit propagation: propagate decisions through the watch graph.
+    ///
+    /// Port of Composer's Solver::propagate.
+    fn propagate(&mut self, level: i32) -> Result<Option<RuleId>, SolverBugError> {
+        while self.decisions.valid_offset(self.propagate_index) {
+            let decision = self.decisions.at_offset(self.propagate_index).clone();
+            self.propagate_index += 1;
+
+            let conflict = self.watch_graph.propagate_literal(
+                decision.literal,
+                level,
+                &mut self.decisions,
+                &self.rules,
+            )?;
+
+            if conflict.is_some() {
+                return Ok(conflict);
+            }
+        }
+
+        Ok(None)
+    }
+
+    /// Revert decisions to a given level.
+    ///
+    /// Port of Composer's Solver::revert.
+    fn revert(&mut self, level: i32) {
+        while !self.decisions.is_empty() {
+            let literal = self.decisions.last_literal();
+            if self.decisions.undecided(literal) {
+                break;
+            }
+            let decision_level = self.decisions.decision_level(literal);
+            if decision_level <= level {
+                break;
+            }
+            self.decisions.revert_last();
+            self.propagate_index = self.decisions.len();
+        }
+
+        while !self.branches.is_empty() && self.branches.last().unwrap().1 >= level {
+            self.branches.pop();
+        }
+    }
+
+    /// Make a decision, propagate, and learn from conflicts.
+    ///
+    /// Port of Composer's Solver::setPropagateLearn.
+    fn set_propagate_learn(
+        &mut self,
+        mut level: i32,
+        literal: Literal,
+        rule_id: RuleId,
+    ) -> Result<i32, SolverError> {
+        level += 1;
+        self.decisions.decide(literal, level, rule_id)?;
+
+        loop {
+            let conflict = self.propagate(level)?;
+
+            let Some(conflict_rule_id) = conflict else {
+                break;
+            };
+
+            if level == 1 {
+                self.analyze_unsolvable(conflict_rule_id);
+                return Ok(0);
+            }
+
+            // Conflict analysis
+            let (learn_literal, new_level, new_rule, why) =
+                self.analyze(level, conflict_rule_id)?;
+
+            if new_level <= 0 || new_level >= level {
+                return Err(SolverBugError {
+                    message: format!(
+                        "Trying to revert to invalid level {new_level} from level {level}."
+                    ),
+                }
+                .into());
+            }
+
+            level = new_level;
+            self.revert(level);
+
+            // Add learned rule
+            self.rules.add(new_rule, RuleType::Learned);
+            let new_rule_id = self.rules.len() - 1;
+
+            self.learned_why.insert(new_rule_id, why);
+
+            let rule_ref = self.rules.rule_by_id(new_rule_id);
+            self.watch_graph.insert(new_rule_id, rule_ref);
+
+            // Adjust watch2 to highest level literal
+            let last_node = self.watch_graph.last_node_idx();
+            let rule_for_watch = self.rules.rule_by_id(new_rule_id);
+            self.watch_graph
+                .watch2_on_highest(last_node, rule_for_watch, &self.decisions);
+
+            self.decisions.decide(learn_literal, level, new_rule_id)?;
+        }
+
+        Ok(level)
+    }
+
+    /// Choose best package from candidates and install.
+    ///
+    /// Port of Composer's Solver::selectAndInstall.
+    fn select_and_install(
+        &mut self,
+        level: i32,
+        decision_queue: Vec<Literal>,
+        rule_id: RuleId,
+    ) -> Result<i32, SolverError> {
+        let required_package = self
+            .rules
+            .rule_by_id(rule_id)
+            .required_package()
+            .map(|s| s.to_string());
+        let mut literals = self.policy.select_preferred_packages(
+            self.pool,
+            &decision_queue,
+            required_package.as_deref(),
+        );
+
+        let selected = literals.remove(0);
+
+        // If there are remaining alternatives, save as branch point
+        if !literals.is_empty() {
+            self.branches.push((literals, level));
+        }
+
+        self.set_propagate_learn(level, selected, rule_id)
+    }
+
+    /// First UIP conflict analysis.
+    ///
+    /// Port of Composer's Solver::analyze.
+    fn analyze(
+        &mut self,
+        level: i32,
+        conflict_rule_id: RuleId,
+    ) -> Result<(Literal, i32, Rule, usize), SolverError> {
+        let mut rule_level: i32 = 1;
+        let mut num: i32 = 0;
+        let mut l1num: i32 = 0;
+        let mut seen: HashSet<PackageId> = HashSet::new();
+        let mut learned_literal: Option<Literal> = None;
+        let mut other_learned_literals: Vec<Literal> = Vec::new();
+
+        let mut decision_id = self.decisions.len();
+
+        self.learned_pool.push(Vec::new());
+        let pool_idx = self.learned_pool.len() - 1;
+
+        let mut current_rule_id = conflict_rule_id;
+
+        loop {
+            self.learned_pool[pool_idx].push(current_rule_id);
+
+            let rule = self.rules.rule_by_id(current_rule_id);
+            let rule_literals = rule.literals().to_vec();
+            let is_multi_conflict = rule.is_multi_conflict;
+
+            for &literal in &rule_literals {
+                // MultiConflictRule: skip undecided literals
+                if is_multi_conflict && !self.decisions.decided(literal) {
+                    continue;
+                }
+
+                // Skip the one true literal
+                if self.decisions.satisfy(literal) {
+                    continue;
+                }
+
+                let pkg_id = literal_to_package_id(literal);
+                if seen.contains(&pkg_id) {
+                    continue;
+                }
+                seen.insert(pkg_id);
+
+                let l = self.decisions.decision_level(literal);
+
+                if l == 1 {
+                    l1num += 1;
+                } else if l == level {
+                    num += 1;
+                } else {
+                    other_learned_literals.push(literal);
+                    if l > rule_level {
+                        rule_level = l;
+                    }
+                }
+            }
+
+            // l1 retry loop
+            let mut l1retry = true;
+            while l1retry {
+                l1retry = false;
+
+                if num == 0 {
+                    l1num -= 1;
+                    if l1num == 0 {
+                        // All level 1 literals done
+                        let why = pool_idx;
+                        let ll = learned_literal.ok_or_else(|| SolverBugError {
+                            message: format!(
+                                "Did not find a learnable literal in analyzed rule {conflict_rule_id}."
+                            ),
+                        })?;
+
+                        let mut all_literals = vec![ll];
+                        all_literals.extend_from_slice(&other_learned_literals);
+
+                        let new_rule =
+                            Rule::new(all_literals, RuleReason::Learned, ReasonData::Learned(why));
+
+                        return Ok((ll, rule_level, new_rule, why));
+                    }
+                }
+
+                loop {
+                    if decision_id == 0 {
+                        return Err(SolverBugError {
+                            message: format!(
+                                "Reached invalid decision id 0 while analyzing rule {conflict_rule_id}."
+                            ),
+                        }
+                        .into());
+                    }
+
+                    decision_id -= 1;
+                    let decision = self.decisions.at_offset(decision_id);
+                    let literal = decision.literal;
+
+                    if seen.contains(&literal_to_package_id(literal)) {
+                        break;
+                    }
+                }
+
+                let decision = self.decisions.at_offset(decision_id);
+                let literal = decision.literal;
+
+                seen.remove(&literal_to_package_id(literal));
+
+                if num != 0 {
+                    num -= 1;
+                    if num == 0 {
+                        learned_literal = Some(-literal);
+
+                        if l1num == 0 {
+                            // Done
+                            let why = pool_idx;
+                            let ll = learned_literal.unwrap();
+
+                            let mut all_literals = vec![ll];
+                            all_literals.extend_from_slice(&other_learned_literals);
+
+                            let new_rule = Rule::new(
+                                all_literals,
+                                RuleReason::Learned,
+                                ReasonData::Learned(why),
+                            );
+
+                            return Ok((ll, rule_level, new_rule, why));
+                        }
+
+                        // Only level 1 marks left
+                        for other in &other_learned_literals {
+                            seen.remove(&literal_to_package_id(*other));
+                        }
+                        l1num += 1;
+                        l1retry = true;
+                    } else {
+                        let decision = self.decisions.at_offset(decision_id);
+                        let next_rule_id = decision.rule_id;
+                        let next_rule = self.rules.rule_by_id(next_rule_id);
+
+                        if next_rule.is_multi_conflict {
+                            // Handle multi-conflict rule
+                            let mcr_literals = next_rule.literals().to_vec();
+                            for &rule_literal in &mcr_literals {
+                                let pkg_id = literal_to_package_id(rule_literal);
+                                if !seen.contains(&pkg_id) && self.decisions.satisfy(-rule_literal)
+                                {
+                                    self.learned_pool[pool_idx].push(next_rule_id);
+                                    let l = self.decisions.decision_level(rule_literal);
+                                    if l == 1 {
+                                        l1num += 1;
+                                    } else if l == level {
+                                        num += 1;
+                                    } else {
+                                        other_learned_literals.push(rule_literal);
+                                        if l > rule_level {
+                                            rule_level = l;
+                                        }
+                                    }
+                                    seen.insert(pkg_id);
+                                    break;
+                                }
+                            }
+                            l1retry = true;
+                        }
+                    }
+                }
+            }
+
+            let decision = self.decisions.at_offset(decision_id);
+            current_rule_id = decision.rule_id;
+        }
+    }
+
+    /// Recursively collect rules involved in an unsolvable conflict.
+    fn analyze_unsolvable_rule(
+        &self,
+        problem: &mut Problem,
+        conflict_rule_id: RuleId,
+        rule_seen: &mut HashSet<RuleId>,
+    ) {
+        if rule_seen.contains(&conflict_rule_id) {
+            return;
+        }
+        rule_seen.insert(conflict_rule_id);
+
+        let rule = self.rules.rule_by_id(conflict_rule_id);
+
+        if rule.rule_type == RuleType::Learned {
+            if let Some(&why) = self.learned_why.get(&conflict_rule_id)
+                && let Some(problem_rules) = self.learned_pool.get(why)
+            {
+                for &pr_id in problem_rules {
+                    if !rule_seen.contains(&pr_id) {
+                        self.analyze_unsolvable_rule(problem, pr_id, rule_seen);
+                    }
+                }
+            }
+            return;
+        }
+
+        if rule.rule_type == RuleType::Package {
+            // Package rules cannot be part of a problem
+            return;
+        }
+
+        problem.next_section();
+        problem.add_rule(conflict_rule_id);
+    }
+
+    /// Analyze an unsolvable conflict at level 1.
+    ///
+    /// Port of Composer's Solver::analyzeUnsolvable.
+    fn analyze_unsolvable(&mut self, conflict_rule_id: RuleId) {
+        let mut problem = Problem::new();
+        problem.add_rule(conflict_rule_id);
+
+        let mut rule_seen = HashSet::new();
+        self.analyze_unsolvable_rule(&mut problem, conflict_rule_id, &mut rule_seen);
+
+        // Collect related decisions
+        let mut seen: HashSet<PackageId> = HashSet::new();
+        let conflict_literals = self.rules.rule_by_id(conflict_rule_id).literals().to_vec();
+        for &lit in &conflict_literals {
+            if self.decisions.satisfy(lit) {
+                continue;
+            }
+            seen.insert(literal_to_package_id(lit));
+        }
+
+        // Walk decisions in reverse
+        for i in (0..self.decisions.len()).rev() {
+            let decision = self.decisions.at_offset(i);
+            let dec_literal = decision.literal;
+            let pkg_id = literal_to_package_id(dec_literal);
+
+            if !seen.contains(&pkg_id) {
+                continue;
+            }
+
+            let why = decision.rule_id;
+            problem.add_rule(why);
+            self.analyze_unsolvable_rule(&mut problem, why, &mut rule_seen);
+
+            let why_literals = self.rules.rule_by_id(why).literals().to_vec();
+            for &lit in &why_literals {
+                if self.decisions.satisfy(lit) {
+                    continue;
+                }
+                seen.insert(literal_to_package_id(lit));
+            }
+        }
+
+        self.problems.push(problem);
+    }
+
+    /// Main SAT loop.
+    ///
+    /// Port of Composer's Solver::runSat.
+    fn run_sat(&mut self) -> Result<(), SolverError> {
+        self.propagate_index = 0;
+
+        let mut level: i32 = 1;
+        let mut system_level: i32 = level + 1;
+
+        loop {
+            // Step 1: propagate at level 1
+            if level == 1 {
+                let conflict = self.propagate(level)?;
+                if let Some(conflict_rule_id) = conflict {
+                    self.analyze_unsolvable(conflict_rule_id);
+                    return Ok(());
+                }
+            }
+
+            // Step 2: handle root require/fixed package rules
+            if level < system_level {
+                let mut made_decision = false;
+
+                // Collect request rule IDs first to avoid borrow issues
+                let request_rule_ids: Vec<RuleId> = self
+                    .rules
+                    .iter_type(RuleType::Request)
+                    .map(|(id, _)| id)
+                    .collect();
+
+                let mut all_satisfied = true;
+
+                for &rule_id in &request_rule_ids {
+                    let rule = self.rules.rule_by_id(rule_id);
+                    if !rule.is_enabled() {
+                        continue;
+                    }
+
+                    let mut decision_queue: Vec<Literal> = Vec::new();
+                    let mut none_satisfied = true;
+
+                    for &lit in rule.literals() {
+                        if self.decisions.satisfy(lit) {
+                            none_satisfied = false;
+                            break;
+                        }
+                        if lit > 0 && self.decisions.undecided(lit) {
+                            decision_queue.push(lit);
+                        }
+                    }
+
+                    if none_satisfied && !decision_queue.is_empty() {
+                        // Prune: prefer fixed packages
+                        let pruned: Vec<Literal> = decision_queue
+                            .iter()
+                            .filter(|&&lit| self.fixed_map.contains(&literal_to_package_id(lit)))
+                            .copied()
+                            .collect();
+
+                        if !pruned.is_empty() {
+                            decision_queue = pruned;
+                        }
+                    }
+
+                    if none_satisfied && !decision_queue.is_empty() {
+                        let old_level = level;
+                        level = self.select_and_install(level, decision_queue, rule_id)?;
+
+                        if level == 0 {
+                            return Ok(());
+                        }
+                        if level <= old_level {
+                            made_decision = true;
+                            break;
+                        }
+                    }
+
+                    // Check if there are more rules to process
+                    all_satisfied = false;
+                }
+
+                system_level = level + 1;
+
+                if made_decision || !all_satisfied {
+                    // Check if we still have unsatisfied request rules
+                    let has_unsatisfied = request_rule_ids.iter().any(|&rule_id| {
+                        let rule = self.rules.rule_by_id(rule_id);
+                        if !rule.is_enabled() {
+                            return false;
+                        }
+                        let mut none_satisfied = true;
+                        for &lit in rule.literals() {
+                            if self.decisions.satisfy(lit) {
+                                none_satisfied = false;
+                                break;
+                            }
+                        }
+                        if !none_satisfied {
+                            return false;
+                        }
+                        rule.literals()
+                            .iter()
+                            .any(|&lit| lit > 0 && self.decisions.undecided(lit))
+                    });
+
+                    if has_unsatisfied {
+                        continue;
+                    }
+                }
+            }
+
+            if level < system_level {
+                system_level = level;
+            }
+
+            // Step 3: fulfill all unresolved rules
+            let mut rules_count = self.rules.len();
+            let mut i: usize = 0;
+            let mut n: usize = 0;
+            let mut made_decision = false;
+
+            while n < rules_count {
+                if i == rules_count {
+                    i = 0;
+                }
+
+                let rule = self.rules.rule_by_id(i);
+                let literals = rule.literals().to_vec();
+
+                i += 1;
+                n += 1;
+
+                if rule.is_disabled() {
+                    continue;
+                }
+
+                let mut decision_queue: Vec<Literal> = Vec::new();
+                let mut skip = false;
+
+                for &lit in &literals {
+                    if lit <= 0 {
+                        if !self.decisions.decided_install(lit) {
+                            skip = true;
+                            break;
+                        }
+                    } else {
+                        if self.decisions.decided_install(lit) {
+                            skip = true;
+                            break;
+                        }
+                        if self.decisions.undecided(lit) {
+                            decision_queue.push(lit);
+                        }
+                    }
+                }
+
+                if skip {
+                    continue;
+                }
+
+                // Need at least 2 undecided positive literals
+                if decision_queue.len() < 2 {
+                    continue;
+                }
+
+                let rule_id = i - 1;
+                level = self.select_and_install(level, decision_queue, rule_id)?;
+
+                if level == 0 {
+                    return Ok(());
+                }
+
+                // Something changed, restart scan
+                rules_count = self.rules.len();
+                n = 0;
+                i = 0;
+                made_decision = true;
+            }
+
+            if level < system_level && made_decision {
+                continue;
+            }
+
+            // Step 4: minimization (backjumping)
+            if !self.branches.is_empty() {
+                let mut last_literal: Option<Literal> = None;
+                let mut last_level: Option<i32> = None;
+                let mut last_branch_index: usize = 0;
+                let mut last_branch_offset: usize = 0;
+
+                for i in (0..self.branches.len()).rev() {
+                    let (ref literals, l) = self.branches[i];
+                    for (offset, &literal) in literals.iter().enumerate() {
+                        if literal > 0 && self.decisions.decision_level(literal) > l + 1 {
+                            last_literal = Some(literal);
+                            last_branch_index = i;
+                            last_branch_offset = offset;
+                            last_level = Some(l);
+                        }
+                    }
+                }
+
+                if let Some(literal) = last_literal {
+                    let last_l = last_level.unwrap();
+
+                    self.branches[last_branch_index]
+                        .0
+                        .remove(last_branch_offset);
+
+                    level = last_l;
+                    self.revert(level);
+
+                    let why = self.decisions.last_reason();
+
+                    level = self.set_propagate_learn(level, literal, why)?;
+
+                    if level == 0 {
+                        return Ok(());
+                    }
+
+                    continue;
+                }
+            }
+
+            break;
+        }
+
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::pool::PoolPackageInput;
+    use crate::rule::{ReasonData, Rule, RuleReason, RuleType};
+
+    fn make_input(name: &str, version: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: version.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    /// Helper: create a simple problem and solve it.
+    /// Creates a pool with N dummy packages (1..=max_id).
+    fn make_rules_and_solve(
+        rules: Vec<(Rule, RuleType)>,
+        fixed: HashSet<PackageId>,
+        max_id: u32,
+    ) -> Result<SolverResult, SolverError> {
+        let mut rs = RuleSet::new();
+        for (rule, rt) in rules {
+            rs.add(rule, rt);
+        }
+        let inputs: Vec<_> = (1..=max_id)
+            .map(|i| make_input(&format!("pkg/{i}"), &format!("{i}.0.0.0")))
+            .collect();
+        let pool = Pool::new(inputs, vec![]);
+        let policy = DefaultPolicy::default();
+        let solver = Solver::new(rs, &pool, policy, fixed);
+        solver.solve()
+    }
+
+    #[test]
+    fn test_single_package_required() {
+        // Root requires package 1
+        let result = make_rules_and_solve(
+            vec![(
+                Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None),
+                RuleType::Request,
+            )],
+            HashSet::new(),
+            3,
+        )
+        .unwrap();
+
+        assert_eq!(result.installed, vec![1]);
+    }
+
+    #[test]
+    fn test_two_packages_required() {
+        // Root requires either package 1 or 2, and also requires 3
+        let result = make_rules_and_solve(
+            vec![
+                (
+                    Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+            ],
+            HashSet::new(),
+            3,
+        )
+        .unwrap();
+
+        assert!(result.installed.contains(&3));
+        // Should install one of 1 or 2
+        assert!(result.installed.contains(&1) || result.installed.contains(&2));
+    }
+
+    #[test]
+    fn test_dependency_chain() {
+        // Root requires 1. Package 1 requires 2.
+        // Rule for root: (1)
+        // Rule for dep: (-1 | 2)
+        let result = make_rules_and_solve(
+            vec![
+                (
+                    Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::new(vec![-1, 2], RuleReason::PackageRequires, ReasonData::None),
+                    RuleType::Package,
+                ),
+            ],
+            HashSet::new(),
+            3,
+        )
+        .unwrap();
+
+        assert!(result.installed.contains(&1));
+        assert!(result.installed.contains(&2));
+    }
+
+    #[test]
+    fn test_conflict_resolution() {
+        // Root requires 1 or 2. Package 1 conflicts with 3.
+        // Package 2 requires 3.
+        // Rules:
+        //   Request: (1 | 2)
+        //   Package: (-1 | -3)  -- conflict
+        //   Package: (-2 | 3)   -- dep
+        //   Request: (3)        -- root also requires 3
+        let result = make_rules_and_solve(
+            vec![
+                (
+                    Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::two_literals(-1, -3, RuleReason::PackageConflict, ReasonData::None),
+                    RuleType::Package,
+                ),
+                (
+                    Rule::new(vec![-2, 3], RuleReason::PackageRequires, ReasonData::None),
+                    RuleType::Package,
+                ),
+                (
+                    Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+            ],
+            HashSet::new(),
+            3,
+        )
+        .unwrap();
+
+        // Package 3 is required, so 1 conflicts, must choose 2
+        assert!(result.installed.contains(&2));
+        assert!(result.installed.contains(&3));
+        assert!(!result.installed.contains(&1));
+    }
+
+    #[test]
+    fn test_same_name_conflict() {
+        // Two versions of same package: 1 and 2. Root requires either.
+        // Same-name rule: (-1 | -2)
+        let result = make_rules_and_solve(
+            vec![
+                (
+                    Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::two_literals(-1, -2, RuleReason::PackageSameName, ReasonData::None),
+                    RuleType::Package,
+                ),
+            ],
+            HashSet::new(),
+            3,
+        )
+        .unwrap();
+
+        // Should install exactly one
+        let has_1 = result.installed.contains(&1);
+        let has_2 = result.installed.contains(&2);
+        assert!(has_1 ^ has_2, "Should install exactly one of 1 or 2");
+    }
+
+    #[test]
+    fn test_unsolvable() {
+        // Root requires 1. Root requires 2. But 1 and 2 conflict.
+        let result = make_rules_and_solve(
+            vec![
+                (
+                    Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::new(vec![2], RuleReason::RootRequire, ReasonData::None),
+                    RuleType::Request,
+                ),
+                (
+                    Rule::two_literals(-1, -2, RuleReason::PackageConflict, ReasonData::None),
+                    RuleType::Package,
+                ),
+            ],
+            HashSet::new(),
+            3,
+        );
+
+        assert!(result.is_err());
+    }
+}
diff --git a/crates/mozart-sat-resolver/src/transaction.rs b/crates/mozart-sat-resolver/src/transaction.rs
new file mode 100644
index 0000000..6462870
--- /dev/null
+++ b/crates/mozart-sat-resolver/src/transaction.rs
@@ -0,0 +1,555 @@
+use crate::decisions::Decisions;
+use crate::pool::{PackageId, Pool, literal_to_package_id};
+use std::collections::{HashMap, HashSet};
+
+/// An operation to perform on a package.
+///
+/// Port of Composer's SolverOperation hierarchy.
+#[derive(Debug, Clone)]
+pub enum Operation {
+    /// Install a new package.
+    Install { package_id: PackageId },
+    /// Update a package from one version to another.
+    Update {
+        initial_id: PackageId,
+        target_id: PackageId,
+    },
+    /// Remove a package.
+    Uninstall { package_id: PackageId },
+}
+
+impl Operation {
+    /// Get the operation type as a string.
+    pub fn operation_type(&self) -> &'static str {
+        match self {
+            Operation::Install { .. } => "install",
+            Operation::Update { .. } => "update",
+            Operation::Uninstall { .. } => "uninstall",
+        }
+    }
+
+    /// Format the operation as a human-readable string using pool data.
+    pub fn pretty_string(&self, pool: &Pool) -> String {
+        match self {
+            Operation::Install { package_id } => {
+                let pkg = pool.package_by_id(*package_id);
+                format!("Installing {} ({})", pkg.name, pkg.pretty_version)
+            }
+            Operation::Update {
+                initial_id,
+                target_id,
+            } => {
+                let initial = pool.package_by_id(*initial_id);
+                let target = pool.package_by_id(*target_id);
+                format!(
+                    "Updating {} ({} => {})",
+                    target.name, initial.pretty_version, target.pretty_version
+                )
+            }
+            Operation::Uninstall { package_id } => {
+                let pkg = pool.package_by_id(*package_id);
+                format!("Removing {} ({})", pkg.name, pkg.pretty_version)
+            }
+        }
+    }
+}
+
+/// Computes install/update/remove operations from solver results.
+///
+/// Port of Composer's Transaction.php.
+pub struct Transaction<'a> {
+    pool: &'a Pool,
+    /// Currently installed package IDs.
+    present_ids: Vec<PackageId>,
+    /// Result package IDs from the solver.
+    result_ids: Vec<PackageId>,
+    /// Computed operations.
+    operations: Vec<Operation>,
+}
+
+impl<'a> Transaction<'a> {
+    /// Create a new transaction from present and result package sets.
+    pub fn new(pool: &'a Pool, present_ids: Vec<PackageId>, result_ids: Vec<PackageId>) -> Self {
+        let mut tx = Transaction {
+            pool,
+            present_ids,
+            result_ids,
+            operations: Vec::new(),
+        };
+        tx.calculate_operations();
+        tx
+    }
+
+    /// Create a transaction from solver decisions.
+    pub fn from_decisions(
+        pool: &'a Pool,
+        present_ids: Vec<PackageId>,
+        decisions: &Decisions,
+    ) -> Self {
+        let mut result_ids = Vec::new();
+        for i in 0..decisions.len() {
+            let decision = decisions.at_offset(i);
+            if decision.literal > 0 {
+                result_ids.push(literal_to_package_id(decision.literal));
+            }
+        }
+        Self::new(pool, present_ids, result_ids)
+    }
+
+    /// Get the computed operations.
+    pub fn operations(&self) -> &[Operation] {
+        &self.operations
+    }
+
+    /// Calculate the delta between present and result packages.
+    fn calculate_operations(&mut self) {
+        // Build maps: name -> package_id for present packages
+        let mut present_by_name: HashMap<&str, PackageId> = HashMap::new();
+        for &id in &self.present_ids {
+            let pkg = self.pool.package_by_id(id);
+            present_by_name.insert(&pkg.name, id);
+        }
+
+        // Track which present packages have been matched
+        let mut matched_present: HashSet<PackageId> = HashSet::new();
+
+        // Build topologically sorted result packages via DFS
+        let sorted_results = self.topological_sort();
+
+        // Process result packages in topological order
+        for &result_id in &sorted_results {
+            let result_pkg = self.pool.package_by_id(result_id);
+
+            if let Some(&present_id) = present_by_name.get(result_pkg.name.as_str()) {
+                matched_present.insert(present_id);
+                let present_pkg = self.pool.package_by_id(present_id);
+
+                // Check if update is needed (version changed)
+                if present_pkg.version != result_pkg.version || present_id != result_id {
+                    self.operations.push(Operation::Update {
+                        initial_id: present_id,
+                        target_id: result_id,
+                    });
+                }
+                // Otherwise: no change needed, skip
+            } else {
+                // New package: install
+                self.operations.push(Operation::Install {
+                    package_id: result_id,
+                });
+            }
+        }
+
+        // Remove packages that are present but not in result
+        let mut uninstalls = Vec::new();
+        for &present_id in &self.present_ids {
+            if !matched_present.contains(&present_id) {
+                uninstalls.push(Operation::Uninstall {
+                    package_id: present_id,
+                });
+            }
+        }
+
+        // Prepend uninstalls (remove before install/update)
+        uninstalls.append(&mut self.operations);
+        self.operations = uninstalls;
+    }
+
+    /// Topologically sort result packages by their dependency order.
+    /// Uses DFS: dependencies are processed before dependents.
+    fn topological_sort(&self) -> Vec<PackageId> {
+        let result_set: HashSet<PackageId> = self.result_ids.iter().copied().collect();
+        let result_by_name: HashMap<&str, Vec<PackageId>> = {
+            let mut map: HashMap<&str, Vec<PackageId>> = HashMap::new();
+            for &id in &self.result_ids {
+                let pkg = self.pool.package_by_id(id);
+                map.entry(&pkg.name).or_default().push(id);
+            }
+            map
+        };
+
+        let mut visited: HashSet<PackageId> = HashSet::new();
+        let mut order: Vec<PackageId> = Vec::new();
+
+        // Find root packages (not required by any other result package)
+        let roots = self.get_root_packages(&result_set, &result_by_name);
+
+        // DFS from roots
+        let mut stack: Vec<(PackageId, bool)> = Vec::new();
+        for &root_id in roots.iter().rev() {
+            stack.push((root_id, false));
+        }
+
+        while let Some((pkg_id, processed)) = stack.pop() {
+            if processed {
+                if visited.insert(pkg_id) {
+                    order.push(pkg_id);
+                }
+                continue;
+            }
+
+            if visited.contains(&pkg_id) {
+                continue;
+            }
+
+            // Push self as "processed" marker
+            stack.push((pkg_id, true));
+
+            // Push dependencies
+            let pkg = self.pool.package_by_id(pkg_id);
+            for req in &pkg.requires {
+                if let Some(provider_ids) = result_by_name.get(req.target.as_str()) {
+                    for &dep_id in provider_ids {
+                        if !visited.contains(&dep_id) {
+                            stack.push((dep_id, false));
+                        }
+                    }
+                }
+            }
+        }
+
+        // Add any remaining unvisited packages
+        for &id in &self.result_ids {
+            if !visited.contains(&id) {
+                order.push(id);
+            }
+        }
+
+        order
+    }
+
+    /// Find root packages: result packages not required by any other result package.
+    fn get_root_packages(
+        &self,
+        result_set: &HashSet<PackageId>,
+        _result_by_name: &HashMap<&str, Vec<PackageId>>,
+    ) -> Vec<PackageId> {
+        // Collect all required package names
+        let mut required_names: HashSet<&str> = HashSet::new();
+        for &id in result_set {
+            let pkg = self.pool.package_by_id(id);
+            for req in &pkg.requires {
+                required_names.insert(&req.target);
+            }
+        }
+
+        // Root packages are those whose name is NOT in required_names
+        let mut roots: Vec<PackageId> = Vec::new();
+        for &id in &self.result_ids {
+            let pkg = self.pool.package_by_id(id);
+            if !required_names.contains(pkg.name.as_str()) {
+                roots.push(id);
+            }
+        }
+
+        // If no roots found (circular), use all
+        if roots.is_empty() {
+            return self.result_ids.clone();
+        }
+
+        roots
+    }
+}
+
+/// Lock transaction: specialization for computing lock file operations.
+///
+/// Port of Composer's LockTransaction.php.
+pub struct LockTransaction<'a> {
+    /// The base transaction.
+    transaction: Transaction<'a>,
+    /// Package IDs that cannot be updated (platform, root, fixed repos).
+    #[allow(dead_code)]
+    unlockable_ids: HashSet<PackageId>,
+    /// All result package IDs.
+    all_result_ids: Vec<PackageId>,
+    /// Non-dev result package IDs.
+    non_dev_ids: Vec<PackageId>,
+    /// Dev result package IDs.
+    dev_ids: Vec<PackageId>,
+}
+
+impl<'a> LockTransaction<'a> {
+    /// Create a lock transaction from solver decisions.
+    pub fn new(
+        pool: &'a Pool,
+        present_ids: Vec<PackageId>,
+        unlockable_ids: HashSet<PackageId>,
+        decisions: &Decisions,
+    ) -> Self {
+        // Extract result packages from decisions
+        let mut all_result_ids = Vec::new();
+        let mut non_dev_ids = Vec::new();
+        for i in 0..decisions.len() {
+            let decision = decisions.at_offset(i);
+            if decision.literal > 0 {
+                let pkg_id = literal_to_package_id(decision.literal);
+                all_result_ids.push(pkg_id);
+                if !unlockable_ids.contains(&pkg_id) {
+                    non_dev_ids.push(pkg_id);
+                }
+            }
+        }
+
+        let transaction = Transaction::new(pool, present_ids, all_result_ids.clone());
+
+        LockTransaction {
+            transaction,
+            unlockable_ids,
+            all_result_ids,
+            non_dev_ids,
+            dev_ids: Vec::new(),
+        }
+    }
+
+    /// Set the non-dev packages from an extraction-only solve result.
+    /// `extraction_ids` are the package IDs that were resolved without dev deps.
+    pub fn set_non_dev_packages(&mut self, extraction_ids: &[PackageId]) {
+        let extraction_names: HashSet<String> = extraction_ids
+            .iter()
+            .map(|&id| self.transaction.pool.package_by_id(id).name.clone())
+            .collect();
+
+        self.non_dev_ids.clear();
+        self.dev_ids.clear();
+
+        for &id in &self.all_result_ids {
+            let pkg = self.transaction.pool.package_by_id(id);
+            if extraction_names.contains(&pkg.name) {
+                self.non_dev_ids.push(id);
+            } else {
+                self.dev_ids.push(id);
+            }
+        }
+    }
+
+    /// Get the computed operations.
+    pub fn operations(&self) -> &[Operation] {
+        self.transaction.operations()
+    }
+
+    /// Get all result package IDs.
+    pub fn all_result_ids(&self) -> &[PackageId] {
+        &self.all_result_ids
+    }
+
+    /// Get non-dev result package IDs.
+    pub fn non_dev_ids(&self) -> &[PackageId] {
+        &self.non_dev_ids
+    }
+
+    /// Get dev result package IDs.
+    pub fn dev_ids(&self) -> &[PackageId] {
+        &self.dev_ids
+    }
+
+    /// Get new lock packages for writing to the lock file.
+    /// If `dev_mode` is true, returns dev packages; otherwise non-dev.
+    pub fn new_lock_package_ids(&self, dev_mode: bool) -> &[PackageId] {
+        if dev_mode {
+            &self.dev_ids
+        } else {
+            &self.non_dev_ids
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::pool::{PoolLink, PoolPackageInput};
+
+    fn make_input(name: &str, version: &str, pretty: &str) -> PoolPackageInput {
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: pretty.to_string(),
+            requires: vec![],
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    fn make_input_with_deps(
+        name: &str,
+        version: &str,
+        pretty: &str,
+        deps: Vec<(&str, &str)>,
+    ) -> PoolPackageInput {
+        let requires = deps
+            .into_iter()
+            .map(|(target, constraint)| PoolLink {
+                target: target.to_string(),
+                constraint: constraint.to_string(),
+                source: name.to_string(),
+            })
+            .collect();
+
+        PoolPackageInput {
+            name: name.to_string(),
+            version: version.to_string(),
+            pretty_version: pretty.to_string(),
+            requires,
+            replaces: vec![],
+            provides: vec![],
+            conflicts: vec![],
+            is_fixed: false,
+        }
+    }
+
+    #[test]
+    fn test_fresh_install() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0", "1.0.0"),
+                make_input("b/b", "2.0.0.0", "2.0.0"),
+            ],
+            vec![],
+        );
+
+        let tx = Transaction::new(&pool, vec![], vec![1, 2]);
+        let ops = tx.operations();
+
+        assert_eq!(ops.len(), 2);
+        assert!(matches!(ops[0], Operation::Install { package_id: _ }));
+        assert!(matches!(ops[1], Operation::Install { package_id: _ }));
+    }
+
+    #[test]
+    fn test_update_package() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0", "1.0.0"),
+                make_input("a/a", "2.0.0.0", "2.0.0"),
+            ],
+            vec![],
+        );
+
+        // Present: a/a 1.0.0 (id=1), Result: a/a 2.0.0 (id=2)
+        let tx = Transaction::new(&pool, vec![1], vec![2]);
+        let ops = tx.operations();
+
+        assert_eq!(ops.len(), 1);
+        match &ops[0] {
+            Operation::Update {
+                initial_id,
+                target_id,
+            } => {
+                assert_eq!(*initial_id, 1);
+                assert_eq!(*target_id, 2);
+            }
+            _ => panic!("Expected update operation"),
+        }
+    }
+
+    #[test]
+    fn test_uninstall_package() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0", "1.0.0"),
+                make_input("b/b", "1.0.0.0", "1.0.0"),
+            ],
+            vec![],
+        );
+
+        // Present: a/a and b/b, Result: only a/a
+        let tx = Transaction::new(&pool, vec![1, 2], vec![1]);
+        let ops = tx.operations();
+
+        assert_eq!(ops.len(), 1);
+        match &ops[0] {
+            Operation::Uninstall { package_id } => {
+                assert_eq!(*package_id, 2);
+            }
+            _ => panic!("Expected uninstall operation"),
+        }
+    }
+
+    #[test]
+    fn test_uninstalls_before_installs() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0", "1.0.0"),
+                make_input("b/b", "1.0.0.0", "1.0.0"),
+            ],
+            vec![],
+        );
+
+        // Present: a/a, Result: b/b (uninstall a, install b)
+        let tx = Transaction::new(&pool, vec![1], vec![2]);
+        let ops = tx.operations();
+
+        assert_eq!(ops.len(), 2);
+        assert!(
+            matches!(ops[0], Operation::Uninstall { .. }),
+            "Uninstalls should come first"
+        );
+        assert!(
+            matches!(ops[1], Operation::Install { .. }),
+            "Installs should come after"
+        );
+    }
+
+    #[test]
+    fn test_dependency_ordering() {
+        // a/a requires b/b — b/b should be installed before a/a
+        let pool = Pool::new(
+            vec![
+                make_input_with_deps("a/a", "1.0.0.0", "1.0.0", vec![("b/b", "^1.0")]),
+                make_input("b/b", "1.0.0.0", "1.0.0"),
+            ],
+            vec![],
+        );
+
+        let tx = Transaction::new(&pool, vec![], vec![1, 2]);
+        let ops = tx.operations();
+
+        assert_eq!(ops.len(), 2);
+        // b/b (dependency) should be installed before a/a
+        match (&ops[0], &ops[1]) {
+            (
+                Operation::Install { package_id: first },
+                Operation::Install { package_id: second },
+            ) => {
+                assert_eq!(*first, 2, "b/b should be installed first");
+                assert_eq!(*second, 1, "a/a should be installed second");
+            }
+            _ => panic!("Expected two install operations"),
+        }
+    }
+
+    #[test]
+    fn test_no_change() {
+        let pool = Pool::new(vec![make_input("a/a", "1.0.0.0", "1.0.0")], vec![]);
+
+        // Same package present and in result
+        let tx = Transaction::new(&pool, vec![1], vec![1]);
+        let ops = tx.operations();
+
+        assert!(ops.is_empty(), "No operations when nothing changed");
+    }
+
+    #[test]
+    fn test_operation_pretty_string() {
+        let pool = Pool::new(
+            vec![
+                make_input("a/a", "1.0.0.0", "1.0.0"),
+                make_input("a/a", "2.0.0.0", "2.0.0"),
+            ],
+            vec![],
+        );
+
+        let install = Operation::Install { package_id: 1 };
+        assert_eq!(install.pretty_string(&pool), "Installing a/a (1.0.0)");
+
+        let update = Operation::Update {
+            initial_id: 1,
+            target_id: 2,
+        };
+        assert_eq!(update.pretty_string(&pool), "Updating a/a (1.0.0 => 2.0.0)");
+
+        let uninstall = Operation::Uninstall { package_id: 1 };
+        assert_eq!(uninstall.pretty_string(&pool), "Removing a/a (1.0.0)");
+    }
+}