Repository navigation
Conversation
Add the reduction from MinimumDominatingSet<SimpleGraph, One> to MinimumHittingSet: one set per vertex v holding its closed neighborhood N[v] over the vertex universe, with identity solution extraction. Includes unit tests, a canonical example, and a paper entry. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED. Both independent scripts pass and the cross-comparison agrees. Type chain. Source Construction. Universe = vertices; one set per vertex Constructor script (7 sections): 4,613,724 checks, 0 failures.
Adversary script (written from the proof alone): 10,749,390 checks, 0 failures.
Cross-comparison. 1,164 shared instances (all graphs for n = 3, 4, 5; paths, stars, complete graphs, cycles for n up to 12; edgeless graphs; complete graphs plus 2 isolated vertices; 25 seeded random graphs up to n = 10), plus 100 solved round trips through Examples. YES: path P5 (edges 01, 12, 23, 34) has the dominating set {1, 3}, optimum 2, reproduced number for number. NO: the same graph with bound k = 1 has no solution on either side (every selection of size ≤ 1 checked). Scripts and the Typst proof follow. Constructor script (Python)#!/usr/bin/env python3
"""Independent finite-model verification; see proof.typ for the full-domain proof.
Setup: uv venv .venv
uv pip install --python .venv/bin/python -r requirements.txt
Run: python3 constructor.py
The local environment is used when the invoking Python lacks the dependencies.
"""
import itertools
import os
from pathlib import Path
import sys
from collections import Counter
try:
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
except ImportError:
interpreter = Path(__file__).parent / ".venv/bin/python"
if interpreter.exists() and Path(sys.executable).absolute() != interpreter.absolute():
os.execv(str(interpreter), [str(interpreter), __file__, *sys.argv[1:]])
raise
SECTIONS = {
1: "symbolic overhead",
2: "exhaustive forward/backward and optima",
3: "extraction of every feasible target witness",
4: "measured target sizes",
5: "target structure and special cases",
6: "YES example",
7: "NO bounded example",
}
checks = Counter()
failures = Counter()
graphs_by_size = Counter()
configurations = 0
optimal_witnesses = 0
def check(section, condition, context):
checks[section] += 1
if not condition:
failures[section] += 1
raise AssertionError(f"section {section}: {context}")
def reduce(n, edges):
seen = set()
for edge in edges:
if len(edge) != 2 or not all(type(x) is int and 0 <= x < n for x in edge):
raise ValueError(f"endpoint out of range: {edge}")
u, v = edge
if u == v:
raise ValueError(f"self-loop: {edge}")
if frozenset(edge) in seen:
raise ValueError(f"repeated edge: {edge}")
seen.add(frozenset(edge))
neighborhoods = [{v} for v in range(n)]
for u, v in edges:
neighborhoods[u].add(v)
neighborhoods[v].add(u)
return {"universe_size": n, "sets": [sorted(row) for row in neighborhoods]}
def configurations_of(n):
return itertools.product((False, True), repeat=n)
def source_value(n, edges, config):
"""Source oracle: selected vertices spread domination across the edge list."""
if len(config) != n or any(type(bit) is not bool for bit in config):
raise ValueError("expected one bool per vertex")
dominated = {v for v, bit in enumerate(config) if bit}
for u, v in edges:
if config[u]:
dominated.add(v)
if config[v]:
dominated.add(u)
return sum(config) if len(dominated) == n else None
def target_value(target, config):
"""Target oracle uses only the constructed universe and family."""
if len(config) != target["universe_size"] or any(type(bit) is not bool for bit in config):
raise ValueError("expected one bool per universe element")
if all(any(config[element] for element in row) for row in target["sets"]):
return sum(config)
return None
def extract_solution(target, config):
if target_value(target, config) is None:
raise ValueError("target witness does not hit every set")
return tuple(config)
def all_graphs(max_n):
for n in range(max_n + 1):
possible = list(itertools.combinations(range(n), 2))
for mask in range(1 << len(possible)):
yield n, tuple(edge for i, edge in enumerate(possible) if mask & (1 << i))
def symbolic_overhead():
# Fit symbolic linear expressions to actual constructed targets, then compare
# them to the independently derived formulas. The proof establishes all n.
n, m = sp.symbols("n m", integer=True, nonnegative=True)
a, b, c = sp.symbols("a b c")
vertex, edge = sp.symbols("vertex edge", integer=True)
per_vertex = sp.Sum(1, (vertex, 0, n - 1)).doit()
per_edge = sp.Sum(2, (edge, 0, m - 1)).doit()
specimens = [(size, edges, reduce(size, edges)) for size, edges in all_graphs(4)]
metrics = (
(lambda target: target["universe_size"], per_vertex, n),
(lambda target: len(target["sets"]), per_vertex, n),
(lambda target: sum(map(len, target["sets"])), per_vertex + per_edge, n + 2 * m),
)
for measure, symbolic_count, expected in metrics:
equations = [a * size + b * len(edges) + c - measure(target)
for size, edges, target in specimens]
solutions = sp.solve(equations, (a, b, c), dict=True)
fitted = (a * n + b * m + c).subs(solutions[0]) if len(solutions) == 1 else None
check(1, fitted is not None and sp.simplify(fitted - symbolic_count) == 0
and sp.simplify(symbolic_count - expected) == 0,
f"measured symbolic overhead {fitted}, expected {expected}")
def measured_sizes(n, edges, target):
check(4, target["universe_size"] == n, (n, edges, "universe"))
check(4, len(target["sets"]) == n, (n, edges, "family multiplicity"))
check(4, sum(map(len, target["sets"])) == n + 2 * len(edges),
(n, edges, "incidence count"))
def structure(n, edges, target):
rows = target["sets"]
check(5, all(row == sorted(set(row)) and all(0 <= v < target["universe_size"] for v in row)
for row in rows), (n, edges, "valid normalized subsets"))
# Compare every incidence to the original edge relation, independently of
# how reduce builds its rows. Includes self-membership and absent edges.
adjacency = {frozenset(edge) for edge in edges}
check(5, len(rows) == n and all(
(u in rows[v]) == (u == v or frozenset((u, v)) in adjacency)
for v in range(n) for u in range(n)), (n, edges, "closed incidence"))
def check_witness(n, edges, target, config):
source = source_value(n, edges, config)
value = target_value(target, config)
check(2, (source is not None) == (value is not None), (n, edges, config, "feasibility"))
if value is not None:
decoded = extract_solution(target, config)
check(3, len(decoded) == n and decoded == config and source_value(n, edges, decoded) == value,
(n, edges, config, "identity extraction and value"))
else:
try:
extract_solution(target, config)
except ValueError:
rejected = True
else:
rejected = False
check(3, rejected, (n, edges, config, "reject non-solution"))
return source, value
def exhaustive():
global configurations, optimal_witnesses
for n, edges in all_graphs(6):
graphs_by_size[n] += 1
target = reduce(n, edges)
measured_sizes(n, edges, target)
structure(n, edges, target)
source_best = target_best = None
target_optima = []
for config in configurations_of(n):
configurations += 1
source, value = check_witness(n, edges, target, config)
if source is not None:
source_best = source if source_best is None else min(source_best, source)
if value is not None:
if target_best is None or value < target_best:
target_best, target_optima = value, [config]
elif value == target_best:
target_optima.append(config)
check(2, source_best == target_best, (n, edges, "optima"))
for config in target_optima:
optimal_witnesses += 1
decoded = extract_solution(target, config)
check(3, source_value(n, edges, decoded) == source_best,
(n, edges, config, "optimal extraction"))
def special_cases():
# Independent expected optima: edgeless, paths, cycles, stars, complete,
# and two disconnected three-vertex paths with an isolated vertex.
cases = [(0, (), 0), (1, (), 1), (6, (), 6)]
for n in range(3, 9):
path = tuple((v, v + 1) for v in range(n - 1))
cases.extend([
(n, path, (n + 2) // 3),
(n, (*path, (0, n - 1)), (n + 2) // 3),
(n, tuple((0, v) for v in range(1, n)), 1),
(n, tuple(itertools.combinations(range(n), 2)), 1),
])
cases.append((7, ((0, 1), (1, 2), (3, 4), (4, 5)), 3))
for n, edges, expected in cases:
target = reduce(n, edges)
measured_sizes(n, edges, target)
structure(n, edges, target)
values = [value for config in configurations_of(n)
if (value := target_value(target, config)) is not None]
check(5, min(values) == expected, (n, edges, "special-case optimum", expected))
for length in {max(0, n - 1), n + 1} - {n}:
try:
extract_solution(target, (False,) * length)
except ValueError:
rejected = True
else:
rejected = False
check(3, rejected, (n, length, "reject wrong length"))
if n:
# (1,)*n would hit every row if coerced to bools, so only a type check rejects it.
for probe in ((0,) * n, (1,) * n):
try:
extract_solution(target, probe)
except ValueError:
rejected = True
else:
rejected = False
check(3, rejected, (n, probe, "reject non-Boolean encoding"))
def admission():
# The library's simple-graph model rejects these; the proof's domain excludes them.
bad = [(3, ((1, 1),)), (3, ((0, 1), (0, 1))), (3, ((0, 1), (1, 0))),
(3, ((0, 3),)), (3, ((-1, 1),)), (0, ((0, 0),)), (2, ((0, 1, 1),))]
for n, edges in bad:
try:
reduce(n, edges)
except ValueError:
rejected = True
else:
rejected = False
check(5, rejected, (n, edges, "inadmissible graph rejected"))
check(5, reduce(3, ((0, 1), (1, 2)))["sets"] == [[0, 1], [0, 1, 2], [1, 2]], "admitted graph")
@st.composite
def arbitrary_graph_and_config(draw):
n = draw(st.integers(0, 10))
possible = list(itertools.combinations(range(n), 2))
present = draw(st.lists(st.booleans(), min_size=len(possible), max_size=len(possible)))
config = tuple(draw(st.lists(st.booleans(), min_size=n, max_size=n)))
return n, tuple(edge for edge, bit in zip(possible, present) if bit), config
@st.composite
def family_graph_and_config(draw):
n = draw(st.integers(3, 12))
family = draw(st.sampled_from(("empty", "path", "cycle", "star", "complete", "matching")))
path = tuple((v, v + 1) for v in range(n - 1))
edges = {
"empty": (), "path": path, "cycle": (*path, (0, n - 1)),
"star": tuple((0, v) for v in range(1, n)),
"complete": tuple(itertools.combinations(range(n), 2)),
"matching": tuple((v, v + 1) for v in range(0, n - 1, 2)),
}[family]
config = tuple(draw(st.lists(st.booleans(), min_size=n, max_size=n)))
return n, edges, config
@seed(20261103)
@settings(max_examples=300, deadline=None, database=None)
@given(arbitrary_graph_and_config())
def hypothesis_arbitrary(case):
hypothesis_case(case)
@seed(20261104)
@settings(max_examples=300, deadline=None, database=None)
@given(family_graph_and_config())
def hypothesis_families(case):
hypothesis_case(case)
def hypothesis_case(case):
n, edges, sampled = case
target = reduce(n, edges)
measured_sizes(n, edges, target)
structure(n, edges, target)
for config in {sampled, (False,) * n, (True,) * n, tuple(v % 2 == 0 for v in range(n))}:
check_witness(n, edges, target, config)
def examples():
n, edges = 5, ((0, 1), (1, 2), (2, 3), (3, 4))
target = reduce(n, edges)
expected = {"universe_size": 5, "sets": [[0, 1], [0, 1, 2], [1, 2, 3], [2, 3, 4], [3, 4]]}
check(6, target == expected, "five-vertex path, full target")
for chosen, expected_value in [({1, 3}, 2), ({0, 2, 4}, 3), ({0, 1, 3}, 3)]:
config = tuple(v in chosen for v in range(n))
check(6, target_value(target, config) == expected_value and
source_value(n, edges, extract_solution(target, config)) == expected_value,
(chosen, expected_value))
source_values = [source_value(n, edges, config) for config in configurations_of(n)]
target_values = [target_value(target, config) for config in configurations_of(n)]
check(6, min(v for v in source_values if v is not None) ==
min(v for v in target_values if v is not None) == 2, "YES bound 2, optima 2")
# Same graph with bound 1: enumerate the empty choice and all five singletons.
for config in configurations_of(n):
if sum(config) <= 1:
check(7, source_value(n, edges, config) is None and target_value(target, config) is None,
(config, "NO bound 1"))
check(7, not any(v is not None and v <= 1 for v in source_values) and
not any(v is not None and v <= 1 for v in target_values), "both bounded problems NO")
def main():
status = 0
try:
# Fixed expected results run before the general constructor checks.
examples()
admission()
symbolic_overhead()
exhaustive()
special_cases()
hypothesis_arbitrary()
hypothesis_families()
except Exception as error:
status = 1
print(f"FAILED: {type(error).__name__}: {error}")
if not sum(failures.values()):
failures[0] += 1
for section, name in SECTIONS.items():
print(f"Section {section} ({name}): {checks[section]} checks, {failures[section]} failures")
print(f"Exhaustive graphs by n: {dict(sorted(graphs_by_size.items()))}")
print(f"Exhaustive configurations: {configurations}; optimal target witnesses: {optimal_witnesses}")
print("Hypothesis: 2 strategies, max_examples=300 each, seeds=20261103/20261104, database=None, deadline=None")
print(f"TOTAL: {sum(checks.values())} checks, {sum(failures.values())} failures")
return status
if __name__ == "__main__":
sys.exit(main())Adversary script, main harness (Python)#!/usr/bin/env python3
"""Adversarial harness for MinimumDominatingSet/SimpleGraph/One -> MinimumHittingSet.
Independent of the constructor script. Every claim of the proof is
attacked by a named check group (see CLAIMS below). The harness is
parameterised by (reduce, extract) so that mutants.py can run it against
deliberately broken constructions and confirm that every group can fail.
Usage:
.venv/bin/python adversary.py [--max-n 6] [--examples 300]
Exit status 0 iff every check passes.
"""
from __future__ import annotations
import argparse
import math
import os
import sys
from collections import Counter
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import core # noqa: E402
from core import ( # noqa: E402
INFEASIBLE,
InvalidConfiguration,
InvalidInput,
all_configs,
all_graphs,
source_eval,
target_eval,
)
SEEDS = (11960301, 11960302, 11960303)
EXAMPLES_RUN = Counter()
# claim -> check group(s) that attack it
CLAIMS = {
"Overhead universe_size = n, num_sets = n, incidences n+2m": ["overhead", "symbolic"],
"(=>) dominating set hits every row, same count": ["forward"],
"(<=) hitting set dominates, same count": ["backward"],
"Optimum equal; bounded equivalence for every k": ["optimum", "bounded"],
"Extraction validates once, copies, every feasible/optimal witness": ["extraction"],
"Extraction rejects wrong length / non-Boolean / unhit": ["reject"],
"Row v = N[v], sorted, in range, diagonal, labels kept, dup rows kept": ["structure"],
"Admission: loops, repeated (incl. reversed), out-of-range rejected": ["admission"],
"YES example P5 number-for-number": ["yes_example"],
"NO example P5 bound k=1": ["no_example"],
"Special cases prose (empty, isolated, disconnected, families, all-false)": ["special"],
"Larger / patterned instances (Hypothesis, 3 strategies)": ["hyp_random", "hyp_family", "hyp_dense"],
}
class Checks:
def __init__(self):
self.ok = Counter()
self.bad = Counter()
self.first = {}
self.site_ok = Counter() # (group, line) -> passes
self.site_bad = Counter() # (group, line) -> failures
def check(self, group, cond, detail="", _depth=1):
site = (group, sys._getframe(_depth).f_lineno)
if cond:
self.ok[group] += 1
self.site_ok[site] += 1
else:
self.bad[group] += 1
self.site_bad[site] += 1
self.first.setdefault(group, detail)
def merge(self, other, group=None):
"""Fold another Checks in, optionally relabelling its groups."""
for (g, line), c in other.site_ok.items():
self.site_ok[(group or g, line)] += c
self.ok[group or g] += c
for (g, line), c in other.site_bad.items():
self.site_bad[(group or g, line)] += c
self.bad[group or g] += c
for g, d in other.first.items():
self.first.setdefault(group or g, f"[{g}] {d}" if group else d)
def total(self):
return sum(self.ok.values()) + sum(self.bad.values())
def failed(self):
return sum(self.bad.values())
def raises(fn, exc_type):
"""True iff fn() raises exc_type (any other exception propagates)."""
try:
fn()
except exc_type:
return True
return False
def adjacency(n, edges):
adj = [[False] * n for _ in range(n)]
for u, v in edges:
adj[u][v] = adj[v][u] = True
return adj
# --------------------------------------------------------- per-instance ---
def attack_instance(C, n, edges, reduce, extract, exhaustive=True, configs=None):
"""All per-instance checks. exhaustive: enumerate all 2^n configs."""
tag = f"n={n} E={edges}"
try:
target = reduce(n, list(edges))
except Exception as exc: # a correct reduction never raises on admitted input
C.check("structure", False, f"{tag}: reduce raised {exc!r}")
return None
U, sets = target
m = len(edges)
adj = adjacency(n, edges)
# overhead (measured)
C.check("overhead", U == n, f"{tag}: universe {U}")
C.check("overhead", len(sets) == n, f"{tag}: num_sets {len(sets)}")
C.check("overhead", sum(len(r) for r in sets) == n + 2 * m, f"{tag}: incidences")
# structure: row v is exactly {v} u N(v), sorted, distinct, in range
for v in range(n):
row = sets[v] if v < len(sets) else None
expect = [u for u in range(n) if u == v or adj[v][u]]
C.check("structure", row == expect, f"{tag}: row {v} = {row}, want {expect}")
if row:
C.check("structure", all(0 <= e < U for e in row), f"{tag}: range row {v}")
C.check("structure", list(row) == sorted(set(row)), f"{tag}: sort row {v}")
C.check("structure", bool(row), f"{tag}: empty row {v}")
C.check("structure", len(sets) == n, f"{tag}: row count (dup rows retained)")
# semantics over configurations
space = all_configs(n) if exhaustive else configs
src_opt = tgt_opt = None
src_vals, tgt_vals = Counter(), Counter()
opt_witnesses = []
for x in space:
sv = source_eval(n, edges, x)
try:
tv = target_eval(target, x)
except InvalidConfiguration:
C.check("forward", False, f"{tag}: target rejected length-n config")
continue
if sv is not INFEASIBLE:
C.check("forward", tv == sv, f"{tag}: x={x} src {sv} tgt {tv}")
src_vals[sv] += 1
if src_opt is None or sv < src_opt:
src_opt = sv
if tv is not INFEASIBLE:
C.check("backward", sv == tv, f"{tag}: y={x} tgt {tv} src {sv}")
tgt_vals[tv] += 1
if tgt_opt is None or tv < tgt_opt:
tgt_opt = tv
# extraction of every feasible target witness
try:
xs = extract(target, list(x))
C.check("extraction", len(xs) == n, f"{tag}: extracted length")
C.check("extraction", source_eval(n, edges, xs) == tv,
f"{tag}: extracted {xs} from {x} value differs")
C.check("extraction", xs == list(x), f"{tag}: not identity")
opt_witnesses.append((x, xs))
except Exception as exc:
C.check("extraction", False, f"{tag}: extract raised on feasible {x}: {exc!r}")
else:
C.check("backward", sv is INFEASIBLE, f"{tag}: y={x} tgt infeasible src {sv}")
C.check("reject", raises(lambda: extract(target, list(x)), InvalidConfiguration),
f"{tag}: extract accepted unhit {x}")
if exhaustive:
C.check("optimum", src_opt == tgt_opt, f"{tag}: opt {src_opt} vs {tgt_opt}")
C.check("optimum", src_opt is not None, f"{tag}: no dominating set")
for x, xs in opt_witnesses:
if target_eval(target, x) == tgt_opt:
C.check("extraction", source_eval(n, edges, xs) == src_opt,
f"{tag}: optimal witness not source-optimal")
# bounded: exists size<=k on both sides, every k
for k in range(-1, n + 2):
s = any(v <= k for v in src_vals)
t = any(v <= k for v in tgt_vals)
C.check("bounded", s == t, f"{tag}: k={k} src {s} tgt {t}")
C.check("bounded", src_vals == tgt_vals, f"{tag}: value histograms differ")
# rejection of malformed witnesses
for bad in ([False] * (n + 1), [False] * max(n - 1, 0) if n > 0 else [True]):
C.check("reject", raises(lambda: extract(target, bad), InvalidConfiguration),
f"{tag}: accepted length {len(bad)}")
if n > 0:
for bad in ([1] * n, [None] * n, ["true"] * n):
C.check("reject", raises(lambda: extract(target, bad), InvalidConfiguration),
f"{tag}: accepted non-Boolean {bad}")
C.check("special", target_eval(target, [False] * n) is INFEASIBLE,
f"{tag}: all-false hits every row")
C.check("special", target_eval(target, [True] * n) == n, f"{tag}: all-true value")
return target, src_opt
def safe_attack(C, n, edges, reduce, extract, **kw):
"""A broken construction may crash a check; count that as a failure."""
try:
attack_instance(C, n, edges, reduce, extract, **kw)
except Exception as exc:
C.check("crash", False, f"n={n} E={edges}: {exc!r}")
# --------------------------------------------------------------- groups ---
def run_exhaustive(C, reduce, extract, max_n, samples):
graphs = 0
for n in range(max_n + 1):
for edges in all_graphs(n):
safe_attack(C, n, edges, reduce, extract)
graphs += 1
samples.append((n, edges))
return graphs
def run_symbolic(C, reduce):
import sympy as sp
n, m, a, b, c = sp.symbols("n m a b c")
rows = []
for nn in range(5):
for edges in all_graphs(nn):
U, sets = reduce(nn, edges)
rows.append((nn, len(edges), U, len(sets), sum(len(r) for r in sets)))
for idx, formula in ((2, n), (3, n), (4, n + 2 * m)):
eqs = [sp.Eq(a * r[0] + b * r[1] + c, r[idx]) for r in rows]
sol = sp.solve(eqs, [a, b, c], dict=True)
fitted = sp.expand((a * n + b * m + c).subs(sol[0])) if sol else None
C.check("symbolic", fitted is not None and sp.simplify(fitted - formula) == 0,
f"column {idx}: fitted {fitted} vs {formula}")
def run_admission(C, reduce):
bad_inputs = [
(2, [(0, 0)]),
(3, [(0, 1), (0, 1)]),
(3, [(0, 1), (1, 0)]),
(2, [(0, 2)]),
(2, [(-1, 0)]),
(3, [(1, 2), (2, 2)]),
]
for n, edges in bad_inputs:
try:
rejected = raises(lambda: reduce(n, edges), InvalidInput)
except Exception as exc: # wrong kind of error
rejected = False
C.check("admission", rejected, f"accepted {n} {edges}")
def run_examples(C, reduce, extract):
n, edges = 5, [(0, 1), (1, 2), (2, 3), (3, 4)]
target = reduce(n, edges)
want = (5, [[0, 1], [0, 1, 2], [1, 2, 3], [2, 3, 4], [3, 4]])
C.check("yes_example", (target[0], [list(r) for r in target[1]]) == want, f"P5 target {target}")
C.check("yes_example", [len(r) for r in target[1]] == [2, 3, 3, 3, 2])
C.check("yes_example", sum(len(r) for r in target[1]) == 13)
y = [False, True, False, True, False]
inters = [sorted(set(r) & {1, 3}) for r in target[1]]
C.check("yes_example", inters == [[1], [1], [1, 3], [3], [3]], f"intersections {inters}")
C.check("yes_example", target_eval(target, y) == 2)
try:
x = extract(target, y)
C.check("yes_example", x == y and source_eval(n, edges, x) == 2)
except Exception as exc:
C.check("yes_example", False, f"extract raised {exc!r}")
for sel in ({0, 2, 4}, {0, 1, 3}):
v = [i in sel for i in range(n)]
C.check("yes_example", target_eval(target, v) == 3 and source_eval(n, edges, v) == 3,
f"suboptimal {sel}")
try:
C.check("yes_example", source_eval(n, edges, extract(target, v)) == 3)
except Exception as exc:
C.check("yes_example", False, f"suboptimal extract {exc!r}")
C.check("yes_example", min(v for v in (target_eval(target, c) for c in all_configs(n))
if v is not None) == 2, "optimum 2")
# NO (bounded k = 1): empty + 5 singletons, table of missed rows
C.check("no_example", target_eval(target, [False] * n) is INFEASIBLE)
C.check("no_example", source_eval(n, edges, [False] * n) is INFEASIBLE)
table = {0: ({0, 1}, 2), 1: ({0, 1, 2}, 3), 2: ({1, 2, 3}, 0), 3: ({2, 3, 4}, 0), 4: ({3, 4}, 0)}
rows = [set(r) for r in target[1]]
for s, (dom, missed) in table.items():
v = [i == s for i in range(n)]
# proof: s dominates v iff s is in row F_v; read it off the target
actual_dom = {u for u in range(n) if s in rows[u]}
C.check("no_example", actual_dom == dom, f"dominated by {s}")
C.check("no_example", s not in rows[missed], f"row {missed} hit by {s}")
C.check("no_example", target_eval(target, v) is INFEASIBLE, f"singleton {s} hits")
C.check("no_example", source_eval(n, edges, v) is INFEASIBLE, f"singleton {s} dominates")
small = [c for c in all_configs(n) if c.count(True) <= 1]
C.check("no_example", len(small) == 6 and all(target_eval(target, c) is INFEASIBLE for c in small))
def path(n):
return [(i, i + 1) for i in range(n - 1)]
def cycle(n):
return path(n) + [(0, n - 1)]
def star(n):
return [(0, i) for i in range(1, n)]
def complete(n):
return core.all_edges(n)
def disjoint(*parts):
n, edges = 0, []
for pn, pe in parts:
edges += [(u + n, v + n) for u, v in pe]
n += pn
return n, edges
def target_opt(target):
return core.brute_min(lambda y: target_eval(target, y), target[0])
def run_special(C, reduce, extract):
# empty graph
t = reduce(0, [])
C.check("special", t[0] == 0 and list(t[1]) == [], f"empty {t}")
C.check("special", target_eval(t, []) == 0)
C.check("special", extract(t, []) == [] if t[0] == 0 else False)
C.check("special", raises(lambda: extract(t, [False]), InvalidConfiguration),
"empty accepted length 1")
# single vertex, edgeless
t = reduce(1, [])
C.check("special", [list(r) for r in t[1]] == [[0]], f"K1 {t}")
for nn in range(1, 9):
t = reduce(nn, [])
C.check("special", target_opt(t) == nn, f"edgeless {nn}")
C.check("special", all(list(r) == [v] for v, r in enumerate(t[1])), f"edgeless rows {nn}")
# disconnected: 2 P3 + isolated
nn, ee = disjoint((3, path(3)), (3, path(3)), (1, []))
t = reduce(nn, ee)
C.check("special", len(t[1]) == 7, "2P3+K1 rows")
C.check("special", target_opt(t) == 3, "2P3+K1 optimum")
comp = [0, 0, 0, 1, 1, 1, 2]
C.check("special", all(len({comp[e] for e in r}) == 1 for r in t[1]), "row crosses component")
# families; ceil(n/3) for paths and cycles n >= 3; also paths n=1,2
for nn in range(1, 11):
C.check("special", target_opt(reduce(nn, path(nn))) == math.ceil(nn / 3), f"P{nn}")
for nn in range(3, 11):
C.check("special", target_opt(reduce(nn, cycle(nn))) == math.ceil(nn / 3), f"C{nn}")
for nn in range(1, 10):
C.check("special", target_opt(reduce(nn, star(nn))) == 1, f"star{nn}")
t = reduce(nn, complete(nn))
C.check("special", target_opt(t) == 1, f"K{nn}")
C.check("special", len(t[1]) == nn and all(list(r) == list(range(nn)) for r in t[1]),
f"K{nn} rows all V, duplicates retained")
# ----------------------------------------------------------- hypothesis ---
def run_hypothesis(C, reduce, extract, examples, samples):
from hypothesis import HealthCheck, given, settings, seed
from hypothesis import strategies as st
cfg = settings(max_examples=examples, deadline=None, database=None, derandomize=False,
suppress_health_check=list(HealthCheck))
@st.composite
def random_graph(draw, max_n=11):
n = draw(st.integers(0, max_n))
pairs = core.all_edges(n)
p = draw(st.sampled_from([0.0, 0.1, 0.3, 0.5, 0.8, 1.0]))
mask = draw(st.lists(st.floats(0, 1, allow_nan=False), min_size=len(pairs),
max_size=len(pairs)))
return n, [e for e, r in zip(pairs, mask) if r < p or (p == 1.0)]
def patterned_configs(n, extra):
cfgs = [[False] * n, [True] * n, [i % 2 == 0 for i in range(n)],
[i % 2 == 1 for i in range(n)], [i % 3 == 1 for i in range(n)]]
cfgs += [[False if i == j else True for i in range(n)] for j in range(n)] # all-but-one
cfgs += [[i == j for i in range(n)] for j in range(n)] # singletons
return cfgs + extra
def do(group, n, edges, extra):
before = C.failed()
sub = Checks()
safe_attack(sub, n, edges, reduce, extract, exhaustive=n <= 10,
configs=patterned_configs(n, extra))
C.merge(sub, group)
samples.append((n, edges))
EXAMPLES_RUN[group] += 1
return C.failed() == before
@seed(SEEDS[0])
@cfg
@given(g=random_graph(), data=st.data())
def h_random(g, data):
n, edges = g
extra = data.draw(st.lists(st.lists(st.booleans(), min_size=n, max_size=n), max_size=8))
do("hyp_random", n, edges, extra)
@st.composite
def family_graph(draw):
kind = draw(st.sampled_from(["path", "cycle", "star", "complete", "edgeless",
"complete+isolated", "union", "matching"]))
k = draw(st.integers(1, 7))
if kind == "path":
return k, path(k)
if kind == "cycle":
k = max(k, 3)
return k, cycle(k)
if kind == "star":
return k, star(k)
if kind == "complete":
return k, complete(k)
if kind == "edgeless":
return k, []
if kind == "complete+isolated":
return disjoint((k, complete(k)), (draw(st.integers(1, 3)), []))
if kind == "matching":
return disjoint(*[(2, [(0, 1)])] * draw(st.integers(1, 5)))
a = draw(random_graph(max_n=5))
b = draw(random_graph(max_n=5))
return disjoint(a, b)
@seed(SEEDS[1])
@cfg
@given(g=family_graph())
def h_family(g):
n, edges = g
do("hyp_family", n, edges, [])
@st.composite
def dense_graph(draw):
# complete graph minus a few edges, randomly relabelled edge order and
# endpoint orientation (attacks orientation and ordering assumptions)
n = draw(st.integers(2, 10))
pairs = core.all_edges(n)
drop = draw(st.sets(st.sampled_from(pairs), max_size=3))
edges = [e for e in pairs if e not in drop]
edges = draw(st.permutations(edges))
flips = draw(st.lists(st.booleans(), min_size=len(edges), max_size=len(edges)))
return n, [(v, u) if f else (u, v) for (u, v), f in zip(edges, flips)]
@seed(SEEDS[2])
@cfg
@given(g=dense_graph())
def h_dense(g):
n, edges = g
do("hyp_dense", n, edges, [])
h_random()
h_family()
h_dense()
# ------------------------------------------------------------------ main ---
def run_all(reduce=core.reduce, extract=core.extract, max_n=6, examples=300, samples=None):
C = Checks()
samples = [] if samples is None else samples
graphs = run_exhaustive(C, reduce, extract, max_n, samples)
for group_fn in (lambda: run_symbolic(C, reduce),
lambda: run_admission(C, reduce),
lambda: run_examples(C, reduce, extract),
lambda: run_special(C, reduce, extract),
lambda: run_hypothesis(C, reduce, extract, examples, samples)):
try:
group_fn()
except Exception as exc: # a broken construction may crash a group
C.check("crash", False, repr(exc))
return C, graphs
def main():
ap = argparse.ArgumentParser()
ap.add_argument("--max-n", type=int, default=6)
ap.add_argument("--examples", type=int, default=300)
args = ap.parse_args()
C, graphs = run_all(max_n=args.max_n, examples=args.examples)
print(f"exhaustive graphs n<=%d: {graphs}" % args.max_n)
print(f"hypothesis: 3 strategies x {args.examples} examples, seeds {SEEDS}, "
f"database=None, deadline=None; examples run {dict(EXAMPLES_RUN)}")
groups = sorted(set(C.ok) | set(C.bad))
for g in groups:
print(f" {g:12s} pass {C.ok[g]:>9d} fail {C.bad[g]:>6d}"
+ (f" first: {C.first[g]}" if g in C.first else ""))
print("claim map:")
for claim, gs in CLAIMS.items():
print(f" {claim}: {', '.join(gs)} ({sum(C.ok[g] for g in gs)} checks)")
assert all(C.ok[g] > 0 for g in gs), f"empty group for {claim}"
print(f"TOTAL checks {C.total()} failures {C.failed()}")
return 1 if C.failed() else 0
if __name__ == "__main__":
sys.exit(main())Adversary script, reference construction (Python)"""Independent re-implementation of the construction in the proof.
Written from the proof text alone (no import of, or reference to, the
constructor script). Graph instances are (n, edges) with edges a list of
2-tuples; targets are (universe_size, sets) with sets a list of lists.
Source evaluator and target evaluator are deliberately written in different
styles so that they do not share a mistake: the source oracle spreads
selection along the edge list, the target oracle scans rows.
"""
from __future__ import annotations
from itertools import combinations, product
INFEASIBLE = None # stands for Min(None)
class InvalidInput(ValueError):
"""Instance rejected by the (simple-graph) admission rules."""
class InvalidConfiguration(ValueError):
"""Wrong length or non-Boolean configuration."""
# ----------------------------------------------------------------- source ---
def validate_simple_graph(n, edges):
"""Admission rules the proof attributes to SimpleGraph::try_new."""
if not isinstance(n, int) or isinstance(n, bool) or n < 0:
raise InvalidInput(f"bad vertex count {n!r}")
seen = set()
for e in edges:
if len(e) != 2:
raise InvalidInput(f"bad edge {e!r}")
u, v = e
for w in (u, v):
if not isinstance(w, int) or isinstance(w, bool) or not 0 <= w < n:
raise InvalidInput(f"endpoint {w!r} out of range")
if u == v:
raise InvalidInput(f"self-loop at {u}")
key = frozenset((u, v))
if key in seen:
raise InvalidInput(f"repeated edge {e!r}")
seen.add(key)
def _check_config(x, length):
if not isinstance(x, (list, tuple)) or len(x) != length:
raise InvalidConfiguration("length mismatch")
for b in x:
if not isinstance(b, bool):
raise InvalidConfiguration(f"non-Boolean entry {b!r}")
def source_eval(n, edges, x):
"""MinimumDominatingSet<SimpleGraph, One>.evaluate: size or None."""
_check_config(x, n)
dominated = list(x)
for u, v in edges:
if x[u]:
dominated[v] = True
if x[v]:
dominated[u] = True
if all(dominated):
return sum(1 for b in x if b) # unit weights
return INFEASIBLE
# ----------------------------------------------------------------- target ---
def validate_target(universe_size, sets):
for i, row in enumerate(sets):
for e in row:
if not 0 <= e < universe_size:
raise InvalidInput(f"row {i} element {e} outside universe")
def target_eval(target, y):
universe_size, sets = target
_check_config(y, universe_size)
for row in sets:
hit = False
for e in row:
if y[e]:
hit = True
break
if not hit:
return INFEASIBLE
return y.count(True)
# --------------------------------------------------------- construction ---
def reduce(n, edges):
"""Proof, Construction steps 1-3: U = V, one row N[v] per vertex in order."""
validate_simple_graph(n, edges)
rows = [{v} for v in range(n)]
for u, v in edges:
rows[u].add(v)
rows[v].add(u)
sets = [sorted(r) for r in rows]
validate_target(n, sets)
return (n, sets)
def extract(target, y):
"""Proof, Solution extraction: validate once, then copy unchanged."""
value = target_eval(target, y) # raises on malformed input
if value is INFEASIBLE:
raise InvalidConfiguration("target witness does not hit every row")
return list(y)
# ------------------------------------------------------------- utilities ---
def all_edges(n):
return list(combinations(range(n), 2))
def all_graphs(n):
pairs = all_edges(n)
for mask in range(1 << len(pairs)):
yield [pairs[i] for i in range(len(pairs)) if mask >> i & 1]
def all_configs(n):
for bits in product((False, True), repeat=n):
yield list(bits)
def brute_min(evaluate, n):
best = None
for x in all_configs(n):
val = evaluate(x)
if val is not None and (best is None or val < best):
best = val
return best
def canonical(target):
"""Canonical form for comparison: sorted rows, row order kept."""
universe_size, sets = target
return (universe_size, tuple(tuple(sorted(set(r))) for r in sets))
def canonical_up_to_row_permutation(target):
"""The only isomorphism the proof allows: permuting rows (multiset)."""
universe_size, sets = target
return (universe_size, tuple(sorted(tuple(sorted(set(r))) for r in sets)))Proof (Typst)#set page(paper: "a4", margin: 22mm)
#set text(size: 10pt)
#set heading(numbering: "1.")
= MinimumDominatingSet/SimpleGraph/One → MinimumHittingSet
*Theorem.* Let $G = (V, E)$ be any finite undirected simple graph admitted by
`MinimumDominatingSet<SimpleGraph, One>`, with $V = {0, dots, n - 1}$
(empty when $n = 0$), $n = |V|$, and $m = |E|$. There is a polynomial-time
construction of a `MinimumHittingSet` instance with the same feasible binary
configurations and the same objective on each configuration. Identity extraction
preserves all feasible solutions and all optima. For every integer bound $k$,
a dominating set of size at most $k$ exists if and only if the constructed
instance has a hitting set of size at most $k$.
== Provenance and pre-construction gates
The construction is the canonical closed-neighborhood incidence formulation,
confirmed before derivation against Max Bannach and Till Tantau,
_Computing Hitting Set Kernels By AC⁰-Circuits_, STACS 2018, Introduction,
*p. 9:1*, #link("https://doi.org/10.4230/LIPIcs.STACS.2018.9")[DOI].
That paragraph explicitly identifies dominating sets with hitting sets of the
closed-neighborhood hypergraph. The page is 9:1, rather than 9:2.
Garey and Johnson, _Computers and Intractability_ (1979), Appendix A,
GT2 p. 190 and SP8 p. 222, are references for the endpoint definitions;
they are not credited with presenting this direct construction. The scanned
book was not independently re-inspected here. Grobler and Siebertz,
_The PACE 2025 … Challenge: Dominating Set and Hitting Set_, Section 2,
#link("https://doi.org/10.4230/LIPIcs.IPEC.2025.32")[DOI], corroborates the
closed-neighborhood Set Cover formulation and its incidence dual Hitting Set;
undirected symmetry gives the same matrix in this case. The explicit proof,
numeric audit, and special-case analysis below are derived here.
Library sibling checks: `src/rules/minimumvertexcover_minimumhittingset.rs`
uses the vertex universe, preserves binary coordinates, validates the target
witness once, and copies it for extraction. Its family has one row per edge;
this construction instead has one row per vertex.
`src/rules/minimumdominatingset_ilp.rs` uses one domination constraint per
vertex. Neither sibling supplies an extra graph precondition for this rule.
The older vertex-cover sibling uses the panicking target constructor; that is
not a reason to bypass fallible construction in a later implementation.
*Type resolution: PASS.* In
`src/models/graph/minimum_dominating_set.rs:178–185`, the generic `Problem`
implementation (`Solution` and `Value` at lines 184–185) declares `Solution = Vec<bool>` and `Value = Min<W::Sum>`.
In `src/types.rs:297–309`, `WeightElement for One` declares `Sum = i64`
and converts each weight to $1$. Substituting `W = One` gives `Min<i64>`.
In `src/models/set/minimum_hitting_set.rs:142–145`, the concrete `Problem`
implementation declares `Solution = Vec<bool>` and `Value = Min<i64>`.
The wrapper `Min<V>` in `src/types.rs:409` contains `Option<V>`.
Both values are therefore exactly `Min<i64>`, with no unresolved associated
type. The verification guide's historical `Min<usize>` target example does
not describe these endpoint files.
Under `docs/src/design.md`, “Result mappings”, the optimization workflow
extracts a target optimum and evaluates the source. An aggregate objective map
is also available here: identity on the whole `Min<i64>` domain, including
`None` and every signed integer. It is total and order-preserving, requires no
range conversion, and cannot clamp or panic. On reachable feasible evaluations
the value is the nonnegative selected cardinality. If a mathematical
cardinality exceeds `i64::MAX`, the source's checked sum and the target's
checked cardinality conversion both report `IntegerOverflow`; this is an
evaluation error, not an infeasible solution and not a value to clamp.
*Redundancy: PASS (novel).* The locally built `pred` at checkout `e7bacb37`
was run with
`pred path MinimumDominatingSet/SimpleGraph/One MinimumHittingSet --limit all --json`.
It resolved the endpoints and reported no reduction path. Thus there is no
existing path whose overall transform could dominate the proposed exact
`universe_size = num_vertices`, `num_sets = num_vertices` transform.
The model descriptions and command output are retained with the gate evidence.
== Admitted inputs and encoding
`SimpleGraph::try_new` and deserialization in `src/topology/graph.rs` reject
self-loops, repeated undirected edges (including reversed duplicates), and
out-of-range endpoints. They admit empty graphs, isolated vertices, disconnected
graphs, and arbitrary degrees within a finite simple graph.
The source requires exactly $n$ unit weights. Each solution is a length-$n$
Boolean vector $x$; define its selected set as
$S(x) = {v in V : x_v = "true"}$.
Source `evaluate` rejects a wrong length, returns `Min(None)` when $S(x)$
fails to dominate, and otherwise returns `Min(Some(|S(x)|))` subject to the
checked numeric contract above.
The target has a universe of indexed elements, a *list* of subsets, and one
Boolean coordinate per universe element. Its constructor sorts and deduplicates
elements *within* each subset, validates their range, and retains duplicate
rows. An empty universe and empty family are admitted; an empty subset in a
nonempty family is admitted but makes a general target infeasible. Target
`evaluate` rejects a wrong length, returns `Min(None)` if any row is unhit,
and otherwise the selected cardinality as `Min<i64>`. No empty row is produced
by this construction. Unit weights are part of the source variant throughout.
== Construction
For each vertex $v in V$, define the open neighborhood
$N(v) = {u in V : {u,v} in E}$ and the closed neighborhood
$N[v] = {v} union N(v)$.
+ Set the target universe to $U = V$, retaining the integer label of every vertex.
+ For every $v = 0, dots, n - 1$, append the subset $F_v = N[v]$ to the family
$cal(F) = (F_0, dots, F_(n-1))$. Store each row in increasing element order.
Preserve one row per vertex even when several rows are equal.
+ Construct `MinimumHittingSet` with `universe_size = n` and `sets =` this
family, validating the target through its fallible constructor. No weights,
auxiliary elements, empty rows, or bound are introduced.
For comparison of independently constructed targets, the canonical representation
uses rows ordered by $v$ and sorted elements. If an implementation enumerates
the same rows in another order, row permutation is the only allowed
isomorphism; multiplicity and vertex labels must remain unchanged.
== Overhead and validity
#table(
columns: (1.6fr, 1fr, 2.6fr), inset: 6pt,
[*Target metric*], [*Exact formula*], [*Derivation*],
[`universe_size`], [`num_vertices = n`], [One element for every vertex, with no auxiliaries.],
[`num_sets`], [`num_vertices = n`], [Exactly one appended row per vertex, retaining equal rows.],
[Total row incidences (auxiliary size audit)], [$n + 2m$],
[One diagonal entry per vertex; each simple undirected edge contributes once in each endpoint row.],
)
Every row consists only of elements in $U$ and contains its own vertex.
Because the graph is simple, the diagonal and its distinct neighbors contribute
$1 + |N(v)|$ distinct entries. Summing degrees gives $2m$. There are no skipped
rows, coefficient normalizations, or graph-dependent branches. Within-row
deduplication changes none of these counts, including when $n = 0$.
Thus both registered target parameter equalities hold on the full admitted
domain, not just on sampled instances.
Building adjacency rows needs $O(n + m)$ insertions and output memory.
Sorting gives an $O((n + m) log(max(2,n)))$ time upper bound.
Construction uses the existing index range; any derived allocation size must be
computed with checked arithmetic. The incidence formula is a mathematical size
audit, not permission for an unchecked `n + 2*m` machine computation.
Extraction validates with the target evaluator, which binary-searches each
selected list, so validation costs $O((n + m) log(max(2,n)))$; copying the vector costs $O(n)$.
== Correctness
*(⇒) Source to target.* Suppose $S subset.eq V$ dominates $G$. Fix a target
row $F_v$. Domination of $v$ supplies either $v in S$ or a selected vertex
$u in S$ joined to $v$ by an edge. In the first case $v in F_v$; in the
second case undirected adjacency gives $u in N(v) subset.eq F_v$.
In either case $S inter F_v != emptyset$. Since this holds for every row,
the same vector is a hitting set. Neither the selected elements nor their
count have changed.
*(⇐) Target to source.* Suppose $H subset.eq U$ hits the entire family.
For each source vertex $v$, hitting the specific row $F_v$ supplies some
$h in H inter F_v$. Membership in $F_v$ means either $h = v$ or
$h$ is adjacent to $v$. In the former case $v$ is selected; in the latter
case the selected vertex $h$ dominates $v$. This argument covers each source
vertex and therefore makes the copied selection a dominating set, with size
$|H|$. It uses the row belonging to the vertex being dominated, rather than
assuming that a selected row covers the universe.
The forward direction maps each source feasible cardinality to a target
feasible cardinality of the same value. The backward direction maps each target
feasible cardinality to a source feasible cardinality of the same value.
Taking minima gives equality of optima; applying any common bound $k$ gives
the bounded equivalence. The entire configuration space is shared, so invalid
selections are infeasible on both sides as well.
== Solution extraction
Given a proposed target vector $y$, first validate its length and feasibility
with the target evaluator, exactly once. A wrong length, malformed non-Boolean
encoding, evaluation error, or unhit row is rejected; it is never silently
truncated or filled. For a valid target witness output $x = y$ unchanged.
The backward argument proves source feasibility, and unit weights give
$sum_(v in S(x)) 1 = |S(x)| = |S(y)|$. Thus every feasible target witness
extracts, including suboptimal witnesses, and every optimal witness extracts
to a source optimum. The optional aggregate map is the total identity described
in the type gate.
== YES example
Take the path with $n = 5$, $m = 4$, and edges
$(0,1), (1,2), (2,3), (3,4)$. The universe is $U = {0,1,2,3,4}$ and the
five rows in order are
$( {0,1}, {0,1,2}, {1,2,3}, {2,3,4}, {3,4} )$.
Their lengths are $2,3,3,3,2$, totaling $13 = 5 + 2 dot 4$.
For bound $k = 2$, choose $H = {1,3}$, vector
`[false,true,false,true,false]`. Its row intersections are
${1}, {1}, {1,3}, {3}, {3}$. It hits all rows and extracts to the same
dominating selection: vertex $1$ dominates ${0,1,2}$ and vertex $3$
dominates ${2,3,4}$. Both values are `Min(Some(2))`.
The selections ${0,2,4}$ and ${0,1,3}$ also hit and dominate, each with
value $3$, demonstrating valid suboptimal extraction.
== NO example (bounded)
Use the same five-vertex path and target, but bound $k = 1$.
The empty selection misses every row. The five singleton possibilities are:
#table(
columns: 3, inset: 5pt,
[*Selected vertex*], [*Vertices it dominates*], [*A missed target row*],
[$0$], [${0,1}$], [$F_2 = {1,2,3}$],
[$1$], [${0,1,2}$], [$F_3 = {2,3,4}$],
[$2$], [${1,2,3}$], [$F_0 = {0,1}$],
[$3$], [${2,3,4}$], [$F_0 = {0,1}$],
[$4$], [${3,4}$], [$F_0 = {0,1}$],
)
These exhaust all selections of size at most $1$. None dominates and none
hits every row, so both bounded questions are NO. Together with the size-$2$
YES witness, this proves both optimization optima equal $2$.
This is not a claim that the unbounded optimization instances are infeasible:
every graph in the source domain has the dominating selection $V$, and the
constructed target has hitting set $U$. A genuinely infeasible unbounded
source instance cannot be supplied without changing the model.
== Special cases
- *Empty graph:* $n=m=0$ gives universe size $0$ and no rows. The empty vector
is the unique configuration, feasible on both sides, with optimum $0$.
- *Isolated vertices and edgeless graphs:* an isolated vertex $v$ produces the
singleton row ${v}$, forcing its selection. An edgeless graph on $n$
vertices therefore has optimum $n$, including the single-vertex optimum $1$.
- *Disconnected graphs:* rows contain no elements from another component;
each component must be dominated and hit separately. Two three-vertex paths
plus an isolated vertex have optimum $1+1+1=3$ and seven rows.
- *Paths, cycles, stars, complete graphs:* these require no special construction
branch. For paths and cycles on $n >= 3$ vertices the optimum is
$ceil(n/3)$; stars and complete graphs have optimum $1$. In a complete graph
all $n$ rows equal $V$; retaining those duplicates is essential for exact
`num_sets = n`. These size formulas for optima are tested independently as
special-family sanity checks, not used to define either evaluator.
- *Loops and parallel edges:* these are excluded by the source's constructor
and deserializer. Mathematically, adding them would not change set-valued
closed neighborhoods after deduplication, but the simple-graph incidence
formula $n+2m$ would no longer apply to multiplicity-counted $m$. No claim
that the registered source receives such inputs is made.
- *Unhit rows and malformed witnesses:* even though the image has a solution,
many candidate vectors do not hit all rows and must be rejected. For $n>0$
the all-false vector is one such candidate. A wrong-length vector is an error,
not evidence of infeasibility. The empty family case still requires length $0$.
== Claim-to-check map and limits
`constructor.py` has seven nonempty audited sections. Every counted assertion
reads the constructed target or values/extractions computed from it; symbolic
expressions are fitted to measured target counts before comparison to the
derived formulas.
#table(
columns: (2fr, 3fr), inset: 5pt,
[*Claim*], [*Constructor section / evidence*],
[Exact overhead equalities and incidences],
[1: SymPy sums of per-vertex and per-edge contributions, compared with
symbolic linear identities from all targets through four vertices;
4: measured counts on every exhaustive and generated target. The derivation
above supplies the full-domain proof that finite checks cannot supply.],
[Feasibility both ways and equal optimum],
[2: every labeled simple graph through six vertices and every binary vector;
independent edge-spreading source oracle and row-intersection target oracle.],
[Every feasible and every optimal target witness extracts with equal value],
[3: every feasible exhaustive witness; all optimal witnesses also checked
against the independently computed source optimum; rejection of infeasible
and wrong-length vectors.],
[Target normalization, diagonal, complete incidence, duplicate-row retention],
[5 and 4: every target checked against the edge relation and actual counts.],
[Empty, isolated, disconnected, path, cycle, star, complete cases],
[5: named families and independently specified optima, plus exhaustive cases.],
[Numerical YES and bounded NO examples], [6 and 7: full target, values,
enumeration of both bounded spaces, and feasible suboptimal selections.],
[Larger and patterned configurations],
[2–5: Hypothesis arbitrary graphs with random vectors, and a separate family
strategy; 300 examples each; all-false, all-true, and alternating vectors;
seeds 20261103 and 20261104, no database or deadline.],
[Concrete Rust values, input admission, total value-map domain],
[Endpoint/type source inspection and real CLI semantic smoke evidence.
Finite Python integers cannot prove machine arithmetic or huge allocations.],
)
This establishes the construction and its constructor checks. Independent
adversarial reconstruction, cross-comparison, and an implementation certificate
remain separate work; no claim of their completion is made here.
|
Collaborator
Author
Agentic Review ReportSubject: rule Structural
Hand trace of
Issue compliance:
QualityThe validation plan in the issue is covered at its stated sizes:
A wrong-length witness on the empty instance is rejected (added in the fix round). Coverage of the rule module is 98.33% of regions (60 regions, 1 missed; lines 100%). The missed region is the Feature testRun from a scratch directory with the built CLI:
FindingsCritical: none. Important: none. Minor: none open. Resolved in the fix round:
The re-review diff contains only these three changes. Afterwards, formatting, clippy (warnings denied), the 7 rule tests, |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1233 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151778 +220
========================================
+ Hits 147308 147532 +224
+ Misses 4250 4246 -4 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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.
Summary
Adds the reduction
MinimumDominatingSet<SimpleGraph, One>→MinimumHittingSet.v, holding its closed neighborhoodN[v], over the vertex universe. A set of vertices dominatesGexactly when it hits everyN[v], so the identity map extracts solutions.universe_size = num_vertices,num_sets = num_vertices(exact).MinimumHittingSet::try_newbecomespub(crate)so the rule can use the validating constructor; behaviour is unchanged.Note: the issue mentions loops and parallel edges; current
mainrejects both inSimpleGraph, and the tests and paper say so.Fixes #1096
🤖 Generated with Claude Code