diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 8e0462b7a..78eb2f639 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -12387,6 +12387,157 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with
  *Example.* #let ex = load-example("ShortestCommonSuperstring", "QUBO")
  The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above.
 ]
+#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_edges = kc_sat.source.instance.graph.edges
+#let kc_sat_m = kc_sat_edges.len()
+#let kc_sat_k = kc_sat.source.instance.num_colors
+#let kc_sat_clauses = kc_sat.target.instance.clauses
+// Clause families counted from the loaded target: positive rows select a color,
+// negative pairs inside one vertex block exclude two colors, the rest are edge conflicts.
+#let kc_sat_block(lit) = calc.quo(calc.abs(lit) - 1, kc_sat_k)
+#let kc_sat_selection = kc_sat_clauses.filter(c => c.literals.all(lit => lit > 0))
+#let kc_sat_pairwise = kc_sat_clauses.filter(c => c.literals.len() == 2 and c.literals.all(lit => lit < 0) and kc_sat_block(c.literals.at(0)) == kc_sat_block(c.literals.at(1)))
+#let kc_sat_conflicts = kc_sat_clauses.filter(c => c.literals.all(lit => lit < 0) and not (c.literals.len() == 2 and kc_sat_block(c.literals.at(0)) == kc_sat_block(c.literals.at(1))))
+#assert(kc_sat_selection.len() + kc_sat_pairwise.len() + kc_sat_conflicts.len() == kc_sat_clauses.len())
+#let kc_sat_pair_count = calc.quo(kc_sat_pairwise.len(), kc_sat_n)
+#reduction-rule("KColoring", "Satisfiability",
+  example: true,
+  example-caption: [Cycle on #kc_sat_n vertices with #kc_sat_k colors],
+  extra: [
+    #pred-commands(
+      "pred create --example " + rule-spec(kc_sat) + " -o coloring.json",
+      "pred path KColoring/graph=SimpleGraph/k=KN Satisfiability -o paths.json",
+      "pred reduce coloring.json --via route.json -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate coloring.json --config " + cli-config(kc_sat_sol.source_config),
+    )
+    Select the direct path from `paths.json` as `route.json` before reducing.
+
+    *YES example.* The fixture has $n=#kc_sat_n$, $m=#kc_sat_m$, $k=#kc_sat_k$
+    and edges #kc_sat_edges.map(e => $(#e.at(0),#e.at(1))$).join(", ").
+    #{
+      let positions = range(kc_sat_n).map(v => (
+        1.5 * calc.cos(90deg + v * 360deg / kc_sat_n),
+        1.5 * calc.sin(90deg + v * 360deg / kc_sat_n),
+      ))
+      align(center, canvas(length: 0.7cm, {
+        for (u, v) in kc_sat_edges { g-edge(positions.at(u), positions.at(v)) }
+        for (v, pos) in positions.enumerate() {
+          let color = kc_sat_sol.source_config.at(v)
+          g-node(pos, name: str(v), fill: graph-colors.at(color), label: str(v))
+        }
+      }))
+    }
+    The target has $#kc_sat.target.instance.num_vars$ variables,
+    $#kc_sat_selection.len()$ selection clauses, $#kc_sat_pairwise.len()$ pairwise
+    exclusions and $#kc_sat_conflicts.len()$ edge conflicts: $#kc_sat_clauses.len()$
+    clauses and $#kc_sat_clauses.map(c => c.literals.len()).sum()$ literal occurrences.
+    For vertex $0$, the selection clause is
+    #repr(kc_sat_clauses.at(0).literals), and its pairwise clauses are
+    #kc_sat_pairwise.slice(0, kc_sat_pair_count).map(c => repr(c.literals)).join(", ").
+    The first stored edge contributes
+    #kc_sat_conflicts.slice(0, calc.quo(kc_sat_conflicts.len(), kc_sat_m)).map(c => repr(c.literals)).join(", ").
+
+    The canonical coloring is #repr(kc_sat_sol.source_config). Its assignment has
+    true literal numbers
+    #kc_sat_sol.target_config.enumerate().filter(((i, b)) => b).map(((i, b)) => str(i + 1)).join(", ").
+    #{
+      let bits = kc_sat_sol.target_config
+      let block_counts = range(kc_sat_n).map(v => bits.slice(v * kc_sat_k, (v + 1) * kc_sat_k).filter(b => b).len())
+      let conflicts = kc_sat_edges.filter(e => kc_sat_sol.source_config.at(e.at(0)) == kc_sat_sol.source_config.at(e.at(1)))
+      let satisfied = kc_sat_clauses.filter(c => c.literals.any(lit => bits.at(calc.abs(lit) - 1) == (lit > 0)))
+      let extracted = range(kc_sat_n).map(v => range(kc_sat_k).find(c => bits.at(v * kc_sat_k + c)))
+      [The true counts per block are #repr(block_counts). There are #conflicts.len()
+       monochromatic edges. The assignment satisfies #satisfied.len() of
+       #kc_sat_clauses.len() clauses and extracts to #repr(extracted).]
+    }
+
+    *NO example.* Restrict the same fixture graph to
+    #let no_k = kc_sat_k - 1
+    #let no_vars = kc_sat_n * no_k
+    #let no_pairs = calc.quo(no_k * (no_k - 1), 2)
+    #let no_clauses = kc_sat_n + kc_sat_n * no_pairs + kc_sat_m * no_k
+    #let no_literals = kc_sat_n * no_k + 2 * kc_sat_n * no_pairs + 2 * kc_sat_m * no_k
+    // The argument below needs the fixture to be the cycle (0,1), ..., (n-1,0) of odd length.
+    #let cycle_edges = range(kc_sat_n).map(v => (v, calc.rem(v + 1, kc_sat_n)))
+    #assert(no_k == 2, message: "NO example expects two colors")
+    #assert(kc_sat_n >= 3 and calc.odd(kc_sat_n), message: "NO example expects an odd cycle")
+    #assert(kc_sat_edges.map(e => (e.at(0), e.at(1))) == cycle_edges, message: "NO example expects the cycle edges in order")
+    #let path_edges = kc_sat_edges.slice(0, kc_sat_n - 1)
+    #let closing = kc_sat_edges.last()
+    // Propagate colors along the path edges from a chosen start color.
+    #let forced(start) = {
+      let colors = range(kc_sat_n).map(_ => start)
+      for e in path_edges { colors.at(e.at(1)) = no_k - 1 - colors.at(e.at(0)) }
+      colors
+    }
+    #let false_clause(colors) = closing.map(v => -(v * no_k + colors.at(v) + 1))
+    #let first = forced(0)
+    #let second = forced(1)
+    #assert(first.at(closing.at(0)) == first.at(closing.at(1)))
+    #assert(second.at(closing.at(0)) == second.at(closing.at(1)))
+    $k=#no_k$ colors. The target then has $#no_vars$ variables,
+    $#no_clauses$ clauses and $#no_literals$ literal occurrences. The fixture
+    edges form a cycle of odd length $#kc_sat_n$. Starting with color zero, its first
+    $#path_edges.len()$ edges force the alternating sequence
+    #repr(first). The closing edge #repr(closing) has equal colors
+    $#first.at(closing.at(0))$ and $#first.at(closing.at(1))$, so the conflict
+    clause #repr(false_clause(first)) is false. Starting with color one instead
+    forces #repr(second), which conflicts on the same closing edge with the false
+    clause #repr(false_clause(second)).
+    Thus none of the $#calc.pow(no_k, kc_sat_n)$ source configurations and none
+    of the $#calc.pow(2, no_vars)$ target assignments is feasible.
+  ],
+)[
+  For a simple undirected graph $G=(V,E)$ with $n=|V|$, $m=|E|$, and runtime
+  color count $k>=0$, encode color selection by Boolean variables $x_(v,c)$.
+  The assignment clauses of @faber2024 (§2.2, equations (8a)–(8b)), together
+  with pairwise at-most-one exclusions, yield an equisatisfiable CNF with
+  $n k$ variables. Garey–Johnson gives the endpoint definitions (@garey1979),
+  rather than this reduction direction. The paper's full ASS-S uses sequential
+  at-most-one and symmetry breaking; neither is used here.
+][
+  _Construction._ Label vertices $0,dots,n-1$ and colors $0,dots,k-1$.
+  Allocate $x_(v,c)$ at Boolean coordinate $v k+c$, with signed one-indexed
+  literal magnitude $v k+c+1$. First append one clause
+  $or.big_(c=0)^(k-1) x_(v,c)$ per vertex, then all pairwise clauses
+  $(not x_(v,a) or not x_(v,b))$ for each vertex and $0<=a<b<k$, and finally
+  $(not x_(u,c) or not x_(v,c))$ for each stored edge $(u,v)$ and color $c$.
+  Preserve empty rows, literal occurrences and stored edge order and orientation.
+
+  _Correctness._ ($arrow.r.double$) Given a proper coloring $f$, set $x_(v,c)$
+  true exactly when $f(v)=c$. Every selection clause holds. Two colors in one
+  vertex cannot both be selected, so all pairwise clauses hold. Adjacent vertices
+  have distinct colors, so each edge conflict has a true negative literal.
+
+  ($arrow.l.double$) A satisfying assignment has at least one true entry in
+  each vertex block by its selection clause. Two true entries would falsify their
+  pairwise exclusion, so each block has exactly one. Extract that unique color.
+  Equal colors across an edge would falsify its conflict clause; therefore the
+  extracted coloring is proper.
+
+  _Solution extraction._ Evaluate the full-length target witness once, reject
+  every non-solution, and read the unique selected color in each block. Reject
+  zero or multiple selected entries; never choose a default. Encoding and
+  extraction are inverse on feasible witnesses, and completed Or values map
+  identically, including infeasibility.
+
+  _Exact overhead and domain._ The three clause families contribute $n$,
+  $n k(k-1)/2$, and $m k$ rows. Their literal counts are $n k$,
+  $n k(k-1)$, and $2m k$. Counts and signed literal indices use checked
+  arithmetic before allocation. Construction takes $O(n+n k^2+m k)$ in the
+  numeric parameters and expanded color domain. If $k=0$ and $n>0$, retained
+  empty clauses make the target infeasible; if $n=0$, the empty CNF and empty
+  coloring are feasible for every $k$. Isolated vertices and components are
+  independent; unused colors are allowed when $k>n$. Odd cycles are not
+  two-colorable, and a complete graph requires $k>=n$. Mathematically a loop
+  would force every color false and parallel edges would duplicate clauses;
+  the SimpleGraph source constructor and deserializer reject both, so they
+  cannot reach this rule.
+]
+
 #let kc_qubo = load-example("KColoring", "DecisionQUBO")
 #let kc_qubo_sol = kc_qubo.solutions.at(0)
 #reduction-rule("KColoring", "DecisionQUBO",
diff --git a/docs/paper/references.bib b/docs/paper/references.bib
index 0dda81fd2..c94e2947a 100644
--- a/docs/paper/references.bib
+++ b/docs/paper/references.bib
@@ -2352,3 +2352,15 @@ @article{een2006
   pages = {1--26},
   doi = {10.3233/SAT190014},
 }
+
+@inproceedings{faber2024,
+  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},
+}
diff --git a/src/rules/kcoloring_satisfiability.rs b/src/rules/kcoloring_satisfiability.rs
new file mode 100644
index 000000000..dbd799fab
--- /dev/null
+++ b/src/rules/kcoloring_satisfiability.rs
@@ -0,0 +1,181 @@
+//! Pairwise one-hot CNF encoding of runtime graph coloring.
+
+use crate::models::formula::{CNFClause, Satisfiability};
+use crate::models::graph::KColoring;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+use crate::variant::KN;
+
+/// A SAT formula whose satisfying assignments encode proper colorings.
+#[derive(Debug, Clone)]
+pub struct ReductionKColoringToSatisfiability {
+    target: Satisfiability,
+    num_vertices: usize,
+    num_colors: usize,
+}
+
+impl ReductionResult for ReductionKColoringToSatisfiability {
+    type Source = KColoring<KN, SimpleGraph>;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Self::Target {
+        &self.target
+    }
+
+    fn extract_solution(&self, solution: &Vec<bool>) -> crate::rules::ExtractionResult<Vec<usize>> {
+        crate::rules::traits::validate_target_witness(
+            self.target_problem(),
+            solution,
+            |value| value.0,
+            "target assignment does not certify a proper coloring",
+        )?;
+        // Validation establishes exactly one true entry in every vertex block.
+        (0..self.num_vertices)
+            .map(|v| {
+                (0..self.num_colors)
+                    .find(|&c| solution[v * self.num_colors + c])
+                    .ok_or_else(|| crate::rules::ExtractionError::invalid("vertex has no color"))
+            })
+            .collect()
+    }
+}
+
+#[crate::aggregate_reduction(identity)]
+impl crate::rules::AggregateReductionResult for ReductionKColoringToSatisfiability {}
+
+fn coloring_sat_size(
+    n: usize,
+    m: usize,
+    k: usize,
+) -> Result<(usize, usize, usize), crate::rules::ReductionError> {
+    let overflow = || {
+        crate::rules::ReductionError::integer_overflow::<KColoring<KN, SimpleGraph>, Satisfiability>(
+            "computing coloring CNF sizes",
+        )
+    };
+    if n == 0 {
+        return Ok((0, 0, 0));
+    }
+    let variables = n.checked_mul(k).ok_or_else(overflow)?;
+    <KColoring<KN, SimpleGraph> as ReduceTo<Satisfiability>>::exact_i64(
+        variables,
+        "checking the SAT literal limit",
+    )?;
+    // Divide the even factor first, avoiding an overflowing intermediate product.
+    let pairs = if k < 2 {
+        0
+    } else if k.is_multiple_of(2) {
+        (k / 2).checked_mul(k - 1).ok_or_else(overflow)?
+    } else {
+        k.checked_mul((k - 1) / 2).ok_or_else(overflow)?
+    };
+    let exclusions = n.checked_mul(pairs).ok_or_else(overflow)?;
+    let conflicts = m.checked_mul(k).ok_or_else(overflow)?;
+    let binary = exclusions.checked_add(conflicts).ok_or_else(overflow)?;
+    let clauses = n.checked_add(binary).ok_or_else(overflow)?;
+    let literals = binary
+        .checked_mul(2)
+        .and_then(|count| variables.checked_add(count))
+        .ok_or_else(overflow)?;
+    Ok((variables, clauses, literals))
+}
+
+fn color_literal(v: usize, k: usize, c: usize) -> Result<i64, crate::rules::ReductionError> {
+    let index = v
+        .checked_mul(k)
+        .and_then(|i| i.checked_add(c))
+        .and_then(|i| i.checked_add(1))
+        .ok_or_else(|| {
+            crate::rules::ReductionError::integer_overflow::<
+                KColoring<KN, SimpleGraph>,
+                Satisfiability,
+            >("indexing a coloring literal")
+        })?;
+    <KColoring<KN, SimpleGraph> as ReduceTo<Satisfiability>>::exact_i64(
+        index,
+        "converting a coloring literal to i64",
+    )
+}
+
+#[crate::reduction(transform = exact {
+    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<Satisfiability> for KColoring<KN, SimpleGraph> {
+    type Result = ReductionKColoringToSatisfiability;
+
+    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
+        let n = self.num_vertices();
+        let k = self.num_colors();
+        let (num_vars, num_clauses, _) = coloring_sat_size(n, self.num_edges(), k)?;
+        let allocation_error = |error| {
+            crate::rules::ReductionError::invalid_target::<Self, Satisfiability>(format!(
+                "cannot allocate coloring CNF: {error}"
+            ))
+        };
+        let mut clauses = Vec::new();
+        clauses
+            .try_reserve_exact(num_clauses)
+            .map_err(allocation_error)?;
+        for v in 0..n {
+            let mut literals = Vec::new();
+            literals.try_reserve_exact(k).map_err(allocation_error)?;
+            for c in 0..k {
+                literals.push(color_literal(v, k, c)?);
+            }
+            clauses.push(CNFClause::new(literals));
+        }
+        for v in 0..n {
+            for a in 0..k {
+                for b in (a + 1)..k {
+                    clauses.push(CNFClause::new(vec![
+                        -color_literal(v, k, a)?,
+                        -color_literal(v, k, b)?,
+                    ]));
+                }
+            }
+        }
+        for (u, v) in self.graph().edges() {
+            for c in 0..k {
+                clauses.push(CNFClause::new(vec![
+                    -color_literal(u, k, c)?,
+                    -color_literal(v, k, c)?,
+                ]));
+            }
+        }
+        Ok(ReductionKColoringToSatisfiability {
+            target: Satisfiability::try_new(num_vars, clauses)
+                .map_err(<Self as ReduceTo<Satisfiability>>::target_construction)?,
+            num_vertices: n,
+            num_colors: k,
+        })
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "kcoloring_to_satisfiability",
+        build: || {
+            let source = KColoring::<KN, _>::with_k(
+                SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]),
+                3,
+            );
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                source,
+                crate::export::SolutionPair {
+                    source_config: serde_json::json!([0, 1, 0, 1, 2]),
+                    target_config: serde_json::json!([
+                        true, false, false, false, true, false, true, false, false, false, true,
+                        false, false, false, true,
+                    ]),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/kcoloring_satisfiability.rs"]
+mod tests;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 7606f4923..83d74437d 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -71,6 +71,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;
@@ -355,6 +356,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(staffscheduling_qubo::canonical_rule_example_specs());
     specs.extend(closestvectorproblem_qubo::canonical_rule_example_specs());
     specs.extend(coloring_qubo::canonical_rule_example_specs());
+    specs.extend(kcoloring_satisfiability::canonical_rule_example_specs());
     specs.extend(sequencingtominimizeweightedcompletiontime_qubo::canonical_rule_example_specs());
     specs.extend(schedulingwithindividualdeadlines_qubo::canonical_rule_example_specs());
     specs.extend(precedenceconstrainedscheduling_qubo::canonical_rule_example_specs());
diff --git a/src/unit_tests/rules/kcoloring_satisfiability.rs b/src/unit_tests/rules/kcoloring_satisfiability.rs
new file mode 100644
index 000000000..1c9ef8ecd
--- /dev/null
+++ b/src/unit_tests/rules/kcoloring_satisfiability.rs
@@ -0,0 +1,257 @@
+use super::*;
+use crate::rules::test_helpers::{
+    assert_parameter_predictions, assert_satisfaction_round_trip_from_satisfaction_target,
+};
+use crate::solvers::BruteForce;
+use crate::traits::Problem;
+use crate::types::Or;
+
+fn cycle(k: usize) -> KColoring<KN, SimpleGraph> {
+    KColoring::with_k(
+        SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]),
+        k,
+    )
+}
+
+#[test]
+fn test_kcoloring_to_satisfiability_closed_loop() {
+    let source = cycle(3);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+    assert_satisfaction_round_trip_from_satisfaction_target(&source, &result, "three-color cycle");
+    let solutions = BruteForce::new()
+        .find_all_witnesses(result.target_problem())
+        .unwrap();
+    assert_eq!(solutions.len(), 30);
+    let expected = vec![0, 1, 0, 1, 2];
+    let bits = vec![
+        true, false, false, false, true, false, true, false, false, false, true, false, false,
+        false, true,
+    ];
+    assert!(result.target_problem().evaluate(&bits).unwrap().0);
+    assert_eq!(result.extract_solution(&bits).unwrap(), expected);
+    assert_eq!(
+        (
+            result.target.num_vars(),
+            result.target.num_clauses(),
+            result.target.num_literals()
+        ),
+        (15, 35, 75)
+    );
+    assert_parameter_predictions(&source, &result);
+    assert_eq!(
+        crate::rules::AggregateReductionResult::extract_value(&result, Or(true)),
+        Or(true)
+    );
+    assert_eq!(
+        crate::rules::AggregateReductionResult::extract_value(&result, Or(false)),
+        Or(false)
+    );
+}
+
+#[test]
+fn odd_cycle_and_complete_graph_are_infeasible() {
+    for source in [
+        cycle(2),
+        KColoring::with_k(
+            SimpleGraph::new(4, vec![(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)]),
+            3,
+        ),
+    ] {
+        let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+        assert!(BruteForce::new().solve(&source).unwrap().is_none());
+        assert!(
+            BruteForce::new()
+                .solve(result.target_problem())
+                .unwrap()
+                .is_none()
+        );
+        assert_parameter_predictions(&source, &result);
+    }
+    let result = ReduceTo::<Satisfiability>::reduce_to(&cycle(2)).unwrap();
+    assert_eq!(
+        (
+            result.target.num_vars(),
+            result.target.num_clauses(),
+            result.target.num_literals()
+        ),
+        (10, 20, 40)
+    );
+}
+
+#[test]
+fn empty_isolated_disconnected_and_excess_color_domains() {
+    let cases = [
+        (0, vec![], 0, 1),
+        (0, vec![], usize::MAX, 1),
+        (1, vec![], 0, 0),
+        (3, vec![], 0, 0),
+        (3, vec![], 1, 1),
+        (2, vec![], 3, 9),
+        (2, vec![(0, 1)], 4, 12),
+        (4, vec![(0, 1), (2, 3)], 2, 4),
+        (3, vec![(0, 1)], 2, 4),
+        (3, vec![(0, 1), (1, 2), (2, 0)], 3, 6),
+    ];
+    for (n, edges, k, count) in cases {
+        let source = KColoring::<KN, _>::with_k(SimpleGraph::new(n, edges), k);
+        let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+        let expected = BruteForce::new().find_all_witnesses(&source).unwrap();
+        let actual = BruteForce::new()
+            .find_all_witnesses(result.target_problem())
+            .unwrap();
+        assert_eq!(expected.len(), count);
+        assert_eq!(actual.len(), count);
+        for bits in actual {
+            let colors = result.extract_solution(&bits).unwrap();
+            assert!(expected.contains(&colors));
+        }
+        assert_parameter_predictions(&source, &result);
+    }
+}
+
+#[test]
+fn clause_order_and_stored_edge_orientation() {
+    let source = KColoring::<KN, _>::with_k(SimpleGraph::new(3, vec![(2, 0), (1, 2)]), 2);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+    let actual: Vec<_> = result
+        .target
+        .clauses()
+        .iter()
+        .map(|clause| clause.literals.clone())
+        .collect();
+    assert_eq!(
+        actual,
+        vec![
+            vec![1, 2],
+            vec![3, 4],
+            vec![5, 6],
+            vec![-1, -2],
+            vec![-3, -4],
+            vec![-5, -6],
+            vec![-5, -1],
+            vec![-6, -2],
+            vec![-3, -5],
+            vec![-4, -6]
+        ]
+    );
+}
+
+#[test]
+fn extraction_rejects_zero_color_blocks() {
+    let result = ReduceTo::<Satisfiability>::reduce_to(&cycle(3)).unwrap();
+    assert!(result.extract_solution(&vec![false; 15]).is_err());
+}
+
+#[test]
+fn extraction_rejects_multiple_color_blocks() {
+    let source = KColoring::<KN, _>::with_k(SimpleGraph::empty(1), 3);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+    assert!(result.extract_solution(&vec![true, true, false]).is_err());
+}
+
+#[test]
+fn extraction_rejects_improper_one_hot_assignment() {
+    let source = KColoring::<KN, _>::with_k(SimpleGraph::new(2, vec![(0, 1)]), 2);
+    let result = ReduceTo::<Satisfiability>::reduce_to(&source).unwrap();
+    assert!(
+        result
+            .extract_solution(&vec![true, false, true, false])
+            .is_err()
+    );
+}
+
+#[test]
+fn extraction_rejects_short_and_long_assignments() {
+    let result = ReduceTo::<Satisfiability>::reduce_to(&cycle(3)).unwrap();
+    for len in [0, 14, 16] {
+        assert!(matches!(
+            result.extract_solution(&vec![true; len]),
+            Err(crate::rules::ExtractionError::Evaluation(_))
+        ));
+    }
+}
+
+#[test]
+fn source_rejects_loops_and_parallel_edges() {
+    for edges in [vec![(0, 0)], vec![(0, 1), (0, 1)], vec![(0, 1), (1, 0)]] {
+        assert!(SimpleGraph::try_new(2, edges.clone()).is_err());
+        let data = serde_json::json!({"num_vertices": 2, "edges": edges});
+        assert!(serde_json::from_value::<SimpleGraph>(data).is_err());
+    }
+}
+
+#[test]
+#[cfg(target_pointer_width = "64")]
+fn checked_sizes_accept_limits_and_reject_overflow() {
+    let max_literal = usize::try_from(i64::MAX).unwrap();
+    assert_eq!(coloring_sat_size(0, 0, usize::MAX).unwrap(), (0, 0, 0));
+    assert_eq!(coloring_sat_size(5, 5, 0).unwrap(), (0, 5, 0));
+    assert_eq!(coloring_sat_size(5, 5, 3).unwrap(), (15, 35, 75));
+    assert_eq!(
+        coloring_sat_size(max_literal, 0, 1).unwrap(),
+        (max_literal, max_literal, max_literal)
+    );
+    // With one isolated vertex the literal count is k^2; 2^32 is its first overflowing k.
+    let k = 4_294_967_295;
+    assert_eq!(
+        coloring_sat_size(1, 0, k).unwrap(),
+        (k, 9_223_372_030_412_324_866, 18_446_744_065_119_617_025)
+    );
+    // At k=1, total literals are n+2m. These edge counts fit the simple-graph bound.
+    let n = 1usize << 33;
+    let m = (usize::MAX - n) / 2;
+    assert_eq!(
+        coloring_sat_size(n, m, 1).unwrap(),
+        (n, n + m, usize::MAX - 1)
+    );
+    for (n, m, k) in [
+        (usize::MAX, 0, 2),
+        (1, 0, max_literal + 1),
+        (1, 0, 6_074_001_001),
+        (3, 0, 4_000_000_000),
+        (n, usize::MAX / 3 + 1, 3),
+        (n, usize::MAX / 3, 3),
+        (n, usize::MAX - n + 1, 1),
+        (1, 0, 4_294_967_297),
+        (1, 0, 4_294_967_296),
+        (n, m + 1, 1),
+    ] {
+        assert!(
+            matches!(
+                coloring_sat_size(n, m, k),
+                Err(crate::rules::ReductionError::IntegerOverflow { .. })
+            ),
+            "n={n},m={m},k={k}"
+        );
+    }
+    let source = KColoring::<KN, _>::with_k(SimpleGraph::empty(1), usize::MAX);
+    assert!(matches!(
+        ReduceTo::<Satisfiability>::reduce_to(&source),
+        Err(crate::rules::ReductionError::IntegerOverflow { .. })
+    ));
+    let source = KColoring::<KN, _>::with_k(SimpleGraph::empty(1), k);
+    assert!(matches!(
+        ReduceTo::<Satisfiability>::reduce_to(&source),
+        Err(crate::rules::ReductionError::InvalidTarget { .. })
+    ));
+}
+
+#[test]
+#[cfg(target_pointer_width = "64")]
+fn signed_literal_indices_are_checked_at_each_boundary() {
+    let max = usize::try_from(i64::MAX).unwrap();
+    assert_eq!(color_literal(0, 3, 0).unwrap(), 1);
+    assert_eq!(color_literal(4, 3, 2).unwrap(), 15);
+    assert_eq!(color_literal(max - 1, 1, 0).unwrap(), i64::MAX);
+    for (v, k, c) in [
+        (max, 1, 0),
+        (usize::MAX, 2, 0),
+        (usize::MAX, 1, 1),
+        (usize::MAX, 1, 0),
+    ] {
+        assert!(matches!(
+            color_literal(v, k, c),
+            Err(crate::rules::ReductionError::IntegerOverflow { .. })
+        ));
+    }
+}