From 84d137a19feb1f79f5bd711faff63a6bbe651cbf Mon Sep 17 00:00:00 2001
From: nsfisis <nsfisis@gmail.com>
Date: Sun, 22 Feb 2026 18:25:16 +0900
Subject: feat(resolver): replace pubgrub with Composer-ported SAT solver
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 crates/mozart-sat-resolver/src/error.rs | 50 +++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 crates/mozart-sat-resolver/src/error.rs

(limited to 'crates/mozart-sat-resolver/src/error.rs')

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)
+    }
+}
-- 
cgit v1.3.1