Repository navigation
Conversation
Collaborator
Author
Verification certificateVerdict: VERIFIED. Source The constructor made 19,237,796 checks, zero failures: symbolic overhead 2; forward/backward and optimum 8,334,270; extraction 9,374,279; measured overhead 764,601; structure 764,602; YES 8; NO bound 34. It exhausts all 1,100 labelled simple graphs with n=0..5 and all 254,254 assignments from {-1,0,1}^n, plus n=6 empty, complete and path families and i64 boundaries. Hypothesis: two strategies, 300 examples each, seeds 1729 and 2718, n=0..7, database disabled. The independent checker made 47,952,097 checks, zero failures: overhead 1,361,184; well-formedness 8,532,099; forward 6,153,378; backward 6,153,378; values/errors 11,232,275; optimum 1,710,083; extraction 12,593,458; YES 19; NO bound 68; special cases 225; Hypothesis 215,930. Exhaustive families: all graphs n≤4 with weights {-2,-1,0,1,2}^n, all graphs n=5 with weights {-1,0,2}^5, and all 32,768 graphs n=6 with five weight patterns and selected configurations. Hypothesis: three strategies, 400 examples each, seeds 41, 42, 43, database disabled, no deadline; twins and isolates n≤8, boundary-weight graphs n≤7, and disjoint unions of paths, cycles, complete and edgeless graphs. Cross-comparison: 42,264 target instances and 359,037 configuration outcomes agree, zero disagreements; families include every graph n≤5, every graph n=6, and 3,000 random graphs n≤12 with i64 weights and shuffled/reversed edges. The bound-1 NO case is a decision bound; unbounded instances are feasible by selecting all vertices. The source listings below omit local paths from comments and prose; executable statements are unchanged. The independent checker comprises the two Python listings. Constructor# /// script
# requires-python = ">=3.12"
# dependencies = ["sympy==1.14.0", "hypothesis==6.170.14"]
# ///
"""Closed-neighbourhood construction checks; run with python3 or uv run."""
import os
import sys
try:
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
except ModuleNotFoundError:
os.execvp("uv", ["uv", "run", "--script", __file__, *sys.argv[1:]])
from collections import Counter
from dataclasses import dataclass
from itertools import combinations, product
LOW, HIGH = -(2**63), 2**63 - 1
COUNTS = Counter()
FAILURES = Counter()
SECTIONS = (
"1 symbolic overhead", "2 forward/backward and optimum",
"3 extraction", "4 measured overhead", "5 target structure",
"6 YES example", "7 NO example",
)
@dataclass(frozen=True)
class Target:
universe_size: int
sets: tuple[tuple[int, ...], ...]
weights: tuple[int, ...]
def reduce(n, edges, weights):
if n < 0 or len(weights) != n or any(not LOW <= w <= HIGH for w in weights):
raise ValueError("invalid source size or weights")
seen = set()
neighborhoods = [{v} for v in range(n)]
for u, v in edges:
edge = (min(u, v), max(u, v))
if not (0 <= u < n and 0 <= v < n) or u == v or edge in seen:
raise ValueError("not a simple graph")
seen.add(edge)
neighborhoods[u].add(v)
neighborhoods[v].add(u)
return Target(n, tuple(tuple(sorted(s)) for s in neighborhoods), tuple(weights))
def check(section, condition, context):
COUNTS[section] += 1
if not condition:
FAILURES[section] += 1
if sum(FAILURES.values()) <= 10:
print(f"FAIL {SECTIONS[section - 1]}: {context}", flush=True)
def configurations(n):
return tuple(product((False, True), repeat=n))
def source_feasible(n, edges, config):
# Vertex-centred predicate, independent of target neighbourhood construction.
if len(config) != n:
raise ValueError("wrong source configuration length")
return all(config[v] or any(
(a == v and config[b]) or (b == v and config[a])
for a, b in edges
) for v in range(n))
def target_feasible(target, config):
if len(config) != len(target.sets):
raise ValueError("wrong target configuration length")
covered = set()
for selected, subset in zip(config, target.sets):
if selected:
covered.update(subset)
return covered == set(range(target.universe_size))
def selected_sum(weights, config):
total = 0
for selected, weight in zip(config, weights):
if selected:
total += weight
if not LOW <= total <= HIGH:
return "overflow"
return total
def source_value(n, edges, weights, config):
return selected_sum(weights, config) if source_feasible(n, edges, config) else None
def target_value(target, config):
return selected_sum(target.weights, config) if target_feasible(target, config) else None
def extract_solution(target, config):
value = target_value(target, config)
if value is None or value == "overflow":
raise ValueError("target witness does not evaluate to a feasible value")
return tuple(config)
PATH_EDGES = ((0, 1), (1, 2), (2, 3), (3, 4))
PATH_WEIGHTS = (3, 1, 4, 1, 3)
PATH_SETS = ((0, 1), (0, 1, 2), (1, 2, 3), (2, 3, 4), (3, 4))
def examples():
# Expected sets, costs and unique optimum are hand-derived in the proof.
target = reduce(5, PATH_EDGES, PATH_WEIGHTS)
check(6, target == Target(5, PATH_SETS, PATH_WEIGHTS), "canonical path target")
optimum = (False, True, False, True, False)
check(6, target_value(target, optimum) == 2, "path optimum has cost 2")
check(6, extract_solution(target, optimum) == optimum
and source_value(5, PATH_EDGES, PATH_WEIGHTS, optimum) == 2,
"path extraction")
for config in ((True, False, False, True, False),
(False, True, False, False, True)):
check(6, target_value(target, config) == 4
and source_value(5, PATH_EDGES, PATH_WEIGHTS, config) == 4,
"feasible suboptimal path cover")
target_optima = [c for c in configurations(5) if target_value(target, c) == 2]
check(6, target_optima == [optimum], "unique optimum")
check(6, min(target_value(target, c) for c in configurations(5)
if target_feasible(target, c)) == 2, "no cheaper cover")
check(6, target_value(target, (False,) * 5) is None, "uncovered path")
# NO means no solution within bound 1, not unbounded infeasibility.
check(7, target == Target(5, PATH_SETS, PATH_WEIGHTS), "NO target sets and costs")
for config in configurations(5):
tv = target_value(target, config)
sv = source_value(5, PATH_EDGES, PATH_WEIGHTS, config)
check(7, (tv is None or tv > 1) and (sv is None or sv > 1),
("NO at bound 1", config, sv, tv))
check(7, target_value(target, optimum) == 2,
"NO-bound instance remains feasible without the bound")
def symbolic():
n = sp.Symbol("n", integer=True, nonnegative=True)
v = sp.Symbol("v", integer=True)
cardinality = sp.summation(1, (v, 0, n - 1))
targets = [reduce(k, (), (0,) * k) for k in range(7)]
for name, measure in (("universe_size", lambda t: t.universe_size),
("num_sets", lambda t: len(t.sets))):
check(1, sp.simplify(cardinality - n) == 0
and all(measure(t) == cardinality.subs(n, k)
for k, t in enumerate(targets)), name)
def rejects_extraction(target, config):
try:
extract_solution(target, config)
except ValueError:
return True
return False
def inspect_instance(n, edges, weights):
target = reduce(n, edges, weights)
check(4, target.universe_size == n, ("universe_size", n, target))
check(4, len(target.sets) == n, ("num_sets", n, target))
check(4, sum(map(len, target.sets)) == n + 2 * len(edges),
("incidences", n, edges, target))
check(5, len(target.weights) == len(target.sets) and target.weights == tuple(weights),
("indexed weights", weights, target))
members_in_range = all(0 <= u < target.universe_size for s in target.sets for u in s)
check(5, members_in_range and all(s == tuple(sorted(set(s))) for s in target.sets),
("target subsets", target))
check(5, all(v in s for v, s in enumerate(target.sets))
and target_feasible(target, (True,) * len(target.sets)),
("self coverage and full cover", target))
if len(target.sets) != n or len(target.weights) != n or not members_in_range:
return target
configs = configurations(n)
source_values, target_values = [], []
for config in configs:
sf = source_feasible(n, edges, config)
tf = target_feasible(target, config)
sv = selected_sum(weights, config) if sf else None
tv = selected_sum(target.weights, config) if tf else None
source_values.append(sv)
target_values.append(tv)
check(2, sf == tf and sv == tv, (n, edges, weights, config, sv, tv))
if tf:
if tv == "overflow":
check(3, rejects_extraction(target, config) and sv == "overflow",
("overflow rejection", weights, config))
else:
extracted = extract_solution(target, config)
check(3, extracted == config
and source_value(n, edges, weights, extracted) == tv,
("extraction", n, edges, weights, config))
else:
check(3, rejects_extraction(target, config), ("non-cover", n, config))
if "overflow" not in source_values and "overflow" not in target_values:
source_optimum = min((x for x in source_values if x is not None), default=None)
target_optimum = min((x for x in target_values if x is not None), default=None)
check(2, source_optimum == target_optimum, ("optima", n, edges, weights))
for config, value in zip(configs, target_values):
if value is not None and value == target_optimum:
check(3, source_value(n, edges, weights,
extract_solution(target, config)) == source_optimum,
("every optimal cover", n, edges, weights, config))
check(3, rejects_extraction(target, (False,) * (len(target.sets) + 1)),
"long witness")
if target.sets:
check(3, rejects_extraction(target, (False,) * (len(target.sets) - 1)),
"short witness")
return target
def exhaustive():
graph_count = instance_count = 0
for n in range(6):
before = instance_count
possible_edges = tuple(combinations(range(n), 2))
for edge_bits in product((False, True), repeat=len(possible_edges)):
edges = tuple(e for e, selected in zip(possible_edges, edge_bits) if selected)
graph_count += 1
for weights in product((-1, 0, 1), repeat=n):
inspect_instance(n, edges, weights)
instance_count += 1
print(f"exhaustive n={n}: {instance_count - before} weighted instances", flush=True)
print(f"exhaustive: {graph_count} graphs, {instance_count} weighted instances", flush=True)
def boundaries():
# Hand-computed results include overflow before cancellation in index order.
cases = (
(0, (), (), (), 0),
(1, (), (-5,), (True,), -5),
(3, (), (0, -5, 2), (True, True, True), -3),
(3, ((0, 1), (1, 2)), (LOW, 0, HIGH), (True, True, True), -1),
(3, ((0, 1), (1, 2)), (HIGH, 1, -1), (True, True, True), "overflow"),
(3, ((0, 1), (1, 2)), (LOW, -1, 1), (True, True, True), "overflow"),
(3, ((0, 1), (1, 2)), (HIGH, 0, 0), (True, True, True), HIGH),
(3, ((0, 1), (1, 2)), (LOW, 0, 0), (True, True, True), LOW),
(3, (), (HIGH, 1, -1), (False, False, False), None),
)
for n, edges, weights, config, expected in cases:
target = inspect_instance(n, edges, weights)
check(2, target_value(target, config) == expected
and source_value(n, edges, weights, config) == expected,
("hand-derived boundary", weights, expected))
# Equal sets remain separate choices, including their signed costs.
target = inspect_instance(3, ((0, 1), (0, 2), (1, 2)), (-5, 0, 2))
check(5, target.sets == ((0, 1, 2),) * 3 and target.weights == (-5, 0, 2),
"duplicate neighbourhoods retain vertex indices")
for edges in ((), tuple(combinations(range(6), 2)),
tuple((v, v + 1) for v in range(5))):
inspect_instance(6, edges, (-2, 0, 3, -2, 0, 3))
WEIGHTS = st.one_of(st.integers(LOW, HIGH), st.sampled_from((LOW, HIGH, -5, -1, 0, 1, 5)))
@st.composite
def arbitrary_graphs(draw):
n = draw(st.integers(0, 7))
possible = tuple(combinations(range(n), 2))
edges = tuple(sorted(draw(st.sets(st.sampled_from(possible))))) if possible else ()
weights = tuple(draw(st.lists(WEIGHTS, min_size=n, max_size=n)))
return n, edges, weights
@st.composite
def isolated_and_twin_graphs(draw):
n = draw(st.integers(3, 7))
# Last vertex is isolated; the first block is a clique with equal neighbourhoods.
block = draw(st.integers(1, n - 1))
edges = tuple(combinations(range(block), 2))
weights = tuple(draw(st.lists(WEIGHTS, min_size=n, max_size=n)))
return n, edges, weights
@seed(1729)
@settings(max_examples=300, deadline=None, database=None)
@given(arbitrary_graphs())
def property_arbitrary(instance):
before = sum(FAILURES.values())
inspect_instance(*instance)
assert sum(FAILURES.values()) == before, instance
@seed(2718)
@settings(max_examples=300, deadline=None, database=None)
@given(isolated_and_twin_graphs())
def property_isolated_and_twins(instance):
before = sum(FAILURES.values())
inspect_instance(*instance)
assert sum(FAILURES.values()) == before, instance
def main():
symbolic()
examples()
boundaries()
exhaustive()
property_arbitrary()
property_isolated_and_twins()
print("Hypothesis: 300 examples per strategy; seeds 1729, 2718; n=0..7; database=None")
for section, label in enumerate(SECTIONS, 1):
print(f"{label}: {COUNTS[section]} checks, {FAILURES[section]} failures")
print(f"TOTAL: {sum(COUNTS.values())} checks, {sum(FAILURES.values())} failures")
return bool(sum(FAILURES.values()))
if __name__ == "__main__":
sys.exit(main())Independent checker core"""Independent adversary implementation of the closed-neighbourhood reduction
MinimumDominatingSet<SimpleGraph, i64> -> MinimumSetCovering<i64>.
Written from the proof and the endpoint model sources only; it does not
import or copy the constructor. Standard library only, so that
the comparison program can import it with a bare python3.
Instance encodings (mirroring the library JSON `data` objects):
source: {"num_vertices": n, "edges": [[u, v], ...], "weights": [w_0, ...]}
target: {"universe_size": u, "sets": [[...], ...], "weights": [c_0, ...]}
"""
from __future__ import annotations
I64_MIN = -(2**63)
I64_MAX = 2**63 - 1
class EvalError(Exception):
"""Mirrors crate::traits::EvaluationError; `kind` is 'length' or 'overflow'."""
def __init__(self, kind: str, msg: str = ""):
super().__init__(f"{kind}: {msg}")
self.kind = kind
class ExtractionError(Exception):
pass
# --------------------------------------------------------------------------
# Source model: admission and evaluation (independent of the construction).
# --------------------------------------------------------------------------
def validate_source(src: dict) -> None:
"""SimpleGraph admission: in-range endpoints, no loops, no repeated edge
(either orientation); exactly one i64 weight per vertex."""
n = src["num_vertices"]
seen = set()
for u, v in src["edges"]:
if not (0 <= u < n and 0 <= v < n):
raise ValueError("endpoint out of range")
if u == v:
raise ValueError("self-loop")
key = (min(u, v), max(u, v))
if key in seen:
raise ValueError("repeated edge")
seen.add(key)
if len(src["weights"]) != n:
raise ValueError("weight count")
for w in src["weights"]:
if not (I64_MIN <= w <= I64_MAX):
raise ValueError("weight outside i64")
def _checked_sum(weights, config):
total = 0
for i, sel in enumerate(config):
if sel:
total += weights[i]
if not (I64_MIN <= total <= I64_MAX):
raise EvalError("overflow", f"at index {i}")
return total
def is_dominating(src: dict, x) -> bool:
"""Domination straight from the edge list (no neighbourhood sets)."""
n = src["num_vertices"]
ok = [bool(x[v]) for v in range(n)]
for u, v in src["edges"]:
if x[u]:
ok[v] = True
if x[v]:
ok[u] = True
return all(ok)
def eval_source(src: dict, x):
"""Returns the cost (int) or None for infeasible; raises EvalError."""
if len(x) != src["num_vertices"]:
raise EvalError("length")
if not is_dominating(src, x):
return None
return _checked_sum(src["weights"], x)
# --------------------------------------------------------------------------
# Target model: admission and evaluation.
# --------------------------------------------------------------------------
def validate_target(tgt: dict) -> None:
if len(tgt["sets"]) != len(tgt["weights"]):
raise ValueError("weights/sets length")
for s in tgt["sets"]:
for e in s:
if not (0 <= e < tgt["universe_size"]):
raise ValueError("element outside universe")
for c in tgt["weights"]:
if not (I64_MIN <= c <= I64_MAX):
raise ValueError("weight outside i64")
def covers(tgt: dict, y) -> bool:
covered = set()
for i, sel in enumerate(y):
if sel:
covered.update(tgt["sets"][i])
return all(e in covered for e in range(tgt["universe_size"]))
def eval_target(tgt: dict, y):
if len(y) != len(tgt["sets"]):
raise EvalError("length")
if not covers(tgt, y):
return None
return _checked_sum(tgt["weights"], y)
def outcome(fn, inst, cfg):
"""Normalised evaluation outcome: ('val', v) / ('val', None) / ('err', kind)."""
try:
return ("val", fn(inst, cfg))
except EvalError as e:
return ("err", e.kind)
# --------------------------------------------------------------------------
# The construction and extraction, as stated in the proof.
# --------------------------------------------------------------------------
def reduce(src: dict) -> dict:
"""Construction steps 1-3: U = V; D_v = N[v] in vertex order (members
stored once, sorted); c_v = w_v; equal subsets kept."""
n = src["num_vertices"]
closed = [{v} for v in range(n)]
for u, v in src["edges"]:
closed[u].add(v)
closed[v].add(u)
return {
"universe_size": n,
"sets": [sorted(closed[v]) for v in range(n)],
"weights": list(src["weights"]),
}
def extract(tgt: dict, y) -> list:
"""Evaluate the target witness once; reject length errors, overflow and
infeasible witnesses; otherwise return x = y."""
try:
val = eval_target(tgt, y)
except EvalError as e:
raise ExtractionError(f"target evaluation failed: {e}") from e
if val is None:
raise ExtractionError("target witness is not a cover")
return [bool(b) for b in y]
def canonical_target(tgt: dict) -> dict:
"""Canonical form up to the one documented isomorphism: within-set order."""
return {
"universe_size": tgt["universe_size"],
"sets": [sorted(s) for s in tgt["sets"]],
"weights": list(tgt["weights"]),
}Independent checker harness# /// script
# requires-python = ">=3.10"
# dependencies = ["hypothesis==6.170.14"]
# ///
"""Adversary harness for MinimumDominatingSet/SimpleGraph/i64 -> MinimumSetCovering/i64.
Independent of the constructor. Run:
python harness.py # full run
python harness.py --quick # n <= 4, fewer examples
Every claim of the proof that is testable is mapped to a section below
(see CLAIMS at the bottom). The harness takes reduce/extract as parameters so
that mutants.py can run it against deliberately broken constructions.
"""
from __future__ import annotations
import itertools
import os
import random
import sys
from collections import Counter, defaultdict
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import core # noqa: E402
from core import ( # noqa: E402
I64_MAX,
I64_MIN,
ExtractionError,
eval_source,
eval_target,
outcome,
validate_source,
validate_target,
)
SECTIONS = [
"S1 overhead",
"S2 well-formed",
"S3 forward",
"S4 backward",
"S5 values/errors",
"S6 optimum",
"S7 extraction",
"S8 YES example",
"S9 NO example",
"S10 special cases",
"S11 hypothesis",
]
class Audit:
def __init__(self):
self.checks = Counter()
self.fails = Counter()
self.examples = defaultdict(list)
def check(self, section, cond, detail=""):
self.checks[section] += 1
if not cond:
self.fails[section] += 1
if len(self.examples[section]) < 3:
self.examples[section].append(detail)
return cond
def total(self):
return sum(self.checks.values()), sum(self.fails.values())
def report(self, out=sys.stdout):
for s in SECTIONS:
print(f" {s:<20} {self.checks[s]:>10} checks, {self.fails[s]:>6} failures", file=out)
for ex in self.examples[s]:
print(f" e.g. {ex}", file=out)
c, f = self.total()
print(f"TOTAL: {c} checks, {f} failures", file=out)
# --------------------------------------------------------------------------
# Generic per-instance checks.
# --------------------------------------------------------------------------
def all_configs(n):
return [list(bits) for bits in itertools.product((False, True), repeat=n)]
def check_instance(a: Audit, src, reduce_fn, extract_fn, configs=None, full=True):
"""Runs S1-S7 on one source instance. `configs`: restrict the
configuration set (None = all 2^n). `full`: also check optimum (needs all
configurations)."""
validate_source(src)
n = src["num_vertices"]
m = len(src["edges"])
tag = f"n={n} E={src['edges']} w={src['weights']}"
try:
tgt = reduce_fn(src)
except Exception as e: # a crash is a failure of S2
a.check("S2 well-formed", False, f"{tag}: reduce raised {e!r}")
return
# S1: overhead, exact formulas, plus the diagnostic membership identity.
a.check("S1 overhead", tgt["universe_size"] == n, f"{tag}: universe_size {tgt['universe_size']}")
a.check("S1 overhead", len(tgt["sets"]) == n, f"{tag}: num_sets {len(tgt['sets'])}")
a.check("S1 overhead", sum(len(s) for s in tgt["sets"]) == n + 2 * m,
f"{tag}: membership {sum(len(s) for s in tgt['sets'])} != {n + 2 * m}")
# S2: target admitted; D_v = N[v] computed from an adjacency matrix;
# members stored once; weights copied; v in D_v; selecting all covers.
try:
validate_target(tgt)
admitted = True
except ValueError as e:
admitted = False
a.check("S2 well-formed", False, f"{tag}: target rejected: {e}")
if admitted:
a.check("S2 well-formed", True)
adj = [[False] * n for _ in range(n)]
for u, v in src["edges"]:
adj[u][v] = adj[v][u] = True
a.check("S2 well-formed", tgt["weights"] == src["weights"], f"{tag}: weights {tgt['weights']}")
if len(tgt["sets"]) == n:
for v in range(n):
s = tgt["sets"][v]
want = {u for u in range(n) if u == v or adj[u][v]}
a.check("S2 well-formed", len(s) == len(set(s)), f"{tag}: D_{v}={s} repeats a member")
a.check("S2 well-formed", set(s) == want, f"{tag}: D_{v}={s} != N[{v}]={sorted(want)}")
a.check("S2 well-formed", v in s, f"{tag}: {v} not in D_{v}")
if admitted and len(tgt["sets"]) == n:
a.check("S2 well-formed", core.covers(tgt, [True] * n), f"{tag}: select-all does not cover")
if not admitted:
return
nt = len(tgt["sets"])
cfgs = all_configs(n) if configs is None else configs
src_best, tgt_best = None, None
src_opt, tgt_opt = set(), set()
for x in cfgs:
so = outcome(eval_source, src, x)
if nt == n:
to = outcome(eval_target, tgt, x)
else:
to = ("err", "length")
# Feasibility from the pure predicates, independent of summation.
s_dom = core.is_dominating(src, x)
t_cov = nt == n and core.covers(tgt, x)
if s_dom:
a.check("S3 forward", t_cov, f"{tag}: x={x} dominates, y=x does not cover")
if t_cov:
a.check("S4 backward", s_dom, f"{tag}: y={x} covers, x=y does not dominate")
a.check("S5 values/errors", so == to, f"{tag}: x={x} source {so} target {to}")
key = tuple(x)
if so[0] == "val" and so[1] is not None:
if src_best is None or so[1] < src_best:
src_best, src_opt = so[1], {key}
elif so[1] == src_best:
src_opt.add(key)
if to[0] == "val" and to[1] is not None:
if tgt_best is None or to[1] < tgt_best:
tgt_best, tgt_opt = to[1], {key}
elif to[1] == tgt_best:
tgt_opt.add(key)
# S7: extraction of every target configuration.
if nt != n:
continue
if to[0] == "val" and to[1] is not None:
try:
xe = extract_fn(tgt, x)
ok = outcome(eval_source, src, xe) == to
a.check("S7 extraction", ok, f"{tag}: y={x} -> x={xe}: source {outcome(eval_source, src, xe)} vs {to}")
except Exception as e:
a.check("S7 extraction", False, f"{tag}: y={x} feasible but extraction raised {e!r}")
else:
try:
xe = extract_fn(tgt, x)
a.check("S7 extraction", False, f"{tag}: y={x} ({to}) extracted to {xe}")
except ExtractionError:
a.check("S7 extraction", True)
except Exception as e:
a.check("S7 extraction", False, f"{tag}: y={x}: wrong exception {e!r}")
if full:
a.check("S6 optimum", src_best == tgt_best, f"{tag}: optimum {src_best} vs {tgt_best}")
a.check("S6 optimum", src_opt == tgt_opt, f"{tag}: optimal sets differ")
# Select-all dominates and covers, so a feasible configuration exists;
# a successful optimum exists unless every feasible one overflows.
a.check("S6 optimum", core.is_dominating(src, [True] * n) and nt == n and core.covers(tgt, [True] * n),
f"{tag}: select-all infeasible")
# Every optimal target witness extracts to an optimal source witness.
for y in sorted(tgt_opt):
try:
xe = extract_fn(tgt, list(y))
a.check("S6 optimum", tuple(xe) in src_opt, f"{tag}: optimal y={y} -> non-optimal x={xe}")
except Exception as e:
a.check("S6 optimum", False, f"{tag}: optimal y={y} extraction raised {e!r}")
# Malformed lengths are rejected by extraction.
if nt == n:
for bad in ([False] * (n + 1), [True] * (n + 1)) + (([True] * (n - 1),) if n > 0 else ()):
try:
extract_fn(tgt, bad)
a.check("S7 extraction", False, f"{tag}: length {len(bad)} accepted")
except ExtractionError:
a.check("S7 extraction", True)
except Exception as e:
a.check("S7 extraction", False, f"{tag}: length {len(bad)}: wrong exception {e!r}")
# --------------------------------------------------------------------------
# Instance families.
# --------------------------------------------------------------------------
def all_graphs(n):
pairs = list(itertools.combinations(range(n), 2))
for mask in range(1 << len(pairs)):
yield [list(p) for i, p in enumerate(pairs) if mask >> i & 1]
def weight_patterns(n):
"""Identity-reduction risk configs: all-zero, all-one, alternating, all-negative."""
return [
[0] * n,
[1] * n,
[(-1) ** i for i in range(n)],
[(-1) ** (i + 1) for i in range(n)],
[-1] * n,
]
def config_patterns(n):
out = [[False] * n, [True] * n,
[i % 2 == 0 for i in range(n)], [i % 2 == 1 for i in range(n)]]
for i in range(n):
out.append([j == i for j in range(n)])
out.append([j != i for j in range(n)])
uniq = []
for c in out:
if c not in uniq:
uniq.append(c)
return uniq
def exhaustive(a, reduce_fn, extract_fn, quick=False):
# n <= 4: every labelled simple graph x every weight vector over {-2,..,2}.
nmax_dense = 3 if quick else 4
for n in range(0, nmax_dense + 1):
for edges in all_graphs(n):
for w in itertools.product((-2, -1, 0, 1, 2), repeat=n):
check_instance(a, {"num_vertices": n, "edges": edges, "weights": list(w)}, reduce_fn, extract_fn)
if quick:
return
# n = 5: every labelled simple graph x every weight vector over {-1, 0, 2}.
for edges in all_graphs(5):
for w in itertools.product((-1, 0, 2), repeat=5):
check_instance(a, {"num_vertices": 5, "edges": edges, "weights": list(w)}, reduce_fn, extract_fn)
# n = 6: every labelled simple graph x identity-risk weight patterns,
# restricted to identity-risk configurations (all-zero/one/alternating,
# singletons, co-singletons).
cp = config_patterns(6)
for edges in all_graphs(6):
for w in weight_patterns(6):
check_instance(a, {"num_vertices": 6, "edges": edges, "weights": w}, reduce_fn, extract_fn,
configs=cp, full=False)
# --------------------------------------------------------------------------
# Worked examples and special cases from the proof's prose.
# --------------------------------------------------------------------------
PATH5 = {"num_vertices": 5, "edges": [[0, 1], [1, 2], [2, 3], [3, 4]], "weights": [3, 1, 4, 1, 3]}
def sel(n, idx):
return [i in idx for i in range(n)]
def yes_example(a, reduce_fn, extract_fn):
S = "S8 YES example"
t = reduce_fn(PATH5)
a.check(S, t["universe_size"] == 5 and len(t["sets"]) == 5, "parameters not 5")
want = [[0, 1], [0, 1, 2], [1, 2, 3], [2, 3, 4], [3, 4]]
a.check(S, [sorted(s) for s in t["sets"]] == want, f"sets {t['sets']}")
a.check(S, t["weights"] == [3, 1, 4, 1, 3], f"weights {t['weights']}")
a.check(S, sum(len(s) for s in t["sets"]) == 13 == 5 + 2 * 4, "membership 13")
y = [False, True, False, True, False]
a.check(S, eval_target(t, y) == 2, "y={1,3} cost 2")
covered = set(t["sets"][1]) | set(t["sets"][3])
a.check(S, covered == set(range(5)), "D1 u D3 = U")
x = extract_fn(t, y)
a.check(S, x == y and eval_source(PATH5, x) == 2, "extraction {1,3} cost 2")
a.check(S, set(t["sets"][1]) == {0, 1, 2} and set(t["sets"][3]) == {2, 3, 4}, "1 dominates 0,1,2; 3 dominates 2,3,4")
vals = {tuple(c): eval_target(t, c) for c in all_configs(5)}
cheap = sorted(tuple(i for i in range(5) if c[i]) for c in all_configs(5)
if sum(PATH5["weights"][i] for i in range(5) if c[i]) < 2)
a.check(S, cheap == [(), (1,), (3,)], f"configurations of cost < 2: {cheap}")
a.check(S, all(vals[tuple(sel(5, c))] is None for c in cheap), "a cost<2 choice covers")
exact2 = [c for c in all_configs(5) if sum(PATH5["weights"][i] for i in range(5) if c[i]) == 2]
a.check(S, exact2 == [y], f"cost exactly 2: {exact2}")
feas = [v for v in vals.values() if v is not None]
a.check(S, min(feas) == 2, "optimum 2")
a.check(S, [k for k, v in vals.items() if v == 2] == [tuple(y)], "unique optimum")
for pair in ((0, 3), (1, 4)):
c = sel(5, pair)
a.check(S, eval_target(t, c) == 4, f"{pair} cost 4")
a.check(S, eval_source(PATH5, extract_fn(t, c)) == 4, f"{pair} extract cost 4")
a.check(S, eval_target(t, [False] * 5) is None and eval_source(PATH5, [False] * 5) is None, "all-false")
# Source-side optimum by independent enumeration.
a.check(S, min(v for c in all_configs(5) if (v := eval_source(PATH5, c)) is not None) == 2, "source optimum 2")
def no_example(a, reduce_fn, extract_fn):
S = "S9 NO example"
t = reduce_fn(PATH5)
# Claim: every admitted input / constructed target is feasible by select-all.
a.check(S, len(t["sets"]) == 5 and core.covers(t, [True] * 5) and core.is_dominating(PATH5, [True] * 5),
"select-all")
bound = 1
cands = [c for c in all_configs(5) if sum(PATH5["weights"][i] for i in range(5) if c[i]) <= bound]
a.check(S, sorted(tuple(i for i in range(5) if c[i]) for c in cands) == [(), (1,), (3,)], "cost<=1 candidates")
unions = {tuple(i for i in range(5) if c[i]):
sorted(set().union(*[set(t["sets"][i]) for i in range(5) if c[i]])) for c in cands}
a.check(S, unions == {(): [], (1,): [0, 1, 2], (3,): [2, 3, 4]}, f"unions {unions}")
for c in all_configs(5):
tv, sv = eval_target(t, c), eval_source(PATH5, c)
a.check(S, not (tv is not None and tv <= bound), f"target YES at {c}")
a.check(S, not (sv is not None and sv <= bound), f"source YES at {c}")
# Unbounded instances stay feasible with common optimum 2.
tf = [v for c in all_configs(5) if (v := eval_target(t, c)) is not None]
a.check(S, min(tf) == 2, "unbounded optimum 2")
def special_cases(a, reduce_fn, extract_fn):
S = "S10 special cases"
def _b0():
# Empty graph.
e = {"num_vertices": 0, "edges": [], "weights": []}
t = reduce_fn(e)
a.check(S, t == {"universe_size": 0, "sets": [], "weights": []}, f"empty -> {t}")
a.check(S, eval_target(t, []) == 0 and eval_source(e, []) == 0, "empty cost 0")
a.check(S, extract_fn(t, []) == [], "empty extraction")
def _b1():
# Single isolated vertex, weight -5.
s1 = {"num_vertices": 1, "edges": [], "weights": [-5]}
t = reduce_fn(s1)
a.check(S, [sorted(x) for x in t["sets"]] == [[0]], "D_0={0}")
opts = [c for c in all_configs(1) if eval_target(t, c) is not None]
a.check(S, opts == [[True]] and eval_target(t, [True]) == -5, "isolated -5 unique witness")
def _b2():
# Three isolated vertices (0,-5,2) force (1,1,1), cost -3.
s3 = {"num_vertices": 3, "edges": [], "weights": [0, -5, 2]}
t = reduce_fn(s3)
feas = [c for c in all_configs(3) if eval_target(t, c) is not None]
a.check(S, feas == [[True] * 3] and eval_target(t, [True] * 3) == -3, f"three isolated: {feas}")
a.check(S, [sorted(x) for x in t["sets"]] == [[0], [1], [2]], "isolated D_v={v}")
def _b3():
# Triangle with (-5,0,2): three equal indexed subsets, optimum -5 at {0} and {0,1}.
tri = {"num_vertices": 3, "edges": [[0, 1], [1, 2], [0, 2]], "weights": [-5, 0, 2]}
t = reduce_fn(tri)
a.check(S, len(t["sets"]) == 3 and all(sorted(x) == [0, 1, 2] for x in t["sets"]), "three equal subsets kept")
a.check(S, t["weights"] == [-5, 0, 2], "triangle weights not merged")
vals = {tuple(i for i in range(3) if c[i]): eval_target(t, c) for c in all_configs(3)}
best = min(v for v in vals.values() if v is not None)
a.check(S, best == -5, f"triangle optimum {best}")
a.check(S, sorted(k for k, v in vals.items() if v == best) == [(0,), (0, 1)], "triangle optimal witnesses")
for k in ((0,), (0, 1)):
a.check(S, eval_source(tri, extract_fn(t, sel(3, k))) == -5, f"triangle extract {k}")
def _b4():
# i64 extremes on a 3-vertex path.
p3 = [[0, 1], [1, 2]]
ex = {"num_vertices": 3, "edges": p3, "weights": [I64_MIN, 0, I64_MAX]}
t = reduce_fn(ex)
a.check(S, t["weights"] == [I64_MIN, 0, I64_MAX], "extreme weights copied")
a.check(S, eval_target(t, [True] * 3) == -1 == eval_source(ex, [True] * 3), "extremes sum -1")
for w in ([I64_MAX, 1, -1], [I64_MIN, -1, 1]):
inst = {"num_vertices": 3, "edges": p3, "weights": w}
t = reduce_fn(inst)
a.check(S, outcome(eval_target, t, [True] * 3) == ("err", "overflow") == outcome(eval_source, inst, [True] * 3),
f"overflow before cancellation {w}")
a.check(S, sum(w) in range(I64_MIN, I64_MAX + 1), "final sum representable")
try:
extract_fn(t, [True] * 3)
a.check(S, False, f"overflowing witness extracted {w}")
except ExtractionError:
a.check(S, True)
def _b5():
# Infeasible configurations return None before summation, even with
# weights whose sum would overflow.
inst = {"num_vertices": 3, "edges": [], "weights": [I64_MAX, I64_MAX, 0]}
t = reduce_fn(inst)
a.check(S, outcome(eval_target, t, [True, True, False]) == ("val", None) == outcome(eval_source, inst, [True, True, False]),
"infeasible before summation")
def _b6():
# Rejection of non-simple inputs (the rule never receives them).
for bad in ({"num_vertices": 2, "edges": [[0, 0]], "weights": [1, 1]},
{"num_vertices": 2, "edges": [[0, 1], [1, 0]], "weights": [1, 1]},
{"num_vertices": 2, "edges": [[0, 2]], "weights": [1, 1]}):
try:
validate_source(bad)
a.check(S, False, f"admitted {bad}")
except ValueError:
a.check(S, True)
def _b7():
# Deterministic ordering: sets in vertex order, independent of edge order
# and orientation in the input.
rnd = random.Random(1095)
for _ in range(200):
n = rnd.randint(1, 7)
edges = [list(p) for p in itertools.combinations(range(n), 2) if rnd.random() < 0.4]
w = [rnd.randint(-9, 9) for _ in range(n)]
sh = [list(reversed(e)) if rnd.random() < 0.5 else e for e in edges]
rnd.shuffle(sh)
t1 = core.canonical_target(reduce_fn({"num_vertices": n, "edges": edges, "weights": w}))
t2 = core.canonical_target(reduce_fn({"num_vertices": n, "edges": sh, "weights": w}))
a.check(S, t1 == t2, f"edge order changes target: {edges} vs {sh}")
for blk in (_b0, _b1, _b2, _b3, _b4, _b5, _b6, _b7):
try:
blk()
except Exception as e: # each special case fails independently
a.check(S, False, f"{blk.__name__} raised {e!r}")
# --------------------------------------------------------------------------
# Hypothesis strategies aimed at the special cases.
# --------------------------------------------------------------------------
def hypothesis_section(a, reduce_fn, extract_fn, quick=False):
from hypothesis import HealthCheck, given, seed, settings
from hypothesis import strategies as st
S = "S11 hypothesis"
N = 60 if quick else 400
cfg = settings(max_examples=N, deadline=None, database=None, derandomize=False,
suppress_health_check=list(HealthCheck))
def run_one(src):
sub = Audit()
check_instance(sub, src, reduce_fn, extract_fn)
c, f = sub.total()
a.checks[S] += c
a.fails[S] += f
for sec in SECTIONS:
for ex in sub.examples[sec]:
if len(a.examples[S]) < 3:
a.examples[S].append(f"[{sec}] {ex}")
@st.composite
def twins_and_isolates(draw):
"""Isolated vertices, cliques (equal closed neighbourhoods), stars and
open-twin pairs, glued by a few random edges, randomly relabelled."""
blocks = draw(st.lists(st.sampled_from(["iso", "clique", "star", "twins"]), min_size=1, max_size=4))
n, edges = 0, set()
for b in blocks:
k = {"iso": 1, "clique": draw(st.integers(2, 3)), "star": draw(st.integers(2, 3)), "twins": 3}[b]
if n + k > 8:
break
vs = list(range(n, n + k))
if b == "clique":
edges |= {(u, v) for u, v in itertools.combinations(vs, 2)}
elif b == "star":
edges |= {(vs[0], v) for v in vs[1:]}
elif b == "twins": # vs[1], vs[2] share open neighbourhood {vs[0]}
edges |= {(vs[0], vs[1]), (vs[0], vs[2])}
n += k
if n >= 2:
extra = draw(st.lists(st.tuples(st.integers(0, n - 1), st.integers(0, n - 1)), max_size=2))
edges |= {(min(u, v), max(u, v)) for u, v in extra if u != v}
perm = draw(st.permutations(list(range(n))))
edges = sorted({tuple(sorted((perm[u], perm[v]))) for u, v in edges})
w = draw(st.lists(st.integers(-3, 3), min_size=n, max_size=n))
return {"num_vertices": n, "edges": [list(e) for e in edges], "weights": w}
extreme = st.sampled_from([I64_MIN, I64_MIN + 1, -(2**62), -1, 0, 1, 2**62, I64_MAX - 1, I64_MAX])
@st.composite
def boundary_weights(draw):
"""Arbitrary graphs with i64-boundary and full-range weights, aimed at
overflow parity and overflow-before-cancellation."""
n = draw(st.integers(0, 7))
pairs = list(itertools.combinations(range(n), 2))
edges = [list(p) for p in pairs if draw(st.booleans())]
w = draw(st.lists(st.one_of(extreme, st.integers(I64_MIN, I64_MAX)), min_size=n, max_size=n))
return {"num_vertices": n, "edges": edges, "weights": w}
@st.composite
def disjoint_unions(draw):
"""Disconnected unions of paths, cycles, complete graphs and edgeless
parts, zero/negative weights (redundant selections can be optimal)."""
parts = draw(st.lists(st.tuples(st.sampled_from(["path", "cycle", "complete", "empty"]),
st.integers(1, 4)), min_size=1, max_size=3))
n, edges = 0, []
for kind, k in parts:
if n + k > 8:
break
vs = list(range(n, n + k))
if kind in ("path", "cycle"):
edges += [[vs[i], vs[i + 1]] for i in range(k - 1)]
if kind == "cycle" and k >= 3:
edges.append([vs[0], vs[-1]])
elif kind == "complete":
edges += [list(p) for p in itertools.combinations(vs, 2)]
n += k
w = draw(st.lists(st.sampled_from([-2, -1, 0, 0, 1]), min_size=n, max_size=n))
return {"num_vertices": n, "edges": edges, "weights": w}
for strat, sd in ((twins_and_isolates(), 41), (boundary_weights(), 42), (disjoint_unions(), 43)):
@seed(sd)
@cfg
@given(strat)
def prop(src):
run_one(src)
prop()
def run(reduce_fn=core.reduce, extract_fn=core.extract, quick=False, hypo=True, out=sys.stdout):
a = Audit()
exhaustive(a, reduce_fn, extract_fn, quick=quick)
for fn in (yes_example, no_example, special_cases):
try:
fn(a, reduce_fn, extract_fn)
except Exception as e: # an exception in a worked example is a failure
sec = {"yes_example": "S8 YES example", "no_example": "S9 NO example",
"special_cases": "S10 special cases"}[fn.__name__]
a.check(sec, False, f"raised {e!r}")
if hypo:
hypothesis_section(a, reduce_fn, extract_fn, quick=quick)
return a
CLAIMS = """
Claim (the proof) -> section
universe_size = num_vertices; num_sets = num_vertices -> S1, S8, S10 (n=0)
membership count n + 2m -> S1, S8
D_v = N[v], members once, vertex order, weights copied, -> S2, S10
equal subsets kept, elements in universe, v in D_v
select-all covers / every input unboundedly feasible -> S2, S6, S9
forward implication (dominating => covering) -> S3
backward implication (covering => dominating) -> S4
identical costs; overflow errors at the same index; None first -> S5, S10, S11(boundary)
optimum and all optimal configurations agree, signed weights -> S6
extraction: once-evaluated, rejects None/overflow/bad length -> S7, S10
YES example numbers, uniqueness, {0,3},{1,4} cost 4 -> S8
NO example (bound 1) both sides, candidate unions -> S9
empty / isolated / triangle / i64 extremes / non-simple rejected -> S10
target independent of edge order/orientation -> S10
Untestable here: allocation limits; Rust integration (cross_compare.py covers pred).
"""
if __name__ == "__main__":
quick = "--quick" in sys.argv
a = run(quick=quick)
print("Adversary harness: MinimumDominatingSet/SimpleGraph/i64 -> MinimumSetCovering/i64")
a.report()
print(CLAIMS)
c, f = a.total()
sys.exit(1 if f or c < 5000 else 0)Proof#set page(margin: 22mm)
#set text(size: 10pt)
#set heading(numbering: "1.")
= Closed neighbourhoods: weighted domination to weighted covering
*Theorem.* For every admitted instance of
`MinimumDominatingSet<SimpleGraph, i64>`, the construction below produces an
admitted `MinimumSetCovering<i64>` instance. The two binary configuration spaces
are in bijection, with equivalent feasibility and identical mathematical costs.
Consequently their mathematical minimum costs and all optimal configurations
agree. Their library evaluations agree as values or as arithmetic failures.
Extraction of a target witness whose evaluation succeeds returns a source
witness with the same value. No restriction on the signs of weights is needed.
== Provenance and endpoint gate
The unweighted construction and both implications are stated in
#link("https://people.cs.umass.edu/~marius/class/cs311-fa18/midterm2-sol.pdf")[
UMass COMPSCI 311, Second Midterm Exam solutions, 14 November 2018,
Problem 8(a), PDF page 5]. The signed weighted extension and the error-parity
argument are *derived here*. Garey and Johnson, _Computers and Intractability_
(W. H. Freeman, 1979), Appendix A, DOMINATING SET (GT2, printed page 190)
and MINIMUM COVER (SP5, printed page 222), support the problem definitions,
rather than this construction or its signed extension. The library already
records the book as `garey1979` in `docs/paper/references.bib`.
Before deriving the weighted proof, the sibling
`src/rules/minimumdominatingset_ilp.rs` was checked: its constraint for vertex
$v$ contains $v$ and all its neighbours. The sibling
`src/rules/minimumvertexcover_minimumsetcovering.rs` uses an indexed family
of target sets, copies vertex weights in vertex order, and copies the witness
back. Here the universe contains vertices, whereas that sibling uses edges.
Equal subsets remain different indexed choices; neither their indices nor
their costs may be merged.
The type-resolution chain on library revision `e7bacb37` is:
- Source: `src/models/graph/minimum_dominating_set.rs`,
`impl<G, W> Problem for MinimumDominatingSet<G, W>` declares
`Solution = Vec<bool>` and `Value = Min<W::Sum>`.
- Target: `src/models/set/minimum_set_covering.rs`,
`impl<W> Problem for MinimumSetCovering<W>` declares
`Solution = Vec<bool>` and `Value = Min<W::Sum>`.
- In both substitutions $W =$ `i64`.
`src/types.rs`, `impl WeightElement for i64`, declares `Sum = i64`.
Both concrete values therefore resolve to `Min<i64>`.
- `WeightElement::to_sum` is the identity for `i64`;
`checked_add_to_sum` delegates to checked integer addition.
`Min<V>` stores `Option<V>`: `None` is infeasibility, distinct from an
`EvaluationError` returned by failed evaluation.
*Full-domain compatibility: PASS.* No objective conversion is required.
Construction copies weights, including the two signed endpoints; it performs
no weight arithmetic. Both `evaluate` methods reject a vector of the wrong
length, test feasibility first, then add selected weights in increasing index
order, returning an integer-overflow error if a partial sum is outside `i64`.
Descriptions of the error context can differ, but the error class agrees.
The admitted source is a finite simple undirected graph with vertex indices in
range and exactly one `i64` weight per vertex. Constructors allow empty graphs,
isolated vertices, disconnected graphs, and arbitrary signed weights.
`src/topology/graph.rs`, `validate_simple_connections`, `SimpleGraph::try_new`,
and its deserializer reject self-loops, repeated undirected edges (including a
reversed duplicate), and out-of-range endpoints. The target constructor requires
one weight per indexed set and all elements in the universe; it permits empty
sets and equal sets. `Problem::evaluate`, rather than the looser convenience
predicates, specifies the witness-length contract used here.
*Redundancy gate: PASS (novel).* On 3 November 2026, after
`cargo build -p problemreductions-cli --bin pred`, the commands
`pred show MinimumDominatingSet/SimpleGraph/i64 --json` and
`pred show MinimumSetCovering/i64 --json` resolved the endpoints, and
`pred path MinimumDominatingSet/SimpleGraph/i64 MinimumSetCovering/i64 --limit all`
returned exit 1 with “No reduction path”. There is no existing path whose
overhead can dominate the proposed edge.
== Construction
Let $n$ be the number of vertices, $V = {0, ..., n-1}$ (empty when $n=0$),
$E$ the set of unordered edges, $m = |E|$, and
$w = (w_0, ..., w_(n-1))$ the signed vertex weights.
For $v in V$, let $N(v) = {u in V : {u,v} in E}$ and
$N[v] = {v} union N(v)$. A configuration $x$ has one Boolean entry $x_v$
per vertex, and $S(x) = {v in V : x_v = 1}$.
+ Set the target universe to $U = V$, represented by `universe_size = n`.
+ For each $v$ in increasing vertex order, create the indexed subset
$D_v = N[v]$. Store each member once. Within-set element order has no semantic
meaning; the script sorts members to give canonical output.
+ Assign target weight $c_v = w_v$ to $D_v$. Keep all $n$ indexed subsets even
when two of them have the same members.
+ Use the same configuration $y=x$: selecting $D_v$ represents selecting $v$.
Every member of every $D_v$ belongs to $U$. There are exactly $n$ subsets and
$n$ weights. These facts establish the target constructor's constraints for
all admitted sources. Also $v in D_v$, so selecting all target sets covers $U$.
== Overhead
#table(
columns: (1.5fr, 1.2fr, 2.8fr),
[Target parameter], [Exact formula], [Derivation],
[`universe_size`], [`num_vertices`], [$U=V$, including $n=0$.],
[`num_sets`], [`num_vertices`], [One indexed set for each vertex; no rows omitted.],
)
There are no branches, coefficient normalizations, or eliminated duplicate
rows that change either count. The two formulas copy a source count; they do
not multiply it or convert a signed value. The diagnostic total membership
count is $sum_(v in V) |D_v| = n + sum_(v in V) |N(v)| = n + 2m$,
because a simple undirected edge contributes once at each endpoint. This
membership count is not a registered target parameter. Adjacency-based
construction takes $O(n+m)$ storage and expected $O(n+m)$ time before optional
sorting; sorting each neighbourhood still gives polynomial time. Python's
unbounded size arithmetic does not establish Rust allocation or index limits;
derived-size boundaries must be checked when implementation begins.
== Correctness
*(Forward implication.)* Suppose $x$ is a dominating source configuration.
Fix any $u in U$. Domination says either $u in S(x)$, in which case
$u in D_u$, or some selected vertex $v$ is adjacent to $u$, in which case
$u in D_v$. In either case a selected target set contains $u$.
This argument holds for every $u$, hence $y=x$ covers $U$.
*(Backward implication.)* Suppose $y$ covers $U$ and define $x=y$.
Fix any source vertex $u$. Coverage supplies an index $v$ with $y_v=1$
and $u in D_v$. The definition of $D_v$ gives either $u=v$ or an edge
${u,v} in E$. Thus $u$ is itself selected or adjacent to a selected vertex.
Every source vertex is dominated.
For any corresponding feasible configurations, the mathematical costs are
$sum_(v in S(x)) w_v = sum_(v : y_v=1) c_v$ term by term.
The inverse maps $x mapsto x$ and $y mapsto y$ form a bijection between
feasible configurations. A cheaper source configuration than an extracted
target optimum would yield a cheaper target cover by the forward implication;
a cheaper target configuration than a source optimum would yield a cheaper
source dominating set by the backward implication. Both contradict optimality.
The argument applies to all optimal target configurations and uses no
nonnegativity or minimal-by-inclusion assumption.
For the executable models, induction over the selected indices proves that
the running totals on both sides are equal before every checked addition.
The next added integer is identical; hence either both additions succeed with
the same result or both fail at that index. Infeasible configurations return
`Min(None)` before summation on both sides. Mathematical sums outside `i64`,
and intermediate overflow before later cancellation, remain evaluation errors;
they are not clamped or treated as infeasible. A library solve that encounters
such an error is not claimed to return a mathematical optimum. When all
evaluations succeed, the library's optimum and every optimal witness agree.
Identity on already returned `Min<i64>` values is a total value map.
== Solution extraction
Evaluate the target witness once, propagating evaluation errors and rejecting
`Min(None)` and malformed lengths. For a successful feasible target witness
$y$, return a copy of its Boolean vector $x=y$. No index conversion, weight
conversion, or reordering is involved. The backward implication proves source
feasibility; the cost and checked-addition arguments prove the same value.
In particular this holds for every successfully evaluated optimal target
witness. Extraction uses $O(n)$ space to copy the vector, plus validation time.
== YES example
Take the five-vertex path with
$E = {{0,1}, {1,2}, {2,3}, {3,4}}$ and weights $(3,1,4,1,3)$.
Its fully constructed target has universe ${0,1,2,3,4}$ and:
#table(
columns: (1fr, 2fr, 1fr),
[Index], [Subset], [Weight],
[0], [${0,1}$], [3],
[1], [${0,1,2}$], [1],
[2], [${1,2,3}$], [4],
[3], [${2,3,4}$], [1],
[4], [${3,4}$], [3],
)
Both target parameters are 5 and its total membership count is
$2+3+3+3+2=13=5+2 dot 4$.
For bound 2, $y=(0,1,0,1,0)$ selects $D_1$ and $D_3$;
their union is the entire universe and cost is $1+1=2$.
Extraction selects source vertices ${1,3}$: vertex 1 dominates 0,1,2 and
vertex 3 dominates 2,3,4, at the same cost 2.
All weights are positive. The only configurations of cost below 2 are
the empty choice and the two individual cost-1 choices; none covers the
universe. The pair ${1,3}$ is the unique configuration of cost exactly 2.
Thus the common optimum is 2 and the displayed witness is its unique optimum.
The choices ${D_0,D_3}$ and ${D_1,D_4}$ each cover the universe at cost
$3+1=4$ and extract to the source choices ${0,3}$ and ${1,4}$ at cost 4.
The all-false configuration covers nothing and is infeasible on both sides.
== NO example
Use the same five-vertex graph, all five subsets and all five weights listed
above, now with bound 1. A candidate of cost at most 1 can only be
$emptyset$, ${1}$, or ${3}$, since every other single weight is at least 3
and two positive weights cost at least 2. Their target unions are respectively
$emptyset$, ${0,1,2}$, and ${2,3,4}$. Each misses a universe element.
On the source side these choices dominate respectively no vertices, only
0,1,2, and only 2,3,4. Neither instance admits a witness of cost at most 1;
both bounded questions are NO. The unbounded optimization instances remain
feasible, with common optimum 2. In fact every admitted dominating-set input
and every constructed target is unboundedly feasible by selecting everything;
an unboundedly infeasible example in this image cannot exist.
== Special cases and executable claim coverage
- Empty graph: $n=m=0$ produces universe size 0, zero sets and zero weights.
The empty vector is feasible on both sides with cost 0. Sections 2--5 of
`constructor.py` enumerate this case; its hand-derived result is also tested.
- Isolated vertices: $D_v={v}$ for an isolated $v$; no other set contains $v$,
so every cover and every dominating set must select it. A single isolated
vertex of weight $-5$ has unique witness $(1)$, cost $-5$; three isolated
vertices with weights $(0,-5,2)$ force $(1,1,1)$, cost $-3$.
- Disconnected graphs need no component assumption. Zero and negative costs
may make redundant selections optimal, so no removal of redundant sets is
allowed. A triangle produces three equal indexed subsets; with weights
$(-5,0,2)$ its optimum is $-5$, attained by selecting vertex 0 with or
without vertex 1. Sections 2, 3, and 5 exercise these cases.
- For i64 extremes, a three-vertex path with weights
$(-2^63,0,2^63-1)$ and all vertices selected has cost $-1$ on both sides.
With $(2^63-1,1,-1)$ or $(-2^63,-1,1)$, checked accumulation fails before
cancellation on both sides, despite a representable final mathematical sum.
Section 2 checks independently specified outcomes and section 3 checks that
failed target evaluation cannot be extracted as a valid witness.
- Self-loops and parallel edges are not admitted by this `SimpleGraph`.
Mathematically, treating a neighbourhood as a set would remove repeated
incidences without changing coverage, but no claim is made that this rule
receives such inputs. Real CLI constructor probes separately check rejection.
- Equal neighbourhoods are kept in vertex order. Within-set permutations
are the only allowed representation difference for later cross-comparison;
canonical sorting makes the Python representation deterministic.
The seven script sections cover: (1) SymPy cardinality identities for both
overhead formulas tied to measured constructed targets; (2) both feasibility
directions, identical evaluated costs/errors, and optimum equality;
(3) every feasible target witness, every optimal witness, invalid covers and
wrong lengths; (4) both exact target sizes and the membership identity;
(5) target domain constraints, copied weights, and self-coverage;
(6) all YES numbers; and (7) exhaustive NO-bound infeasibility on both sides.
Enumeration covers every labelled simple graph through five vertices and
every weight vector over $(-1,0,1)$, exceeding the four-vertex validation plan.
It also checks empty/complete/path families at six vertices. Two seeded
Hypothesis strategies cover arbitrary graphs and graphs with isolated vertices
and equal neighbourhoods, with full-range i64 weights, up to seven vertices,
300 examples each, seeds 1729 and 2718, no example database or deadline.
Finite tests do not prove arbitrary-size identities or all i64 combinations;
the preceding universal arguments do. Allocation failure and Rust reduction
integration are outside this construction verification. Independent adversary
verification and cross-comparison remain subsequent work.
|
Collaborator
Author
Review ReportVerdict: approve. Subject: rule Structural and semantic
Quality
Feature testRun with
FindingsNo open findings.
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1230 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151821 +263
========================================
+ Hits 147308 147575 +267
+ 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.
Adds a direct weighted reduction from MinimumDominatingSet on simple graphs to MinimumSetCovering. Each vertex becomes its closed-neighborhood set with the same weight, and a covering witness maps back to the same vertex selection.
Includes a worked example, paper entry, exhaustive small-graph tests, and boundary and extraction tests. The current models use
i64weights;SimpleGraphrejects loops and repeated edges.Fixes #1095