Repository navigation
Conversation
Collaborator
Author
Verification certificateVerdict: VERIFIED — HamiltonianCircuit/SimpleGraph → Satisfiability. Both exhaustive checks pass with zero failures, and the two constructions agree on all shared inputs. Types and semantics
Exhaustive and randomized coverageBoth checks cover all 1,100 labelled simple graphs through five vertices, compare all source permutations with the actual CNF, and extract all 3,942 satisfying Boolean assignments. The first uses Minisat22, with a complete Boolean cross-check through three vertices. The independent check exhausts Boolean assignments through four vertices with NumPy and uses CaDiCaL 1.5.3 at five vertices; it also checks the source using Held–Karp DP.
First-check Hypothesis settings: seed Independent-check settings: seeds The two constructions are identical, including literal and clause order, on 34,684 shared graphs: every simple graph through six vertices, 800 seeded graphs at sizes seven through ten (seed The five-cycle with chord 02 gives ReproductionSave the following files under the shown names in one directory. Run position_encoding_check.py#!/usr/bin/env python3
# /// script
# requires-python = ">=3.12"
# dependencies = ["sympy==1.14.0", "hypothesis==6.170.14", "python-sat==1.9.dev17"]
# ///
"""Construction-side checks; run with python3 or uv run --script.
Public comparison interface: reduce_graph(n, edges) -> (num_vars, clauses),
extract_solution(n, target, assignment) -> vertex ordering. Clauses are lists
of signed, 1-indexed integers, in the order specified by hamiltonian_sat_theorem.typ.
PySAT/Minisat22 decides and enumerates the actual CNF, including at n=5;
SAT search is never restricted to the permutation candidates.
"""
import os
from pathlib import Path
import sys
import traceback
from itertools import combinations, permutations, product
from math import comb, factorial
try:
import sympy as sp
from hypothesis import Phase, given, seed, settings, strategies as st
from pysat.solvers import Minisat22
except ModuleNotFoundError:
# Keep dependencies in uv's isolated script environment, never system Python.
if __name__ != "__main__":
raise
os.execvp("uv", ["uv", "run", "--script", str(Path(__file__).resolve()), *sys.argv[1:]])
SECTIONS = {
"1": "symbolic overhead identities and bounds",
"2": "exhaustive forward/backward feasibility and Hypothesis",
"3": "extraction from every satisfying SAT model",
"4": "measured sizes against derived exact counts and bounds",
"5": "structural validity and special cases",
"6": "YES example, both orientations, and mutation",
"7": "NO example and closing-edge rejection",
}
AUDIT = {section: [0, 0] for section in SECTIONS}
def check(section, condition, description):
AUDIT[section][0] += 1
if not condition:
AUDIT[section][1] += 1
if sum(counts[1] for counts in AUDIT.values()) <= 20:
print(f"FAIL section {section}: {description}", flush=True)
return bool(condition)
def reduce_graph(n, edges):
if n < 3:
return 1, [[1], [-1]]
adjacent = {frozenset((u, v)) for u, v in edges}
def literal(vertex, position):
return vertex * n + position + 1
clauses = []
for position in range(n):
clauses.append([literal(vertex, position) for vertex in range(n)])
clauses.extend([-literal(u, position), -literal(v, position)]
for u, v in combinations(range(n), 2))
for vertex in range(n):
clauses.append([literal(vertex, position) for position in range(n)])
clauses.extend([-literal(vertex, p), -literal(vertex, q)]
for p, q in combinations(range(n), 2))
for position in range(n):
successor = (position + 1) % n
for u in range(n):
for v in range(n):
if u == v or frozenset((u, v)) not in adjacent:
clauses.append([-literal(u, position), -literal(v, successor)])
return n * n, clauses
def extract_solution(n, target, assignment):
if n < 3 or not satisfies(target, assignment):
raise ValueError("target witness is not a satisfying assignment")
ordering = []
for position in range(n):
occupants = [v for v in range(n) if assignment[v * n + position]]
if len(occupants) != 1:
raise ValueError("position must have exactly one vertex")
ordering.append(occupants[0])
if len(set(ordering)) != n:
raise ValueError("vertices must not repeat")
return ordering
def is_circuit(n, edges, ordering):
"""Source semantics, independently expressed using vertex permutations."""
return (
n >= 3
and sorted(ordering) == list(range(n))
and all(
(u, v) in edges or (v, u) in edges
for u, v in zip(ordering, ordering[1:] + ordering[:1])
)
)
def encode_order(ordering):
"""Vertex-major matrix, expressed without the constructor's literal helper."""
return tuple(vertex == occupant for vertex in range(len(ordering)) for occupant in ordering)
def satisfies(target, assignment):
num_vars, clauses = target
return (
len(assignment) == num_vars
and all(isinstance(value, bool) for value in assignment)
and all(
any(assignment[abs(literal) - 1] == (literal > 0) for literal in clause)
for clause in clauses
)
)
def sizes(target):
num_vars, clauses = target
return num_vars, len(clauses), sum(map(len, clauses))
def exact_sizes(n, m):
if n < 3:
return 1, 2, 2
# Two positive families, two pairwise families, n forbidden-pair blocks.
return n * n, 2 * n + n * n * (n - 1) + n * (n * n - 2 * m), 4 * n**3 - 4 * n * m
def upper_bounds(n):
return n * n + 1, 2 * n + n * n * (n - 1) + n**3 + 2, 4 * n**3 + 2
def symbolic_checks():
n, m = sp.symbols("n m", integer=True, nonnegative=True)
forbidden = n**2 - 2 * m
pairwise = 2 * n * n * (n - 1) / 2
derived = (n**2, 2 * n + pairwise + n * forbidden,
2 * n**2 + 2 * pairwise + 2 * n * forbidden)
exact = (n**2, 2 * n + n**2 * (n - 1) + n * (n**2 - 2 * m), 4 * n**3 - 4 * n * m)
bounds = (n**2 + 1, 2 * n + n**2 * (n - 1) + n**3 + 2, 4 * n**3 + 2)
for label, measured, expected in zip(("variables", "clauses", "literals"), derived, exact):
check("1", sp.expand(measured - expected) == 0, f"derived {label}")
for bound, count, slack in zip(bounds, exact, (1, 2 * n * m + 2, 4 * n * m + 2)):
check("1", sp.expand(bound - count - slack) == 0, "bound-minus-exact identity")
check("1", sp.sympify(slack).is_nonnegative is True, "nonnegative main-branch slack")
for small_n in range(3):
for bound, count in zip(bounds, (1, 2, 2)):
check("1", bound.subs(n, small_n) >= count, f"small branch n={small_n}")
check("1", sp.expand(n * n * (n - 1) - pairwise) == 0, "pairwise coefficient normalization")
# At maximum legal m, forbidden pairs are exactly the n diagonal pairs.
check("1", sp.expand(forbidden.subs(m, n * (n - 1) / 2) - n) == 0,
"forbidden pairs at complete graph boundary")
check("1", sp.expand(n * n - forbidden - 2 * m) == 0, "two ordered pairs per edge")
def graph_cases():
for n in range(6):
possible = tuple(combinations(range(n), 2))
for mask in range(1 << len(possible)):
yield n, tuple(edge for bit, edge in enumerate(possible) if mask & (1 << bit))
def inspect_target(n, edges, target):
num_vars, clauses = target
context = f"n={n}, edges={edges}"
for measured, expected in zip(sizes(target), exact_sizes(n, len(edges))):
check("4", measured == expected, f"exact size: {context}")
for measured, bound in zip(sizes(target), upper_bounds(n)):
check("4", measured <= bound, f"upper bound: {context}")
check("5", all(clause for clause in clauses), f"no empty clauses: {context}")
check("5", all(type(lit) is int and 1 <= abs(lit) <= num_vars
for clause in clauses for lit in clause), f"signed literal range: {context}")
check("5", {abs(lit) for clause in clauses for lit in clause} == set(range(1, num_vars + 1)),
f"no unused variables: {context}")
check("5", all(len(clause) == len(set(map(abs, clause))) for clause in clauses),
f"no repeated variable within clause: {context}")
if n < 3:
check("5", target == (1, [[1], [-1]]), f"fixed contradiction: {context}")
else:
check("5", sum(len(clause) == n and all(lit > 0 for lit in clause)
for clause in clauses) == 2 * n, f"positive occupancy clauses: {context}")
check("5", all(len(clause) == n and all(lit > 0 for lit in clause)
or len(clause) == 2 and all(lit < 0 for lit in clause)
for clause in clauses), f"clause arities and signs: {context}")
block = 1 + comb(n, 2)
positions = clauses[:n * block:block]
vertices = clauses[n * block:2 * n * block:block]
check("5", positions == [list(range(p + 1, n * n + 1, n)) for p in range(n)],
f"vertex-major position block: {context}")
check("5", vertices == [list(range(v * n + 1, (v + 1) * n + 1)) for v in range(n)],
f"vertex-major vertex block: {context}")
check("5", all(sorted(lit for clause in family for lit in clause) == list(range(1, n * n + 1))
for family in (positions, vertices)), f"literal-index bijection in generated occupancy families: {context}")
def exhaustive_checks():
graph_counts = [0] * 6
witness_count = 0
for n, edges in graph_cases():
graph_counts[n] += 1
target = reduce_graph(n, edges)
inspect_target(n, edges, target)
source_witnesses = set()
for ordering in permutations(range(n)):
accepted = is_circuit(n, edges, ordering)
if accepted:
source_witnesses.add(ordering)
if n >= 3:
check("2", satisfies(target, encode_order(ordering)) == accepted,
f"permutation assignment iff circuit: n={n}, edges={edges}, order={ordering}")
else:
check("2", not accepted, f"small source rejected: n={n}, order={ordering}")
sat_witnesses = set()
sat_assignments = set()
with Minisat22(bootstrap_with=target[1]) as solver:
check("2", solver.solve() == bool(source_witnesses), f"independent SAT iff source: n={n}, edges={edges}")
for model in solver.enum_models():
positive = {lit for lit in model if lit > 0}
assignment = tuple(index in positive for index in range(1, target[0] + 1))
check("3", len(model) == target[0] and satisfies(target, assignment), "SAT model satisfies original CNF")
ordering = tuple(extract_solution(n, target, assignment))
check("3", is_circuit(n, edges, ordering), "every SAT model extracts a source circuit")
check("3", encode_order(ordering) == assignment, "extraction/encoding are exact inverses")
check("3", ordering not in sat_witnesses, "distinct SAT models preserve distinct orderings")
sat_witnesses.add(ordering)
sat_assignments.add(assignment)
witness_count += 1
check("3", sat_witnesses == source_witnesses, f"all and only source witnesses extracted: n={n}, edges={edges}")
if n <= 3:
boolean_models = set()
for assignment in product((False, True), repeat=target[0]):
evaluated = satisfies(target, assignment)
check("2", evaluated == (assignment in sat_assignments), "full Boolean enumeration agrees with SAT solver")
if evaluated:
boolean_models.add(assignment)
check("2", boolean_models == sat_assignments, "complete Boolean model set")
check("2", graph_counts == [1, 1, 2, 8, 64, 1024], "all labeled simple graphs through five vertices")
# Each ordering fixes n of binom(n,2) edges; each other edge is optional.
expected_witnesses = sum(factorial(n) * 2 ** (comb(n, 2) - n) for n in range(3, 6))
check("3", witness_count == expected_witnesses, "independently counted circuit/SAT witnesses")
print(f"EXHAUSTIVE: {sum(graph_counts)} graphs, n=0..5; {witness_count} SAT models extracted")
@st.composite
def arbitrary_graphs(draw):
n = draw(st.integers(min_value=0, max_value=6))
possible = tuple(combinations(range(n), 2))
edges = draw(st.sets(st.sampled_from(possible))) if possible else set()
return n, tuple(sorted(edges))
@st.composite
def shuffled_cycles_with_chords(draw):
n = draw(st.integers(min_value=3, max_value=7))
ordering = tuple(draw(st.permutations(tuple(range(n)))))
cycle = {tuple(sorted((ordering[p], ordering[(p + 1) % n]))) for p in range(n)}
extra = draw(st.sets(st.sampled_from(tuple(combinations(range(n), 2)))))
return n, tuple(sorted(cycle | extra)), ordering
@seed(20261102)
@settings(max_examples=100, deadline=None, database=None, phases=(Phase.generate, Phase.shrink))
@given(arbitrary_graphs())
def hypothesis_arbitrary_graphs(case):
n, edges = case
target = reduce_graph(n, edges)
expected = any(is_circuit(n, edges, ordering) for ordering in permutations(range(n)))
with Minisat22(bootstrap_with=target[1]) as solver:
assert check("2", solver.solve() == expected, "Hypothesis arbitrary graph feasibility")
if expected:
positives = {lit for lit in solver.get_model() if lit > 0}
assignment = tuple(i in positives for i in range(1, target[0] + 1))
assert check("3", is_circuit(n, edges, tuple(extract_solution(n, target, assignment))),
"Hypothesis arbitrary SAT witness extraction")
inspect_target(n, edges, target)
@seed(20261102)
@settings(max_examples=100, deadline=None, database=None, phases=(Phase.generate, Phase.shrink))
@given(shuffled_cycles_with_chords())
def hypothesis_cycles(case):
n, edges, ordering = case
target = reduce_graph(n, edges)
for orientation in (ordering, ordering[::-1]):
assignment = encode_order(orientation)
assert check("2", satisfies(target, assignment), "Hypothesis relabeled cycle orientation satisfies CNF")
assert check("3", tuple(extract_solution(n, target, assignment)) == orientation,
"Hypothesis orientation extracted without rotation or reversal")
inspect_target(n, edges, target)
def special_cases():
for n, edges in ((4, ((0, 1), (1, 2), (0, 2))),
(6, ((0, 1), (1, 2), (0, 2), (3, 4), (4, 5), (3, 5)))):
target = reduce_graph(n, edges)
with Minisat22(bootstrap_with=target[1]) as solver:
check("5", not solver.solve(), "isolated vertex or disconnected triangles are UNSAT")
check("5", not any(is_circuit(n, edges, p) for p in permutations(range(n))),
"isolated vertex or disconnected triangles have no source circuit")
for n, edges in ((3, ((0, 1), (1, 2), (0, 2))), (5, ((0, 1), (1, 2), (2, 3), (3, 4)))):
extended = edges + tuple((v, v) for v in range(n)) + edges + tuple((v, u) for u, v in edges)
check("5", reduce_graph(n, extended) == reduce_graph(n, edges), "loops and parallel copies preserve CNF")
for ordering in permutations(range(n)):
check("5", is_circuit(n, extended, ordering) == is_circuit(n, edges, ordering),
"loops and parallel copies preserve source acceptance")
def expect_rejected(n, target, assignment):
try:
extract_solution(n, target, assignment)
except ValueError:
return True
return False
def yes_example():
edges = ((0, 1), (1, 2), (2, 3), (3, 4), (0, 4), (0, 2))
target = reduce_graph(5, edges)
check("6", sizes(target) == (25, 175, 380), "YES counts from independently counted families")
check("6", upper_bounds(5) == (26, 237, 502), "YES overhead numbers")
for ordering, true_ids in (((0, 1, 2, 3, 4), (1, 7, 13, 19, 25)),
((0, 4, 3, 2, 1), (1, 22, 18, 14, 10))):
assignment = tuple(i in true_ids for i in range(1, 26))
check("6", is_circuit(5, edges, ordering), "explicit orientation is a source circuit")
check("6", satisfies(target, assignment), "literal-numbered orientation satisfies target")
check("6", tuple(extract_solution(5, target, assignment)) == ordering, "explicit orientation round trip")
for clause in ([-1, -17], [-5, -16], [-7, -18]):
check("6", clause in target[1], "worked forbidden-successor clause")
mutated = (0, 1, 3, 2, 4)
check("6", not is_circuit(5, edges, mutated), "swapped source witness rejected")
check("6", not satisfies(target, encode_order(mutated)), "swapped target witness rejected")
with Minisat22(bootstrap_with=target[1]) as solver:
check("6", sum(1 for _ in solver.enum_models()) == 10, "YES has ten SAT witnesses")
check("6", sum(is_circuit(5, edges, p) for p in permutations(range(5))) == 10, "YES has ten source orderings")
valid = encode_order((0, 1, 2, 3, 4))
for invalid in (valid[:-1], valid + (False,), (False,) * 25, (True,) * 25,
encode_order(mutated), encode_order((0, 0, 2, 3, 4))):
check("3", expect_rejected(5, target, invalid), "invalid target witness rejected before decoding")
def no_example():
edges = ((0, 1), (1, 2), (2, 3), (3, 4))
target = reduce_graph(5, edges)
check("7", sizes(target) == (25, 195, 420), "NO counts from independently counted families")
check("7", upper_bounds(5) == (26, 237, 502), "NO overhead numbers")
check("7", not any(is_circuit(5, edges, p) for p in permutations(range(5))), "all path permutations rejected")
with Minisat22(bootstrap_with=target[1]) as solver:
check("7", not solver.solve(), "path CNF is UNSAT over all Boolean assignments")
check("7", [-25, -1] in target[1], "explicit last-to-first forbidden clause")
check("7", not satisfies(target, encode_order((0, 1, 2, 3, 4))), "path-order target rejected at closure")
def main():
print("SAT: PySAT/Minisat22 on the full Boolean CNF, not permutation-only SAT")
print("HYPOTHESIS: two strategies, seed=20261102, max_examples=100 each, deadline=None, database=None")
symbolic_checks()
# Fixed independently calculated examples run before the exhaustive search.
yes_example()
no_example()
exhaustive_checks()
special_cases()
hypothesis_arbitrary_graphs()
hypothesis_cycles()
if __name__ == "__main__":
try:
main()
except Exception:
check("2", False, "verification aborted with an exception")
traceback.print_exc()
for section, description in SECTIONS.items():
checks, failures = AUDIT[section]
print(f"SECTION {section}: {checks} checks, {failures} failures — {description}")
total = sum(counts[0] for counts in AUDIT.values())
failed = sum(counts[1] for counts in AUDIT.values())
print(f"TOTAL: {total} checks, {failed} failures")
sys.exit(bool(failed))permutation_cnf.py"""Independent implementation of HamiltonianCircuit/SimpleGraph -> Satisfiability.
Absolute position encoding (Velev-Gao 2009).
Pure Python, no third-party imports, so other scripts can import it directly.
Conventions taken from the proof:
* vertices 0..n-1, positions 0..n-1;
* variable x[v,p] has signed literal number ell(v,p) = v*n + p + 1;
* n < 3 gives the fixed contradiction (1, [[1], [-1]]);
* clause order: position block (at-least-one, then pairwise u<v), vertex block
(at-least-one, then pairwise p<q), then successor block (p ascending, ordered
pairs (u, v) lexicographic, emitted when u == v or {u, v} is not an edge).
"""
from __future__ import annotations
from itertools import permutations
from typing import Iterable, Sequence
class ExtractionError(ValueError):
"""The target assignment does not encode a Hamiltonian circuit."""
def lit(n: int, v: int, p: int) -> int:
return v * n + p + 1
def adjacency(n: int, edges: Iterable[Sequence[int]]) -> list[list[bool]]:
"""Adjacency predicate A(u, v) on distinct vertices.
Loops are ignored and parallel copies collapse (the proof's mathematical
extension); endpoints out of range raise.
"""
adj = [[False] * n for _ in range(n)]
for e in edges:
u, v = int(e[0]), int(e[1])
if not (0 <= u < n and 0 <= v < n):
raise ValueError(f"edge {e} out of range for n={n}")
if u != v:
adj[u][v] = adj[v][u] = True
return adj
def reduce(n: int, edges: Iterable[Sequence[int]]) -> tuple[int, list[list[int]]]:
if n < 3:
return 1, [[1], [-1]]
adj = adjacency(n, edges)
clauses: list[list[int]] = []
# 3. position block
for p in range(n):
clauses.append([lit(n, v, p) for v in range(n)])
for u in range(n):
for v in range(u + 1, n):
clauses.append([-lit(n, u, p), -lit(n, v, p)])
# 4. vertex block
for v in range(n):
clauses.append([lit(n, v, p) for p in range(n)])
for p in range(n):
for q in range(p + 1, n):
clauses.append([-lit(n, v, p), -lit(n, v, q)])
# 5. successor block
for p in range(n):
q = (p + 1) % n
for u in range(n):
for v in range(n):
if u == v or not adj[u][v]:
clauses.append([-lit(n, u, p), -lit(n, v, q)])
return n * n, clauses
def clause_holds(clause: Sequence[int], assignment: Sequence[bool]) -> bool:
for l in clause:
val = assignment[abs(l) - 1]
if (l > 0) == val:
return True
return False
def satisfies(target: tuple[int, list[list[int]]], assignment: Sequence[bool]) -> bool:
num_vars, clauses = target
if len(assignment) != num_vars:
return False
return all(clause_holds(c, assignment) for c in clauses)
def is_hamiltonian_order(n: int, edges: Iterable[Sequence[int]], order: Sequence[int]) -> bool:
"""Source semantics, mirroring HamiltonianCircuit's evaluator."""
if n < 3 or len(order) != n:
return False
if sorted(order) != list(range(n)):
return False
adj = adjacency(n, edges)
return all(adj[order[i]][order[(i + 1) % n]] for i in range(n))
def hamiltonian_orders(n: int, edges: Iterable[Sequence[int]]) -> list[tuple[int, ...]]:
edges = list(edges)
if n < 3:
return []
return [o for o in permutations(range(n)) if is_hamiltonian_order(n, edges, o)]
def has_hamiltonian_circuit_dp(n: int, edges: Iterable[Sequence[int]]) -> bool:
"""Held-Karp bitmask DP, independent of the permutation enumerator."""
if n < 3:
return False
adj = adjacency(n, edges)
full = (1 << n) - 1
reach = [0] * (1 << n) # reach[mask] = bitset of end vertices of paths from 0 covering mask
reach[1] = 1
for mask in range(1, full + 1):
if not (mask & 1) or not reach[mask]:
continue
ends = reach[mask]
for v in range(n):
if ends >> v & 1:
for w in range(n):
if not (mask >> w & 1) and adj[v][w]:
reach[mask | 1 << w] |= 1 << w
ends = reach[full]
return any(ends >> v & 1 and adj[v][0] for v in range(1, n))
def encode(n: int, order: Sequence[int]) -> list[bool]:
a = [False] * (n * n)
for p, v in enumerate(order):
a[v * n + p] = True
return a
def extract(n: int, target: tuple[int, list[list[int]]], assignment: Sequence) -> list[int]:
num_vars, clauses = target
if len(assignment) != num_vars:
raise ExtractionError("wrong assignment length")
if any(not isinstance(b, bool) for b in assignment):
raise ExtractionError("non-Boolean entry")
if not satisfies(target, assignment):
raise ExtractionError("assignment falsifies a clause")
if n < 3:
raise ExtractionError("small branch has no satisfying assignment") # unreachable
return scan_positions(n, assignment)
def scan_positions(n: int, assignment: Sequence[bool]) -> list[int]:
"""The position scan alone (no clause validation), so its rejections can be tested."""
if len(assignment) != n * n:
raise ExtractionError("wrong assignment length")
order = []
for p in range(n):
hits = [v for v in range(n) if assignment[v * n + p]]
if len(hits) != 1:
raise ExtractionError(f"position {p} holds {len(hits)} vertices")
order.append(hits[0])
if len(set(order)) != n:
raise ExtractionError("repeated vertex")
return order
def exact_counts(n: int, m: int) -> tuple[int, int, int]:
if n < 3:
return 1, 2, 2
return n * n, 2 * n + n * n * (n - 1) + n * (n * n - 2 * m), 4 * n ** 3 - 4 * n * m
def upper_bounds(n: int) -> tuple[int, int, int]:
return n * n + 1, 2 * n + n * n * (n - 1) + n ** 3 + 2, 4 * n ** 3 + 2
def measured(target: tuple[int, list[list[int]]]) -> tuple[int, int, int]:
num_vars, clauses = target
return num_vars, len(clauses), sum(len(c) for c in clauses)independent_encoding_check.py# /// script
# requires-python = ">=3.10"
# dependencies = [
# "sympy==1.14.0",
# "hypothesis==6.170.14",
# "python-sat==1.9.dev17",
# "numpy>=1.26",
# ]
# ///
"""Independent exhaustive verification of HamiltonianCircuit/SimpleGraph -> Satisfiability.
Uses a separate absolute-position encoder.
Run: uv run --script independent_encoding_check.py
"""
from __future__ import annotations
import os
import sys
from collections import Counter
from itertools import combinations, permutations
from math import comb, factorial
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 # noqa: E402
from hypothesis import strategies as st # noqa: E402
from pysat.solvers import Solver # noqa: E402
from permutation_cnf import ( # noqa: E402
ExtractionError,
encode,
exact_counts,
extract,
hamiltonian_orders,
has_hamiltonian_circuit_dp,
is_hamiltonian_order,
measured,
reduce,
satisfies,
scan_positions,
upper_bounds,
)
SEED = 10984
SOLVER = "cadical153" # different solver from the first check
counts: Counter = Counter()
failures: list[str] = []
section = "?"
def check(cond: bool, msg: str) -> None:
counts[section] += 1
if not cond:
failures.append(f"[{section}] {msg}")
if len(failures) < 30:
print("FAIL:", section, msg)
def try_extract(n, target, a):
"""extract() where success is expected; a rejection becomes a failed check, not a crash."""
try:
return extract(n, target, a)
except ExtractionError as exc:
check(False, f"unexpected extraction rejection: {exc}")
return None
def expect_raise(fn, msg: str) -> None:
try:
fn()
except ExtractionError:
check(True, msg)
return
check(False, msg + " (no ExtractionError)")
# ---------------------------------------------------------------- helpers
def all_graphs(n: int):
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 connected(n: int, edges) -> bool:
if n == 0:
return True
adj = {v: set() for v in range(n)}
for u, v in edges:
adj[u].add(v)
adj[v].add(u)
seen, stack = {0}, [0]
while stack:
for w in adj[stack.pop()]:
if w not in seen:
seen.add(w)
stack.append(w)
return len(seen) == n
def bruteforce_models(target) -> set[tuple[bool, ...]]:
"""All satisfying assignments by full enumeration (numpy), num_vars <= 16."""
nv, clauses = target
idx = np.arange(1 << nv, dtype=np.int64)
bits = ((idx[:, None] >> np.arange(nv)) & 1).astype(bool) # column k = variable k+1
ok = np.ones(1 << nv, dtype=bool)
for c in clauses:
sat = np.zeros(1 << nv, dtype=bool)
for l in c:
col = bits[:, abs(l) - 1]
sat |= col if l > 0 else ~col
ok &= sat
return {tuple(bool(b) for b in bits[i]) for i in np.nonzero(ok)[0]}
def solver_models(target, limit=None) -> set[tuple[bool, ...]]:
nv, clauses = target
out = set()
with Solver(name=SOLVER, bootstrap_with=clauses) as s:
while s.solve():
model = s.get_model()
a = [False] * nv
for l in model:
if 1 <= abs(l) <= nv:
a[abs(l) - 1] = l > 0
out.add(tuple(a))
if limit is not None and len(out) >= limit:
break
s.add_clause([-(i + 1) if a[i] else (i + 1) for i in range(nv)])
return out
def solver_sat(target):
nv, clauses = target
with Solver(name=SOLVER, bootstrap_with=clauses) as s:
if not s.solve():
return None
a = [False] * nv
for l in s.get_model():
if 1 <= abs(l) <= nv:
a[abs(l) - 1] = l > 0
return a
# ---------------------------------------------------------------- 1. symbolic
def sec_symbolic():
global section
section = "1 symbolic"
n, m = sp.symbols("n m", integer=True, nonnegative=True)
b = n**2 - 2 * m
pos_cl, pos_lit = 2 * n, 2 * n * n # two at-least-one families, n clauses of n literals each
pair_cl = 2 * n * sp.binomial(n, 2)
succ_cl = n * b
clauses = sp.expand(sp.expand_func(pos_cl + pair_cl + succ_cl))
lits = sp.expand(sp.expand_func(pos_lit + 2 * pair_cl + 2 * succ_cl))
check(sp.expand(sp.expand_func(pair_cl) - n**2 * (n - 1)) == 0, "pairwise = n^2(n-1)")
check(sp.expand(clauses - (2 * n + n**2 * (n - 1) + n * (n**2 - 2 * m))) == 0, "clause formula")
check(sp.expand(lits - (4 * n**3 - 4 * n * m)) == 0, "literal formula 4n^3-4nm")
check(sp.expand(2 * n**2 + 2 * n**2 * (n - 1) + 2 * n * (n**2 - 2 * m) - (4 * n**3 - 4 * n * m)) == 0,
"proof's literal sum equals 4n^3-4nm")
vb, cb, lb = n**2 + 1, 2 * n + n**2 * (n - 1) + n**3 + 2, 4 * n**3 + 2
check(sp.expand(vb - n**2) == 1, "var slack 1")
check(sp.expand(cb - clauses - (2 * n * m + 2)) == 0, "clause slack 2nm+2")
check(sp.expand(lb - lits - (4 * n * m + 2)) == 0, "literal slack 4nm+2")
# small branch slack as the proof states
check(sp.expand(vb - 1 - n**2) == 0, "small var slack n^2")
check(sp.expand(cb - 2 - (2 * n + n**2 * (n - 1) + n**3)) == 0, "small clause slack")
check(sp.expand(lb - 2 - 4 * n**3) == 0, "small literal slack 4n^3")
for k in range(3):
s = (2 * n + n**2 * (n - 1) + n**3).subs(n, k)
check((s == 0) == (k == 0) and s >= 0, f"small clause slack zero exactly at n=0 (n={k}: {s})")
# nonnegativity of exact counts over 0 <= m <= C(n,2), n>=3 (checked on a grid; minima at m=C(n,2))
for k in range(3, 60):
M = comb(k, 2)
c_min = 2 * k + k * k * (k - 1) + k * (k * k - 2 * M)
l_min = 4 * k**3 - 4 * k * M
check(c_min > 0 and l_min > 0, f"counts positive at n={k}, m=C(n,2)")
check(k * k - 2 * M == k, "complete graph forbids only the n equal pairs")
# literal index bijection, symbolically: ell(v,p)=vn+p+1 ranges over 1..n^2
v, p = sp.symbols("v p", integer=True, nonnegative=True)
ell = v * n + p + 1
check(sp.simplify(ell.subs({v: 0, p: 0})) == 1 and sp.expand(ell.subs({v: n - 1, p: n - 1}) - n**2) == 0,
"ell range endpoints 1..n^2")
# ---------------------------------------------------------------- 2/3/4/5. exhaustive
def sec_exhaustive():
global section
total_graphs = 0
witness_total = 0
for n in range(0, 6):
for edges in all_graphs(n):
total_graphs += 1
m = len(edges)
target = reduce(n, edges)
nv, clauses = target
orders = hamiltonian_orders(n, edges)
encs = {tuple(encode(n, o)) for o in orders} if n >= 3 else set()
section = "2 equivalence"
dp = has_hamiltonian_circuit_dp(n, edges)
check(dp == bool(orders), f"DP vs permutations n={n} {edges}")
if n <= 4:
models = bruteforce_models(target)
via = "brute force"
else:
models = solver_models(target)
via = SOLVER
check(bool(models) == bool(orders), f"feasibility n={n} {edges} ({via})")
# stronger: satisfying assignments are exactly the encodings of source witnesses
check(models == encs, f"model set == encoded circuits n={n} {edges}")
if n <= 4:
check(solver_models(target) == models, f"{SOLVER} vs brute force n={n} {edges}")
if n >= 3 and not connected(n, edges):
check(not models and not orders, f"disconnected graph is NO n={n} {edges}")
if n >= 3:
deg = [0] * n
for u, w in edges:
deg[u] += 1
deg[w] += 1
if min(deg) < 2:
check(not models, f"vertex of degree<2 forces NO n={n} {edges}")
section = "3 extraction"
witness_total += len(models)
for a in models:
o = try_extract(n, target, list(a))
if o is None:
continue
check(is_hamiltonian_order(n, edges, o), f"extracted order valid {o}")
check(tuple(encode(n, o)) == a, "re-encoding recovers the assignment exactly")
rev = [o[0]] + o[:0:-1]
rev2 = list(reversed(o))
for r in (rev, rev2):
ra = encode(n, r)
check(tuple(ra) in models and r != o, f"other orientation {r} is a distinct witness")
check(try_extract(n, target, ra) == r, "other orientation extracts unchanged")
rot = o[1:] + o[:1]
check(try_extract(n, target, encode(n, rot)) == rot, "rotation extracts unchanged")
# every single-bit flip of a witness must be rejected
for i in range(nv):
bad = list(a)
bad[i] = not bad[i]
expect_raise(lambda: extract(n, target, bad), f"flip {i}")
expect_raise(lambda: scan_positions(n, bad), f"scan rejects flip {i}")
# non-Hamiltonian permutation matrices: well-formed blocks but must be rejected
if n >= 3:
for o in permutations(range(n)):
if o in set(orders):
continue
a = encode(n, o)
check(not satisfies(target, a), f"non-circuit permutation {o} unsatisfying")
expect_raise(lambda: extract(n, target, a), f"extract rejects non-circuit {o}")
check(scan_positions(n, a) == list(o), "scan alone reads a permutation matrix")
# wrong lengths, non-Booleans
expect_raise(lambda: extract(n, target, [False] * (nv - 1)), "short assignment")
expect_raise(lambda: extract(n, target, [False] * (nv + 1)), "long assignment")
if orders:
ints = [int(x) for x in encode(n, orders[0])]
expect_raise(lambda: extract(n, target, ints), "0/1 ints rejected as non-Boolean")
if n < 3:
for a in ([False], [True]):
expect_raise(lambda: extract(n, target, a), f"small branch {a}")
section = "4 sizes"
check(measured(target) == exact_counts(n, m), f"exact counts n={n} m={m}")
check(all(x <= y for x, y in zip(measured(target), upper_bounds(n))), f"bounds n={n} m={m}")
if n >= 3:
d = [y - x for x, y in zip(measured(target), upper_bounds(n))]
check(d == [1, 2 * n * m + 2, 4 * n * m + 2], f"slack n={n} m={m}: {d}")
fam_pos = [c for c in clauses if all(l > 0 for l in c)]
check(len(fam_pos) == 2 * n and all(len(c) == n for c in fam_pos), "2n positive clauses of size n")
b = n * n - 2 * m
check(len(clauses) - 2 * n - n * n * (n - 1) == n * b, "successor block size n*b")
else:
check(measured(target) == (1, 2, 2), "small tuple (1,2,2)")
check(target == (1, [[1], [-1]]), "small target literally [[1],[-1]]")
section = "5 structure"
check(all(len(c) > 0 for c in clauses), "no empty clause")
check(all(1 <= abs(l) <= nv for c in clauses for l in c), "literal range")
check(all(len({abs(l) for l in c}) == len(c) for c in clauses), "no repeated variable in a clause")
check(all(all(l > 0 for l in c) or all(l < 0 for l in c) for c in clauses), "clauses pure-sign")
if n >= 3:
check(sorted(v * n + p + 1 for v in range(n) for p in range(n)) == list(range(1, nv + 1)),
"ell bijection")
check(all(len(c) == 2 for c in clauses if c[0] < 0), "negative clauses binary")
# successor clauses link consecutive positions with q=(p+1) mod n
succ = clauses[2 * n + n * n * (n - 1):]
ok = True
for c in succ:
(u, p), (v, q) = divmod(-c[0] - 1, n), divmod(-c[1] - 1, n)
ok &= q == (p + 1) % n
ok &= u == v or (u, v) not in {(a, b) for a, b in edges} | {(b, a) for a, b in edges}
check(ok, "successor clauses are exactly forbidden consecutive pairs")
# duplicates (as sets): equal-successor clauses repeat vertex exclusions; proof keeps them
keys = Counter(frozenset(c) for c in clauses)
dup = sum(k - 1 for k in keys.values())
check(dup == n * n, f"exactly n^2 duplicate clauses retained (got {dup})")
section = "3 extraction"
expected = sum(factorial(n) * 2 ** (comb(n, 2) - n) for n in range(3, 6))
check(witness_total == expected == 3942, f"aggregate witness count {witness_total} vs {expected}")
section = "2 equivalence"
check(total_graphs == 1100, f"graph count {total_graphs}")
# ---------------------------------------------------------------- malformed blocks (direct)
def sec_malformed():
global section
section = "3 extraction"
for n in range(3, 7):
base = list(range(n))
a = encode(n, base)
for p in range(n):
z = list(a)
z[base[p] * n + p] = False # empty column
expect_raise(lambda: scan_positions(n, z), f"empty column n={n} p={p}")
for v in range(n):
if v != base[p]:
d = list(a)
d[v * n + p] = True # two vertices in a column
expect_raise(lambda: scan_positions(n, d), f"double column n={n} p={p} v={v}")
# repeated vertex: every column has exactly one entry but vertex 0 appears twice
rep = [0, 0] + list(range(2, n))
expect_raise(lambda: scan_positions(n, encode(n, rep)), f"repeated vertex n={n}")
expect_raise(lambda: scan_positions(n, [False] * (n * n)), "all false")
expect_raise(lambda: scan_positions(n, [True] * (n * n)), "all true")
expect_raise(lambda: scan_positions(n, a[:-1]), "short to scan")
# ---------------------------------------------------------------- 6. YES example
def sec_yes():
global section
section = "6 YES example"
n = 5
E = [(0, 1), (1, 2), (2, 3), (3, 4), (0, 4), (0, 2)]
t = reduce(n, E)
nv, cl = t
check(measured(t) == (25, 175, 380), f"sizes {measured(t)}")
check(upper_bounds(5) == (26, 237, 502), "bounds (26,237,502)")
check(25 - 2 * len(E) == 13, "b=13")
pos = [c for c in cl if all(l > 0 for l in c)]
check((len(pos), sum(map(len, pos))) == (10, 50), "positive (10,50)")
check((n * n * (n - 1), 2 * n * n * (n - 1)) == (100, 200), "pairwise (100,200)")
succ = cl[110:]
check((len(succ), sum(map(len, succ))) == (65, 130), "successor (65,130)")
fwd = [0, 1, 2, 3, 4]
a = encode(n, fwd)
check(sorted(i + 1 for i, x in enumerate(a) if x) == [1, 7, 13, 19, 25], "forward literal set")
check(satisfies(t, a) and try_extract(n, t, a) == fwd, "forward extracts")
rev = [0, 4, 3, 2, 1]
ra = encode(n, rev)
check({i + 1 for i, x in enumerate(ra) if x} == {1, 22, 18, 14, 10}, "reverse literal set")
check(satisfies(t, ra) and try_extract(n, t, ra) == rev, "reverse extracts")
check([-1, -17] in cl, "[-1,-17] present (literal order)")
check([-5, -16] in cl, "[-5,-16] present (literal order)")
sw = encode(n, [0, 1, 3, 2, 4])
falsified = [c for c in cl if not any((l > 0) == sw[abs(l) - 1] for l in c)]
check([-7, -18] in falsified, f"swap falsifies [-7,-18]; falsified={falsified}")
models = solver_models(t)
check(len(models) == 10, f"ten satisfying assignments ({len(models)})")
orders = hamiltonian_orders(n, E)
check(len(orders) == 10, "ten accepted orderings")
cycles = {frozenset(frozenset((o[i], o[(i + 1) % n])) for i in range(n)) for o in orders}
check(cycles == {frozenset(frozenset(e) for e in [(0, 1), (1, 2), (2, 3), (3, 4), (4, 0)])},
"the five-cycle is the only undirected Hamiltonian cycle")
check(models == {tuple(encode(n, o)) for o in orders}, "models = encoded orderings")
# ---------------------------------------------------------------- 7. NO example
def sec_no():
global section
section = "7 NO example"
n = 5
E = [(0, 1), (1, 2), (2, 3), (3, 4)]
t = reduce(n, E)
nv, cl = t
check(measured(t) == (25, 195, 420), f"sizes {measured(t)}")
check(25 - 2 * len(E) == 17, "b=17")
succ = cl[110:]
check((len(succ), sum(map(len, succ))) == (85, 170), "successor (85,170)")
check(hamiltonian_orders(n, E) == [], "no source circuit")
check(solver_sat(t) is None, "target UNSAT")
check(not solver_models(t), "zero target models")
nat = encode(n, [0, 1, 2, 3, 4])
falsified = [c for c in cl if not any((l > 0) == nat[abs(l) - 1] for l in c)]
check([-25, -1] in falsified, f"closing pair falsifies [-25,-1]; falsified={falsified}")
# every placement of vertex 0 violates a successor clause in every permutation assignment
for o in permutations(range(n)):
a = encode(n, o)
p = o.index(0)
nb = {o[(p - 1) % n], o[(p + 1) % n]}
check(nb != {1} and not satisfies(t, a), f"permutation {o} rejected")
# ---------------------------------------------------------------- special cases
def sec_special():
global section
section = "5 structure"
# loops and parallel edges (mathematical extension): CNF unchanged
for n in range(3, 6):
for edges in all_graphs(n):
noisy = edges + edges + [(v, v) for v in range(n)] + [(b, a) for a, b in edges]
check(reduce(n, noisy) == reduce(n, edges), "loops/parallels leave CNF unchanged")
m_raw = len(noisy)
if edges:
check(exact_counts(n, m_raw) != measured(reduce(n, noisy)),
"raw multiplicity would give wrong exact counts")
# disconnected graphs where each component contains a cycle
section = "2 equivalence"
for parts in ([3, 3], [3, 4], [4, 4], [3, 3, 3], [5, 3]):
n, edges, off = sum(parts), [], 0
for k in parts:
edges += [(off + i, off + j) for i, j in combinations(range(k), 2)] # complete components
off += k
t = reduce(n, edges)
check(solver_sat(t) is None and not has_hamiltonian_circuit_dp(n, edges),
f"disjoint cliques {parts} NO")
# isolated vertex attached to a complete graph
for k in range(3, 8):
edges = list(combinations(range(k), 2))
check(solver_sat(reduce(k + 1, edges)) is None, f"K{k}+isolated NO")
check(solver_sat(reduce(k, edges)) is not None, f"K{k} YES")
# ---------------------------------------------------------------- hypothesis
def run_instance(n, edges, tag):
global section
section = f"H {tag}"
t = reduce(n, edges)
m = len({frozenset(e) for e in edges if e[0] != e[1]})
check(measured(t) == exact_counts(n, m), "exact counts")
check(all(x <= y for x, y in zip(measured(t), upper_bounds(n))), "bounds")
src = has_hamiltonian_circuit_dp(n, edges)
a = solver_sat(t)
check(src == (a is not None), f"feasibility n={n} edges={edges}")
if a is not None:
o = try_extract(n, t, a)
check(o is not None and is_hamiltonian_order(n, edges, o), "extracted is a circuit")
check(encode(n, o) == a, "re-encode exact")
if n <= 6:
models = solver_models(t)
check(models == {tuple(encode(n, o)) for o in hamiltonian_orders(n, edges)}, "model set exact")
return src
@st.composite
def arbitrary_graph(draw):
n = draw(st.integers(0, 8))
pairs = list(combinations(range(n), 2))
dens = draw(st.sampled_from([0.2, 0.5, 0.7, 0.9]))
edges = [e for e in pairs if draw(st.floats(0, 1)) < dens]
return n, edges
@st.composite
def cycle_with_chords(draw):
n = draw(st.integers(3, 9))
perm = draw(st.permutations(list(range(n))))
edges = {frozenset((perm[i], perm[(i + 1) % n])) for i in range(n)}
chords = draw(st.lists(st.tuples(st.integers(0, n - 1), st.integers(0, n - 1)), max_size=2 * n))
edges |= {frozenset(c) for c in chords if c[0] != c[1]}
return n, sorted(tuple(sorted(e)) for e in edges)
@st.composite
def disconnected_or_isolated(draw):
k1 = draw(st.integers(1, 5))
k2 = draw(st.integers(1, 4))
n = k1 + k2
pairs = [(u, v) for u, v in combinations(range(n), 2) if (u < k1) == (v < k1)]
edges = [e for e in pairs if draw(st.booleans())]
perm = draw(st.permutations(list(range(n))))
return n, [(perm[u], perm[v]) for u, v in edges]
@st.composite
def complete_or_tiny(draw):
n = draw(st.integers(0, 7))
if n < 3 and draw(st.booleans()):
pairs = list(combinations(range(n), 2))
return n, [e for e in pairs if draw(st.booleans())]
return n, list(combinations(range(n), 2))
@st.composite
def multigraph(draw):
n = draw(st.integers(0, 6))
raw = draw(st.lists(st.tuples(st.integers(0, max(n - 1, 0)), st.integers(0, max(n - 1, 0))),
max_size=3 * n * n)) if n else []
return n, raw
HSET = settings(max_examples=150, deadline=None, database=None,
suppress_health_check=list(HealthCheck))
def sec_hypothesis():
@seed(SEED)
@HSET
@given(arbitrary_graph())
def h_arbitrary(g):
run_instance(*g, "arbitrary")
@seed(SEED + 1)
@HSET
@given(cycle_with_chords())
def h_cycle(g):
check(run_instance(*g, "cycle+chords"), "cycle with chords is YES")
@seed(SEED + 2)
@HSET
@given(disconnected_or_isolated())
def h_disc(g):
check(not run_instance(*g, "disconnected/isolated"), "disconnected is NO")
@seed(SEED + 3)
@HSET
@given(complete_or_tiny())
def h_complete(g):
n, e = g
r = run_instance(n, e, "complete/tiny")
check(r == (n >= 3 and len(e) == comb(n, 2)), "K_n YES iff n>=3; tiny graphs NO")
if n < 3:
check(reduce(n, e) == (1, [[1], [-1]]), "small contradiction")
elif n <= 6:
check(len(solver_models(reduce(n, e))) == factorial(n), "K_n has n! models")
@seed(SEED + 4)
@HSET
@given(multigraph())
def h_multi(g):
n, raw = g
simple = sorted({tuple(sorted(e)) for e in raw if e[0] != e[1]})
check(reduce(n, raw) == reduce(n, simple), "multigraph CNF = simplified CNF")
run_instance(n, raw, "multigraph")
for f in (h_arbitrary, h_cycle, h_disc, h_complete, h_multi):
f()
def main():
sec_symbolic()
sec_exhaustive()
sec_malformed()
sec_yes()
sec_no()
sec_special()
sec_hypothesis()
print("\nSection checks")
for k in sorted(counts):
print(f" {k:<26} {counts[k]:>8}")
total = sum(counts.values())
print(f" {'TOTAL':<26} {total:>8}")
print(f"failures: {len(failures)}")
if failures:
for f in failures[:50]:
print(" ", f)
sys.exit(1)
if total < 5000:
print("too few checks")
sys.exit(1)
print("INDEPENDENT CHECK PASSED")
if __name__ == "__main__":
main()hamiltonian_sat_theorem.typ#set document(title: "Hamiltonian Circuit to Satisfiability: absolute positions")
#set page(margin: 20mm)
#set text(size: 10pt)
= Theorem
For every finite undirected simple graph $G = (V,E)$, with
$V = {0, dots, n - 1}$ and $n = |V|$, the construction below produces
a CNF formula $F(G)$ that is satisfiable if and only if
HamiltonianCircuit/SimpleGraph accepts a vertex ordering of $G$.
For $n=0$, the vertex set is empty.
Extraction returns that ordering, including its orientation and starting vertex.
The construction has cubic size and takes $O(n^3)$ time with an adjacency table.
== Literature search and construction match
Miroslav N. Velev and Ping Gao, _Efficient SAT Techniques for Absolute
Encoding of Permutation Problems: Application to Hamiltonian Cycles_,
Proceedings of SARA 2009, AAAI Press, pp. 159–166,
#link("https://miroslav-velev.com/Velev_and_Gao_SARA09.pdf")[author-hosted paper].
The abstract (p. 159) introduces one object-position predicate for each pair.
“SAT Representation of HCPs” (p. 162) describes occupancy, positional
exclusivity, and exclusions for nonadjacent vertices in consecutive positions,
including the last-to-first pair for cycles. This is the direct Boolean
specialization of that absolute encoding. We retain explicit exactly-one
constraints on both matrix axes; equal-successor exclusions are redundant
for permutations but retained for a fixed construction. The paper also studies
other domain encodings and enumerative adjacency constraints, which are not
used here. Our literal order, small-instance branch, and counts are specified
and proved below rather than attributed to the paper.
Background: Stephen A. Cook, _The Complexity of Theorem-Proving Procedures_,
STOC 1971, pp. 151–158,
#link("https://doi.org/10.1145/800157.805047")[doi:10.1145/800157.805047],
establishes the generic NP-to-CNF result. Michael R. Garey and David S.
Johnson, _Computers and Intractability_, W. H. Freeman, 1979,
Appendix A1, GT37, p. 199, supplies the Hamiltonian Circuit definition.
Neither background reference is claimed to give this position encoding.
== Construction
An edge is an unordered pair of distinct vertices. Write $m = |E|$.
For vertices $u,v$, let $A(u,v)$ mean that their unordered pair belongs to $E$.
A clause is a disjunction of its literals, and the target is the conjunction
of the following clause list. Clauses are retained with multiplicity, without
normalization or removal of redundant clauses.
1. If $n < 3$, use one Boolean variable $z$ with literal number 1 and
clauses $(z)$ and $(not z)$, stored as `[[1], [-1]]`. Stop construction.
2. For $n >= 3$, introduce $x_(v,p)$ for every vertex $v$ and cyclic
position $p$ in $V$. It means that vertex $v$ occupies position $p$.
Fix the vertex-major literal index
$ell(v,p) = v n + p + 1$.
Positive `ell(v,p)` denotes $x_(v,p)$ and its negative denotes
$not x_(v,p)$. Assignment offset $v n + p$ holds that Boolean value.
This is a bijection from $V times V$ to the integers $1, dots, n^2$.
3. For positions $p$ in increasing order, append the at-least-one clause
$∨_(v in V) x_(v,p)$, then the clauses
$not x_(u,p) or not x_(v,p)$ for $0 <= u < v < n$, in lexicographic
pair order. Each position contains exactly one vertex.
4. For vertices $v$ in increasing order, append
$∨_(p in V) x_(v,p)$, then
$not x_(v,p) or not x_(v,q)$ for $0 <= p < q < n$, in lexicographic
pair order. Each vertex occurs in exactly one position.
5. For positions $p$ in increasing order, define $q = (p+1) mod n$.
Iterate ordered pairs $(u,v)$ lexicographically over $V times V$.
Whenever $u=v$ or $not A(u,v)$, append
$not x_(u,p) or not x_(v,q)$.
No other clauses or auxiliary variables are introduced.
For cross-comparison the variable numbering is fixed. Ignoring clause-list
order and literal order within each clause is an identity isomorphism on
variables; the canonical construction above fixes those orders as well.
== Correctness
*Forward (source YES ⇒ target SAT).* Let
$c = (c_0, dots, c_(n-1))$ be an accepted source ordering.
The source semantics give $n >= 3$, all vertices occur exactly once, and
$A(c_p,c_((p+1) mod n))$ holds at every position $p$.
Assign $x_(v,p)$ true precisely when $v=c_p$. Every position clause has
one true literal, and every position exclusion has at least one false
underlying variable. Every vertex clause has one true literal, and the
vertex exclusions hold because vertices do not repeat. In a successor
clause both underlying variables could be true only for the actual cyclic
successor pair, which is distinct and is an edge. Such a pair is not forbidden.
Thus every emitted successor clause holds, and the entire CNF is satisfied.
*Backward (target SAT ⇒ source YES).* Suppose an assignment satisfies the
emitted CNF. The one-variable branch has opposite unit clauses, so a
satisfying assignment implies $n >= 3$. At each position the positive
clause forces at least one vertex and the pairwise exclusions force at most
one; denote its unique vertex by $c_p$. For each vertex the positive row
clause forces an occurrence, and its pairwise exclusions prohibit any second
occurrence. Therefore $c$ is a permutation of $V$. Fix any cyclic position
$p$ and its successor $q$. If $c_p=c_q$ or their pair is absent from $E$,
step 5 contains the clause excluding exactly these two true matrix entries,
which the assignment would falsify. Hence each cyclic successor is a
distinct adjacent vertex, including $p=n-1$ and $q=0$. The source evaluator
accepts $c$. This argument establishes that every satisfying Boolean
assignment is the matrix of a permutation, with no unconstrained variables.
== Solution extraction
Validate the target witness once: its length is the target variable count,
its entries are Boolean, and every target clause holds. For $n >= 3$ scan
each position $p$ and return the unique $v$ whose offset $v n + p$ is true,
in position order. Reject a column with zero or multiple true entries rather
than substituting a vertex; reject repeated vertices. Correctness proves
these rejection cases cannot occur after successful validation.
There is no satisfying witness to extract in the small-instance branch.
The scan costs $O(n^2)$, in addition to validation of the $O(n^3)$ target.
Encoding this ordering recovers the original satisfying assignment exactly.
No rotation or reversal is identified: both orientations and every starting
vertex are preserved as distinct witnesses.
== Size overhead and derivation
For $n >= 3$, let $b = n^2 - 2m$ be the number of forbidden ordered
vertex pairs. Each of the $m$ undirected edges allows exactly two ordered
pairs; all $n$ equal pairs are forbidden. The two sets of positive clauses
contribute $2n$ clauses and $2n^2$ literal occurrences. The pairwise sets
contribute $2n binom(n,2) = n^2(n-1)$ clauses and twice as many literals.
Successor constraints contribute $n b$ clauses, with two literals each.
Counting the actual retained clauses, including redundant ones, gives:
#table(
columns: 3, inset: 6pt,
[Target parameter], [Exact for $n >= 3$], [Upper bound for all $n >= 0$],
[`num_vars`], [$n^2$], [$n^2+1$],
[`num_clauses`], [$2n+n^2(n-1)+n(n^2-2m)$],
[$2n+n^2(n-1)+n^3+2$],
[`num_literals`], [$2n^2+2n^2(n-1)+2n(n^2-2m) = 4n^3-4n m$],
[$4n^3+2$],
)
The exact small-branch tuple is $(1,2,2)$ for $n=0,1,2$.
In the main branch the bound-minus-exact differences are respectively
$1$, $2n m+2$, and $4n m+2$, all nonnegative. In the small branch the
variable-bound slack is $n^2$, the clause-bound slack is
$2n+n^2(n-1)+n^3$, and the literal-bound slack is $4n^3$.
The clause slack is zero at $n=0$ and positive at $n=1,2$.
Thus the bounds cover every branch, including the empty graph, and the
registration must declare `upper_bound`. They are not equalities.
Since $0 <= m <= binom(n,2)$, the main-branch counts are nonnegative.
No clause simplification changes these counts. Building the adjacency table
costs $O(n^2+m)$ and the nested clause loops cost $O(n^3)$.
Integer identities hold over mathematical integers; an implementation
must reject size or signed-literal overflow rather than wrap arithmetic.
== Special cases
- *Fewer than three vertices:* every source ordering is rejected; the fixed
contradiction rejects both Boolean values of $z$, independently of edges.
- *Isolated vertex, $n >= 3$:* it must occupy some position. The following
position must contain a distinct vertex, but its successor pair is forbidden.
Both the source and target are NO.
- *Disconnected graph, $n >= 3$:* a cyclic permutation visiting every vertex
must cross between components, since successive edges would otherwise keep
every visited vertex in one component. That crossing falsifies a successor
clause. Both sides are NO, even when each component contains a cycle.
- *Loops and parallel edges, as a mathematical extension:* retain the
adjacency predicate on distinct vertices and count $m$ as the number of
distinct unordered non-loop edges. A loop never permits an equal successor;
parallel copies never change the adjacency predicate. Thus adding either
leaves source feasibility, the CNF, and extraction unchanged. Raw edge
multiplicity cannot be substituted for $m$ in the exact counts. Rust
`SimpleGraph::try_new` and its deserializer reject loops and duplicate
undirected edges (`src/topology/graph.rs:109–170` for validation and
construction, `src/topology/graph.rs:302–312` for deserialization); these mathematical
extensions are not claimed to be accepted Rust inputs.
== YES example: five-cycle with chord 02
Let $n=5$ and
$E = {{0,1},{1,2},{2,3},{3,4},{0,4},{0,2}}$, so $m=6$.
There are 25 variables and $b=25-12=13$ forbidden ordered pairs.
The positive clauses number 10 and contain 50 literals; the pairwise clauses
number 100 and contain 200 literals; the successor clauses number 65 and
contain 130 literals. The totals are *25 variables, 175 clauses, 380 literals*.
The general bounds at $n=5$ give $(26,237,502)$.
The ordering $(0,1,2,3,4)$ sets exactly the literal numbers
$(1,7,13,19,25)$ true, with all other variables false. It satisfies all
clauses and extracts the same ordering, closing via edge $4$–$0$.
The reverse ordering $(0,4,3,2,1)$ sets exactly
$(1,22,18,14,10)$ true and also extracts unchanged.
The missing edge $0$–$3$ gives the clause $not x_(0,0) or not x_(3,1)$,
stored as `[-1, -17]`; its closing-position counterpart is `[-5, -16]`.
Swapping vertices 2 and 3 in the forward ordering gives $(0,1,3,2,4)$.
The forbidden step $1$–$3$ falsifies `[-7, -18]`.
There are exactly ten accepted orderings (five rotations of each orientation):
using chord $0$–$2$ would leave vertices 1 or the path through 3 and 4
outside the single spanning cycle, so the original five-cycle is the only
undirected Hamiltonian cycle.
== NO example: five-vertex path
Let $n=5$ and $E={{0,1},{1,2},{2,3},{3,4}}$, so $m=4$.
The target has 25 variables and $b=25-8=17$ forbidden ordered pairs.
Its positive and pairwise contributions remain $(10,50)$ and $(100,200)$
in (clauses, literals); successor contributions are $(85,170)$.
The totals are *25 variables, 195 clauses, 420 literals*, with bounds
$(26,237,502)$. Vertex 0 has only neighbor 1. A permutation cycle with
five distinct vertices would need two distinct neighbors of vertex 0, one
before and one after it. At least one of these two steps is absent from $E$,
contradicting source acceptance and falsifying the corresponding successor
clause in every permutation assignment. The backward proof rules out every
non-permutation satisfying assignment as well. There are zero source
circuits and zero target satisfying assignments. In the natural path order,
the closing pair $4$–$0$ falsifies `[-25, -1]`. |
Collaborator
Author
Review ReportSubject: rule Structural and semantic
Quality
Feature test
FindingsNone open. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1229 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151864 +306
========================================
+ Hits 147308 147612 +304
- Misses 4250 4252 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Collaborator
Author
Coverage pathsCodecov reports 99.34641% patch coverage and 97.20% project coverage; both status checks pass the configured 95% targets. The remaining rule gap is the fallible |
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
HamiltonianCircuit/SimpleGraph → Satisfiabilityreduction using Velev–Gao's absolute position encoding.predcan construct the CNF, recover the vertex ordering from a satisfying assignment, and map completed YES/NO values identically.The rule uses vertex-major literals
v*n+p+1, checked size/index arithmetic, and a fixed contradiction for graphs with fewer than three vertices. It includes the canonical five-cycle with chord 02, a paper entry and reference, and 12 rule tests covering all simple graphs through four vertices, both orientations, malformed witnesses, aggregate recovery and numeric boundaries.For the worked YES graph, the target has 25 variables, 175 clauses and 380 literals. The five-vertex path produces 25 variables, 195 clauses and 420 literals and is unsatisfiable.
Validation:
make check: 7,219 tests passed, including the unchanged shared example-consistency test.make paper: passed.pred reduceexactly on 1,117 graphs.pred reduce --aggregateand completed true/false recovery pass on the worked examples.Fixes #1098