[Rule] KColoring to Satisfiability

[isPANN]

Source

KColoring/SimpleGraph

Target

Satisfiability

Motivation

This standard CNF encoding gives every registered K-Coloring variant a direct decision-to-decision path to SAT. It is structurally simple but exercises exactly-one constraints, runtime color counts, and solution extraction.

Reference

Garey and Johnson, Computers and Intractability, 1979, GT4 and LO1, provide the Graph K-Colorability and Satisfiability problem definitions; they do not present this reduction direction.

Faber, Jabrayilov, and Mutzel, “SAT Encoding of Partial Ordering Models for Graph Coloring Problems,” SAT 2024, §2.2, equations (8a)–(8b), explicitly give the assignment-based clauses for K-Colorability: one at-least-one-color clause per vertex and one same-color conflict clause per edge and color. The paper also discusses at-most-one encodings; this issue uses the standard pairwise (binomial) encoding. DOI: https://doi.org/10.4230/LIPIcs.SAT.2024.12.

Reduction Algorithm

Given G=(V,E), n=|V|, m=|E|, and k=num_colors:

1. Create variable x[v,c] for every vertex v and color c in {0,...,k-1}.
2. For each vertex v, add (x[v,0] OR ... OR x[v,k-1]).
3. For each vertex v and colors a<b, add (not x[v,a] OR not x[v,b]).
4. For each edge {u,v} and each color c, add (not x[u,c] OR not x[v,c]).
5. Extract the unique true color for each vertex.

For the forward direction, a valid coloring satisfies the CNF by setting exactly x[v,color(v)] true for every vertex: the vertex clauses hold, pairwise exclusions hold, and every edge-conflict clause holds because adjacent vertices have different colors. For the backward direction, the clauses from steps 2 and 3 make exactly one x[v,c] true for each vertex; extracting that color gives a coloring, and step 4 forbids equal colors on every edge. The construction is polynomial, with the exact counts below.

The construction also handles the repository domain beyond the standard literature convention of a loop-free graph and positive k. When k=0, a nonempty graph receives an empty at-least-one clause and is infeasible, while the empty graph remains feasible. A self-loop makes every possible color conflict with itself and is therefore infeasible; parallel edges only duplicate conflict clauses; isolated vertices, disconnected graphs, and k>|V| require no special handling. All cases match the source definition.

Size Overhead

Target metric	Formula
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

Validation Method

• Exhaust all simple graphs through four vertices for k=2 and k=3.
• Brute-force all colorings and SAT assignments and compare feasibility.
• Check extraction and the k=0, empty-graph, isolated-vertex, odd-cycle, and complete-graph cases.

Example

1. Source instance: the five-cycle 01,12,23,34,40 with k=3.
2. Construction: 15 variables. Each vertex receives one 3-literal at-least-one clause and three pairwise exclusion clauses; each of five edges contributes three color-conflict clauses.
3. Target witness: colors [0,1,0,1,2], encoded by true variables x[0,0],x[1,1],x[2,0],x[3,1],x[4,2].
4. Round trip: extraction returns the valid coloring. The same graph is not 2-colorable, making the instance sensitive to incorrect color-count handling rather than being a trivial bipartite example.

BibTeX

@book{GareyJohnson1979,
  author = {Garey, Michael R. and Johnson, David S.},
  title = {Computers and Intractability: A Guide to the Theory of NP-Completeness},
  publisher = {W. H. Freeman},
  year = {1979}
}

@inproceedings{FaberJabrayilovMutzel2024,
  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)},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {305},
  pages = {12:1--12:20},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
  year = {2024},
  doi = {10.4230/LIPIcs.SAT.2024.12}
}

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	pred path KColoring Satisfiability --json reports no existing path, and an all-state title search found no duplicate proposal besides #1099.
Non-trivial	✅ Pass	The rule introduces n·k Boolean variables and three clause families (at-least-one, pairwise at-most-one, and edge-conflict clauses), with explicit witness extraction.
Correctness	❌ Fail	The only cited source, Garey–Johnson (1979), defines Graph K-Colorability but does not present this KColoring → SAT encoding; its GT4 entry instead points to a transformation from 3SAT. The construction is independently corroborated by modern SAT-encoding literature, but the issue needs a citation that actually contains the proposed encoding/proof.
Completeness	⚠️ Warn	Hand traces and exhaustive small-simple-graph checks support the full code construction, including k=0; however, the cited textbook's standard domain is K positive with `K ≤
Well-written	✅ Pass	All required sections are substantive; source/target symbols and target size fields are consistent; the five-cycle example is non-degenerate and round-trip testable.

Overall: 3 passed, 1 failed, 1 warning

---

Usefulness

• Both endpoints resolve: KColoring {graph: SimpleGraph, k: KN} and Satisfiability.
• pred path KColoring Satisfiability --json returns no reduction path.
• Searching all issue states for KColoring Satisfiability in titles returns only [Rule] KColoring to Satisfiability #1099.
• The motivation is concrete: a direct CNF route avoids composition through structurally larger intermediate models and exercises runtime color counts and solution extraction.

Non-trivial

This is not a subtype cast or renaming. For each vertex/color pair it creates a Boolean variable, then creates new CNF structure enforcing at least one color, at most one color, and edge compatibility. Extraction maps the unique true variable in each vertex block back to a color.

Correctness

Cited reference. Garey and Johnson, Computers and Intractability (1979), is real and appears in the project bibliography. Appendix A1, GT4, p. 191 defines Graph K-Colorability for a graph G=(V,E) and a positive integer K ≤ |V|. It does not give the proposed reduction to SAT; the entry says “Transformation from 3SAT,” which is the opposite direction. Consequently, the issue's sole reference does not support the proposed construction as required by this quality gate.

Independent verification. The proposed clauses match the classical assignment encoding described by Faber, Jabrayilov, and Mutzel, “SAT Encoding of Partial Ordering Models for Graph Coloring Problems,” SAT 2024, §2.2, equations (8a)–(8b): one at-least-one clause per vertex and one same-color conflict clause per edge/color. That paper also discusses adding an at-most-one encoding; #1099 uses the standard pairwise form. See https://doi.org/10.4230/LIPIcs.SAT.2024.12. SATLIB independently describes the same variable-per-vertex/color, edge-conflict, and exactly-one strategy: https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/GCP/descr.html.

Semantic check. The temporary validator exhaustively compared source colorability with target satisfiability for every simple graph through four vertices for k=2 and k=3, and checked the canonical five-cycle example. It completed with validated 10 candidate rules and all canonical examples. Direct logical proof is also immediate: a coloring sets exactly one x[v,c] per vertex and satisfies every edge clause; conversely, the vertex clauses select exactly one color and every edge clause forbids equal endpoint colors.

Required fix. Add a reference that actually states the assignment-based KColoring-to-SAT encoding (for example, the SAT 2024 paper above), including the relevant section/equations. Garey–Johnson may remain as the problem-definition reference.

Completeness

Literature scope. Garey–Johnson GT4 states the standard instance with positive K ≤ |V|; it does not cover the repository's runtime KN edge cases. Faber et al. define undirected edges as 2-element subsets and use colors 1,…,k, so their stated model excludes self-loops and k=0. This does not produce a counterexample to #1099's explicit construction, but the issue should distinguish the literature's standard domain from the larger code domain.

Codebase scope. KColoring<KN, SimpleGraph> has size fields num_colors, num_edges, and num_vertices. with_k accepts any usize; SimpleGraph::new permits empty graphs, isolated vertices, self-loops, and parallel edges. Satisfiability accepts zero variables, zero clauses, and empty clauses. Existing same-source rules (coloring_ilp.rs, coloring_qubo.rs, and kcoloring_partitionintocliques.rs) also use one-hot/color-class constructions and do not reject these inputs.

Hand traces beyond the worked example.

1. Empty graph, n=0, k=0: the construction creates zero variables and zero clauses. The empty CNF is satisfiable, matching the source's empty coloring; extraction returns [].
2. One isolated vertex, n=1, k=0: the construction creates zero variables and one empty at-least-one clause, hence UNSAT. The source has no configuration because its sole dimension has size zero, hence is infeasible.
3. One vertex with a self-loop, k=1: the clauses are (x[0,0]) and (¬x[0,0] ∨ ¬x[0,0]), hence UNSAT, matching the source validator, which rejects a self-loop under every coloring.
4. Parallel copies of an edge: each copy duplicates the corresponding conflict clauses. Duplication does not change satisfiability or extraction, and the overhead formulas count each stored edge consistently.

No semantic failure was found. The warning is documentation/evidence scope: explicitly document self-loops, parallel edges, and k>|V| (which the same proof handles), so the issue describes every legitimate source instance rather than only the standard simple-graph statement.

Well-written

• All required sections are present and implementable.
• n, m, and k are defined before use; the metric names num_vars, num_clauses, and num_literals exactly match the target schema.
• The overhead counts are correct: nk variables, n + n·k(k−1)/2 + mk clauses, and nk + n·k(k−1) + 2mk literal occurrences.
• The C5 example with k=3 is meaningfully nontrivial and contrasts with the same graph at k=2; the listed witness [0,1,0,1,2] is valid.

Recommendations

• Add Faber–Jabrayilov–Mutzel (SAT 2024), §2.2, equations (8a)–(8b), or another primary source that explicitly states the assignment-based SAT encoding.
• Add one sentence covering self-loops, parallel edges, and k>|V|; no algorithm change is needed for these cases.

[isPANN]

Rule Fix

Diagnosis:

• Literature support: the original sole citation defines the endpoint problems but does not present KColoring → Satisfiability.
• Proof coverage: the construction was correct, but the two correctness directions were only summarized rather than stated explicitly.
• Domain coverage: the issue did not document how the encoding handles repository-supported k=0, self-loops, parallel edges, and k>|V| inputs.

Literature:

• Faber, Jabrayilov, and Mutzel, SAT 2024, §2.2, equations (8a)–(8b), gives the canonical assignment-based K-Colorability clauses. Its discussion of at-most-one encodings corroborates the pairwise/binomial choice used here.
• Garey and Johnson remains cited only for the endpoint problem definitions, not for this reduction direction.

Changes:

• Added the SAT 2024 source and corrected the scope of the Garey–Johnson citation.
• Added independent forward and backward correctness arguments and stated polynomiality.
• Documented the behavior for k=0, empty/disconnected graphs, isolated vertices, self-loops, parallel edges, and k>|V|.

Smoke test:

• 103 instances passed across YES, NO, edge-case, feasibility-agreement, extraction, overhead, and target-validity buckets.
• Key confirming instances: C5 with k=3 (YES), C5 with k=2 (NO), empty graph with k=0, an isolated vertex with k=0, a self-loop, a parallel edge, and k>|V|.

[isPANN]

Issue Quality Check — Rule (Re-check)

Check	Result	Details
Usefulness	✅ Pass	pred path KColoring Satisfiability --json still reports no existing path.
Non-trivial	✅ Pass	The rule creates n*k Boolean variables, three clause families, and an explicit witness extraction.
Correctness	✅ Pass	The revised issue accurately scopes Garey–Johnson to the endpoint definitions and cites Faber–Jabrayilov–Mutzel (SAT 2024), §2.2, equations (8a)–(8b), for the assignment encoding.
Completeness	✅ Pass	The body now distinguishes the literature's standard domain and explicitly covers k=0, empty/disconnected graphs, isolated vertices, self-loops, parallel edges, and `k>
Well-written	✅ Pass	The construction, both proof directions, extraction, polynomiality, exact overhead, validation plan, and worked C5 example are complete and consistent.

Overall: 5 passed, 0 failed, 0 warnings

Previously: 3 passed, 1 failed, 1 warning. The unsupported reduction citation and undocumented repository-domain cases have been repaired.

---

Usefulness

• Both endpoints resolve as KColoring {graph: SimpleGraph, k: KN} and Satisfiability.
• No registered reduction path currently connects KColoring to Satisfiability.
• The direct CNF encoding avoids a larger composite route and exercises runtime color counts plus witness extraction.

Non-trivial

For each vertex/color pair the rule creates a Boolean variable. It then builds at-least-one, pairwise at-most-one, and edge-conflict clauses and maps a satisfying assignment back to a coloring. This is a genuine structural transformation rather than a cast or relabeling.

Correctness

• Garey and Johnson (1979), GT4 and LO1, is now cited only for the Graph K-Colorability and SAT definitions, which is the support it actually provides.
• Faber, Jabrayilov, and Mutzel, “SAT Encoding of Partial Ordering Models for Graph Coloring Problems,” SAT 2024, §2.2, equations (8a)–(8b), explicitly states the vertex at-least-one and edge/color conflict clauses for deciding k-colorability and discusses at-most-one encodings: https://doi.org/10.4230/LIPIcs.SAT.2024.12.
• The pairwise clauses used by the issue are the standard binomial at-most-one encoding. Together with the at-least-one clause, they make each vertex block one-hot.
• The forward and backward arguments are now independent and explicit. A valid coloring induces a satisfying assignment; any satisfying assignment has one selected color per vertex, and every edge clause prevents equal endpoint colors.
• A 103-instance smoke test passed the C5 YES/NO examples, feasibility agreement, extraction, exact size counts, and target validity.

Completeness

The cited paper formulates the standard positive-k, loop-free graph-coloring domain. The issue now says so and separately proves how the same direct clauses cover the repository's broader legal inputs.

Traced cases:

1. n=0, k=0: zero variables and zero clauses; both problems are feasible with the empty witness.
2. n=1, k=0: one empty at-least-one clause; both problems are infeasible.
3. One self-loop with k=1: the unit selection clause conflicts with the loop clause; both problems are infeasible.
4. Parallel copies of an edge duplicate clauses without changing feasibility; the formulas count both stored edges.
5. k>|V|: unused colors cause no problem; exactly one color is still extracted per vertex.

Disconnected graphs and isolated vertices are handled independently by the per-vertex clauses. No legitimate source instance requires an unstated precondition.

Well-written

• All required sections are substantive.
• G=(V,E), n, m, and k are defined before use.
• Target metric names match Satisfiability: num_vars, num_clauses, and num_literals.
• Exact counts agree with construction: nk variables, n + n*k*(k-1)/2 + mk clauses, and nk + n*k*(k-1) + 2mk literal occurrences.
• The five-cycle example exercises both the 3-colorable YES case and the 2-colorable NO case, and includes a concrete round-trip witness.

Recommendations

• None blocking; the issue is ready for implementation.