Repository navigation
Conversation
Collaborator
Author
Verification certificateVerdict: VERIFIED for Resolved types. Construction and proof. Selection, pairwise exclusion and edge/color conflict clauses establish a bijection between proper colorings and satisfying assignments. Exact sizes are Reference checker audit
All 76 labeled simple graphs through n=4, each k=0..4 (380 instances), exhaust every coloring and Boolean assignment. Additional n=5 samples: 300 instances per edge count m=0..10, with replacement, 60 per color count, seed 20261104. Each sample checks every coloring and a sampled Boolean assignment. Two Hypothesis strategies (random simple graphs and isolated-vertex blocks) use 200 examples each, seeds 20261102/20261103, deadline=None, database=None. Both C5 examples exhaust both witness domains. Independent checker audit
Exhaustive target enumeration covers 4,522 instances, with Boolean cubes up to 2^20: all labeled simple graphs through n=4 for k=0..5 when nk<=16; all 1,024 labeled n=5 graphs for k=0..3; all 34 unlabeled n=5 graphs for k=4. Every satisfying assignment is decoded and re-encoded. The mathematical extensions cover 3,636 further instances. Invalid witness lengths, zero-hot/multi-hot blocks and improper one-hot colorings are rejected. Three Hypothesis strategies (random graphs, special families, malformed witnesses) use 400 examples each, seeds 20261199/20261200/20261201, deadline=None, database=None, with independent backtracking coloring and SAT feasibility checks. The seeded family sampling uses 10994. Dropped clauses, changed indices and truncated rows are detected. Cross-comparison. The two builders agree exactly on 817 instances. On all 815 legal SimpleGraph inputs, the compiled CLI emits the same variable count, clause sequence and literal order as both builders: 0 disagreements. One hundred additional end-to-end cases pass (48 feasible, 52 infeasible). The C5 examples have sizes (15,35,75) for k=3 and (10,20,40) for k=2; the former has 30 feasible witnesses and the latter none. No ordering isomorphism is needed. The following complete mathematical checkers and proof make the results reproducible. Only module documentation and the companion import name are adapted for the displayed filenames; executable checker semantics are unchanged. Mathematical proof (Typst)#set page(paper: "a4", margin: 20mm)
#set text(size: 10pt)
#set heading(numbering: "1.")
= One-hot KColoring/SimpleGraph/KN → Satisfiability
*Theorem.* Let $n, k$ be nonnegative integers, let
$V = {0, dots, n-1}$ (empty when $n=0$), and let $G=(V,E)$ be an
undirected simple graph with $m=|E|$. The construction below produces a CNF
formula $F$ such that $G$ has a proper coloring with colors
$C={0, dots, k-1}$ (empty when $k=0$) if and only if $F$ is satisfiable.
Encoding and extraction are inverse bijections between proper colorings and
satisfying assignments. Both endpoint values are existential decision values.
== Reference
Daniel Faber, Adalat Jabrayilov and Petra Mutzel,
_SAT Encoding of Partial Ordering Models for Graph Coloring Problems_,
SAT 2024, LIPIcs 305, 12:1–12:20, §2.2, pp. 12:6–12:7,
#link("https://doi.org/10.4230/LIPIcs.SAT.2024.12")[doi:10.4230/LIPIcs.SAT.2024.12],
is the construction reference. Its equations (8a)–(8b) give the vertex selection
and edge conflict clauses below. The paper discusses optional at-most-one
constraints and the binomial alternative; its displayed full ASS-S uses
sequential constraints (9a)–(9d) and symmetry breaking (10a)–(10b).
Here we choose pairwise at-most-one clauses and introduce neither auxiliary
variables nor symmetry breaking. Their exclusion of two true colors is proved
below. Thus this is the assignment construction with the specified cardinality
choice, rather than a transcription of full ASS-S. The paper uses positive
color labels; our labels are shifted down by one. Its graph convention excludes
loops and its usual coloring domain has positive $k$; the extensions below are
proved separately.
Michael R. Garey and David S. Johnson, _Computers and Intractability_,
W. H. Freeman, 1979, GT4 and LO1, is cited only for endpoint definitions.
== Construction
Fix the stored order of edges in $E$; in the mathematical extensions it is a
list and $m$ counts every stored edge. For $v in V$, $c in C$, define the
Boolean $x_(v,c)$ with zero-based coordinate $i(v,c)=v k+c$ and positive
literal number $j(v,c)=v k+c+1$. The negative literal is $-j(v,c)$.
Coordinates are ordered by vertex first, then increasing color. A source
coloring is denoted by $f:V arrow C$ and a target Boolean assignment by $b$.
1. Allocate exactly $n k$ variables, with $b_(i(v,c))$ representing $x_(v,c)$.
2. For each vertex in increasing order append the selection clause
$A_v = or.big_(c in C) x_(v,c)$.
3. For each vertex in increasing order, then colors $0 <= a < d < k$
in lexicographic order, append the pairwise exclusion clause
$B_(v,a,d) = (not x_(v,a) or not x_(v,d))$.
4. For each stored edge $(u,v)$ in its input order, then each increasing color,
append $D_(u,v,c) = (not x_(u,c) or not x_(v,c))$.
5. Let $F$ be the conjunction of these clauses. Do not simplify or deduplicate
clauses or literal occurrences. In particular, retain every $A_v$ when $k=0$.
== Exact overhead and construction cost
#table(
columns: (1fr, 2fr), inset: 6pt,
[*Target parameter*], [*Exact formula*],
[`num_vars`], [$n k$],
[`num_clauses`], [$n + n k(k-1)/2 + m k$],
[`num_literals`], [$n k + n k(k-1) + 2 m k$],
)
There are $k$ variables per vertex, one selection row of length $k$ per vertex,
one binary row for each unordered color pair per vertex, and $k$ binary rows
per stored edge. The number of unordered pairs is
$sum_(a=0)^(k-1) (k-1-a)=k(k-1)/2$; the empty sum is zero when $k=0$.
Multiplying each row count by its row length gives the literal count. No branch
omits rows, no coefficient is normalized, and no row is merged, establishing
equality over the whole mathematical domain, including empty instances and
repeated edges in the extension.
Time and output storage are $O(n + n k^2 + m k)$, including the $n$ empty rows
at $k=0$. This is polynomial in the numeric parameters and expanded color
domain; it is not a bit-length bound for an unbounded binary encoding of $k$.
Extraction after target validation takes $O(n k+n)$; validation scans at most
all literal occurrences and rows. Python integers in the constructor are exact.
In a finite Rust representation, derived counts, products, additions, and
$v k+c+1$ must be checked, with explicit handling of $k=0$ before subtracting
one and a literal limit of i64 maximum. A fallible implementation must report
unrepresentable sizes; wraparound is not part of this construction.
== Correctness
*(⇒) Coloring to satisfying assignment.* Suppose $f$ is a proper coloring.
Set $x_(v,c)$ true exactly when $f(v)=c$. Every vertex receives one color, so
its selection clause has a true literal. Distinct colors $a,d$ cannot both
equal $f(v)$, so each pairwise exclusion contains a true negative literal.
For an edge $(u,v)$, properness says $f(u) != f(v)$; for any fixed color $c$
at least one endpoint has color different from $c$. Its negative literal
satisfies the corresponding edge clause. Every clause is satisfied, hence
$F$ is true. If $V$ is empty the same assignment is empty and satisfies the
empty CNF. If $k=0$ and $n>0$ there is no proper coloring, so the implication
has no feasible antecedent.
*(⇐) Satisfying assignment to one-hot blocks to proper coloring.* Let $b$
satisfy $F$. For each vertex, $A_v$ ensures that some $x_(v,c)$ is true.
If two distinct colors $a,d$ were true, their pairwise clause would have two
false negative literals. Thus at most one is true. Together these facts give
exactly one true coordinate in each vertex block. Define $f(v)$ to be its
color. This is in $C$. If an edge had equal endpoint colors $c$, both variables
in $D_(u,v,c)$ would be true, making that clause false. This contradicts the
assumed satisfaction. Every edge therefore has differently colored endpoints,
so $f$ is proper. For $k=0,n>0$, $A_v$ is empty and cannot be satisfied; for
$n=0$, the resulting function is the empty coloring.
== Solution extraction
Require the target witness to have exactly $n k$ Boolean coordinates and to
satisfy the constructed formula, using one target evaluation before decoding.
Reject malformed lengths and every non-solution. Scan each length-$k$ block
and require exactly one true entry; reject a block with zero or multiple true
entries, never choose a default or an arbitrary true entry. Return its unique
color for each vertex. The backward proof guarantees the result is a proper
source solution, and the forward assignment of this coloring equals the input
witness. Encoding any proper source coloring and then extracting returns that
same coloring. The empty graph extracts to the empty vector for every $k$.
This also explains why the added pairwise family is necessary for the chosen
unique-color extraction, even though other SAT encodings may permit multiple
colors in a vertex block and use different extraction.
== Domain and special cases
- *Zero colors:* if $n>0$, the $n$ empty selection clauses make the target
infeasible and there is no source configuration in the Cartesian color
domain. If $n=0,k=0$, both have the single empty witness.
- *Empty graph:* with no vertices the edge set is empty, so every target count
is zero for every $k$ and both sides are feasible.
- *Isolated vertices:* for $k>0$, their blocks allow each of the $k$ colors
independently; for $k=1$, their only clause is a unit selection clause.
An edgeless graph has $k^n$ witnesses with the convention $0^0=1$.
- *Disconnected graphs:* constraints never mix components, so colorings and
satisfying assignments combine by independent choices on components.
- *More colors than vertices:* no requirement uses every color. In a loop-free
graph with $k>n$, giving distinct colors to all vertices supplies a witness;
no unused-color block or auxiliary vertex is introduced.
- *Odd cycles:* with two colors, traversing edges forces alternation. After an
odd number of steps the closing edge has equal endpoint colors, so both sides
are infeasible. Three colors suffice: alternate two colors on the first even
number of vertices and give the final vertex the third color.
- *Complete graphs:* all $n$ vertex colors must differ, so feasibility is exactly
$k>=n$, including the empty graph. For $k>=n$, the number of witnesses is
the falling factorial $k(k-1) dots (k-n+1)$; for $k<n$ it is zero.
- *Self-loops (mathematical extension only):* a loop contributes
$(not x_(v,c) or not x_(v,c))$ for every color, forcing each entry false.
This conflicts with selection when $k>0$; at $k=0$ selection is already empty.
The source likewise cannot make a vertex's color differ from itself.
- *Parallel edges (mathematical extension only):* each stored copy adds the
same conflict rows. Satisfaction and extraction are unchanged, while $m$
and the occurrence counts include every copy. Reversed copies behave alike.
The Rust `SimpleGraph::try_new` and deserializer reject loops and repeated
undirected edges (`src/topology/graph.rs:109–131,151–155,302–310`), so those
two extensions are not legal inputs to this exact source variant.
== Worked YES example: C5 with three colors
Let $n=5$, $k=3$, and let the stored edges be
$(0,1),(1,2),(2,3),(3,4),(4,0)$, so $m=5$. In the following tables,
each parenthesized list denotes a disjunction of signed literals and a
semicolon separates clauses.
#table(
columns: (auto, 1fr, 2fr), inset: 5pt,
[*Vertex*], [*Selection*], [*Pairwise exclusions*],
[0], [`(1,2,3)`], [`(-1,-2); (-1,-3); (-2,-3)`],
[1], [`(4,5,6)`], [`(-4,-5); (-4,-6); (-5,-6)`],
[2], [`(7,8,9)`], [`(-7,-8); (-7,-9); (-8,-9)`],
[3], [`(10,11,12)`], [`(-10,-11); (-10,-12); (-11,-12)`],
[4], [`(13,14,15)`], [`(-13,-14); (-13,-15); (-14,-15)`],
)
#table(
columns: (auto, 1fr), inset: 5pt,
[*Edge*], [*Conflicts, in color order*],
[`(0,1)`], [`(-1,-4); (-2,-5); (-3,-6)`],
[`(1,2)`], [`(-4,-7); (-5,-8); (-6,-9)`],
[`(2,3)`], [`(-7,-10); (-8,-11); (-9,-12)`],
[`(3,4)`], [`(-10,-13); (-11,-14); (-12,-15)`],
[`(4,0)`], [`(-13,-1); (-14,-2); (-15,-3)`],
)
The exact counts are $n k=15$ variables,
$5+5 dot 3+5 dot 3=35$ clauses and $15+30+30=75$ literal occurrences.
Take the proper coloring `[0,1,0,1,2]`: edge color pairs are
`(0,1), (1,0), (0,1), (1,2), (2,0)`, all unequal.
The true literal numbers are `1,5,7,11,15`, and all other variables are false:
`[true,false,false, false,true,false, true,false,false, false,true,false, false,false,true]`.
Each selection row contains its listed true variable; no pair of true variables
lies in one block, and no edge row negates two selected variables. All 35
clauses hold. Scanning the blocks extracts exactly `[0,1,0,1,2]`.
The cycle coloring count is $(3-1)^5-(3-1)=30$; the exhaustive check finds
all 30 source witnesses and all 30 satisfying target assignments.
== Worked NO example: C5 with two colors
Keep the same five vertices and edges, now with $k=2$.
The five selection clauses are `(1,2), (3,4), (5,6), (7,8), (9,10)`.
The five pairwise exclusions are
`(-1,-2), (-3,-4), (-5,-6), (-7,-8), (-9,-10)`.
The ten edge clauses, grouped by stored edge, are
`(-1,-3); (-2,-4)`;
`(-3,-5); (-4,-6)`;
`(-5,-7); (-6,-8)`;
`(-7,-9); (-8,-10)`;
`(-9,-1); (-10,-2)`.
There are $10$ variables, $5+5+10=20$ clauses and $10+10+20=40$
literal occurrences.
If vertex 0 has color 0, the first four edges force colors `[0,1,0,1,0]`.
The closing edge joins color 0 to color 0. On the target side, the first four
edges force true variables `1,4,5,8,9`; the clause `(-9,-1)` is false.
If vertex 0 instead has color 1, the forced coloring is `[1,0,1,0,1]`;
true variables `2,3,6,7,10` falsify `(-10,-2)`. Selection and pairwise
exclusion force one of those two starts and then every subsequent choice,
so no other satisfying assignment remains. Exhaustion of all $2^5=32$
source configurations and $2^10=1024$ target assignments finds zero witnesses
on each side.Reference checker (coloring_cnf_check.py)# /// script
# requires-python = ">=3.12"
# dependencies = ["sympy==1.14.0", "hypothesis==6.170.14"]
# ///
'One-hot graph-coloring CNF checker. Run with Python 3 or uv run --script.'
import os
import random
import sys
from itertools import combinations, product
try:
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
except ModuleNotFoundError:
# The completion command uses python3; uv supplies isolated, pinned dependencies.
os.execvp("uv", ["uv", "run", "--script", __file__, *sys.argv[1:]])
def reduce(n, edges, k):
clauses = [tuple(v*k+c+1 for c in range(k)) for v in range(n)]
clauses.extend((-(v*k+a+1), -(v*k+b+1))
for v in range(n) for a, b in combinations(range(k), 2))
clauses.extend((-(u*k+c+1), -(v*k+c+1)) for u, v in edges for c in range(k))
return n*k, tuple(clauses)
def extract_solution(n, k, target, assignment):
if target[0] != n*k or not target_evaluate(target, assignment):
raise ValueError("target witness does not certify a coloring")
colors = []
for v in range(n):
selected = [c for c in range(k) if assignment[v*k+c]]
if len(selected) != 1:
raise ValueError("vertex block must contain exactly one true color")
colors.append(selected[0])
return tuple(colors)
SECTION_NAMES = {
1: "symbolic overhead identities",
2: "exhaustive forward and backward feasibility",
3: "extraction from every satisfying assignment",
4: "measured exact overhead",
5: "target structure, domain cases, Hypothesis",
6: "C5 YES example",
7: "C5 NO example",
}
checks = dict.fromkeys(SECTION_NAMES, 0)
failures = dict.fromkeys(SECTION_NAMES, 0)
def check(section, condition, context):
checks[section] += 1
if not condition:
failures[section] += 1
if sum(failures.values()) <= 20:
print(f"FAIL section {section}: {context}")
def rejects(action):
try:
action()
except ValueError:
return True
return False
def source_evaluate(n, edges, k, colors):
"""KColoring::evaluate: malformed configurations are errors, conflicts false."""
if len(colors) != n or any(c < 0 or c >= k for c in colors):
raise ValueError("invalid source configuration")
return all(colors[u] != colors[v] for u, v in edges)
def target_evaluate(target, assignment):
"""Satisfiability::evaluate on its Vec<bool> witness domain."""
num_vars, clauses = target
if len(assignment) != num_vars or any(type(b) is not bool for b in assignment):
raise ValueError("invalid target configuration")
return all(any(assignment[abs(lit) - 1] == (lit > 0) for lit in row)
for row in clauses)
def encode(colors, k):
return tuple(c == selected for selected in colors for c in range(k))
def mask_of(assignment):
return sum(1 << i for i, value in enumerate(assignment) if value)
def clause_masks(target):
"""Exact bit representation of disjunction, independently checked in section 5."""
return tuple((sum(1 << (lit - 1) for lit in set(row) if lit > 0),
sum(1 << (-lit - 1) for lit in set(row) if lit < 0))
for row in target[1])
def mask_satisfies(masks, assignment):
return all((assignment & pos) or (~assignment & neg) for pos, neg in masks)
def size_formula(n, m, k):
return (n * k, n + n * (k * (k - 1) // 2) + m * k,
n * k + n * k * (k - 1) + 2 * m * k)
def measured_size(target):
return target[0], len(target[1]), sum(map(len, target[1]))
def structure(n, edges, k, target):
num_vars, rows = target
check(4, measured_size(target) == size_formula(n, len(edges), k), (n, edges, k))
# CNFClause does not simplify or deduplicate rows or literal occurrences.
check(5, num_vars <= 2**63 - 1 and all(
type(lit) is int and 1 <= abs(lit) <= num_vars for row in rows for lit in row),
("valid signed one-based literals", n, edges, k))
positive = [row for row in rows if all(lit > 0 for lit in row)]
check(5, len(positive) == n and all(len(row) == k for row in positive),
("one selection row per vertex, including empty rows", n, k))
check(5, all(len(row) == 2 and all(lit < 0 for lit in row)
for row in rows if row not in positive), ("binary exclusions", n, k))
check(5, {abs(lit) for row in rows for lit in row} == set(range(1, num_vars + 1)),
("every variable appears", n, k))
def verify_instance(n, edges, k):
"""Enumerate *every* coloring and Boolean assignment, without SAT solving."""
target = reduce(n, edges, k)
structure(n, edges, k, target)
expected = set()
for colors in product(range(k), repeat=n):
feasible = source_evaluate(n, edges, k, colors)
bits = encode(colors, k)
check(2, target_evaluate(target, bits) == feasible, ("forward", n, edges, k, colors))
if feasible:
expected.add(mask_of(bits))
masks = clause_masks(target)
found = set()
for assignment in range(1 << target[0]):
feasible = mask_satisfies(masks, assignment)
# Membership comes from the independent graph predicate on every coloring.
check(2, feasible == (assignment in expected), ("backward", n, edges, k, assignment))
if feasible:
found.add(assignment)
bits = tuple(bool(assignment & (1 << i)) for i in range(target[0]))
colors = extract_solution(n, k, target, bits)
check(3, source_evaluate(n, edges, k, colors), ("proper extraction", n, edges, k, bits))
check(3, encode(colors, k) == bits, ("unique one-hot inverse", n, k, bits))
check(2, found == expected, ("complete witness sets and feasibility", n, edges, k))
return len(expected), len(found)
def symbolic():
n, m, k, c, a = sp.symbols("n m k c a", integer=True, nonnegative=True)
# Variables: k per vertex. Selection: one row of k literals per vertex.
# Exclusions: sum_a (k-1-a) unordered pairs per vertex, two literals each.
# Edges: k binary rows per stored edge. No normalization removes occurrences.
pairs = sp.summation(k - 1 - a, (a, 0, k - 1))
variables = n * sp.summation(1, (c, 0, k - 1))
clauses = n + n * pairs + m * sp.summation(1, (c, 0, k - 1))
literals = n * k + 2 * n * pairs + 2 * m * k
formulas = (n*k, n + n*k*(k-1)/2 + m*k, n*k + n*k*(k-1) + 2*m*k)
for actual, formula in zip((variables, clauses, literals), formulas):
check(1, sp.simplify(actual - formula) == 0, (actual, formula))
for colors in (0, 1):
check(1, pairs.subs(k, colors) == 0, ("empty pair range", colors))
@st.composite
def simple_graphs(draw):
n = draw(st.integers(0, 5))
possible = tuple(combinations(range(n), 2))
edges = draw(st.sets(st.sampled_from(possible), max_size=len(possible))) if possible else set()
return n, tuple(sorted(edges)), draw(st.integers(0, 5))
@seed(20261102)
@settings(max_examples=200, deadline=None, database=None)
@given(simple_graphs(), st.data())
def random_graph_witnesses(instance, data):
n, edges, k = instance
target = reduce(n, edges, k)
structure(n, edges, k, target)
bits = tuple(data.draw(st.lists(st.booleans(), min_size=n*k, max_size=n*k)))
check(5, target_evaluate(target, bits) == mask_satisfies(clause_masks(target), mask_of(bits)),
("mask evaluator agrees with literal semantics", instance, bits))
if target_evaluate(target, bits):
colors = extract_solution(n, k, target, bits)
check(3, source_evaluate(n, edges, k, colors) and encode(colors, k) == bits,
("Hypothesis extraction", instance, bits))
else:
check(5, rejects(lambda: extract_solution(n, k, target, bits)),
("reject non-solution", instance, bits))
if k or not n:
colors = tuple(data.draw(st.lists(st.integers(0, max(0, k-1)), min_size=n, max_size=n)))
check(2, target_evaluate(target, encode(colors, k)) == source_evaluate(n, edges, k, colors),
("Hypothesis forward", instance, colors))
@seed(20261103)
@settings(max_examples=200, deadline=None, database=None)
@given(st.integers(1, 6), st.integers(0, 5), st.data())
def isolated_vertex_blocks(n, k, data):
"""Second strategy forces zero-, one-, and multi-hot blocks without edge effects."""
bits = tuple(data.draw(st.lists(st.booleans(), min_size=n*k, max_size=n*k)))
target = reduce(n, (), k)
expected = all(sum(bits[v*k:(v+1)*k]) == 1 for v in range(n))
check(5, target_evaluate(target, bits) == expected, ("exactly one", n, k, bits))
if expected:
colors = extract_solution(n, k, target, bits)
check(3, source_evaluate(n, (), k, colors) and encode(colors, k) == bits,
("isolated extraction", n, k, bits))
else:
check(5, rejects(lambda: extract_solution(n, k, target, bits)), ("malformed block", n, k, bits))
def domain_cases():
# These expectations follow from graph theory, rather than a second clause generator.
cases = [
(0, (), 0, 1), (0, (), 7, 1), (3, (), 0, 0), (3, (), 1, 1),
(2, ((0, 1),), 4, 12),
(4, ((0, 1), (2, 3)), 2, 4),
(3, ((0, 1), (1, 2), (2, 0)), 2, 0),
(4, tuple(combinations(range(4), 2)), 3, 0),
(4, tuple(combinations(range(4), 2)), 4, 24),
(1, ((0, 0),), 1, 0), (1, ((0, 0),), 3, 0),
(2, ((0, 1), (1, 0)), 2, 2),
]
for n, edges, k, count in cases:
check(5, verify_instance(n, edges, k) == (count, count), ("domain", n, edges, k, count))
# A loop's repeated negative literal is counted twice, not normalized away.
check(4, measured_size(reduce(1, ((0, 0),), 1)) == (1, 2, 3), "loop occurrences")
for bits in ((False, False), (True, True), (), (True,), (True, False, False)):
check(5, rejects(lambda: extract_solution(1, 2, reduce(1, (), 2), bits)),
("reject zero/multi-hot or wrong length", bits))
check(5, rejects(lambda: extract_solution(2, 2, reduce(2, ((0, 1),), 2),
(True, False, True, False))), "edge conflict")
check(5, rejects(lambda: source_evaluate(1, (), 0, (0,))), "k=0 source error")
check(5, rejects(lambda: source_evaluate(1, (), 2, ())), "source length error")
# Test the optimized enumerator against literal semantics on arbitrary CNFs,
# including duplicate literals, tautologies, empty clauses and unused variables.
rows = ((), (1,), (-1,), (1, -1), (-1, -1), (1, -2), (2, 3))
for clauses in product(rows, repeat=2):
target = (3, clauses)
for bits in product((False, True), repeat=3):
check(5, target_evaluate(target, bits) == mask_satisfies(clause_masks(target), mask_of(bits)),
("literal/mask calibration", clauses, bits))
def sampled_larger_graphs():
# Full target enumeration at n=5,k=4 costs 2**20 assignments per graph.
# Cover each (n=5,m=0..10) with 300 seeded instances (60 per k), with replacement.
rng = random.Random(20261104)
possible = tuple(combinations(range(5), 2))
for m in range(11):
for sample in range(300):
k = sample % 5
edges = tuple(sorted(rng.sample(possible, m)))
target = reduce(5, edges, k)
structure(5, edges, k, target)
expected = set()
for colors in product(range(k), repeat=5):
bits = encode(colors, k)
valid = source_evaluate(5, edges, k, colors)
check(2, target_evaluate(target, bits) == valid, ("sampled n=5 forward", edges, k, colors))
if valid:
expected.add(mask_of(bits))
assignment = rng.randrange(1 << target[0])
bits = tuple(bool(assignment & (1 << i)) for i in range(target[0]))
valid = target_evaluate(target, bits)
check(2, valid == (assignment in expected), ("sampled n=5 backward", edges, k, bits))
if valid:
colors = extract_solution(5, k, target, bits)
check(3, source_evaluate(5, edges, k, colors) and encode(colors, k) == bits,
("sampled n=5 extraction", edges, k, bits))
print("Sampled: n=5, 300 instances per m=0..10; k=0..4, seed=20261104")
CYCLE = ((0, 1), (1, 2), (2, 3), (3, 4), (4, 0))
def examples():
colors = (0, 1, 0, 1, 2)
target = reduce(5, CYCLE, 3)
bits = encode(colors, 3)
check(6, source_evaluate(5, CYCLE, 3, colors), "C5 witness")
check(6, measured_size(target) == (15, 35, 75), "C5 YES exact overhead")
check(6, tuple(i+1 for i, value in enumerate(bits) if value) == (1, 5, 7, 11, 15), "C5 true literals")
check(6, target_evaluate(target, bits), "C5 satisfying assignment")
check(6, extract_solution(5, 3, target, bits) == colors, "C5 round trip")
check(6, verify_instance(5, CYCLE, 3) == (30, 30), "C5 YES all witnesses")
target = reduce(5, CYCLE, 2)
check(7, measured_size(target) == (10, 20, 40), "C5 NO exact overhead")
check(7, verify_instance(5, CYCLE, 2) == (0, 0), "C5 NO both sides exhaustively infeasible")
check(7, not source_evaluate(5, CYCLE, 2, (0, 1, 0, 1, 0)), "closing edge prevents alternating colors")
def main():
symbolic()
if "--smoke" in sys.argv:
examples()
else:
instances = 0
for n in range(5):
possible = tuple(combinations(range(n), 2))
for mask in range(1 << len(possible)):
edges = tuple(edge for i, edge in enumerate(possible) if mask & (1 << i))
for k in range(5):
verify_instance(n, edges, k)
instances += 1
print(f"Exhaustive: {instances} labeled simple graph/color-count instances; n=0..4, k=0..4")
domain_cases()
sampled_larger_graphs()
random_graph_witnesses()
isolated_vertex_blocks()
examples()
for section, name in SECTION_NAMES.items():
print(f"Section {section} ({name}): {checks[section]} checks, {failures[section]} failures")
print(f"TOTAL: {sum(checks.values())} checks, {sum(failures.values())} failures")
return int(any(failures.values()))
if __name__ == "__main__":
sys.exit(main())Independent checker companion (cnf_model.py)'CNF construction, extraction and Boolean/coloring predicates. Vertex-major coordinates v*k+c use signed literal magnitudes v*k+c+1. Clause order is selection rows, pairwise exclusions, then conflicts in stored edge order and orientation.'
from itertools import product
def lit(v, c, k):
return v * k + c + 1
def reduce(n, edges, k):
"""Return (num_vars, clauses) with clauses a list of lists of signed 1-indexed literals."""
clauses = []
for v in range(n):
clauses.append([lit(v, c, k) for c in range(k)])
for v in range(n):
for a in range(k):
for d in range(a + 1, k):
clauses.append([-lit(v, a, k), -lit(v, d, k)])
for (u, v) in edges:
for c in range(k):
clauses.append([-lit(u, c, k), -lit(v, c, k)])
return n * k, clauses
# ---------- independent evaluators ----------
def source_eval(n, edges, k, coloring):
"""KColoring::evaluate semantics: malformed -> None (error), else bool."""
if len(coloring) != n or any((not isinstance(c, int)) or c < 0 or c >= k for c in coloring):
return None
return all(coloring[u] != coloring[v] for (u, v) in edges)
def target_eval(num_vars, clauses, b):
"""Satisfiability::evaluate semantics: wrong length -> None (error), else bool."""
if len(b) != num_vars:
return None
for cl in clauses:
ok = False
for l in cl:
if l == 0 or abs(l) > num_vars:
raise ValueError("illegal literal %r" % l)
val = b[abs(l) - 1]
if (l > 0 and val) or (l < 0 and not val):
ok = True
break
if not ok:
return False
return True
def encode(n, k, coloring):
b = [False] * (n * k)
for v, c in enumerate(coloring):
b[v * k + c] = True
return b
def extract(n, k, num_vars, clauses, b):
"""Proof, "Solution extraction": validate length and satisfaction once, then require each
length-k block to have exactly one true entry. Returns the coloring or None (rejected)."""
if len(b) != n * k or num_vars != n * k:
return None
if target_eval(num_vars, clauses, b) is not True:
return None
out = []
for v in range(n):
block = b[v * k:(v + 1) * k]
ones = [c for c, x in enumerate(block) if x]
if len(ones) != 1:
return None
out.append(ones[0])
return out
def decode_blocks_unvalidated(n, k, b):
"""Block decoder WITHOUT the satisfaction check, used to probe the block rule alone."""
if len(b) != n * k:
return None
out = []
for v in range(n):
ones = [c for c in range(k) if b[v * k + c]]
if len(ones) != 1:
return None
out.append(ones[0])
return out
def proper_colorings(n, edges, k):
return [list(f) for f in product(range(k), repeat=n) if source_eval(n, edges, k, list(f))]
def overhead(n, m, k):
return {
"num_vars": n * k,
"num_clauses": n + n * k * (k - 1) // 2 + m * k,
"num_literals": n * k + n * k * (k - 1) + 2 * m * k,
}Independent checker (coloring_cnf_independent.py)# /// script
# requires-python = ">=3.10"
# dependencies = ["numpy>=1.26", "hypothesis>=6.100", "sympy>=1.12"]
# ///
'Independent graph-coloring CNF checker. Save the companion module as cnf_model.py beside this file and run with uv run --script.'
import os
import random
import sys
from itertools import combinations, permutations, product
from math import perm
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import numpy as np # noqa: E402
import sympy as sp # noqa: E402
from hypothesis import HealthCheck, given, seed, settings, strategies as st # noqa: E402
from cnf_model import ( # noqa: E402
decode_blocks_unvalidated, encode, extract, lit, overhead, proper_colorings, reduce,
source_eval, target_eval,
)
CHECKS = {}
FAILS = []
SECTION = ["?"]
def check(cond, msg):
CHECKS[SECTION[0]] = CHECKS.get(SECTION[0], 0) + 1
if not cond:
FAILS.append("[%s] %s" % (SECTION[0], msg))
if len(FAILS) <= 20:
print("FAIL", FAILS[-1])
def section(name):
SECTION[0] = name
CHECKS.setdefault(name, 0)
# ---------- helpers ----------
def all_simple_graphs(n):
pairs = list(combinations(range(n), 2))
for mask in range(1 << len(pairs)):
yield [pairs[i] for i in range(len(pairs)) if mask >> i & 1]
def canon(n, edges):
best = None
for p in permutations(range(n)):
f = tuple(sorted(tuple(sorted((p[u], p[v]))) for u, v in edges))
if best is None or f < best:
best = f
return best
def iso_reps(n):
seen = {}
for g in all_simple_graphs(n):
seen.setdefault(canon(n, g), g)
return list(seen.values())
def sat_mask(num_vars, clauses):
"""Boolean array over all 2^num_vars assignments; assignment integer a has coordinate i = bit i."""
a = np.arange(1 << num_vars, dtype=np.uint64)
bits = [((a >> np.uint64(i)) & np.uint64(1)).astype(bool) for i in range(num_vars)]
ok = np.ones(1 << num_vars, dtype=bool)
for cl in clauses:
c = np.zeros(1 << num_vars, dtype=bool)
for l in cl:
c |= bits[l - 1] if l > 0 else ~bits[-l - 1]
ok &= c
return ok
def int_to_bits(x, N):
return [bool(x >> i & 1) for i in range(N)]
def bits_to_int(b):
return sum(1 << i for i, x in enumerate(b) if x)
def dpll(num_vars, clauses):
"""Independent tiny SAT solver (unit propagation + branching). Returns model or None."""
def solve(assign):
while True:
unit = None
for cl in clauses:
sat = False
free = []
for l in cl:
v = assign.get(abs(l))
if v is None:
free.append(l)
elif v == (l > 0):
sat = True
break
if sat:
continue
if not free:
return None
if len(free) == 1:
unit = free[0]
break
if unit is None:
break
assign = dict(assign)
assign[abs(unit)] = unit > 0
for v in range(1, num_vars + 1):
if v not in assign:
for val in (True, False):
r = solve({**assign, v: val})
if r is not None:
return r
return None
return assign
m = solve({})
if m is None:
return None
return [m.get(v, False) for v in range(1, num_vars + 1)]
def color_search(n, edges, k):
adj = [set() for _ in range(n)]
for u, v in edges:
adj[u].add(v)
adj[v].add(u)
col = [-1] * n
def go(v):
if v == n:
return True
for c in range(k):
if all(col[w] != c for w in adj[v]) and not (v in adj[v]):
col[v] = c
if go(v + 1):
return True
col[v] = -1
return False
return list(col) if go(0) else None
def full_instance_check(n, edges, k, extract_all_unsat=True):
"""Exhaustive both-direction + bijection + extraction check on one instance."""
N, cls = reduce(n, edges, k)
tag = "n=%d k=%d E=%s" % (n, k, edges)
mask = sat_mask(N, cls)
sat_ints = set(np.nonzero(mask)[0].tolist())
cols = proper_colorings(n, edges, k)
enc_ints = {bits_to_int(encode(n, k, f)) for f in cols}
check((len(cols) > 0) == (len(sat_ints) > 0), "feasibility mismatch " + tag)
check(enc_ints == sat_ints, "witness sets differ (not a bijection) " + tag)
check(len(enc_ints) == len(cols), "encoding not injective " + tag)
for f in cols: # forward: encoded coloring satisfies, via the literal evaluator
check(target_eval(N, cls, encode(n, k, f)) is True, "forward fails %s f=%s" % (tag, f))
check(extract(n, k, N, cls, encode(n, k, f)) == f, "extract(encode(f)) != f " + tag)
for x in sat_ints: # backward + extraction from every satisfying assignment
b = int_to_bits(x, N)
check(target_eval(N, cls, b) is True, "numpy/literal evaluator disagree " + tag)
f = extract(n, k, N, cls, b)
check(f is not None and source_eval(n, edges, k, f) is True, "extracted not proper " + tag)
check(f is not None and encode(n, k, f) == b, "re-encode differs " + tag)
check(decode_blocks_unvalidated(n, k, b) is not None, "satisfying assignment not one-hot " + tag)
if extract_all_unsat:
for x in range(1 << N):
if x not in sat_ints:
b = int_to_bits(x, N)
check(extract(n, k, N, cls, b) is None, "non-solution extracted " + tag)
return len(cols)
def main():
rng = random.Random(10994)
# ---------------- 1. symbolic overhead ----------------
section("1 symbolic overhead")
n, m, k, a = sp.symbols("n m k a", integer=True, nonnegative=True)
pairs = sp.summation(k - 1 - a, (a, 0, k - 1))
check(sp.simplify(pairs - k * (k - 1) / 2) == 0, "pair count sum")
rows = n + n * pairs + m * k
lits = n * k + 2 * n * pairs + 2 * m * k
check(sp.simplify(rows - (n + n * k * (k - 1) / 2 + m * k)) == 0, "num_clauses formula")
check(sp.simplify(lits - (n * k + n * k * (k - 1) + 2 * m * k)) == 0, "num_literals formula")
check(pairs.subs(k, 0) == 0 and pairs.subs(k, 1) == 0, "pair count at k=0,1")
for kk in range(0, 40):
check((kk * (kk - 1)) % 2 == 0, "k(k-1) even")
# ---------------- 2. exhaustive both directions, bijection, extraction ----------------
section("2 exhaustive correctness")
inst = 0
for nn in range(0, 5):
for g in all_simple_graphs(nn):
for kk in range(0, 6):
if nn * kk > 16:
continue
full_instance_check(nn, g, kk, extract_all_unsat=(nn * kk <= 9))
inst += 1
for g in all_simple_graphs(5):
for kk in range(0, 4):
full_instance_check(5, g, kk, extract_all_unsat=(kk <= 1))
inst += 1
reps5 = iso_reps(5)
check(len(reps5) == 34, "34 unlabeled graphs on 5 vertices")
for g in reps5:
full_instance_check(5, g, 4, extract_all_unsat=False)
inst += 1
print(" exhaustive instances:", inst)
# mathematical extensions: self-loops and parallel / reversed edges (multigraph lists)
section("2b loops and parallel edges")
ext = 0
for nn in range(1, 4):
allpairs = [(u, v) for u in range(nn) for v in range(nn)]
for r in range(0, 4):
for es in product(allpairs, repeat=r):
for kk in range(0, 4):
if nn * kk > 9:
continue
cnt = full_instance_check(nn, list(es), kk, extract_all_unsat=False)
if any(u == v for u, v in es):
check(cnt == 0, "self-loop instance feasible")
N, cls = reduce(nn, list(es), kk)
ov = overhead(nn, len(es), kk)
check(len(cls) == ov["num_clauses"], "multigraph clause count")
ext += 1
print(" extension instances:", ext)
# ---------------- 3. extraction attacks ----------------
section("3 extraction attacks")
for nn in range(0, 5):
for g in all_simple_graphs(nn):
for kk in range(0, 5):
N, cls = reduce(nn, g, kk)
# wrong lengths
for L in {max(0, N - 1), N + 1, N + kk, 0 if N else 1}:
if L != N:
check(extract(nn, kk, N, cls, [False] * L) is None, "wrong length accepted")
check(extract(nn, kk, N, cls, [True] * L) is None, "wrong length accepted (all true)")
if nn == 0:
check(extract(0, kk, N, cls, []) == [], "empty graph extracts to []")
continue
if kk == 0:
check(extract(nn, 0, N, cls, []) is None, "k=0 nonempty must reject")
continue
base = rng.choice(proper_colorings(nn, g, kk) or [[rng.randrange(kk) for _ in range(nn)]])
for v in range(nn):
# zero-hot block
b = encode(nn, kk, base)
for c in range(kk):
b[v * kk + c] = False
check(extract(nn, kk, N, cls, b) is None, "zero-hot block accepted")
check(target_eval(N, cls, b) is False, "zero-hot block satisfies CNF")
# multi-hot block
if kk >= 2:
b = encode(nn, kk, base)
b[v * kk + (base[v] + 1) % kk] = True
check(extract(nn, kk, N, cls, b) is None, "multi-hot block accepted")
check(target_eval(N, cls, b) is False, "multi-hot block satisfies CNF")
# one-hot but improper coloring must be rejected
for f in product(range(kk), repeat=nn):
if not source_eval(nn, g, kk, list(f)):
b = encode(nn, kk, list(f))
check(target_eval(N, cls, b) is False, "improper one-hot satisfies CNF")
check(extract(nn, kk, N, cls, b) is None, "improper one-hot extracted")
# all-true / all-false
check(extract(nn, kk, N, cls, [True] * N) is None or (kk == 1 and not g),
"all-true accepted wrongly")
check(extract(nn, kk, N, cls, [False] * N) is None, "all-false accepted")
# necessity of the pairwise family for unique-color extraction (proof claim)
section("3b pairwise family necessity")
for nn in range(1, 4):
for g in all_simple_graphs(nn):
for kk in range(2, 4):
N, cls = reduce(nn, g, kk)
no_pair = [c for c in cls if not (len(c) == 2 and (abs(c[0]) - 1) // kk == (abs(c[1]) - 1) // kk
and c[0] < 0 and c[1] < 0 and c[0] != c[1])]
mask = sat_mask(N, no_pair)
multi = [x for x in np.nonzero(mask)[0].tolist()
if decode_blocks_unvalidated(nn, kk, int_to_bits(x, N)) is None]
# a multi-hot model exists iff some proper coloring leaves a vertex a second colour
# unused by its neighbours (then that extra colour can also be switched on)
nbr = [set() for _ in range(nn)]
for u, v in g:
nbr[u].add(v)
nbr[v].add(u)
expect = any(any(c != f[v] and all(f[w] != c for w in nbr[v]) for v in range(nn) for c in range(kk))
for f in proper_colorings(nn, g, kk))
check(bool(multi) == expect,
"pairwise-dropped multi-hot existence mismatch n=%d k=%d g=%s" % (nn, kk, g))
if multi:
check(all(extract(nn, kk, N, no_pair, int_to_bits(x, N)) is None for x in multi),
"multi-hot model of the weakened CNF would need a default colour")
# ---------------- 4. exact overhead, measured ----------------
section("4 exact overhead")
for nn in range(0, 7):
for kk in range(0, 8):
for _ in range(6):
pairs_ = list(combinations(range(nn), 2))
g = [p for p in pairs_ if rng.random() < 0.5]
rng.shuffle(g)
g = [(v, u) if rng.random() < 0.5 else (u, v) for u, v in g]
N, cls = reduce(nn, g, kk)
ov = overhead(nn, len(g), kk)
check(N == ov["num_vars"], "num_vars")
check(len(cls) == ov["num_clauses"], "num_clauses")
check(sum(map(len, cls)) == ov["num_literals"], "num_literals")
for (nn, mm, kk) in [(10**6, 10**6, 10**3), (3, 0, 0), (0, 0, 10**9), (2**31, 5, 2**16)]:
ov = overhead(nn, mm, kk)
check(ov["num_clauses"] == nn + sp.binomial(kk, 2) * nn + mm * kk, "big-int num_clauses")
check(ov["num_literals"] == nn * kk + 2 * sp.binomial(kk, 2) * nn + 2 * mm * kk, "big-int num_literals")
# ---------------- 5. structure ----------------
section("5 structure")
for nn in range(0, 6):
for kk in range(0, 6):
g = [p for p in combinations(range(nn), 2) if rng.random() < 0.4]
N, cls = reduce(nn, g, kk)
idx = 0
for v in range(nn): # selection rows
check(cls[idx] == [v * kk + c + 1 for c in range(kk)], "selection row order")
idx += 1
for v in range(nn):
for x in range(kk):
for y in range(x + 1, kk):
check(cls[idx] == [-(v * kk + x + 1), -(v * kk + y + 1)], "pair row order")
idx += 1
for (u, v) in g:
for c in range(kk):
check(cls[idx] == [-(u * kk + c + 1), -(v * kk + c + 1)], "edge row order")
idx += 1
check(idx == len(cls), "no extra rows")
used = set()
for cl in cls:
for l in cl:
check(l != 0 and 1 <= abs(l) <= N, "literal in range")
used.add(abs(l))
check(len(cl) == 2 or len(cl) == kk, "row length is 2 or k")
check(len(set(cl)) == len(cl), "no repeated literal inside a simple-graph row")
check(used == set(range(1, N + 1)) or (nn > 0 and kk == 0) or N == 0, "every var used")
check(sum(1 for cl in cls if not cl) == (nn if kk == 0 else 0), "empty rows exactly at k=0")
check(all(l > 0 for cl in cls[:nn] for l in cl) and all(l < 0 for cl in cls[nn:] for l in cl),
"sign pattern")
# index order v*k+c is a bijection onto 1..nk
for nn in range(0, 8):
for kk in range(0, 8):
js = [lit(v, c, kk) for v in range(nn) for c in range(kk)]
check(js == list(range(1, nn * kk + 1)), "literal numbering bijective & ordered")
# ---------------- 5b. closed-form family counts ----------------
section("5b families")
for nn in range(0, 6):
for kk in range(0, 6):
if nn * kk > 16:
continue
# edgeless: k^n with 0^0 = 1
N, cls = reduce(nn, [], kk)
check(int(sat_mask(N, cls).sum()) == kk ** nn, "edgeless count k^n")
# complete: falling factorial
Kn = list(combinations(range(nn), 2))
N, cls = reduce(nn, Kn, kk)
cnt = int(sat_mask(N, cls).sum())
check(cnt == (perm(kk, nn) if kk >= nn else 0), "complete graph falling factorial")
check((cnt > 0) == (kk >= nn), "complete feasible iff k>=n")
# k > n witness: distinct colors
if kk > nn:
check(target_eval(N, cls, encode(nn, kk, list(range(nn)))) is True, "k>n distinct coloring")
# cycles (n >= 3): chromatic polynomial
if nn >= 3:
C = [(i, (i + 1) % nn) for i in range(nn)]
N, cls = reduce(nn, C, kk)
cnt = int(sat_mask(N, cls).sum())
check(cnt == (kk - 1) ** nn + (-1) ** nn * (kk - 1), "cycle chromatic polynomial")
if nn % 2 == 1:
check((cnt == 0) == (kk <= 2), "odd cycle needs 3 colors")
# disconnected: product of component counts
for _ in range(150):
n1, n2 = rng.randint(0, 3), rng.randint(0, 3)
kk = rng.randint(0, 3)
g1 = [p for p in combinations(range(n1), 2) if rng.random() < 0.5]
g2 = [p for p in combinations(range(n2), 2) if rng.random() < 0.5]
g = g1 + [(u + n1, v + n1) for u, v in g2]
c = lambda nn, gg: int(sat_mask(*reduce(nn, gg, kk)).sum()) # noqa: E731
check(c(n1 + n2, g) == c(n1, g1) * c(n2, g2), "disconnected count multiplies")
# ---------------- 5c. mutation sensitivity (checks must catch broken constructions) -------
section("5c mutation sensitivity")
def detects(mutant):
for nn in range(1, 4):
for g in all_simple_graphs(nn):
for kk in range(1, 4):
N, cls = mutant(nn, g, kk)
sat = set(np.nonzero(sat_mask(N, cls))[0].tolist())
enc = {bits_to_int(encode(nn, kk, f)) for f in proper_colorings(nn, g, kk)}
if sat != enc:
return True
return False
def drop_last_edge_row(nn, g, kk):
N, cls = reduce(nn, g, kk)
return N, (cls[:-1] if g and kk else cls)
def drop_pairs(nn, g, kk):
N, cls = reduce(nn, g, kk)
return N, cls[:nn] + cls[nn + nn * kk * (kk - 1) // 2:]
def color_major(nn, g, kk): # x[v,c] -> c*n+v: isomorphic but a different literal map
N, cls = reduce(nn, g, kk)
mp = {v * kk + c + 1: c * nn + v + 1 for v in range(nn) for c in range(kk)}
return N, [[(1 if l > 0 else -1) * mp[abs(l)] for l in cl] for cl in cls]
def selection_off_by_one(nn, g, kk):
N, cls = reduce(nn, g, kk)
return N, [cl[:-1] if i < nn and kk > 1 else cl for i, cl in enumerate(cls)]
check(detects(drop_last_edge_row), "dropping an edge row undetected")
check(detects(drop_pairs), "dropping pairwise rows undetected")
check(detects(color_major), "color-major indexing undetected by the witness-set comparison")
check(detects(selection_off_by_one), "truncated selection row undetected")
# ---------------- 6/7. worked examples ----------------
section("6 YES example C5 k=3")
C5 = [(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)]
N, cls = reduce(5, C5, 3)
table_sel = [[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12], [13, 14, 15]]
table_pair = [[-1, -2], [-1, -3], [-2, -3], [-4, -5], [-4, -6], [-5, -6], [-7, -8], [-7, -9], [-8, -9],
[-10, -11], [-10, -12], [-11, -12], [-13, -14], [-13, -15], [-14, -15]]
table_edge = [[-1, -4], [-2, -5], [-3, -6], [-4, -7], [-5, -8], [-6, -9], [-7, -10], [-8, -11], [-9, -12],
[-10, -13], [-11, -14], [-12, -15], [-13, -1], [-14, -2], [-15, -3]]
check(cls == table_sel + table_pair + table_edge, "C5 k=3 clauses equal the proof's tables")
check((N, len(cls), sum(map(len, cls))) == (15, 35, 75), "C5 k=3 counts 15/35/75")
w = [0, 1, 0, 1, 2]
check(source_eval(5, C5, 3, w) is True, "witness proper")
b = encode(5, 3, w)
check([i + 1 for i, x in enumerate(b) if x] == [1, 5, 7, 11, 15], "true literals 1,5,7,11,15")
check(b == [True, False, False, False, True, False, True, False, False, False, True, False,
False, False, True], "printed assignment")
check(target_eval(N, cls, b) is True, "all 35 clauses hold")
check(extract(5, 3, N, cls, b) == w, "extracts [0,1,0,1,2]")
check(len(proper_colorings(5, C5, 3)) == 30, "30 source witnesses")
check(int(sat_mask(N, cls).sum()) == 30, "30 target witnesses")
section("7 NO example C5 k=2")
N, cls = reduce(5, C5, 2)
exp = ([[1, 2], [3, 4], [5, 6], [7, 8], [9, 10]] + [[-1, -2], [-3, -4], [-5, -6], [-7, -8], [-9, -10]]
+ [[-1, -3], [-2, -4], [-3, -5], [-4, -6], [-5, -7], [-6, -8], [-7, -9], [-8, -10], [-9, -1], [-10, -2]])
check(cls == exp, "C5 k=2 clauses equal the proof's listing")
check((N, len(cls), sum(map(len, cls))) == (10, 20, 40), "C5 k=2 counts 10/20/40")
check(len(proper_colorings(5, C5, 2)) == 0, "0 of 32 source configurations")
check(sum(1 for f in product(range(2), repeat=5)) == 32, "32 source configurations")
check(int(sat_mask(N, cls).sum()) == 0, "0 of 1024 target assignments")
# forced patterns: [0,1,0,1,0] -> trues 1,4,5,8,9 falsify (-9,-1); [1,0,1,0,1] -> 2,3,6,7,10 falsify (-10,-2)
for f, trues, bad in (([0, 1, 0, 1, 0], [1, 4, 5, 8, 9], [-9, -1]), ([1, 0, 1, 0, 1], [2, 3, 6, 7, 10], [-10, -2])):
b = encode(5, 2, f)
check([i + 1 for i, x in enumerate(b) if x] == trues, "forced true variables")
falsified = [cl for cl in cls if not any((l > 0) == b[abs(l) - 1] for l in cl)]
check(falsified == [bad], "exactly the closing clause is falsified")
# ---------------- 8. Hypothesis ----------------
section("8 hypothesis")
@st.composite
def random_graph(draw):
nn = draw(st.integers(0, 7))
pairs_ = list(combinations(range(nn), 2))
es = draw(st.lists(st.sampled_from(pairs_), unique=True) if pairs_ else st.just([]))
es = [(v, u) if draw(st.booleans()) else (u, v) for u, v in es]
kk = draw(st.integers(0, nn + 2))
return nn, es, kk
@st.composite
def structured_graph(draw):
fam = draw(st.sampled_from(["empty", "edgeless", "odd_cycle", "even_cycle", "complete", "disjoint", "k0"]))
nn = draw(st.integers(0, 7))
if fam == "empty":
nn, es = 0, []
elif fam in ("edgeless", "k0"):
es = []
elif fam == "odd_cycle":
nn = 2 * draw(st.integers(1, 3)) + 1
es = [(i, (i + 1) % nn) for i in range(nn)]
elif fam == "even_cycle":
nn = 2 * draw(st.integers(2, 3))
es = [(i, (i + 1) % nn) for i in range(nn)]
elif fam == "complete":
es = list(combinations(range(nn), 2))
else:
h = draw(st.integers(0, 3))
es = list(combinations(range(h), 2)) + [(h + 1 + i, h + 2 + i) for i in range(max(0, nn - h - 2))]
nn = max(nn, h)
es = [(u, v) for u, v in es if u < nn and v < nn]
kk = 0 if fam == "k0" else draw(st.integers(0, nn + 3))
return nn, es, kk
def oracle_check(nn, es, kk):
N, cls = reduce(nn, es, kk)
ov = overhead(nn, len(es), kk)
check((N, len(cls), sum(map(len, cls))) == (ov["num_vars"], ov["num_clauses"], ov["num_literals"]),
"hyp overhead")
col = color_search(nn, es, kk)
model = dpll(N, cls)
check((col is not None) == (model is not None), "hyp feasibility n=%d k=%d %s" % (nn, kk, es))
if col is not None:
check(target_eval(N, cls, encode(nn, kk, col)) is True, "hyp forward")
if model is not None:
f = extract(nn, kk, N, cls, model)
check(f is not None and source_eval(nn, es, kk, f) is True, "hyp backward/extract")
check(f is not None and encode(nn, kk, f) == model, "hyp re-encode")
if kk == 0:
check((model is not None) == (nn == 0), "k=0 feasible iff empty graph")
if kk > nn:
check(col is not None, "k>|V| feasible for simple graphs")
@seed(20261199)
@settings(max_examples=400, deadline=None, database=None, suppress_health_check=list(HealthCheck))
@given(random_graph())
def h_random(inst):
oracle_check(*inst)
@seed(20261200)
@settings(max_examples=400, deadline=None, database=None, suppress_health_check=list(HealthCheck))
@given(structured_graph())
def h_struct(inst):
oracle_check(*inst)
@seed(20261201)
@settings(max_examples=400, deadline=None, database=None, suppress_health_check=list(HealthCheck))
@given(random_graph(), st.data())
def h_malformed(inst, data):
nn, es, kk = inst
N, cls = reduce(nn, es, kk)
L = data.draw(st.sampled_from([N, N, N + 1, max(0, N - 1)]))
b = data.draw(st.lists(st.booleans(), min_size=L, max_size=L))
f = extract(nn, kk, N, cls, b)
ok = target_eval(N, cls, b) if L == N else None
if L != N:
check(f is None, "hyp wrong length accepted")
elif ok:
check(f is not None and encode(nn, kk, f) == b and source_eval(nn, es, kk, f), "hyp sat not extracted")
else:
check(f is None, "hyp non-solution extracted")
h_random()
h_struct()
h_malformed()
# ---------------- audit ----------------
print("\nPer-section check counts:")
for s, c in CHECKS.items():
print(" %-30s %d" % (s, c))
total = sum(CHECKS.values())
for f in FAILS[:50]:
print(f)
print("TOTAL: %d checks, %d failures" % (total, len(FAILS)))
return 1 if FAILS else 0
if __name__ == "__main__":
sys.exit(main()) |
Collaborator
Author
Agentic Review ReportSubject: rule Changed files: (a) Structural and semanticHard fails: none.
Rule checklist
Semantic check by hand
Issue compliance (body and all three comments)
(b) QualityThe 11 rule tests run in 0.06 s.
(c) Feature testThese were run from a scratch directory with the CLI built from this branch:
All outputs agree with the issue's example. FindingsCritical: none. Important: none. Minor
|
Collaborator
Author
|
The three Minor paper suggestions are deferred follow-ups: describe the swapped-color witness as conflicting on the same closing edge (its false clause is |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1228 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151853 +295
========================================
+ Hits 147308 147602 +294
- Misses 4250 4251 +1 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Collaborator
Author
|
Codecov reports 99.66102% patch coverage and 97.20% project coverage; both checks pass the configured 95% targets. The single uncovered patch line is in the |
Count the YES example's clause families from the loaded target, assert the odd-cycle structure the NO example relies on, and name the swapped assignment's own false clause on the closing edge.
Collaborator
Author
|
Addressed the three Minor paper points from the review in 0178e25 (paper only,
|
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the direct
KColoring/SimpleGraph/KN → Satisfiabilityreduction using vertex-major one-hot variables, pairwise exclusions, and edge/color conflict clauses. Extraction validates the SAT witness once and returns each vertex's unique selected color. Size arithmetic and literal indices are checked before allocation.Includes exact parameter transforms, a C5 canonical example, and the paper construction/proof with YES and NO examples. The encoding is cited to Faber–Jabrayilov–Mutzel (SAT 2024), §2.2, equations (8a)–(8b), with the pairwise at-most-one choice stated explicitly. Empty graphs, zero colors, isolated/disconnected graphs, excess colors, malformed witnesses, and overflow limits are covered; SimpleGraph rejects loops and parallel edges.
Validation:
make check: 7,218 tests and doctests passed; formatting and Clippy passed.make paper: passed.Fixes #1099