refactor(graphs): remove unused coloring workflow (#1308)

Author: morluto

src/jacobian/contracts/graph_coloring.py

@@ -6,9 +6,7 @@
 
 from pydantic import Field, StrictInt, StringConstraints, model_validator
 
-from jacobian.contracts.common import ArtifactUri, Sha256Digest
 from jacobian.contracts.results import ContractModel
-from jacobian.contracts.sat import CanonicalCnf
 
 GraphVertex = Annotated[
     str,
@@ -41,71 +39,6 @@ def require_simple_graph(self) -> Self:
         return self
 
 
-class GraphColoringEncodingRequest(ContractModel):
-    """Materialize the exact CNF semantics of k-colorability."""
-
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-
-
-class GraphColoringEncodingClaim(ContractModel):
-    """Claim that one graph/color-count pair has a canonical encoding."""
-
-    claim_schema_version: Literal["1"] = "1"
-    predicate: Literal["GRAPH_K_COLORABILITY_ENCODING"] = (
-        "GRAPH_K_COLORABILITY_ENCODING"
-    )
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-
-
-class GraphColoringEncodingScope(ContractModel):
-    """Graph-owned scope binding the encoding to the SAT CNF artifact."""
-
-    scope_schema_version: Literal["1"] = "1"
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-    cnf_uri: ArtifactUri
-    cnf_object_digest: Sha256Digest
-    cnf: CanonicalCnf
-
-
-class GraphColoringEncodingCandidate(ContractModel):
-    """Pointer candidate checked against the graph-owned encoding scope."""
-
-    candidate_schema_version: Literal["1"] = "1"
-    cnf_uri: ArtifactUri
-    scope_uri: ArtifactUri
-
-
-class GraphColoringEncodingReplay(ContractModel):
-    """Certificate payload for independent graph-to-CNF replay."""
-
-    method: Literal["INDEPENDENT_GRAPH_COLORING_CNF_REPLAY"] = (
-        "INDEPENDENT_GRAPH_COLORING_CNF_REPLAY"
-    )
-    claim_uri: ArtifactUri
-    candidate_uri: ArtifactUri
-    scope_uri: ArtifactUri
-
-
-class GraphColoringEncodingOutput(ContractModel):
-    """Materialized encoding and its replay certificate."""
-
-    graph: ChromaticGraph
-    colors: StrictInt = Field(ge=1, le=32)
-    cnf_uri: ArtifactUri
-    scope_uri: ArtifactUri
-    claim_uri: ArtifactUri
-    candidate_uri: ArtifactUri
-    certificate_uri: ArtifactUri
-    variable_count: StrictInt = Field(ge=0, le=1_000_000)
-    clause_count: StrictInt = Field(ge=0, le=1_000_000)
-    encoding_version: Literal["exactly-one-and-edge-separation/v1"] = (
-        "exactly-one-and-edge-separation/v1"
-    )
-
-
 class ChromaticNumberBudget(ContractModel):
     """Total wall-clock budget for the bounded coloring search."""
 

src/jacobian/domains/graph_optimization/operations.py

@@ -10,7 +10,53 @@
     ChromaticSearchStep,
     GraphChromaticNumberOutput,
 )
-from jacobian.graphs.coloring_semantics import canonical_graph, coloring_cnf
+
+
+def canonical_graph(graph: ChromaticGraph) -> ChromaticGraph:
+    """Normalize vertex and undirected edge order for solver input."""
+
+    edges = tuple(
+        sorted(
+            (min(edge_left, edge_right), max(edge_left, edge_right))
+            for edge_left, edge_right in graph.edges
+        )
+    )
+    return ChromaticGraph(vertices=tuple(sorted(graph.vertices)), edges=edges)
+
+
+def coloring_cnf(
+    graph: ChromaticGraph,
+    colors: int,
+) -> tuple[tuple[str, ...], tuple[tuple[int, ...], ...]]:
+    """Build exactly-one and edge-separation clauses for one graph and k."""
+
+    variable_names = tuple(
+        f"v{vertex:02d}_c{color:02d}"
+        for vertex in range(len(graph.vertices))
+        for color in range(colors)
+    )
+
+    def variable(vertex: int, color: int) -> int:
+        return vertex * colors + color + 1
+
+    clauses: list[tuple[int, ...]] = []
+    for vertex in range(len(graph.vertices)):
+        clauses.append(tuple(variable(vertex, color) for color in range(colors)))
+        for color_left in range(colors):
+            for color_right in range(color_left + 1, colors):
+                clauses.append(
+                    (-variable(vertex, color_left), -variable(vertex, color_right))
+                )
+    vertex_index = {vertex: index for index, vertex in enumerate(graph.vertices)}
+    for edge_left, edge_right in graph.edges:
+        for color in range(colors):
+            clauses.append(
+                (
+                    -variable(vertex_index[edge_left], color),
+                    -variable(vertex_index[edge_right], color),
+                )
+            )
+    return variable_names, tuple(clauses)
 
 
 def build_simple_graph(graph: ChromaticGraph) -> Any:

src/jacobian/graphs/__init__.py

@@ -1,9 +1,5 @@
-"""Graph construction, property, coloring, and composition capabilities."""
+"""Graph construction, property, and composition capabilities."""
 
-from jacobian.graphs.coloring import (
-    GraphColoringInstallation,
-    install_graph_coloring_capabilities,
-)
 from jacobian.graphs.composition import (
     GraphCompositionInstallation,
     install_graph_composition_capabilities,
@@ -15,12 +11,10 @@
 )
 
 __all__ = [
-    "GraphColoringInstallation",
     "GraphCompositionInstallation",
     "GraphInstallation",
     "GraphIsomorphismInstallation",
     "install_graph_capabilities",
-    "install_graph_coloring_capabilities",
     "install_graph_composition_capabilities",
     "install_graph_isomorphism",
 ]