Repository navigation
Conversation
…anningTree Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED. Rule Constructor script (independent finite check, Python + sympy + hypothesis; seeds 2026110403 / 2026110404, Hypothesis 300 examples per strategy): 32,452,955 checks, 0 failures
Instance ranges: all 1,100 labelled simple graphs with n ≤ 5 (n = 0…5, including empty, edgeless and disconnected graphs), with 8,087,708 spanning trees enumerated (2,995,360 at n = 5) and a determinant (matrix-tree) audit of the enumeration; 600 Hypothesis-generated arbitrary graphs; bounds k from −3 to n+2 plus signed i64 extremes (±2⁶³, −2⁶²) and usize/i64 overflow boundaries. Adversary script (written from the proof only; seeds as above): 14,108,426 checks, 0 failures over the same n ≤ 5 range (1,100 graphs, 2,995,360 trees) including an independent connected-dominating-set oracle (max leaves = N − γ_c), and a mutation run (35 deliberately broken variants of the construction, extraction and oracles) is caught by the adversary in every case; the constructor script alone misses 6 of them (size-formula and extraction-detail mutants), which the adversary and the Rust tests cover. Cross-comparison against Topology / redundancy: no existing path from the source to the target, so the rule is novel (PASS). The scripts and the Typst proof follow (the adversary scripts are in the next comment). Constructor script (Python)#!/usr/bin/env python3
"""Independent finite verification; run with Python plus sympy and hypothesis.
Sections 1–7 correspond to the proof's computational coverage paragraph.
Only --examples skips exhaustive verification (for the initial failing test).
No Rust implementation, external solver, mocks, or source-text tests are used.
"""
from collections import Counter
from dataclasses import dataclass
from itertools import combinations, product
import sys
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
SEED = 2026110403
I64_MIN, I64_MAX = -(1 << 63), (1 << 63) - 1
U64_MAX = (1 << 64) - 1
LABELS = {
1: "symbolic overhead and threshold",
2: "exhaustive equivalence, optimum, forward witnesses",
3: "every target witness and extraction",
4: "measured sizes and arithmetic boundaries",
5: "structure, generic enumeration, invalid witnesses",
6: "worked YES example",
7: "worked NO example",
}
CHECKS, FAILURES, STATS = Counter(), Counter(), Counter()
def check(section, condition, context):
CHECKS[section] += 1
if not condition:
FAILURES[section] += 1
raise AssertionError(f"section {section}: {context}")
@dataclass(frozen=True)
class Target:
n: int
edges: tuple
bound: int
def construct(n, edges, k):
edges = tuple(edges)
if n < 0 or not I64_MIN <= k <= I64_MAX:
raise ValueError("invalid source size or signed bound")
if any(not (0 <= u < n and 0 <= v < n) or u == v for u, v in edges):
raise ValueError("invalid simple graph edge")
if len({tuple(sorted(edge)) for edge in edges}) != len(edges):
raise ValueError("duplicate undirected edge")
vertices, _, bound = checked_shape(n, len(edges), min(n, max(-1, k)))
root = n + len(edges)
target_edges = [(root, v) for v in range(n)]
for j, (u, v) in enumerate(edges):
target_edges.extend(((u, n + j), (v, n + j)))
target_edges.extend(((root, root + 1), (root, root + 2)))
return Target(vertices, tuple(target_edges), bound)
def checked_sizes(n, m):
"""Model checked u64/64-bit usize arithmetic before signed conversion."""
def unsigned(value):
if not 0 <= value <= U64_MAX:
raise OverflowError("size outside u64/64-bit usize")
return value
unsigned(n)
unsigned(m)
vertices = unsigned(unsigned(n + m) + 3)
edge_count = unsigned(unsigned(n + unsigned(2 * m)) + 2)
return vertices, edge_count
def checked_shape(n, m, normalized_bound):
def signed(value):
if not I64_MIN <= value <= I64_MAX:
raise OverflowError("bound outside i64")
return value
vertices, edge_count = checked_sizes(n, m)
bound = signed(signed(vertices - 1) - signed(normalized_bound))
return vertices, edge_count, bound
def source_covers(n, edges):
"""Independent definition: every edge has a selected endpoint."""
return [bits for bits in product((False, True), repeat=n)
if all(bits[u] or bits[v] for u, v in edges)]
def tree_degrees(target, bits):
"""Model semantics: length, n-1 edges, BFS connectivity, degree-one leaves."""
if len(bits) != len(target.edges) or any(type(x) is not bool for x in bits):
raise ValueError("invalid edge selection encoding")
if sum(bits) != target.n - 1:
return None
adj = [[] for _ in range(target.n)]
for selected, (u, v) in zip(bits, target.edges):
if selected:
adj[u].append(v)
adj[v].append(u)
seen = {0}
pending = [0]
for v in pending:
for u in adj[v]:
if u not in seen:
seen.add(u)
pending.append(u)
if len(seen) != target.n:
return None
return tuple(map(len, adj))
def target_accepts(target, bits):
degree = tree_degrees(target, bits)
return degree is not None and degree.count(1) >= target.bound
def extract(n, target, bits):
degree = tree_degrees(target, bits)
if degree is None or degree.count(1) < target.bound:
raise ValueError("target witness does not satisfy decision instance")
return tuple(d >= 2 for d in degree[:n])
def forward(n, edges, target, cover):
bits = [True] * n
for u, v in edges:
if not (cover[u] or cover[v]):
raise ValueError("not a source cover")
bits.extend((cover[u], not cover[u]))
bits.extend((True, True))
if len(bits) != len(target.edges):
raise ValueError("target layout differs")
return tuple(bits)
def structured_trees(n, target):
"""Complete forest/component-root/attachment bijection proved in proof.typ.
Read the incidence endpoints from the constructed target, not the source.
Edge indices are preserved; orientations of undirected edges are immaterial.
"""
m = (len(target.edges) - n - 2) // 2
pairs = [target.edges[n + 2 * j:n + 2 * j + 2] for j in range(m)]
endpoints = [tuple(next(v for v in edge if v < n) for edge in pair)
for pair in pairs]
for both in range(1 << m):
parent = list(range(n))
def find(v):
while parent[v] != v:
v = parent[v]
return v
selected = [False] * len(target.edges)
valid = True
for j, (u, v) in enumerate(endpoints):
if both >> j & 1:
a, b = find(u), find(v)
if a == b:
valid = False
break
parent[a] = b
selected[n + 2 * j:n + 2 * j + 2] = (True, True)
if not valid:
continue
components = {}
for v in range(n):
components.setdefault(find(v), []).append(v)
singles = [j for j in range(m) if not both >> j & 1]
selected[-2:] = (True, True)
for roots in product(*components.values()):
selected[:n] = [False] * n
for v in roots:
selected[v] = True
for attachments in product((0, 1), repeat=len(singles)):
for j, side in zip(singles, attachments):
selected[n + 2 * j:n + 2 * j + 2] = (side == 0, side == 1)
yield tuple(selected)
def generic_trees(target):
"""Independent oracle: choose n-1 edges, then BFS; no gadget assumptions."""
for chosen in combinations(range(len(target.edges)), target.n - 1):
bits = [False] * len(target.edges)
for i in chosen:
bits[i] = True
bits = tuple(bits)
if tree_degrees(target, bits) is not None:
yield bits
def tree_count_by_determinant(target):
"""Matrix-tree theorem, evaluated from the target adjacency only."""
laplacian = sp.zeros(target.n)
for u, v in target.edges:
laplacian[u, u] += 1
laplacian[v, v] += 1
laplacian[u, v] -= 1
laplacian[v, u] -= 1
return laplacian[:-1, :-1].det(method="domain-ge")
def check_structure(n, edges, target):
m, root = len(edges), n + len(edges)
adj = [set() for _ in range(target.n)]
canonical = set()
for u, v in target.edges:
check(5, 0 <= u < target.n and 0 <= v < target.n and u != v,
(n, edges, "simple edge", u, v))
canonical.add(tuple(sorted((u, v))))
adj[u].add(v)
adj[v].add(u)
check(5, len(canonical) == len(target.edges), "duplicate target edges")
left = {root, *range(n, n + m)}
check(5, all((u in left) != (v in left) for u, v in target.edges), "bipartition")
check(5, adj[root] == set(range(n)) | {root + 1, root + 2}, "root neighbors")
check(5, adj[root + 1] == adj[root + 2] == {root}, "private leaves")
check(5, all(adj[n + j] == set(edge) for j, edge in enumerate(edges)),
"subdivision neighbors")
reachable, queue = {root}, [root]
for v in queue:
for u in adj[v] - reachable:
reachable.add(u)
queue.append(u)
check(5, len(reachable) == target.n, "target disconnected")
isolated = set(range(n)) - {v for edge in edges for v in edge}
check(5, all(adj[v] == {root} for v in isolated), "isolated original")
def audit_graph(n, edges, exhaustive=False):
edges = tuple(edges)
target = construct(n, edges, n)
check(4, (target.n, len(target.edges)) == (n + len(edges) + 3, n + 2 * len(edges) + 2),
(n, edges, "size formula"))
check_structure(n, edges, target)
covers = source_covers(n, edges)
minimum = min(map(sum, covers))
# Covers come from exhaustive source subsets, independent of any target tree.
for cover in covers:
bound_target = construct(n, edges, sum(cover))
bits = forward(n, edges, bound_target, cover)
check(2, target_accepts(bound_target, bits), (n, edges, cover, "forward"))
check(2, sum(extract(n, bound_target, bits)) <= sum(cover), "forward extraction")
maximum, tree_count, accepted = -1, 0, 0
for bits in structured_trees(n, target):
degree = tree_degrees(target, bits)
check(3, degree is not None, (n, edges, bits, "enumerated nontree"))
leaves = degree.count(1)
maximum = max(maximum, leaves)
tree_count += 1
internal_originals = tuple(d >= 2 for d in degree[:n])
check(3, all(internal_originals[u] or internal_originals[v] for u, v in edges)
and sum(internal_originals) <= target.n - leaves - 1,
(n, edges, "backward inequality for arbitrary tree"))
if leaves >= target.bound:
cover = extract(n, target, bits)
# k_min is the tightest source threshold at which this tree is feasible.
k_min = target.n - 1 - leaves
check(3, all(cover[u] or cover[v] for u, v in edges) and sum(cover) <= k_min,
(n, edges, bits, "extraction at tightest accepting bound", k_min))
accepted += 1
else:
try:
extract(n, target, bits)
except ValueError:
check(3, not target_accepts(target, bits), "below-bound rejection")
else:
check(3, False, "accepted a below-bound tree")
check(3, degree[n + len(edges)] >= 2 and degree[-2:] == (1, 1), "forced root")
check(2, maximum == target.n - 1 - minimum, (n, edges, "optimum", maximum, minimum))
check(5, tree_count == tree_count_by_determinant(target), (n, edges, "matrix-tree count"))
STATS["determinant_audits"] += 1
for k in [I64_MIN, -2, *range(-1, n + 2), I64_MAX]:
bounded = construct(n, edges, k)
check(2, bounded.n == target.n and bounded.edges == target.edges
and (minimum <= k) == (maximum >= bounded.bound), (n, edges, k, "equivalence"))
if n <= 3:
generic, structured = set(generic_trees(target)), set(structured_trees(n, target))
check(5, generic == structured and len(structured) == tree_count,
(n, edges, "complete duplicate-free tree enumeration"))
STATS["generic_trees"] += len(generic)
STATS["exhaustive_graphs" if exhaustive else "hypothesis_graphs"] += 1
STATS["trees"] += tree_count
STATS["feasible_extractions"] += accepted
def symbolic():
n, m, k = sp.symbols("n m k", integer=True)
target = construct(4, ((0, 1), (1, 2), (2, 3), (3, 0)), 2)
values = {n: 4, m: 4, k: 2}
for blocks, formula, observed in [
(n + m + 1 + 2, n + m + 3, target.n),
(n + 2 * m + 2, n + 2 * m + 2, len(target.edges)),
((n + m + 1 + 2) - 1 - k, n + m + 2 - k, target.bound),
]:
check(1, sp.expand(blocks - formula) == 0 and formula.subs(values) == observed,
(blocks, formula, observed))
def arithmetic():
# Each expected result follows from mathematical integers, independently
# of checked_shape's intermediate checks; no huge graph is allocated.
size_cases = [
(U64_MAX - 3, 0, (U64_MAX, U64_MAX - 1)),
(U64_MAX - 2, 0, None),
(U64_MAX, 1, None),
(0, U64_MAX // 2 - 1, (U64_MAX // 2 + 2, U64_MAX - 1)),
(0, U64_MAX // 2, None),
(0, U64_MAX // 2 + 1, None),
(3, U64_MAX // 2 - 2, (U64_MAX // 2 + 4, U64_MAX)),
(4, U64_MAX // 2 - 2, None),
(5, U64_MAX // 2 - 2, None),
]
for n, m, expected in size_cases:
try:
actual = checked_sizes(n, m)
except OverflowError:
actual = None
check(4, actual == expected, (n, m, actual, expected, "size boundary"))
cases = [
(0, 0, -1, (3, 2, 3)),
(0, 0, 0, (3, 2, 2)),
(I64_MAX - 2, 0, 0, (I64_MAX + 1, I64_MAX, I64_MAX)),
(I64_MAX - 2, 0, -1, None),
(I64_MAX - 1, 0, 0, None),
(0, 0, I64_MIN + 3, (3, 2, I64_MAX)),
(0, 0, I64_MIN + 2, None),
(U64_MAX - 3, 0, 0, None),
(U64_MAX - 2, 0, 0, None),
(U64_MAX, 1, 0, None),
(0, U64_MAX // 2, 0, None),
(0, U64_MAX // 2 + 1, 0, None),
]
for n, m, k_prime, expected in cases:
try:
actual = checked_shape(n, m, k_prime)
except OverflowError:
actual = None
check(4, actual == expected, (n, m, k_prime, actual, expected))
target = construct(4, ((0, 1),), I64_MAX)
# An unnormalized arithmetic helper must preserve a negative signed result.
for raw in (target.n - 2, target.n - 1, target.n):
shape = checked_shape(4, 1, raw)
check(4, shape == (target.n, len(target.edges), target.n - 1 - raw), "no clamp")
for k in (I64_MIN, -1, 0, 4, 5, I64_MAX):
bounded = construct(4, ((0, 1),), k)
check(4, bounded.bound == target.n - 1 - min(4, max(-1, k)), "signed normalization")
def malformed():
edges = ((0, 1), (1, 2), (2, 3), (3, 0))
target = construct(4, edges, 2)
invalid = [(), (False,) * 13, (False,) * 15, (False,) * 14, (True,) * 14]
# Right edge count, but one private leaf is disconnected and a cycle is selected.
invalid.append(tuple(i in {0, 1, 2, 3, 4, 5, 6, 7, 8, 12} for i in range(14)))
for bits in invalid:
try:
extract(4, target, bits)
except ValueError:
check(5, len(bits) != len(target.edges) or not target_accepts(target, bits), "invalid rejection")
else:
check(5, False, "malformed witness accepted")
for endpoints, leaf_count in [((0, 1, 2, 0), 7), ((0, 1, 2, 3), 6)]:
bits = [True] * 4
for (u, v), parent in zip(edges, endpoints):
bits.extend((parent == u, parent == v))
bits = tuple(bits) + (True, True)
degree = tree_degrees(target, bits)
check(5, degree is not None and degree.count(1) == leaf_count,
"suboptimal tree must remain a valid underlying tree")
try:
extract(4, target, bits)
except ValueError:
check(5, not target_accepts(target, bits), "suboptimal decision rejection")
else:
check(5, False, "below-bound tree accepted")
def examples():
edges = ((0, 1), (1, 2), (2, 3), (3, 0))
yes = construct(4, edges, 2)
expected_edges = ((8, 0), (8, 1), (8, 2), (8, 3), (0, 4), (1, 4), (1, 5),
(2, 5), (2, 6), (3, 6), (3, 7), (0, 7), (8, 9), (8, 10))
witness = (True, True, True, True, True, False, False, True,
True, False, False, True, True, True)
check(6, (yes.n, len(yes.edges), yes.bound, yes.edges) == (11, 14, 8, expected_edges), "YES target")
check(6, tree_degrees(yes, witness) == (3, 1, 3, 1, 1, 1, 1, 1, 6, 1, 1), "YES degrees")
check(6, target_accepts(yes, witness) and sum(witness) == 10, "YES witness")
check(6, extract(4, yes, witness) == (True, False, True, False), "YES extraction")
check(6, forward(4, edges, yes, (True, False, True, False)) == witness, "YES forward")
covers = source_covers(4, edges)
maximum = max(tree_degrees(yes, bits).count(1) for bits in generic_trees(yes))
check(6, min(map(sum, covers)) == 2 and maximum == 8, "YES optima")
no = construct(4, edges, 1)
check(7, (no.n, len(no.edges), no.bound, no.edges) == (11, 14, 9, expected_edges), "NO target")
check(7, not any(sum(cover) <= 1 for cover in covers) and maximum < no.bound,
"NO infeasible on both sides")
check(7, not any(target_accepts(no, bits) for bits in generic_trees(no)), "NO all target trees")
try:
extract(4, no, witness)
except ValueError:
check(7, not target_accepts(no, witness), "NO rejects YES witness")
else:
check(7, False, "NO extracted an infeasible witness")
print("Examples: minimum cover 2, maximum leaves 8; YES b=8; NO b=9", flush=True)
@st.composite
def arbitrary_graphs(draw):
n = draw(st.integers(0, 5))
possible = list(combinations(range(n), 2))
edges = draw(st.lists(st.sampled_from(possible), unique=True, max_size=len(possible))) if possible else []
flips = draw(st.lists(st.booleans(), min_size=len(edges), max_size=len(edges)))
edges = tuple((v, u) if flip else (u, v) for (u, v), flip in zip(edges, flips))
k = draw(st.one_of(st.integers(-2, n + 2), st.sampled_from((I64_MIN, I64_MAX))))
return n, edges, k
@st.composite
def disconnected_graphs(draw):
n = draw(st.integers(2, 5))
cut = draw(st.integers(1, n - 1))
# Vertex n-1 stays isolated; both sides of cut may contain other components.
possible = [(u, v) for u, v in combinations(range(n - 1), 2) if (u < cut) == (v < cut)]
edges = draw(st.lists(st.sampled_from(possible), unique=True, max_size=len(possible))) if possible else []
k = draw(st.one_of(st.integers(-2, n + 2), st.sampled_from((I64_MIN, I64_MAX))))
return n, tuple(edges), k
def property_check(case):
n, edges, k = case
audit_graph(n, edges)
target = construct(n, edges, k)
minimum = min(map(sum, source_covers(n, edges)))
actual = any(target_accepts(target, bits) for bits in structured_trees(n, target))
check(2, actual == (minimum <= k), (case, "Hypothesis decision"))
@seed(SEED)
@settings(max_examples=300, deadline=None, database=None)
@given(arbitrary_graphs())
def random_arbitrary(case):
property_check(case)
@seed(SEED + 1)
@settings(max_examples=300, deadline=None, database=None)
@given(disconnected_graphs())
def random_disconnected(case):
property_check(case)
def main():
examples()
if "--examples" in sys.argv:
return
symbolic()
arithmetic()
malformed()
for n in range(6):
possible = list(combinations(range(n), 2))
for mask in range(1 << len(possible)):
edges = tuple(edge for i, edge in enumerate(possible) if mask >> i & 1)
audit_graph(n, edges, exhaustive=True)
print(f"Exhaustive n={n} finished; {STATS['trees']} trees audited", flush=True)
check(2, STATS["exhaustive_graphs"] == 1100 and STATS["generic_trees"] > 0,
"exhaustive enumeration coverage")
random_arbitrary()
print("Hypothesis arbitrary graphs complete", flush=True)
random_disconnected()
print(f"Statistics: {dict(STATS)}; seeds={SEED},{SEED + 1}; Hypothesis 300 per strategy", flush=True)
if __name__ == "__main__":
try:
main()
except Exception:
if not sum(FAILURES.values()):
FAILURES[0] += 1
raise
finally:
for section, label in LABELS.items():
print(f"SECTION {section}: {CHECKS[section]} checks, {FAILURES[section]} failures — {label}")
print(f"TOTAL: {sum(CHECKS.values())} checks, {sum(FAILURES.values())} failures")Proof (Typst)#set text(size: 10pt)
#set heading(numbering: "1.")
= Vertex cover to maximum-leaf decision spanning tree
*Theorem.* For every finite simple undirected graph $G=(V,E)$ and signed
integer $k$, the construction below produces a connected simple graph $H$
and integer $b$ such that $G$ has a vertex cover of size at most $k$ if and
only if $H$ has a spanning tree with at least $b$ degree-one vertices.
Extraction works for every feasible target witness, including nonoptimal trees.
== Endpoint semantics and type-resolution gate
Source: `DecisionMinimumVertexCover/SimpleGraph/One`, namely
`Decision<MinimumVertexCover<SimpleGraph, One>>`. In
`src/models/graph/minimum_vertex_cover.rs:162–163`, the solution is `Vec<bool>`
over vertices and the inner value is `Min<W::Sum>`.
`src/types.rs:297–308` resolves `One::Sum = i64`, with each selected vertex
contributing one. In `src/models/decision.rs:302–320`, the wrapper retains
the solution and yields `Or`, comparing the inner value to the bound.
`src/types.rs:475–492` resolves the bound to `i64` and the comparison to ≤.
Use the signed `bound()`; the weighted variant's convenience `k()` getter
clamps negative values and is inappropriate here.
Target: `DecisionMaximumLeafSpanningTree/SimpleGraph`, namely the planned
`Decision<MaximumLeafSpanningTree<SimpleGraph>>`. Its existing inner model
(`src/models/graph/maximum_leaf_spanning_tree.rs:169–199`) has edge-indexed
`Vec<bool>` solutions and value `Max<i64>`. The same wrapper yields `Or`
and an `i64` bound with comparison ≥. Thus the proposed rule is `Or → Or`,
with the identity aggregate map. The bare optimization endpoints would be
`Min<i64> → Max<i64>` and must not be substituted for this decision rule.
Malformed witness lengths give evaluation errors. A source noncover or target
nontree gives an infeasible inner value and hence `Or(false)`. A target tree
has exactly $N-1$ selected edges and is connected; leaves have degree exactly
one. The target constructor admits graphs with at least two vertices, including
disconnected graphs, though this construction always yields a connected graph
with at least three. The source admits $n=0$. `SimpleGraph::try_new`
(`src/topology/graph.rs:109–170`) rejects loops, repeated undirected edges,
and out-of-range endpoints; no multigraph extension is claimed.
*Baseline gate, 2026-11-04.* Built the unchanged checkout with
`cargo build -p problemreductions-cli --bin pred`. The exact-source command
`pred path DecisionMinimumVertexCover/SimpleGraph/One MaximumLeafSpanningTree/SimpleGraph --limit all`
reports no path. `pred show` reports no incoming edges to that optimization
target. The command with `DecisionMaximumLeafSpanningTree/SimpleGraph` reports
an unknown problem, as the decision registration is absent. Redundancy: *PASS*
(no existing path to dominate this edge). This is the baseline gate; the
decision endpoint must be registered and the gate rerun before rule delivery.
The complete output is in the topology check output.
== Provenance
Paul Bonsma, _Max-Leaves Spanning Tree is APX-hard for Cubic Graphs_, Journal
of Discrete Algorithms 12 (2012), 14–23,
#link("https://doi.org/10.1016/j.jda.2011.06.005")[doi:10.1016/j.jda.2011.06.005].
The primary #link("https://arxiv.org/pdf/0912.0226")[preprint, pp. 2–3,
last paragraph before Section 2] describes adding a universal vertex and
subdividing the original edges, for cubic vertex cover. The two private leaves,
the arbitrary-simple-graph proof, direct extraction without normalizing the
tree, empty inputs, and signed bounds are *derived here*. The library sibling
`src/rules/minimumvertexcover_maximumindependentset.rs` uses complementation,
retains exact graph sizes, and validates a target witness before extraction.
`src/rules/maximumleafspanningtree_ilp.rs` supplies the existing target's outgoing
ILP rule, not an incoming vertex-cover construction. No sibling supplies this
edge. These searches preceded this derivation.
== Construction
Let $n=|V|$, $m=|E|$, label $V=\{0, dots, n-1\}$, and enumerate the input
edges in their stored order as $e_j=(u_j,v_j)$ for $0 <= j < m$.
1. Retain the $n$ original vertices. For each $e_j$, introduce a distinct
subdivision vertex $a_j=n+j$.
2. Introduce the root $r=n+m$ and two private vertices $p=r+1$, $q=r+2$.
Set $N=n+m+3$.
3. Insert the following edges in this order: $(r,v)$ for $v=0, dots,n-1$;
then $(u_j,a_j),(v_j,a_j)$ for each $j$ in order; then $(r,p),(r,q)$.
Set $M=n+2m+2$. Vertex and edge labels are part of the encoding;
comparisons may ignore undirected endpoint orientation only.
4. Normalize the source bound to $k'=min(n,max(-1,k))$ and set
$b=N-1-k'$. This normalization preserves feasibility since a cover size
lies between zero and $n$. Negative bounds all yield $k'=-1$ and $b=N$.
5. Encode a target witness by an $M$-entry Boolean vector, selecting its tree
edges. A forward witness for a cover $C$ selects all root spokes, both
private edges, and exactly one incidence edge to an endpoint in $C$ for
each subdivision vertex (choose the first stored endpoint in $C$).
== Exact overhead
The vertex blocks are disjoint, with sizes $n,m,1,2$. The three edge blocks
have sizes $n,2m,2$. The two endpoints of every input edge are distinct;
incidences for different edges use different subdivision vertices. Therefore
there are no loops, duplicate edges, discarded edges, or conditional blocks.
These counts hold on every successful construction, including $n=m=0$.
#table(columns: 3, inset: 5pt,
[Target parameter], [Formula], [Contract],
[`num_vertices`], [$n+m+3$], [exact],
[`num_edges`], [$n+2m+2$], [exact],
)
Bounds are semantic data, not registered size parameters. The graph is
bipartite with parts $\{r\} union \{a_j:0 <= j<m\}$ and $V union \{p,q\}$.
Every original vertex is adjacent to $r$; every subdivision vertex has two
original neighbors; $p,q$ have only neighbor $r$. Thus $H$ is connected.
== Correctness
*Forward (⇒).* Let $C$ be any source cover with $|C| <= k$. Necessarily
$k >= 0$, and $|C| <= k'$ because $|C| <= n$. Step 5's selected subgraph
connects all original vertices to the root, each subdivision vertex to a
chosen covered endpoint, and the two private vertices to the root. It has
$n+m+2=N-1$ edges and is connected, so it is a tree. Its only possible
internal vertices are the root and vertices in $C$. It therefore has at least
$N-1-|C| >= N-1-k'=b$ leaves. Unused selected cover vertices may remain leaves;
the argument requires an inequality, not equality for arbitrary covers.
*Backward (⇐).* Let $T$ be any spanning tree of $H$ with $L >= b$ leaves.
Both private edges are forced, so $r$ is internal. For each input edge $e_j$,
follow the simple tree path from $a_j$ to $r$. Its first step reaches an
original endpoint of $e_j$. That endpoint is neither endpoint of the path,
so it has at least two incident tree edges. Hence the original vertices
with tree degree at least two form a cover $C_T$. A tree with $N >= 3$
has $N-L$ internal vertices; one is $r$, giving
$|C_T| <= N-L-1 <= N-b-1=k'$. If $k<0$, then $b=N$, impossible since $r$
is internal. Otherwise $k' <= k$ proves $|C_T| <= k$.
*Optimum identity.* Let $tau$ be the minimum cover size and $lambda$ the
maximum target leaf count. The forward argument with a minimum cover yields
$lambda >= N-1-tau$. The backward argument applied to every tree yields
$tau <= |C_T| <= N-L-1$, hence $lambda <= N-1-tau$. Thus
$lambda=n+m+2-tau$. No assumption that subdivision vertices are leaves in
an arbitrary target tree is needed.
== Solution extraction
Validate the complete target witness once: Boolean encoding and length,
$N-1$ selected edges, connectivity, and $L >= b$. Reject an invalid length,
nontree, or below-bound tree. Compute degrees and return the length-$n$
Boolean vector whose entry at $v$ is true exactly when $deg_T(v) >= 2$.
The backward proof establishes cover feasibility and the source bound.
Construction and extraction take $O(n+m)$ time and space, including a
linear-time connectivity validation. There is no need to optimize the tree.
== Special cases and numeric boundaries
For $n=m=0$, $H$ is the path $p-r-q$, $N=3$, $M=2$, $lambda=2$, and the
extracted cover is empty. It is YES precisely for $k >= 0$. For an edgeless
graph with arbitrary isolated vertices, $H$ is a star with $n+2$ leaves and
the optimum cover is empty. In a general graph isolated originals have only
their root edge and can never be extracted. Disconnected sources require no
preprocessing: the root connects all components. Both signed extremes,
$-2^63$ and $2^63-1$, use the same normalization without negating $k$.
Arithmetic in the theorem is over mathematical integers. A finite machine
implementation must check $n+m$, addition of three, $2m$, and both additions
in $n+2m+2$ against its index and canonical parameter ranges; convert $N-1$
to `i64` fallibly and subtract the normalized signed bound with checked
arithmetic. An unrepresentable intermediate, bound, or allocation is an error,
not a wrapped or saturated graph. In particular $N-1=2^63-1$, $k'=-1$ makes
the final subtraction overflow and must fail. Numerical helper tests use
abstract counts without allocating huge graphs; successful sizes still obey
the exact formulas. They do not establish that such huge graphs are allocatable.
The branch $k'>N-1$ is unreachable: $k' <= n < n+m+2=N-1$. Thus no negative
bound arises after normalization. If a reusable arithmetic helper receives
unnormalized $k'>N-1$, its signed result is negative when representable;
it must not clamp to zero. The verifier checks both sides of equality and
both sides of each machine boundary. This distinction matters for $k>n$:
normalization is the specified mathematical definition, not saturation after
an underflow.
== YES example
Let $n=4$, $E=[(0,1),(1,2),(2,3),(3,0)]$, $m=4$, $k=2$.
The cover $C=\{0,2\}$ has size two; the disjoint edges $(0,1),(2,3)$
prove $tau=2$. The vertices are originals $0,1,2,3$, subdivision vertices
$4,5,6,7$, root $8$, and private leaves $9,10$. Thus $N=11$, $M=14$,
$k'=2$, $b=8$. The complete ordered target edges are
```
[(8,0),(8,1),(8,2),(8,3),
(0,4),(1,4),(1,5),(2,5),(2,6),(3,6),(3,7),(0,7),
(8,9),(8,10)]
```
Select the vector
```
[true,true,true,true,true,false,false,true,true,false,false,true,true,true]
```
It has ten edges; its degrees are $(3,1,3,1,1,1,1,1,6,1,1)$ and it is
connected. Its eight leaves meet $b$, and extraction gives
`[true,false,true,false]`. Exhaustive target optimization gives $lambda=8$.
== NO example
Use the same four-cycle but $k=1$. All vertices and the fourteen target edges
remain as above; $N=11$, $M=14$, $k'=1$, $b=9$. The two disjoint edges
require two distinct selected originals, so no source cover of size one
exists. A target tree with nine leaves would have at most one original
internal vertex, contradicting its extracted cover of these two edges.
Exhaustive enumeration gives $lambda=8<9$. The YES example's vector has
eight leaves and fails this target bound. Other target trees attach subdivision
vertices $(4,5,6,7)$ to originals $(0,1,2,0)$ or $(0,1,2,3)$, respectively;
they have seven or six leaves and fail even the YES bound of eight.
== Computational coverage and witness enumeration
`constructor.py` has seven nonempty audit sections. Section 1 uses SymPy to
check the block counts and threshold identity against constructed targets.
Section 2 independently enumerates all source subsets and all target trees
for every one of the 1,100 labeled simple graphs with $0 <= n <= 5$, and
checks every threshold transition plus signed extremes. It also tests forward
construction for every source cover. Section 3 checks extraction on every
target tree that can meet any normalized bound, rejects below-bound trees,
and checks internal-vertex inequalities on all trees. Section 4 measures
constructed graph sizes and tests checked arithmetic boundaries. Section 5
checks simplicity, connectivity, bipartition, forced neighbors, malformed
witnesses, and generic edge-subset enumeration against the structured
enumerator for every graph through three vertices. It independently counts
trees by the matrix-tree determinant on every constructed target. Sections 6 and 7 reproduce
the complete YES and NO examples. Two seeded Hypothesis strategies (300
examples each) cover arbitrary ordered simple graphs and disconnected graphs
with isolated vertices and signed/extreme bounds.
For complete structured enumeration, in an arbitrary tree let $D$ be the
source edges whose subdivision vertices use both incidences. Contract those
subdivision vertices. The resulting graph consists of a forest $D$ on the
originals plus root spokes, with exactly one root spoke in each forest
component. Every other subdivision vertex chooses exactly one endpoint as
its parent and is a leaf. Conversely any such forest, component-root choices,
and remaining attachments give a tree. This is a bijection, so enumeration
includes trees with missing root spokes and internal subdivision vertices.
The independent generic enumerator chooses all $(N-1)$-edge subsets and
tests connectivity; on small graphs its witness set must match exactly.
The proof, not finite tests, covers arbitrary sizes, enumeration completeness,
and asymptotic complexity. Source/model semantics and registry types are
established by the file inspection and CLI gate above; this Python verifier
does not run Rust evaluations. Independent adversarial verification and
cross-comparison belong to the subsequent stage and are not claimed here.
Cross-comparison script (Python)#!/usr/bin/env python3
"""Compare `pred reduce` with both verified scripts on shared instances.
python3 cross_compare.py --pred <path to pred binary> [--keep DIR]
Rule: DecisionMinimumVertexCover/SimpleGraph/One ->
DecisionMaximumLeafSpanningTree/SimpleGraph. For each shared instance this
writes the source JSON (the model's serialisation, as `pred create` writes it),
selects the one-step path from `pred path ... --json`, runs `pred reduce` and
compares the bundle's target (vertex count, ordered edge list, bound) with the
target of the constructor script and of the adversary core. Edge
endpoint orientation is the only documented isomorphism; it is reported but not
a mismatch. Then, on each instance, it evaluates witnesses with `pred
evaluate` on the target (a forward witness from a minimum cover, and a tree
just below the bound) and recovers the source with `pred extract`, comparing
both with the scripts. Exits non-zero on any mismatch or pred failure.
"""
import argparse
import json
import os
import random
import subprocess
import sys
import tempfile
from itertools import combinations
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, os.path.join(HERE, "adversary"))
sys.path.insert(1, HERE)
import adv_core as A # noqa: E402
import constructor as K # noqa: E402
SOURCE = "DecisionMinimumVertexCover/SimpleGraph/One"
TARGET = "DecisionMaximumLeafSpanningTree/SimpleGraph"
TARGET_TYPE, TARGET_VARIANT = "DecisionMaximumLeafSpanningTree", {"graph": "SimpleGraph"}
def shared_instances():
"""Deterministic: all graphs n<=3 and special families under signed and
threshold bounds, plus seeded random graphs n<=8 in random order/orientation."""
out = []
for n in range(4):
pairs = list(combinations(range(n), 2))
for mask in range(1 << len(pairs)):
E = [pairs[i] for i in range(len(pairs)) if mask >> i & 1]
out.append((n, E))
out += [(5, []), (6, [(0, 1), (2, 3)]), (4, [(0, 1), (1, 2), (2, 3), (3, 0)]),
(5, [(0, i) for i in range(1, 5)]), (6, [(0, 1), (1, 2), (0, 2), (4, 5)])]
rng = random.Random(1199)
for _ in range(25):
n = rng.randint(4, 8)
pairs = list(combinations(range(n), 2))
E = rng.sample(pairs, rng.randint(0, min(len(pairs), 11)))
out.append((n, [(v, u) if rng.random() < 0.5 else (u, v) for u, v in E]))
cases = []
for n, E in out:
tau = A.min_cover(n, E)
ks = sorted({A.I64_MIN, -1, 0, tau - 1, tau, n, n + 1, A.I64_MAX})
cases += [(n, E, k, tau) for k in ks]
return cases
def source_json(n, E, k):
return {"type": "DecisionMinimumVertexCover",
"variant": {"graph": "SimpleGraph", "weight": "One"},
"data": {"bound": k,
"inner": {"graph": {"num_vertices": n, "edges": [list(e) for e in E]},
"weights": [1] * n}}}
class PredError(Exception):
pass
def run_pred(pred, *args):
cmd = ([sys.executable, pred] if pred.endswith(".py") else [pred]) + list(args)
p = subprocess.run(cmd, capture_output=True, text=True)
if p.returncode != 0:
raise PredError(f"{' '.join(args[:2])}: exit {p.returncode}: {p.stderr.strip()[:300]}")
return p.stdout
def parse_target(bundle):
t = bundle["target"]
if t.get("type") != TARGET_TYPE or t.get("variant") != TARGET_VARIANT:
raise ValueError(f"bundle target is {t.get('type')} {t.get('variant')}")
data = t["data"]
g = data["inner"]["graph"]
return t, g["num_vertices"], [tuple(e) for e in g["edges"]], data["bound"]
def minimum_cover(n, E):
for s in range(n + 1):
for c in combinations(range(n), s):
if all(u in c or v in c for u, v in E):
return set(c)
def main():
ap = argparse.ArgumentParser(description=__doc__.split("\n")[0])
ap.add_argument("--pred", required=True)
ap.add_argument("--keep", help="directory to keep the instance and bundle files in")
args = ap.parse_args()
if args.keep:
os.makedirs(args.keep, exist_ok=True)
return compare(args.pred, args.keep)
with tempfile.TemporaryDirectory(prefix="cross_compare_") as work:
return compare(args.pred, work)
def compare(pred, work):
class _A:
pass
args = _A()
args.pred = pred
problems, stats = [], {"instances": 0, "targets equal": 0, "orientation differs": 0,
"evaluations": 0, "extractions": 0}
def bad(msg):
problems.append(msg)
if len(problems) <= 20:
print("MISMATCH:", msg)
# 1. the direct path
path_file = os.path.join(work, "paths.json")
try:
run_pred(args.pred, "path", SOURCE, TARGET, "--json", "-q", "-o", path_file)
with open(path_file) as f:
paths = json.load(f)["paths"]
direct = [p for p in paths if p.get("steps") == 1]
if not direct:
raise PredError(f"no one-step path among {len(paths)} paths")
except (PredError, OSError, ValueError, KeyError) as ex:
print(f"PRED FAILURE: pred path {SOURCE} {TARGET}: {ex}")
return 2
via = os.path.join(work, "via.json")
with open(via, "w") as f:
json.dump(direct[0], f)
for idx, (n, E, k, tau) in enumerate(shared_instances()):
stats["instances"] += 1
tag = f"#{idx} n={n} E={E} k={k}"
src = os.path.join(work, f"src{idx}.json")
out = os.path.join(work, f"bundle{idx}.json")
with open(src, "w") as f:
json.dump(source_json(n, E, k), f)
try:
run_pred(args.pred, "reduce", src, "--via", via, "-q", "-o", out)
with open(out) as f:
bundle = json.load(f)
tobj, N, T, b = parse_target(bundle)
except (PredError, OSError, ValueError, KeyError, TypeError) as ex:
bad(f"pred reduce failed {tag}: {ex}")
continue
Na, Ta, ba = A.reduce(n, E, k)
kc = K.construct(n, tuple(E), k)
same = True
for name, (N2, T2, b2) in (("adversary", (Na, Ta, ba)),
("constructor", (kc.n, list(kc.edges), kc.bound))):
if (N, b) != (N2, b2) or [frozenset(e) for e in T] != [frozenset(e) for e in T2]:
bad(f"target differs from {name} {tag}: pred N={N} b={b} E={T}; "
f"{name} N={N2} b={b2} E={T2}")
same = False
if not same:
continue
stats["targets equal"] += 1
if T != Ta:
stats["orientation differs"] += 1
tfile = os.path.join(work, f"target{idx}.json")
with open(tfile, "w") as f:
json.dump(tobj, f)
# witnesses: forward witness of a minimum cover (L >= N-1-tau), and,
# when tau >= 1, the forward witness of a cover one larger is checked too
cover = minimum_cover(n, E)
witnesses = [A.forward_witness(n, E, cover)]
if len(cover) < n:
bigger = cover | {min(set(range(n)) - cover)}
witnesses.append(A.forward_witness(n, E, bigger))
for w in witnesses:
expect_a = A.is_spanning_tree(N, T, w) and A.leaves(N, T, w) >= b
expect_k = K.target_accepts(kc, tuple(w))
try:
ev = json.loads(run_pred(args.pred, "evaluate", tfile, "--config",
json.dumps(w), "--json", "-q"))
got = {"Or(true)": True, "Or(false)": False}[ev["result"]]
except (PredError, ValueError, KeyError) as ex:
bad(f"pred evaluate failed {tag}: {ex}")
continue
stats["evaluations"] += 1
if not got == expect_a == expect_k:
bad(f"evaluation differs {tag} w={w}: pred={got} adv={expect_a} con={expect_k}")
if not got:
continue
try:
ex_out = json.loads(run_pred(args.pred, "extract", out, "--config",
json.dumps(w), "--json", "-q"))
sol = ex_out["solution"]
except (PredError, ValueError, KeyError) as ex:
bad(f"pred extract failed {tag}: {ex}")
continue
stats["extractions"] += 1
xa = A.extract(n, N, T, b, w)
xk = list(K.extract(n, kc, tuple(w)))
if not sol == xa == xk:
bad(f"extraction differs {tag}: pred={sol} adv={xa} con={xk}")
print("cross_compare:", ", ".join(f"{k} {v}" for k, v in stats.items()),
f"; {len(problems)} mismatches/failures; files in {work}")
return 1 if problems else 0
if __name__ == "__main__":
sys.exit(main()) |
Collaborator
Author
Verification certificate (continued): adversary scriptsAdversary harness (Python)#!/usr/bin/env python3
"""Adversarial verifier for DecisionMinimumVertexCover/SimpleGraph/One ->
DecisionMaximumLeafSpanningTree/SimpleGraph, written from the proof only.
Usage: python3 adversary.py [--quick] [--jobs J]
Ends with "TOTAL: <checks> checks, <failures> failures"; exit 1 on any failure.
The harness is parameterised by an implementation object (reduce, extract,
forward_witness) so that mutants.py can run it against broken constructions.
"""
import argparse
import os
import random
import sys
import types
from collections import Counter
from itertools import combinations
from multiprocessing import Pool
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import adv_core as C # noqa: E402
SEED = 1199_4
EXTREMES = [C.I64_MIN, C.I64_MIN + 1, -(2 ** 62), C.I64_MAX - 1, C.I64_MAX]
def default_impl():
return types.SimpleNamespace(reduce=C.reduce, extract=C.extract,
forward_witness=C.forward_witness,
checked_sizes=C.checked_sizes, checked_bound=C.checked_bound,
claimed_N=lambda n, m: n + m + 3, # proof's overhead table
claimed_M=lambda n, m: n + 2 * m + 2)
class Audit:
def __init__(self, stop_on_fail=False):
self.checks = Counter()
self.fails = Counter()
self.first = {}
self.sites = Counter() # (section, line) -> calls
self.site_fails = Counter() # (section, line) -> failures
self.stop = stop_on_fail
def ok(self, sec, cond, msg=""):
self.checks[sec] += 1
site = (sec, sys._getframe(1).f_lineno)
self.sites[site] += 1
if not cond:
self.site_fails[site] += 1
self.fails[sec] += 1
self.first.setdefault(sec, msg)
if self.stop:
raise StopIteration(f"{sec}: {msg}")
return cond
def merge(self, other):
self.checks.update(other.checks)
self.fails.update(other.fails)
self.sites.update(other.sites)
self.site_fails.update(other.site_fails)
for k, v in other.first.items():
self.first.setdefault(k, v)
def all_graphs(n):
pairs = list(combinations(range(n), 2))
for mask in range(1 << len(pairs)):
yield [pairs[i] for i in range(len(pairs)) if (mask >> i) & 1]
def safe_extract(impl, n, N, T, b, w):
try:
return impl.extract(n, N, T, b, w)
except Exception:
return None
# ------------------------------------------------------------------ section 1
def section_symbolic(au, impl):
import sympy as sp
n, m, k = sp.symbols("n m k", integer=True, nonnegative=True)
N = n + m + 1 + 2 # block sizes: originals + subdivisions + root + private
M = n + 2 * m + 2 # block sizes: spokes + incidences + private edges
au.ok("1 symbolic", sp.simplify(N - impl.claimed_N(n, m)) == 0, "N formula")
au.ok("1 symbolic", sp.simplify(M - impl.claimed_M(n, m)) == 0, "M formula")
N, M = impl.claimed_N(n, m), impl.claimed_M(n, m)
kp = sp.Symbol("kp", integer=True)
b = N - 1 - kp
# the symbolic bound evaluated at concrete inputs equals the implementation's bound
for nn, E, kk in [(0, [], 0), (3, [(0, 1)], 1), (4, [(0, 1), (2, 3)], -5), (2, [(0, 1)], 9)]:
vals = {n: nn, m: len(E), kp: C.normalize_bound(nn, kk)}
au.ok("1 symbolic", int(b.subs(vals)) == impl.reduce(nn, E, kk)[2], "b formula vs impl")
tau = sp.Symbol("tau", integer=True)
lam = N - 1 - tau
au.ok("1 symbolic", sp.simplify(lam - (n + m + 2 - tau)) == 0, "lambda identity")
# feasibility identity: lam >= b <=> tau <= kp (difference is identical)
au.ok("1 symbolic", sp.simplify((lam - b) - (kp - tau)) == 0)
# tree edge count: N-1 = spokes + one incidence per a_j + 2 private
au.ok("1 symbolic", sp.simplify((N - 1) - (n + m + 2)) == 0, "tree edges")
# k' <= n < N-1, so no negative bound after normalisation
au.ok("1 symbolic", sp.simplify((N - 1 - n) - (m + 2)) == 0, "N-1-n = m+2 > 0")
# measured on concrete instances with the formulas as sympy lambdas
fN, fM = sp.lambdify((n, m), N), sp.lambdify((n, m), M)
for nn in range(0, 7):
for E in [list(combinations(range(nn), 2))[:t] for t in range(0, nn * (nn - 1) // 2 + 1)]:
Nt, T, _ = impl.reduce(nn, E, 0)
au.ok("1 symbolic", Nt == fN(nn, len(E)) and len(T) == fM(nn, len(E)),
f"size n={nn} m={len(E)}")
# ------------------------------------------- per-graph exhaustive work (2-5)
def check_graph(args):
n, E, impl_name = args
au = Audit()
try:
return _check_graph(n, E, impl_name, au)
except Exception as ex: # an implementation that crashes on a valid input
au.ok("0 crash", False, f"{type(ex).__name__}: {ex} n={n} E={E}")
return au, 0
def _check_graph(n, E, impl_name, au):
impl = get_impl(impl_name)
m = len(E)
tau = C.min_cover(n, E)
Nexp, Mexp = n + m + 3, n + 2 * m + 2
N, T, _ = impl.reduce(n, E, 0)
# section 4: measured size vs exact formula
au.ok("4 overhead", N == Nexp, f"N {N}!={Nexp} n={n} E={E}")
au.ok("4 overhead", len(T) == Mexp, f"M {len(T)}!={Mexp} n={n} E={E}")
# section 5: structure
sec = "5 structure"
r, p, q = n + m, n + m + 1, n + m + 2
au.ok(sec, all(0 <= u < N and 0 <= v < N for u, v in T), "range")
au.ok(sec, all(u != v for u, v in T), "loop")
au.ok(sec, len({frozenset(e) for e in T}) == len(T), "duplicate edge")
nbr = [set() for _ in range(max(N, 1))]
for u, v in T:
if 0 <= u < N and 0 <= v < N:
nbr[u].add(v)
nbr[v].add(u)
if N == Nexp:
au.ok(sec, nbr[p] == {r} and nbr[q] == {r}, "private leaves")
au.ok(sec, all(r in nbr[v] for v in range(n)), "spokes")
au.ok(sec, all(nbr[n + j] == {u, v} for j, (u, v) in enumerate(E)), "subdivision nbrs")
au.ok(sec, nbr[r] == set(range(n)) | {p, q}, "root nbrs")
A = {r} | set(range(n, n + m))
au.ok(sec, all((u in A) != (v in A) for u, v in T), "bipartite")
expected = [(r, v) for v in range(n)] + [x for j, (u, v) in enumerate(E)
for x in ((u, n + j), (v, n + j))] + [(r, p), (r, q)]
au.ok(sec, T == expected, "exact labelled edge order of step 3")
# connectivity
seen, st = {0}, [0]
while st:
x = st.pop()
for y in nbr[x]:
if y not in seen:
seen.add(y)
st.append(y)
au.ok(sec, len(seen) == N, "connected")
# bound mapping for the k range
ks = list(range(-3, n + 3)) + EXTREMES
bounds = {}
for k in ks:
Nk, Tk, bk = impl.reduce(n, E, k)
au.ok("4 overhead", Nk == N and Tk == T, "graph depends on k")
bounds[k] = bk
au.ok("4 overhead", bk == N - 1 - C.normalize_bound(n, k), f"b k={k}")
# enumerate every spanning tree generically
trees = C.enumerate_spanning_trees(N, T)
au.ok("5 structure", len(trees) == C.count_spanning_trees(N, T), "tree count vs matrix-tree")
lam = -1
sec3 = "3 extraction"
for tr in trees:
w = [i in tr for i in range(len(T))]
deg = C.degrees(N, T, w)
L = sum(1 for d in deg if d == 1)
lam = max(lam, L)
if N == Nexp:
au.ok("6 prose", w[-1] and w[-2], "private edges forced")
au.ok("6 prose", deg[r] >= 2, "root internal")
au.ok("6 prose", all(deg[v] == 1 for v in range(n) if not any(v in e for e in E)),
"isolated original is a leaf")
# extraction at the tightest bound the tree meets, and rejection above it
kstar = N - 1 - L # smallest k' with L >= b
if kstar <= n:
b = N - 1 - kstar
c = safe_extract(impl, n, N, T, b, w)
if au.ok(sec3, c is not None and len(c) == n, f"extract failed n={n} E={E}"):
au.ok(sec3, C.is_cover(n, E, c), f"extracted noncover n={n} E={E} tree={sorted(tr)}")
au.ok(sec3, sum(c) <= kstar, f"|C|={sum(c)}>k*={kstar}=N-L-1 n={n} E={E}")
au.ok(sec3, c == [deg[v] >= 2 for v in range(n)],
"extraction is exactly deg_T(v) >= 2 (proof, solution extraction)")
au.ok(sec3, safe_extract(impl, n, N, T, L + 1, w) is None, "below-bound tree accepted")
# malformed witnesses
if trees:
w = [i in trees[0] for i in range(len(T))]
lo = -10 ** 9
au.ok(sec3, safe_extract(impl, n, N, T, lo, w[:-1]) is None, "short witness accepted")
au.ok(sec3, safe_extract(impl, n, N, T, lo, w + [False]) is None, "long witness accepted")
au.ok(sec3, safe_extract(impl, n, N, T, lo, [False] * len(T)) is None, "empty selection accepted")
au.ok(sec3, safe_extract(impl, n, N, T, lo, [True] * len(T)) is None or len(T) == N - 1,
"all-edges accepted")
# an N-1 edge non-tree (contains a cycle) when one exists
rng = random.Random(hash((n, tuple(E))) & 0xffff)
for _ in range(4):
sub = rng.sample(range(len(T)), N - 1)
ws = [i in sub for i in range(len(T))]
if not C.is_spanning_tree(N, T, ws):
au.ok(sec3, safe_extract(impl, n, N, T, lo, ws) is None, "non-tree accepted")
# section 2: equivalence for every bound, optimum identity, two oracles
sec2 = "2 equivalence"
au.ok(sec2, lam == n + m + 2 - tau, f"lambda={lam} tau={tau} n={n} E={E}")
au.ok(sec2, lam == C.max_leaves_by_cds(N, T), "lambda vs CDS oracle")
for k in ks:
src = tau <= k
tgt = lam >= bounds[k]
au.ok(sec2, src == tgt, f"k={k} src={src} tgt={tgt} n={n} E={E}")
# section 4b (forward): proof step 5 witness for every cover, every bound it meets
sec = "4 forward"
for cov in C.all_covers(n, E):
try:
w = impl.forward_witness(n, E, cov)
except Exception:
au.ok(sec, False, "forward witness raised")
continue
okt = C.is_spanning_tree(N, T, w)
au.ok(sec, okt, f"forward witness not a tree n={n} E={E} C={cov}")
if not okt:
continue
deg = C.degrees(N, T, w)
L = sum(1 for d in deg if d == 1)
au.ok(sec, {x for x in range(N) if deg[x] >= 2} <= {r} | cov, "internal not within {r} u C")
for k in ks:
if k >= len(cov):
au.ok(sec, L >= bounds[k], f"forward below bound k={k} C={cov}")
c = safe_extract(impl, n, N, T, bounds[len(cov)], w)
au.ok(sec, c is not None and C.is_cover(n, E, c) and sum(c) <= len(cov), "round trip")
return au, len(trees)
def exhaustive(au, impl_name, nmax, jobs):
work = [(n, E, impl_name) for n in range(nmax + 1) for E in all_graphs(n)]
total_trees = 0
if jobs > 1:
with Pool(jobs) as pool:
results = pool.map(check_graph, work, chunksize=4)
else:
results = map(check_graph, work)
for a, t in results:
au.merge(a)
total_trees += t
return len(work), total_trees
# ------------------------------------------------------------------ section 6
def section_special(au, impl):
sec = "6 prose"
# n = m = 0: path p - r - q, N=3, M=2, lambda=2, empty extraction, YES iff k>=0
N, T, b = impl.reduce(0, [], 0)
au.ok(sec, N == 3 and sorted(map(frozenset, T), key=sorted) == sorted(
[frozenset((0, 1)), frozenset((0, 2))], key=sorted), "empty graph is p-r-q")
trees = C.enumerate_spanning_trees(N, T)
au.ok(sec, len(trees) == 1)
w = [True] * len(T)
au.ok(sec, C.leaves(N, T, w) == 2)
au.ok(sec, safe_extract(impl, 0, N, T, b, w) == [], "empty extraction")
for k in [C.I64_MIN, -1, 0, 1, C.I64_MAX]:
_, _, bk = impl.reduce(0, [], k)
au.ok(sec, (2 >= bk) == (k >= 0), f"empty graph k={k}")
# edgeless graphs: star with n+2 leaves
for n in range(1, 9):
N, T, b = impl.reduce(n, [], 0)
au.ok(sec, N == n + 3 and C.max_leaves_by_cds(N, T) == n + 2, "edgeless star")
au.ok(sec, b == n + 2, "edgeless bound at k=0")
# k' > N-1 unreachable
for n in range(0, 7):
for E in [list(combinations(range(n), 2))[:t] for t in range(0, n * (n - 1) // 2 + 1)]:
Nk, _, bk = impl.reduce(n, E, C.I64_MAX)
au.ok(sec, n < Nk - 1 and bk >= 1, "k'<=n<N-1: bound positive")
# unused cover vertices may remain leaves (inequality, not equality)
E = [(0, 1)]
N, T, b = impl.reduce(2, E, 2)
w = impl.forward_witness(2, E, {0, 1})
deg = C.degrees(N, T, w)
au.ok(sec, deg[1] == 1 and C.leaves(N, T, w) == N - 1 - 1, "unused cover vertex is a leaf")
# signed extremes produce the normalised bound without negation
for n, E in [(0, []), (3, [(0, 1), (1, 2)]), (4, [(0, 1), (2, 3)])]:
m = len(E)
N = n + m + 3
_, _, bmin = impl.reduce(n, E, C.I64_MIN)
_, _, bmax = impl.reduce(n, E, C.I64_MAX)
au.ok(sec, bmin == N and bmax == N - 1 - n, "extremes")
# checked arithmetic boundaries, both sides
sec = "4 overhead"
U = C.USIZE_MAX
def tried(f, *args):
try:
return f(*args)
except C.ReductionError:
return None
au.ok(sec, tried(impl.checked_sizes, U - 3, 0) == (U, U - 1)) # N exactly usize::MAX
for n, m in [(U - 2, 0), (U, 1), (0, U // 2 + 1), (1, U // 2)]:
try:
res = impl.checked_sizes(n, m)
except C.ReductionError:
res = None
au.ok(sec, res is None, f"size overflow missed n={n} m={m}")
au.ok(sec, tried(impl.checked_sizes, 1, (U - 3) // 2) == ((U - 3) // 2 + 4, U)) # M = usize::MAX
au.ok(sec, tried(impl.checked_bound, 2 ** 63 - 1, -1) == C.I64_MAX) # N-1 = 2^63-2
for N, kp in [(2 ** 63, -1), (2 ** 63 + 1, 0), (2 ** 64, 5)]:
try:
res = impl.checked_bound(N, kp)
except C.ReductionError:
res = None
au.ok(sec, res is None, f"bound overflow missed N={N} kp={kp}")
au.ok(sec, tried(impl.checked_bound, 2 ** 63, 0) == C.I64_MAX) # N-1 = 2^63-1, k'=0
au.ok(sec, tried(impl.checked_bound, 5, 7) == -3, "unnormalised k'>N-1 is negative, not clamped")
# ------------------------------------------------------------------ section 7
def section_examples(au, impl):
sec = "7 examples"
n, E = 4, [(0, 1), (1, 2), (2, 3), (3, 0)]
T_exp = [(8, 0), (8, 1), (8, 2), (8, 3), (0, 4), (1, 4), (1, 5), (2, 5), (2, 6), (3, 6),
(3, 7), (0, 7), (8, 9), (8, 10)]
w = [True, True, True, True, True, False, False, True, True, False, False, True, True, True]
# YES
N, T, b = impl.reduce(n, E, 2)
au.ok(sec, N == 11 and len(T) == 14 and b == 8, "YES sizes/bound")
au.ok(sec, [frozenset(e) for e in T] == [frozenset(e) for e in T_exp], "YES edge list")
au.ok(sec, T == T_exp, "YES edge list orientation")
au.ok(sec, sum(w) == 10 and C.is_spanning_tree(N, T, w), "YES witness tree")
au.ok(sec, len(T) == 14 and C.degrees(N, T, w) == [3, 1, 3, 1, 1, 1, 1, 1, 6, 1, 1], "YES degrees")
au.ok(sec, len(T) == 14 and C.leaves(N, T, w) == 8, "YES leaves")
au.ok(sec, safe_extract(impl, n, N, T, b, w) == [True, False, True, False], "YES extraction")
au.ok(sec, C.min_cover(n, E) == 2 and C.is_cover(n, E, [True, False, True, False]))
au.ok(sec, impl.forward_witness(n, E, {0, 2}) == w, "YES witness = step-5 forward witness")
lam_enum = max(C.leaves(N, T, [i in t for i in range(len(T))])
for t in C.enumerate_spanning_trees(N, T))
au.ok(sec, lam_enum == 8 and C.max_leaves_by_cds(N, T) == 8, "lambda = 8")
# NO
N, T, b = impl.reduce(n, E, 1)
au.ok(sec, N == 11 and len(T) == 14 and b == 9, "NO sizes/bound")
au.ok(sec, not any(C.is_cover(n, E, [v == x for x in range(n)]) for v in range(n))
and C.min_cover(n, E) > 1, "NO source infeasible")
au.ok(sec, lam_enum < 9, "NO target infeasible")
au.ok(sec, safe_extract(impl, n, N, T, b, w) is None, "NO: YES vector fails b=9")
for attach, L in [((0, 1, 2, 0), 7), ((0, 1, 2, 3), 6)]:
ww = [True] * 4
for j, (u, v) in enumerate(E):
ww += [attach[j] == u, attach[j] == v]
ww += [True, True]
au.ok(sec, len(T) == 14 and C.is_spanning_tree(N, T, ww) and C.leaves(N, T, ww) == L,
f"suboptimal tree {attach}")
au.ok(sec, safe_extract(impl, n, N, T, 8, ww) is None, "suboptimal fails YES bound")
# the two disjoint edges force two distinct cover vertices
au.ok(sec, not set(E[0]) & set(E[2]))
# ------------------------------------------------------------------ section 8
def section_hypothesis(au, impl, examples):
from hypothesis import given, settings, strategies as st, HealthCheck, seed
sec = "8 hypothesis"
def full_check(n, E, k):
tau = C.min_cover(n, E)
N, T, b = impl.reduce(n, E, k)
m = len(E)
au.ok(sec, N == n + m + 3 and len(T) == n + 2 * m + 2, "sizes")
lam = C.max_leaves_by_cds(N, T)
au.ok(sec, lam == n + m + 2 - tau, f"lambda n={n} E={E}")
au.ok(sec, (tau <= k) == (lam >= b), f"equivalence n={n} E={E} k={k}")
# forward witness from an optimal cover and a random cover
cov = next(c for c in C.all_covers(n, E) if len(c) == tau) if n <= 12 else None
if cov is not None:
w = impl.forward_witness(n, E, cov)
au.ok(sec, C.is_spanning_tree(N, T, w) and C.leaves(N, T, w) >= N - 1 - tau, "forward")
return N, T, b, tau
# strategy A: arbitrary ordered/oriented simple graphs, bounds at tau-1, tau, tau+1
@st.composite
def ordered_graphs(draw):
n = draw(st.integers(0, 7))
pairs = list(combinations(range(n), 2))
chosen = draw(st.lists(st.sampled_from(pairs), unique=True, max_size=10)) if pairs else []
E = [(v, u) if draw(st.booleans()) else (u, v) for (u, v) in chosen]
d = draw(st.integers(-2, 2))
return n, E, d
@settings(max_examples=examples, deadline=None, database=None,
suppress_health_check=list(HealthCheck))
@seed(SEED)
@given(ordered_graphs())
def strat_a(case):
n, E, d = case
tau = C.min_cover(n, E)
full_check(n, E, tau + d)
# strategy B: special families (isolated vertices, disconnected unions, stars,
# matchings, complete bipartite), with signed-extreme and boundary bounds
@st.composite
def special_graphs(draw):
kind = draw(st.sampled_from(["isolated", "matching", "star", "kab", "union", "path"]))
if kind == "isolated":
n = draw(st.integers(0, 9)); E = []
elif kind == "matching":
t = draw(st.integers(1, 4)); iso = draw(st.integers(0, 2))
n = 2 * t + iso; E = [(2 * i, 2 * i + 1) for i in range(t)]
elif kind == "star":
t = draw(st.integers(1, 7)); iso = draw(st.integers(0, 2))
n = t + 1 + iso; E = [(0, i) for i in range(1, t + 1)]
elif kind == "kab":
a = draw(st.integers(1, 3)); c = draw(st.integers(1, 3))
n = a + c; E = [(i, a + j) for i in range(a) for j in range(c)]
elif kind == "path":
n = draw(st.integers(1, 8)); E = [(i, i + 1) for i in range(n - 1)]
else: # union of a triangle and a path with isolated vertices between
iso = draw(st.integers(0, 2))
E = [(0, 1), (1, 2), (0, 2)] + [(3 + iso + i, 4 + iso + i) for i in range(2)]
n = 6 + iso
perm = draw(st.permutations(list(range(n))))
E = [(perm[u], perm[v]) for u, v in E]
E = draw(st.permutations(E))
k = draw(st.sampled_from(EXTREMES + [-1, 0, n, n + 1, "tau-1", "tau"]))
return n, list(E), k
@settings(max_examples=examples, deadline=None, database=None,
suppress_health_check=list(HealthCheck))
@seed(SEED + 1)
@given(special_graphs())
def strat_b(case):
n, E, k = case
if isinstance(k, str):
k = C.min_cover(n, E) - (1 if k == "tau-1" else 0)
N, T, b, tau = full_check(n, E, k)
r = n + len(E)
for v in range(n):
if not any(v in e for e in E):
# isolated: its only edge is the spoke, so it is a leaf in every tree
au.ok(sec, sum(1 for e in T if v in e) == 1, "isolated vertex degree 1")
# strategy C: random spanning trees (random-weight Kruskal) of larger targets;
# extraction must give a cover of size <= N-L-1 and the bound mapping must agree
@st.composite
def graphs_with_tree(draw):
n = draw(st.integers(1, 10))
pairs = list(combinations(range(n), 2))
chosen = draw(st.lists(st.sampled_from(pairs), unique=True, max_size=18)) if pairs else []
E = [(v, u) if draw(st.booleans()) else (u, v) for (u, v) in chosen]
s = draw(st.integers(0, 2 ** 32))
return n, E, s
@settings(max_examples=examples, deadline=None, database=None,
suppress_health_check=list(HealthCheck))
@seed(SEED + 2)
@given(graphs_with_tree())
def strat_c(case):
n, E, s = case
N, T, _ = impl.reduce(n, E, 0)
rng = random.Random(s)
for _ in range(5):
order = list(range(len(T)))
rng.shuffle(order)
parent = list(range(N))
def find(x):
while parent[x] != x:
parent[x] = parent[parent[x]]
x = parent[x]
return x
pick = set()
for i in order:
a, c = find(T[i][0]), find(T[i][1])
if a != c:
parent[a] = c
pick.add(i)
w = [i in pick for i in range(len(T))]
L = C.leaves(N, T, w)
kstar = N - 1 - L
if kstar > n: # internal subdivision vertices: meets no bound
_, _, bn = impl.reduce(n, E, n)
au.ok(sec, safe_extract(impl, n, N, T, bn, w) is None, "below-bound accepted")
continue
_, _, b = impl.reduce(n, E, kstar)
c = safe_extract(impl, n, N, T, b, w)
au.ok(sec, c is not None and C.is_cover(n, E, c) and sum(c) <= kstar,
f"random tree extraction n={n} E={E}")
for f in (strat_a, strat_b, strat_c):
try:
f()
except StopIteration:
raise
except Exception as ex: # a failing assertion inside hypothesis
au.ok(sec, False, f"hypothesis error {type(ex).__name__}: {ex}"[:300])
IMPLS = {"default": default_impl}
def get_impl(name):
if name not in IMPLS:
import mutants # registers mutant implementations
IMPLS.update(mutants.ADV_IMPLS)
return IMPLS[name]()
def _guard(au, fn, impl):
try:
fn(au, impl)
except Exception as ex:
au.ok("0 crash", False, f"{fn.__name__}: {type(ex).__name__}: {ex}")
def run(impl_name="default", nmax=5, jobs=os.cpu_count() or 1, examples=300,
verbose=True, stop_on_fail=False):
impl = get_impl(impl_name)
au = Audit(stop_on_fail=stop_on_fail)
_guard(au, section_symbolic, impl)
ngraphs, ntrees = exhaustive(au, impl_name, nmax, jobs)
_guard(au, section_special, impl)
_guard(au, section_examples, impl)
if examples:
section_hypothesis(au, impl, examples)
total, fails = sum(au.checks.values()), sum(au.fails.values())
if verbose:
print(f"exhaustive graphs n<={nmax}: {ngraphs}, spanning trees enumerated: {ntrees}")
for sec in sorted(au.checks):
print(f" {sec:16s} {au.checks[sec]:>10d} checks {au.fails[sec]:>6d} failures"
+ (f" first: {au.first[sec]}" if sec in au.first else ""))
print(f"TOTAL: {total} checks, {fails} failures")
return au, ngraphs, ntrees
if __name__ == "__main__":
ap = argparse.ArgumentParser()
ap.add_argument("--quick", action="store_true", help="n<=4 and 50 hypothesis examples")
ap.add_argument("--jobs", type=int, default=os.cpu_count() or 1)
a = ap.parse_args()
au, _, _ = run(nmax=4 if a.quick else 5, jobs=a.jobs, examples=50 if a.quick else 300)
sys.exit(1 if sum(au.fails.values()) else 0)Adversary core (Python)"""Independent implementation of the construction in the proof.
Written from the proof alone. Source: simple graph G on vertices 0..n-1 with
an ordered edge list and a signed bound k (is there a vertex cover of size
<= k?). Target: graph H plus a signed bound b (is there a spanning tree of H
with at least b degree-one vertices?). Nothing here imports the constructor.
"""
from itertools import combinations
I64_MIN, I64_MAX = -(2 ** 63), 2 ** 63 - 1
USIZE_MAX = 2 ** 64 - 1
class ReductionError(Exception):
pass
class InvalidWitness(Exception):
pass
# ---------------------------------------------------------------- construction
def normalize_bound(n, k):
"""k' = min(n, max(-1, k)) (proof, construction step 4)."""
return min(n, max(-1, k))
def reduce(n, edges, k):
"""Return (N, target_edges, b) following construction steps 1-4."""
m = len(edges)
N, M = checked_sizes(n, m)
r = n + m
p, q = r + 1, r + 2
tedges = [(r, v) for v in range(n)]
for j, (u, v) in enumerate(edges):
a = n + j
tedges.append((u, a))
tedges.append((v, a))
tedges += [(r, p), (r, q)]
assert len(tedges) == M
b = checked_bound(N, normalize_bound(n, k))
return N, tedges, b
def forward_witness(n, edges, cover):
"""Step 5: all root spokes, both private edges, and for each subdivision
vertex the incidence to the first stored endpoint in the cover."""
m = len(edges)
w = [True] * n
for (u, v) in edges:
if u in cover:
w += [True, False]
elif v in cover:
w += [False, True]
else:
raise ValueError("not a cover")
w += [True, True]
assert len(w) == n + 2 * m + 2
return w
def degrees(N, tedges, witness):
deg = [0] * N
for (u, v), s in zip(tedges, witness):
if s:
deg[u] += 1
deg[v] += 1
return deg
def is_spanning_tree(N, tedges, witness):
if len(witness) != len(tedges):
return False
sel = [e for e, s in zip(tedges, witness) if s]
if len(sel) != N - 1:
return False
parent = list(range(N))
def find(x):
while parent[x] != x:
parent[x] = parent[parent[x]]
x = parent[x]
return x
for u, v in sel:
a, c = find(u), find(v)
if a == c:
return False
parent[a] = c
return True
def leaves(N, tedges, witness):
return sum(1 for d in degrees(N, tedges, witness) if d == 1)
def extract(n, N, tedges, b, witness):
"""Validate the target witness once, then return deg_T(v) >= 2 on originals."""
if len(witness) != len(tedges) or not all(isinstance(x, bool) for x in witness):
raise InvalidWitness("length/encoding")
if not is_spanning_tree(N, tedges, witness):
raise InvalidWitness("not a spanning tree")
if leaves(N, tedges, witness) < b:
raise InvalidWitness("below bound")
deg = degrees(N, tedges, witness)
return [deg[v] >= 2 for v in range(n)]
# ------------------------------------------------- checked machine arithmetic
def checked_sizes(n, m, usize_max=USIZE_MAX):
"""N = n+m+3 and M = n+2m+2 with every intermediate checked against usize."""
def add(a, c):
s = a + c
if s > usize_max:
raise ReductionError("overflow")
return s
nm = add(n, m)
N = add(nm, 3)
twom = add(m, m)
M = add(add(n, twom), 2)
return N, M
def checked_bound(N, kprime):
"""b = (N-1) - k' in i64, conversion and subtraction checked; never clamped."""
nm1 = N - 1
if nm1 > I64_MAX or nm1 < I64_MIN:
raise ReductionError("N-1 not representable in i64")
b = nm1 - kprime
if b > I64_MAX or b < I64_MIN:
raise ReductionError("bound overflow")
return b
# ------------------------------------------------------------- source oracle
def is_cover(n, edges, sel):
return len(sel) == n and all(sel[u] or sel[v] for u, v in edges)
def min_cover(n, edges):
for s in range(n + 1):
for c in combinations(range(n), s):
cs = set(c)
if all(u in cs or v in cs for u, v in edges):
return s
raise AssertionError
def all_covers(n, edges):
for mask in range(1 << n):
if all((mask >> u) & 1 or (mask >> v) & 1 for u, v in edges):
yield {v for v in range(n) if (mask >> v) & 1}
# ------------------------------------------------------------ target oracles
def enumerate_spanning_trees(N, tedges):
"""Generic grow-a-tree enumeration from vertex 0 (each tree exactly once).
Yields frozensets of edge indices. Knows nothing about the construction."""
inc = [[] for _ in range(N)]
for i, (u, v) in enumerate(tedges):
inc[u].append(i)
inc[v].append(i)
full = (1 << N) - 1
def other(i, intree):
u, v = tedges[i]
return v if (intree >> u) & 1 else u
out = []
def rec(intree, F, chosen):
if intree == full:
out.append(frozenset(chosen))
return
if not F:
return
e, rest = F[0], F[1:]
v = other(e, intree)
nt = intree | (1 << v)
newF = [f for f in rest if other(f, intree) != v]
for f in inc[v]:
a, c = tedges[f]
w = c if a == v else a
if not (nt >> w) & 1:
newF.append(f)
chosen.append(e)
rec(nt, newF, chosen)
chosen.pop()
rec(intree, rest, chosen)
if N == 1:
return [frozenset()]
rec(1, list(inc[0]), [])
return out
def max_leaves_by_cds(N, tedges):
"""Independent oracle: for a connected graph with N >= 3, maximum leaves
= N - (minimum connected dominating set size)."""
adj = [0] * N
for u, v in tedges:
adj[u] |= 1 << v
adj[v] |= 1 << u
full = (1 << N) - 1
for s in range(1, N + 1):
for c in combinations(range(N), s):
mask = 0
dom = 0
for x in c:
mask |= 1 << x
dom |= adj[x] | (1 << x)
if dom != full:
continue
# connected?
seen = 1 << c[0]
frontier = seen
while frontier:
nxt = 0
for x in range(N):
if (frontier >> x) & 1:
nxt |= adj[x] & mask
nxt &= ~seen
seen |= nxt
frontier = nxt
if seen == mask:
return N - s
raise AssertionError
def count_spanning_trees(N, tedges):
"""Matrix-tree theorem with exact Bareiss elimination."""
if N == 1:
return 1
L = [[0] * N for _ in range(N)]
for u, v in tedges:
L[u][u] += 1
L[v][v] += 1
L[u][v] -= 1
L[v][u] -= 1
A = [row[1:] for row in L[1:]]
n = N - 1
sign, prev = 1, 1
for i in range(n):
if A[i][i] == 0:
for j in range(i + 1, n):
if A[j][i] != 0:
A[i], A[j] = A[j], A[i]
sign = -sign
break
else:
return 0
for j in range(i + 1, n):
for l in range(i + 1, n):
A[j][l] = (A[j][l] * A[i][i] - A[j][i] * A[i][l]) // prev
prev = A[i][i]
return sign * A[n - 1][n - 1] |
Collaborator
Author
Agentic Review ReportSubject: rule Verdict: approve: no open findings. The one Minor finding from the first review has been fixed and verified, and nothing else in the diff changed. Structural and semanticHard fails: none.
Rule (
Decision variant (
Hand trace (C₄, k = 2). The target has N = 11 and M = 14, with edges Proof and paper. The construction is Bonsma's universal vertex plus edge subdivision for cubic vertex cover (arXiv:0912.0226, last paragraph before §2, "n − y + m leaves"). It adds two private leaves, which makes the root internal. The bound is therefore Issue compliance. The issue's 4-cycle example appears in a test and in the canonical example: YES at k = 2, NO at k = 1, and the 7- and 6-leaf suboptimal trees are rejected. The source and target optima are confirmed by brute force. The tests cover signed bounds ( Quality
Feature test
FindingsNone open. Resolved: Minor 1, the paper's rule command block could not be run as written.
|
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1242 +/- ##
==========================================
+ Coverage 97.19% 97.20% +0.01%
==========================================
Files 1146 1149 +3
Lines 151558 152106 +548
==========================================
+ Hits 147308 147859 +551
+ Misses 4250 4247 -3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Collaborator
Author
|
Please kindly check the following items (PR #1242):
Join the discussion on Zulip — feel free to ask questions or leave feedback there. |
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 rule
DecisionMinimumVertexCover<SimpleGraph, One>→DecisionMaximumLeafSpanningTree<SimpleGraph>(Bonsma's universal-vertex construction with subdivided edges and two private leaves), with the closed-loop and exhaustive small-graph tests, a canonical example, and a paper entry with reproduciblepredcommands.Target size:
num_vertices + num_edges + 3vertices andnum_vertices + 2·num_edges + 2edges; the leaf bound isN − 1 − k.New target variant. As the issue asks, the decision variant
DecisionMaximumLeafSpanningTree/SimpleGraphis introduced in this same PR (model-local decision wrapper, registry entry, ILP pipeline, tests). Maintainers may want to triage the endpoint registration separately.Fixes #1199