From 87c6dcf92d39916549ff60714a9a2402b9d06b11 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 12:41:29 +0800 Subject: [PATCH 1/4] Add plan for #1099: KColoring to Satisfiability --- .../2026-08-02-kcoloring-to-satisfiability.md | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 docs/plans/2026-08-02-kcoloring-to-satisfiability.md diff --git a/docs/plans/2026-08-02-kcoloring-to-satisfiability.md b/docs/plans/2026-08-02-kcoloring-to-satisfiability.md new file mode 100644 index 000000000..e62aa8abb --- /dev/null +++ b/docs/plans/2026-08-02-kcoloring-to-satisfiability.md @@ -0,0 +1,47 @@ +# Implement KColoring to Satisfiability reduction + +Issue: #1099 + +Base commit: `a9067297c9b7759b4f1139692553a465de49fed3` + +Reference: Daniel Faber, Adalat Jabrayilov, and Petra Mutzel, “SAT Encoding of Partial Ordering Models for Graph Coloring Problems,” SAT 2024, Section 2.2, DOI `10.4230/LIPIcs.SAT.2024.12`. + +## Required behavior + +For `KColoring` with `n` vertices, `m` stored edges, and runtime color count `k`, construct a `Satisfiability` instance with Boolean variable `x[v,c]` at one-based SAT index `v * k + c + 1`: + +1. For every vertex `v`, add the at-least-one clause `(x[v,0] ∨ ... ∨ x[v,k-1])`. +2. For every vertex `v` and pair `a < b`, add `(¬x[v,a] ∨ ¬x[v,b])`. +3. For every stored edge `(u,v)` and color `c`, add `(¬x[u,c] ∨ ¬x[v,c])`. +4. Extract one source color per vertex by finding the true variable in its `k`-wide block. + +Register only the runtime `KN` / `SimpleGraph` endpoint as the primitive reduction. The exact target sizes are: + +- `num_vars = num_vertices * num_colors` +- `num_clauses = num_vertices + num_vertices * num_colors * (num_colors - 1) / 2 + num_edges * num_colors` +- `num_literals = num_vertices * num_colors + num_vertices * num_colors * (num_colors - 1) + 2 * num_edges * num_colors` + +The construction must preserve the repository's complete legal domain: empty graphs, `k = 0`, isolated vertices, disconnected graphs, self-loops, parallel edges, and `k > n`. + +## Batch 1: verification and Rust implementation + +Follow `.claude/skills/add-rule/SKILL.md` Steps 0–5 and Step 7, including the default mathematical verification in `.claude/skills/verify-reduction/SKILL.md`. + +1. Produce an ephemeral standalone Typst proof with independent forward and backward correctness directions, extraction, exact overhead, a feasible five-cycle example with `k = 3`, and an infeasible five-cycle example with `k = 2`. +2. Produce and run an ephemeral constructor verifier with symbolic overhead checks, exhaustive/simple-graph feasibility agreement through five vertices, extraction checks for every satisfying assignment tested, exact target-size checks, structural checks, and at least 5,000 checks. +3. Independently adversarially verify the proof with a separately written constructor/extractor, exhaustive tests through five vertices, two Hypothesis strategies, at least 5,000 checks, and cross-comparison against the constructor verifier. +4. Add `src/rules/kcoloring_satisfiability.rs` containing the direct `ReductionResult`, `ReduceTo` implementation, exact `#[reduction(overhead = ...)]` metadata, construction, extraction, and the linked test module. Use `CNFClause` and the target's signed one-based literal convention directly. +5. Register the module in `src/rules/mod.rs` with no new dispatch or compatibility layer. +6. Add `src/unit_tests/rules/kcoloring_satisfiability.rs`. Cover the semantic closed loop, exact clause families and sizes, extraction, five-cycle `k=3`/`k=2`, empty `n=0,k=0`, nonempty `k=0`, isolated vertices, self-loop infeasibility, parallel-edge clause duplication, and `k>n`. Keep each test below five seconds. +7. Add the canonical C5 `k=3` rule example through the rule module's `canonical_rule_example_specs()`, using source colors `[0,1,0,1,2]` and the corresponding 15-bit one-hot SAT assignment. +8. Run focused tests, format checks, graph/schema exports, fixture regeneration, and `make test clippy`. Do not commit ephemeral verification scripts or generated ignored documentation exports. + +## Batch 2: paper documentation and final verification + +Follow `.claude/skills/add-rule/SKILL.md` Step 6 with fresh context after Batch 1 is complete. + +1. Add the Faber–Jabrayilov–Mutzel SAT 2024 BibTeX entry to `docs/paper/references.bib` if it is not already present. +2. Add a `reduction-rule("KColoring", "Satisfiability", ...)` entry to `docs/paper/reductions.typ` based on the verified proof. State the construction, both correctness directions, variable mapping, extraction, and exact scaling. Explicitly distinguish the standard positive-`k`, loop-free literature domain from the repository edge cases handled by the same clauses. +3. Build a fixture-driven tutorial example for C5 with `k=3`. Start the extra block with `pred-commands()` derived from the loaded example, show the 15 variables and 35 clauses, verify `[0,1,0,1,2]` end to end, and explain witness multiplicity without relying on fixture solution counts. +4. Regenerate graph/schema exports and example fixtures after the documentation is connected, then run `make paper`, `make fmt-check`, `make test`, and `make clippy`. +5. Inspect the final diff and working tree. Keep only files directly required by #1099, delete this plan file before the final push, and leave the branch clean. From 0e5429e677e816d0072e1d393af6eeb6776a820c Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:16:23 +0800 Subject: [PATCH 2/4] Implement #1099: KColoring to Satisfiability --- src/rules/kcoloring_satisfiability.rs | 112 ++++++++++++ src/rules/mod.rs | 2 + .../rules/kcoloring_satisfiability.rs | 173 ++++++++++++++++++ 3 files changed, 287 insertions(+) create mode 100644 src/rules/kcoloring_satisfiability.rs create mode 100644 src/unit_tests/rules/kcoloring_satisfiability.rs diff --git a/src/rules/kcoloring_satisfiability.rs b/src/rules/kcoloring_satisfiability.rs new file mode 100644 index 000000000..922d816a9 --- /dev/null +++ b/src/rules/kcoloring_satisfiability.rs @@ -0,0 +1,112 @@ +//! Reduction from graph K-Coloring to Boolean Satisfiability. + +use crate::models::formula::{CNFClause, Satisfiability}; +use crate::models::graph::KColoring; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::variant::KN; + +/// Result of reducing K-Coloring to Satisfiability. +#[derive(Debug, Clone)] +pub struct ReductionKColoringToSatisfiability { + target: Satisfiability, + num_vertices: usize, + num_colors: usize, +} + +impl ReductionResult for ReductionKColoringToSatisfiability { + type Source = KColoring; + type Target = Satisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + (0..self.num_vertices) + .map(|vertex| { + let start = vertex * self.num_colors; + target_solution[start..start + self.num_colors] + .iter() + .position(|&value| value == 1) + .expect("satisfying assignment must select one color per vertex") + }) + .collect() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices * num_colors", + num_clauses = "num_vertices + num_vertices * num_colors * (num_colors - 1) / 2 + num_edges * num_colors", + num_literals = "num_vertices * num_colors + num_vertices * num_colors * (num_colors - 1) + 2 * num_edges * num_colors", + } +)] +impl ReduceTo for KColoring { + type Result = ReductionKColoringToSatisfiability; + + fn reduce_to(&self) -> Self::Result { + let num_vertices = self.graph().num_vertices(); + let num_colors = self.num_colors(); + let variable = |vertex: usize, color: usize| (vertex * num_colors + color + 1) as i32; + let mut clauses = Vec::new(); + + for vertex in 0..num_vertices { + clauses.push(CNFClause::new( + (0..num_colors) + .map(|color| variable(vertex, color)) + .collect(), + )); + } + + for vertex in 0..num_vertices { + for first_color in 0..num_colors { + for second_color in first_color + 1..num_colors { + clauses.push(CNFClause::new(vec![ + -variable(vertex, first_color), + -variable(vertex, second_color), + ])); + } + } + } + + for (first_vertex, second_vertex) in self.graph().edges() { + for color in 0..num_colors { + clauses.push(CNFClause::new(vec![ + -variable(first_vertex, color), + -variable(second_vertex, color), + ])); + } + } + + ReductionKColoringToSatisfiability { + target: Satisfiability::new(num_vertices * num_colors, clauses), + num_vertices, + num_colors, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "kcoloring_to_satisfiability", + build: || { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + source, + SolutionPair { + source_config: vec![0, 1, 0, 1, 2], + target_config: vec![1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/kcoloring_satisfiability.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..c1d0ef5d2 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -53,6 +53,7 @@ pub(crate) mod kcoloring_bicliquecover; mod kcoloring_casts; pub(crate) mod kcoloring_clustering; pub(crate) mod kcoloring_partitionintocliques; +pub(crate) mod kcoloring_satisfiability; pub(crate) mod kcoloring_twodimensionalconsecutivesets; mod knapsack_qubo; pub(crate) mod ksatisfiability_acyclicpartition; @@ -464,6 +465,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec) -> ReductionKColoringToSatisfiability { + ReduceTo::::reduce_to(source) +} + +#[test] +fn test_kcoloring_to_satisfiability_closed_loop() { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let reduction = reduce(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "KColoring->Satisfiability closed loop", + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_clause_families_and_sizes() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1)]), 3); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 6); + assert_eq!(target.num_clauses(), 11); + assert_eq!(target.num_literals(), 24); + assert_eq!( + target.clauses(), + &[ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![4, 5, 6]), + CNFClause::new(vec![-1, -2]), + CNFClause::new(vec![-1, -3]), + CNFClause::new(vec![-2, -3]), + CNFClause::new(vec![-4, -5]), + CNFClause::new(vec![-4, -6]), + CNFClause::new(vec![-5, -6]), + CNFClause::new(vec![-1, -4]), + CNFClause::new(vec![-2, -5]), + CNFClause::new(vec![-3, -6]), + ] + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_extracts_canonical_coloring() { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let reduction = reduce(&source); + let assignment = vec![1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1]; + + assert!(reduction.target_problem().evaluate(&assignment).0); + assert_eq!(reduction.extract_solution(&assignment), vec![0, 1, 0, 1, 2]); +} + +#[test] +fn test_kcoloring_to_satisfiability_five_cycle_feasibility() { + let solver = BruteForce::new(); + + let feasible = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let feasible_reduction = reduce(&feasible); + assert_eq!(feasible_reduction.target_problem().num_vars(), 15); + assert_eq!(feasible_reduction.target_problem().num_clauses(), 35); + assert_eq!(feasible_reduction.target_problem().num_literals(), 75); + assert!(solver + .find_witness(feasible_reduction.target_problem()) + .is_some()); + + let infeasible = KColoring::::with_k(SimpleGraph::cycle(5), 2); + let infeasible_reduction = reduce(&infeasible); + assert_eq!(infeasible_reduction.target_problem().num_vars(), 10); + assert_eq!(infeasible_reduction.target_problem().num_clauses(), 20); + assert_eq!(infeasible_reduction.target_problem().num_literals(), 40); + assert!(solver + .find_witness(infeasible_reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_empty_zero_colors_is_satisfiable() { + let source = KColoring::::with_k(SimpleGraph::empty(0), 0); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 0); + assert!(target.clauses().is_empty()); + assert_eq!(BruteForce::new().find_witness(target), Some(vec![])); + assert_eq!(reduction.extract_solution(&[]), Vec::::new()); +} + +#[test] +fn test_kcoloring_to_satisfiability_nonempty_zero_colors_is_infeasible() { + let source = KColoring::::with_k(SimpleGraph::empty(2), 0); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 0); + assert_eq!( + target.clauses(), + &[CNFClause::new(vec![]), CNFClause::new(vec![])] + ); + assert!(BruteForce::new().find_witness(target).is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_isolated_and_disconnected_vertices() { + let source = KColoring::::with_k(SimpleGraph::new(5, vec![(0, 1), (2, 3)]), 2); + let reduction = reduce(&source); + let target_solution = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("disconnected bipartite graph must be colorable"); + let source_solution = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&source_solution).0); + assert_eq!(source_solution.len(), 5); +} + +#[test] +fn test_kcoloring_to_satisfiability_self_loop_is_infeasible() { + let source = KColoring::::with_k(SimpleGraph::new(1, vec![(0, 0)]), 1); + let reduction = reduce(&source); + + assert_eq!( + reduction.target_problem().clauses(), + &[CNFClause::new(vec![1]), CNFClause::new(vec![-1, -1])] + ); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_parallel_edges_duplicate_conflicts() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1), (0, 1)]), 2); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_clauses(), 8); + assert_eq!( + target + .clauses() + .iter() + .filter(|clause| clause.literals == vec![-1, -3]) + .count(), + 2 + ); + assert_eq!( + target + .clauses() + .iter() + .filter(|clause| clause.literals == vec![-2, -4]) + .count(), + 2 + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_more_colors_than_vertices() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1)]), 3); + let reduction = reduce(&source); + let target_solution = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("an edge is colorable with three colors"); + + assert!( + source + .evaluate(&reduction.extract_solution(&target_solution)) + .0 + ); +} From aa1c1808dcfaab162a5826b075e79aeb22e6475f Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:33:57 +0800 Subject: [PATCH 3/4] Document KColoring to Satisfiability reduction --- docs/paper/reductions.typ | 70 +++++++++++++++++++++++++++++++++++++++ docs/paper/references.bib | 17 ++++++++++ 2 files changed, 87 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..a3906113b 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12189,6 +12189,76 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$. ] +#let kc_sat = load-example("KColoring", "Satisfiability") +#let kc_sat_sol = kc_sat.solutions.at(0) +#let kc_sat_n = graph-num-vertices(kc_sat.source.instance) +#let kc_sat_m = graph-num-edges(kc_sat.source.instance) +#let kc_sat_k = kc_sat.source.instance.num_colors +#let kc_sat_num_vars = kc_sat.target.instance.num_vars +#let kc_sat_num_clauses = sat-num-clauses(kc_sat.target.instance) +#let kc_sat_num_literals = kc_sat.target.instance.clauses.map(c => c.literals.len()).sum() +#reduction-rule("KColoring", "Satisfiability", + example: true, + example-caption: [Five-cycle ($n = #kc_sat_n$, $|E| = #kc_sat_m$) with $k = #kc_sat_k$ colors], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(kc_sat.source) + " -o kcoloring.json", + "pred reduce kcoloring.json --to " + target-spec(kc_sat) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate kcoloring.json --config " + kc_sat_sol.source_config.map(str).join(","), + ) + + #{ + let edges = kc_sat.source.instance.graph.edges + let vertices = range(kc_sat_n).map(i => { + let angle = -calc.pi / 2 + 2 * calc.pi * i / kc_sat_n + (1.15 * calc.cos(angle), 1.15 * calc.sin(angle)) + }) + let fills = kc_sat_sol.source_config.map(c => graph-colors.at(c)) + align(center, canvas(length: 0.8cm, { + for (u, v) in edges { g-edge(vertices.at(u), vertices.at(v)) } + for (v, pos) in vertices.enumerate() { + g-node(pos, name: str(v), fill: fills.at(v), label: str(v)) + } + })) + } + + *Step 1 -- Start from the source cycle.* The fixture supplies $C_#kc_sat_n$ with edges #kc_sat.source.instance.graph.edges.map(e => $paren.l #e.at(0), #e.at(1) paren.r$).join(", ") and $k = #kc_sat_k$. Its stored proper coloring is $(#kc_sat_sol.source_config.map(str).join(", "))$, shown above. With only two colors, alternating colors around this odd cycle would force the last edge to have equal-colored endpoints, so the same $C_#kc_sat_n$ instance with $k=2$ is infeasible. + + *Step 2 -- Create assignment variables.* Each vertex-color pair receives one Boolean variable. The fixture therefore has $n k = #kc_sat_n times #kc_sat_k = #kc_sat_num_vars$ variables, ordered in vertex blocks as $x_(0,0), x_(0,1), x_(0,2), dots.c, x_(4,2)$. SAT literal $x_(v,c)$ has one-based index $v k + c + 1$. + + *Step 3 -- Emit the three clause families.* The construction creates #kc_sat_n at-least-one clauses, $n k(k-1)/2 = #(kc_sat_n * kc_sat_k * (kc_sat_k - 1) / 2)$ pairwise at-most-one clauses, and $m k = #(kc_sat_m * kc_sat_k)$ edge clauses. Altogether the fixture contains #kc_sat_num_clauses clauses and #kc_sat_num_literals literal occurrences: $#kc_sat_n$ clauses of length $#kc_sat_k$ and $#(kc_sat_num_clauses - kc_sat_n)$ binary clauses. + + *Step 4 -- Verify the target assignment.* One-hot encoding $(#kc_sat_sol.source_config.map(str).join(", "))$ gives the Boolean vector of length #kc_sat_num_vars, namely $(#kc_sat_sol.target_config.map(str).join(", "))$. Every vertex block has exactly one 1, so all at-least-one and at-most-one clauses hold. Each cycle edge joins different selected colors, so every edge clause holds. Extracting the position of the 1 in each block returns $(#kc_sat_sol.source_config.map(str).join(", "))$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. The pairwise clauses force exactly one true bit per vertex, so encoding and extraction give a bijection between proper labeled colorings and satisfying assignments. In particular, $C_5$ has $(k-1)^5-(k-1) = 30$ proper colorings for $k=3$, hence 30 satisfying assignments; this count follows from the cycle chromatic polynomial, not from the fixture length. + ], +)[ + This $O(n k^2 + m k)$ assignment-variable reduction uses $n k$ Boolean variables and emits at-least-one, pairwise at-most-one, and edge-conflict clauses. The assignment variables and the first and third clause families are the standard assignment encoding in @faber_et_al:LIPIcs.SAT.2024.12[Section 2.2]; the repository uses the pairwise (binomial) at-most-one encoding rather than the sequential encoding analyzed there. +][ + _Construction._ Let $G = (V,E)$ be the stored undirected graph, with vertices $V = {0, dots, n-1}$, stored edge sequence $E$, and available colors $C = {0, dots, k-1}$. Introduce a Boolean variable $x_(v,c)$ for every $(v,c) in V times C$. The CNF formula is the conjunction of three clause families: + $ + or.big_(c in C) x_(v,c) & quad forall v in V, \ + not x_(v,a) or not x_(v,b) & quad forall v in V, thin a,b in C, thin a < b, \ + not x_(u,c) or not x_(v,c) & quad forall (u,v) in E, thin c in C. + $ + The first family selects at least one color, the second selects at most one, and the third forbids equal colors across every stored edge. The exact output has + $ + N &= n k, \ + M &= n + n k(k-1)/2 + m k, \ + L &= n k + n k(k-1) + 2 m k + $ + variables, clauses, and literal occurrences, respectively, where $m$ is the length of the stored edge sequence. + + _Correctness._ ($arrow.r.double$) Let $c: V -> C$ be a proper coloring. Set $x_(v,c(v)) = 1$ and all other $x_(v,d) = 0$. Every vertex then satisfies its at-least-one clause, no vertex violates a pairwise at-most-one clause, and properness gives $c(u) eq.not c(v)$ for each stored edge $(u,v)$, so no edge clause has both literals false. Hence the CNF is satisfiable. ($arrow.l.double$) Conversely, let $bold(x)$ satisfy the CNF. For every vertex, the at-least-one clause supplies some true $x_(v,c)$, while the pairwise at-most-one clauses make that color unique. Define $c(v)$ to be this unique color. For every stored edge $(u,v)$ and every color $d$, the edge clause forbids $x_(u,d) = x_(v,d) = 1$; therefore $c(u) eq.not c(v)$ and $c$ is proper. + + _Variable mapping._ The zero-based source pair $(v,c)$ occupies target configuration position $v k + c$ and signed SAT literal index $v k + c + 1$. Positive literals denote selection; negative literals denote non-selection. + + _Solution extraction._ Partition a satisfying assignment into $n$ consecutive blocks of length $k$ and return, for each vertex, the position of its unique 1. + + _Repository edge-case semantics._ The literature presentation assumes $k > 0$ and a loop-free graph. The same clauses cover the repository's full stored-graph domain without separate cases. When $n=k=0$, the empty CNF is satisfiable and extracts the empty coloring. When $n>0$ and $k=0$, every vertex contributes an empty at-least-one clause, making the formula unsatisfiable. A self-loop contributes $not x_(v,c) or not x_(v,c)$ for every color and therefore makes a positive-$k$ instance infeasible. Parallel edges deliberately duplicate their edge clauses but do not change satisfiability. Isolated vertices, disconnected components, and $k>n$ require no modification. +] + #reduction-rule("MaximumSetPacking", "QUBO")[ Set packing selects mutually disjoint sets of maximum total weight. Two sets conflict if and only if they share a universe element — the same adjacency structure as an independent set on the _intersection graph_. This reduction builds the intersection graph implicitly and applies the IS penalty method directly: each set becomes a QUBO variable, diagonal entries reward selection, and off-diagonal entries penalize pairs of overlapping sets with a penalty large enough to forbid any overlap. ][ diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 186f70de2..bdda1e85c 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -2143,3 +2143,20 @@ @article{berlekampMcElieceTilborg1978 doi = {10.1109/TIT.1978.1055873} } +@inproceedings{faber_et_al:LIPIcs.SAT.2024.12, + author = {Faber, Daniel and Jabrayilov, Adalat and Mutzel, Petra}, + title = {{SAT Encoding of Partial Ordering Models for Graph Coloring Problems}}, + booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, + pages = {12:1--12:20}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + isbn = {978-3-95977-334-8}, + issn = {1868-8969}, + year = {2024}, + volume = {305}, + editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.12}, + urn = {urn:nbn:de:0030-drops-205340}, + doi = {10.4230/LIPIcs.SAT.2024.12} +} From cc67770ab3b29447cf0bcfcb1291966e06be3823 Mon Sep 17 00:00:00 2001 From: Xiwei Pan Date: Sun, 2 Aug 2026 13:33:57 +0800 Subject: [PATCH 4/4] chore: remove plan file after implementation --- .../2026-08-02-kcoloring-to-satisfiability.md | 47 ------------------- 1 file changed, 47 deletions(-) delete mode 100644 docs/plans/2026-08-02-kcoloring-to-satisfiability.md diff --git a/docs/plans/2026-08-02-kcoloring-to-satisfiability.md b/docs/plans/2026-08-02-kcoloring-to-satisfiability.md deleted file mode 100644 index e62aa8abb..000000000 --- a/docs/plans/2026-08-02-kcoloring-to-satisfiability.md +++ /dev/null @@ -1,47 +0,0 @@ -# Implement KColoring to Satisfiability reduction - -Issue: #1099 - -Base commit: `a9067297c9b7759b4f1139692553a465de49fed3` - -Reference: Daniel Faber, Adalat Jabrayilov, and Petra Mutzel, “SAT Encoding of Partial Ordering Models for Graph Coloring Problems,” SAT 2024, Section 2.2, DOI `10.4230/LIPIcs.SAT.2024.12`. - -## Required behavior - -For `KColoring` with `n` vertices, `m` stored edges, and runtime color count `k`, construct a `Satisfiability` instance with Boolean variable `x[v,c]` at one-based SAT index `v * k + c + 1`: - -1. For every vertex `v`, add the at-least-one clause `(x[v,0] ∨ ... ∨ x[v,k-1])`. -2. For every vertex `v` and pair `a < b`, add `(¬x[v,a] ∨ ¬x[v,b])`. -3. For every stored edge `(u,v)` and color `c`, add `(¬x[u,c] ∨ ¬x[v,c])`. -4. Extract one source color per vertex by finding the true variable in its `k`-wide block. - -Register only the runtime `KN` / `SimpleGraph` endpoint as the primitive reduction. The exact target sizes are: - -- `num_vars = num_vertices * num_colors` -- `num_clauses = num_vertices + num_vertices * num_colors * (num_colors - 1) / 2 + num_edges * num_colors` -- `num_literals = num_vertices * num_colors + num_vertices * num_colors * (num_colors - 1) + 2 * num_edges * num_colors` - -The construction must preserve the repository's complete legal domain: empty graphs, `k = 0`, isolated vertices, disconnected graphs, self-loops, parallel edges, and `k > n`. - -## Batch 1: verification and Rust implementation - -Follow `.claude/skills/add-rule/SKILL.md` Steps 0–5 and Step 7, including the default mathematical verification in `.claude/skills/verify-reduction/SKILL.md`. - -1. Produce an ephemeral standalone Typst proof with independent forward and backward correctness directions, extraction, exact overhead, a feasible five-cycle example with `k = 3`, and an infeasible five-cycle example with `k = 2`. -2. Produce and run an ephemeral constructor verifier with symbolic overhead checks, exhaustive/simple-graph feasibility agreement through five vertices, extraction checks for every satisfying assignment tested, exact target-size checks, structural checks, and at least 5,000 checks. -3. Independently adversarially verify the proof with a separately written constructor/extractor, exhaustive tests through five vertices, two Hypothesis strategies, at least 5,000 checks, and cross-comparison against the constructor verifier. -4. Add `src/rules/kcoloring_satisfiability.rs` containing the direct `ReductionResult`, `ReduceTo` implementation, exact `#[reduction(overhead = ...)]` metadata, construction, extraction, and the linked test module. Use `CNFClause` and the target's signed one-based literal convention directly. -5. Register the module in `src/rules/mod.rs` with no new dispatch or compatibility layer. -6. Add `src/unit_tests/rules/kcoloring_satisfiability.rs`. Cover the semantic closed loop, exact clause families and sizes, extraction, five-cycle `k=3`/`k=2`, empty `n=0,k=0`, nonempty `k=0`, isolated vertices, self-loop infeasibility, parallel-edge clause duplication, and `k>n`. Keep each test below five seconds. -7. Add the canonical C5 `k=3` rule example through the rule module's `canonical_rule_example_specs()`, using source colors `[0,1,0,1,2]` and the corresponding 15-bit one-hot SAT assignment. -8. Run focused tests, format checks, graph/schema exports, fixture regeneration, and `make test clippy`. Do not commit ephemeral verification scripts or generated ignored documentation exports. - -## Batch 2: paper documentation and final verification - -Follow `.claude/skills/add-rule/SKILL.md` Step 6 with fresh context after Batch 1 is complete. - -1. Add the Faber–Jabrayilov–Mutzel SAT 2024 BibTeX entry to `docs/paper/references.bib` if it is not already present. -2. Add a `reduction-rule("KColoring", "Satisfiability", ...)` entry to `docs/paper/reductions.typ` based on the verified proof. State the construction, both correctness directions, variable mapping, extraction, and exact scaling. Explicitly distinguish the standard positive-`k`, loop-free literature domain from the repository edge cases handled by the same clauses. -3. Build a fixture-driven tutorial example for C5 with `k=3`. Start the extra block with `pred-commands()` derived from the loaded example, show the 15 variables and 35 clauses, verify `[0,1,0,1,2]` end to end, and explain witness multiplicity without relying on fixture solution counts. -4. Regenerate graph/schema exports and example fixtures after the documentation is connected, then run `make paper`, `make fmt-check`, `make test`, and `make clippy`. -5. Inspect the final diff and working tree. Keep only files directly required by #1099, delete this plan file before the final push, and leave the branch clean.