Repository navigation
Conversation
Each vertex becomes a Boolean variable and each edge (u, v) the clauses (x_u OR x_v) and (NOT x_u OR NOT x_v), so every assignment satisfies exactly m + cut clauses (Gramm, Hirsch, Niedermeier, Rossmanith 2003). Extraction returns the assignment unchanged. Includes unit tests, the canonical example (4-cycle plus a diagonal) and the paper entry with the gramm2003 citation. Fixes #1102 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED. The construction was checked by two independently written scripts (a constructor and an adversary that saw only the proof), cross-compared on shared instances, and the Rust rule was compared target-for-target against both. Type resolutionRedundancy: Source checked: Gramm, Hirsch, Niedermeier, Rossmanith, ECCC TR00-037, Section 5 (p. 10) and Corollary 2 (p. 12): each edge of weight w becomes Constructor: 2,280,976 checks, 0 failures
Instances: every simple graph with n ≤ 5 and every configuration; every simple graph with n = 6 (32,768 graphs × 64 configurations, via edge bitmasks); every edge multiset with loops/parallel edges for n ≤ 3 (mathematical extension only: Adversary: 897,287 checks, 0 failures
Instances: all 1,100 simple graphs for n = 0..5 with every configuration; edge multisets with loops/multiplicity for n = 1..3, m = 1..4; all 32,768 six-vertex simple graphs on all-zero, all-one and alternating configurations. Hypothesis 6.155.7: 2 strategies (arbitrary ordered edge lists on up to 8 vertices and 30 edges; two disconnected blocks with a forced repeated self-loop), 400 examples each, seeds 846703 and 846704, The adversary found one wording error in an earlier draft of the proof (it claimed Cross-comparison
Targets are compared for exact equality; no isomorphism or reordering is used. The remaining 239 shared instances contain loops or parallel edges and are compared between the scripts only. Typst proof#set page(width: 18cm, height: auto, margin: 1.5cm)
#set text(size: 10.5pt)
#set heading(numbering: "1.")
= MaxCut/SimpleGraph/One $arrow.r$ Maximum2Satisfiability
*Source.* Gramm, Hirsch, Niedermeier, Rossmanith, "Worst-case upper bounds for MAX-2-SAT with an
application to MAX-CUT", _Discrete Applied Mathematics_ 130(2):139--155, 2003,
DOI 10.1016/S0166-218X(02)00402-X; preprint ECCC TR00-037, Section 5 "Application to MAX-CUT"
(p. 10) and Corollary 2 (p. 12). Section 5 translates a graph $G=(V,E)$ into the 2-CNF formula with the
vertices as variables and, for each edge $(i,j)$ of weight $w$, the two clauses $(w,{i,j})$ and
$(w,{overline(i),overline(j)})$, and states that $G$ has a cut of weight $k$ iff the formula has
simultaneously satisfiable clauses of weight $M+k$, $M$ the total edge weight; every optimal
assignment translates into a maximum cut. The construction below is that one with all weights 1 (the
paper credits the reduction to Poljak and Tuza). Shen and Zhang, "Improving Exact Algorithms for
MAX-2-SAT" (DOI 10.1007/s10472-005-7036-z), Theorem 5.1, is reported to state the unit-weight case.
*Type resolution.* Source `MaxCut<SimpleGraph, One>`: `Value = Max<W::Sum>` with `W = One` and
`<One as WeightElement>::Sum = i64` (`src/types.rs`), so `Max<i64>`. Target `Maximum2Satisfiability`:
`Value = Max<i64>` (`src/models/formula/maximum_2_satisfiability.rs`). `Max<i64> -> Max<i64>`:
witness-compatible. *Redundancy:* `pred path MaxCut/SimpleGraph/One Maximum2Satisfiability` reports no
path, so the edge is novel (PASS).
== Definitions
A source instance is a graph $G=(V,E)$ with $V={0,dots,n-1}$ and an edge list
$E=(e_0,dots,e_(m-1))$, $e_j=(u_j,v_j)$ with $u_j,v_j in V$. A configuration is
$x in {0,1}^n$ and its value is $"cut"(x) = |{j : x_(u_j) != x_(v_j)}|$, counted over list positions.
The library's `SimpleGraph` rejects self-loops ($u_j=v_j$) and repeated pairs; the statements below are
proved for arbitrary lists, so they hold on that domain and on multigraphs alike.
A target instance is a number of variables $N$ and a list of clauses, each a list of two nonzero
integer literals $ell$ with $|ell| <= N$. Literal $ell > 0$ is true under $y in {0,1}^N$ iff
$y_(ell-1)=1$; literal $ell<0$ is true iff $y_(-ell-1)=0$. A clause is satisfied iff some literal in it
is true, and the value of $y$ is $"sat"(y)$, the number of satisfied clauses. Both problems maximize.
#strong[Theorem.] _For every source instance $G$ with $m$ edges, the instance $phi(G)$ built below
satisfies $"sat"(x) = m + "cut"(x)$ for every $x in {0,1}^n$. Hence for every integer $k$, $G$ has a cut
of value $>= k$ iff $phi(G)$ has an assignment satisfying $>= m+k$ clauses, the optima satisfy
$"OPT"(phi(G)) = m + "OPT"(G)$, and the identity map sends optimal assignments to maximum cuts._
== Construction
+ Set $N = n$: variable $x_v$ (library index $v$, literal $v+1$) stands for vertex $v$; $x_v = 1$
places $v$ on side 1 of the cut, $x_v=0$ on side 0.
+ For each position $j = 0, dots, m-1$ of the edge list, with $e_j=(u_j,v_j)$, append in this order the
clauses $P_j = (x_(u_j) or x_(v_j))$, encoded $[u_j+1, v_j+1]$, and
$Q_j = (not x_(u_j) or not x_(v_j))$, encoded $[-(u_j+1), -(v_j+1)]$.
+ No other clause is created. A self-loop $u_j=v_j$ yields the repeated-literal clauses
$[u_j+1,u_j+1]$ and $[-(u_j+1),-(u_j+1)]$; a repeated pair yields a repeated clause pair, kept with its
multiplicity because the clauses form a list.
Every literal has magnitude $u_j+1 <= n = N$ and is nonzero, and every clause has two literals, so
$phi(G)$ is accepted by `Maximum2Satisfiability::try_new`.
== Overhead
#table(
columns: 2,
[*Target parameter*], [*Formula*],
[`num_vars`], [`num_vertices`],
[`num_clauses`], [`2 * num_edges`],
)
Step 1 creates one variable per vertex; step 2 creates exactly two clauses per edge-list position with
no branch, no omitted clause and no merging of duplicates, so both formulas are exact.
== Correctness
*Lemma (one edge).* For each $j$ and each $x$, the number of satisfied clauses among $P_j, Q_j$ equals
$1 + [x_(u_j) != x_(v_j)]$.
_Proof._ Write $a = x_(u_j)$, $b = x_(v_j)$. If $a != b$, one of $a,b$ is 1, so $P_j$ holds, and one of
them is 0, so $Q_j$ holds: two clauses, $= 1+1$. If $a = b = 1$, $P_j$ holds and both literals of
$Q_j$ are false: one clause. If $a=b=0$, $P_j$ fails and $Q_j$ holds: one clause. In both equal cases
the count is $1 = 1+0$. A self-loop always has $a=b$ and falls in the equal cases. $square$
*Identity.* Each clause of $phi(G)$ belongs to exactly one pair $(P_j,Q_j)$, so summing the lemma over
$j$ gives $"sat"(x) = sum_j (1 + [x_(u_j) != x_(v_j)]) = m + "cut"(x)$ for every $x in {0,1}^n$.
*($arrow.r.double$) Source YES gives target YES.* Let $x$ be a configuration with $"cut"(x) >= k$. Take
the target assignment $y = x$ (same length $n = N$). By the identity, $"sat"(y) = m + "cut"(x) >= m+k$,
so $phi(G)$ has an assignment satisfying at least $m+k$ clauses.
*($arrow.l.double$) Target YES gives source YES.* Let $y in {0,1}^N$ satisfy at least $m+k$ clauses of
$phi(G)$. Define the configuration $x$ by $x_v = y_v$ for $v in V$, which is well defined because
$N = n$. By the identity applied to $x$, $"cut"(x) = "sat"(y) - m >= (m+k) - m = k$, so $G$ has a cut of
value at least $k$.
*Optima.* The map $x |-> x$ is a bijection between source configurations and target assignments, and
by the identity it adds the constant $m$ to the value. A strictly increasing shift preserves the
argmax: $"OPT"(phi(G)) = m + "OPT"(G)$, and $y$ is optimal for $phi(G)$ iff $y$, read as a
configuration, is a maximum cut.
== Solution extraction
Given a target assignment $y$ of length $N = n$, return the configuration $x$ with $x_v = y_v$,
position for position (`true` $|->$ side 1). Its value is $"cut"(x) = "sat"(y) - m$; if $y$ is optimal,
$x$ is a maximum cut by the paragraph above. An assignment of any other length is not a target
solution and is rejected, as both `evaluate` functions reject wrong lengths.
== Special cases
- *Empty graph* ($n=m=0$): $N=0$, no clauses; the empty assignment has value $0 = 0+0$ and extracts to
the empty configuration.
- *Isolated vertices*: a vertex $w$ in no edge gets a variable $x_w$ occurring in no clause, and $w$
is an endpoint of no edge, so changing $x_w$ alone changes neither $"sat"$ nor $"cut"$. Both values
need not be zero: with $n=3$, $E=((0,1))$ and $x=(0,1,0)$, $"cut"=1$ and $"sat"=2=1+1$. Each value of
$x_w$ extracts to a valid position.
- *Edgeless graphs* ($m=0$, $n >= 1$): $phi(G)$ has $n$ variables and no clause, so every assignment
has $"sat"=0="cut"=0+0$.
- *Disconnected graphs*: clauses of distinct components share no variable, and both values are sums
over edge positions, so the identity holds component by component and adds up; no connectivity is
used anywhere in the proof.
- *Self-loops*: contribute exactly one satisfied clause and never cross the cut (lemma, equal case).
- *Parallel edges*: each occurrence is its own position $j$ with its own pair; it contributes
$1+[x_u != x_v]$ once per occurrence, matching the source, which also counts per position.
`SimpleGraph::try_new` (and deserialization, which calls it) rejects the last two cases, so the
library rule never meets them; the construction stays correct if the source domain admits them.
== YES example
Source: $n=4$, $E = (0,1),(1,2),(2,3),(3,0),(0,2)$ (the 4-cycle plus the diagonal $0 2$), $m=5$.
Target: $N=4$ and the ten clauses, in order,
$[1,2],[-1,-2],[2,3],[-2,-3],[3,4],[-3,-4],[4,1],[-4,-1],[1,3],[-1,-3]$, i.e.
$(x_0 or x_1)$, $(not x_0 or not x_1)$, $(x_1 or x_2)$, $(not x_1 or not x_2)$, $(x_2 or x_3)$,
$(not x_2 or not x_3)$, $(x_3 or x_0)$, $(not x_3 or not x_0)$, $(x_0 or x_2)$, $(not x_0 or not x_2)$.
Witness $x = y = (0,1,0,1)$. The cycle edges $01, 12, 23, 30$ cross, the diagonal $02$ does not:
$"cut"(x) = 4$. Per edge the satisfied counts are $2,2,2,2,1$, so $"sat"(y) = 9 = 5+4$.
All on one side, $x=(0,0,0,0)$: $"cut" = 0$ and $"sat"=5 = m$ (every $Q_j$ holds, every $P_j$ fails).
Over all 16 configurations the cut values are $0$ (twice: one side empty), $2$ (four times: vertex 1 or
3 alone), $3$ (eight times: vertex 0 or 2 alone, or the splits ${0,1}|{2,3}$, ${0,3}|{1,2}$) and $4$
(twice: ${0,2}|{1,3}$). Target values are these plus 5: $5,7,8,9$ with the same multiplicities.
So $"OPT"(G)=4$, $"OPT"(phi(G))=9$, the optimal assignments are exactly $(0,1,0,1)$ and $(1,0,1,0)$,
and extraction from either returns a cut of value 4.
== NO example
*Single edge (threshold check).* $n=2$, $E=((0,1))$, $m=1$; clauses $[1,2],[-1,-2]$. A single edge
cuts at most one edge, so no cut has value $>= 2$. The target values are $1,2,2,1$ for
$y = 00,01,10,11$, so its optimum is 2 and the corresponding threshold $m+2=3$ is unattainable. Both
sides are NO, as the theorem requires.
*Triangle (three vertices).* $n=3$, $E=(0,1),(1,2),(0,2)$, $m=3$; clauses
$[1,2],[-1,-2],[2,3],[-2,-3],[1,3],[-1,-3]$. Threshold $k=3$: a cut of value 3 would need all three
edges to cross, i.e. $x_0 != x_1 != x_2 != x_0$ over two values, impossible on an odd cycle; the cut
values are $0$ (twice) and $2$ (six times). For the target threshold $m+k=6$, all six clauses would
need to hold, i.e. both clauses of every pair, which by the lemma requires every edge to cross;
by the same parity argument some edge has equal endpoints and its pair contributes 1. The target values
are $3$ (twice) and $5$ (six times), maximum $5 < 6$. Both sides are NO.
== Evidence
The constructor script checks every claim: Section 1 (symbolic overhead and per-edge polynomial
identity), 2 (pointwise identity and every threshold, exhaustive over all simple graphs with $n <= 6$
and all configurations, all multigraphs with loops/parallel edges for $n <= 3$, two Hypothesis
strategies), 3 (extraction from every assignment and every optimal witness, wrong lengths rejected),
4 (sizes), 5 (literal range, clause length, complementary pairs, special cases), 6 and 7 (both examples,
number for number). Checked arithmetic for $2m$ and $v+1$ on machine integers is left to the Rust unit
tests, since Python integers are unbounded.Constructor script#!/usr/bin/env python3
"""Constructor verification: MaxCut/SimpleGraph/One -> Maximum2Satisfiability.
Construction (Gramm, Hirsch, Niedermeier, Rossmanith 2003, Section 5):
one Boolean variable x_v per vertex v; for every edge occurrence {u, v}, in edge
order, the two clauses [u+1, v+1] and [-(u+1), -(v+1)] (signed, 1-indexed
literals). Extraction copies the assignment position for position.
The scripts mirror the library semantics:
* MaxCut<SimpleGraph, One>::evaluate: length must equal num_vertices, value is
the number of edges (u, v) with config[u] != config[v] (Max<i64>);
* Maximum2Satisfiability::evaluate: length must equal num_vars, value is the
number of clauses with some literal true, literal l > 0 true iff
assignment[l-1], l < 0 true iff not assignment[-l-1] (Max<i64>);
* Maximum2Satisfiability::try_new: num_vars <= i64::MAX, every literal is
nonzero, not i64::MIN, |l| <= num_vars, and every clause has length 2.
* SimpleGraph::try_new rejects self-loops and parallel edges; the
construction is additionally checked on multigraphs (loops, parallel
edges) because the proof claims it for them.
Sections (how-to-verify): 1 symbolic, 2 exhaustive forward/backward,
3 extraction, 4 size vs formula, 5 structure, 6 YES example, 7 NO example.
Ends with the line: TOTAL: <checks> checks, <failures> failures
"""
import itertools
import os
import random
import shutil
import sys
# ---------------------------------------------------------------- environment
os.environ.setdefault("HYPOTHESIS_STORAGE_DIRECTORY",
os.path.join(__import__("tempfile").gettempdir(), "maxcut_m2s_hypothesis"))
try:
import sympy # noqa: F401
import hypothesis # noqa: F401
except ImportError: # re-run in an ephemeral environment that has both
if os.environ.get("MAXCUT_M2S_REEXEC") != "1" and shutil.which("uv"):
os.environ["MAXCUT_M2S_REEXEC"] = "1"
os.execvp("uv", ["uv", "run", "--quiet", "--no-project",
"--with", "sympy==1.14.0", "--with", "hypothesis",
"python", "-I", os.path.abspath(__file__)] + sys.argv[1:])
raise
import sympy as sp
from hypothesis import given, settings, HealthCheck, strategies as st
SEED = 1102
random.seed(SEED)
COUNTS = {}
FAILURES = []
SECTION = None
def section(name):
global SECTION
SECTION = name
COUNTS.setdefault(name, 0)
print(f"--- {name}")
def check(cond, msg):
COUNTS[SECTION] += 1
if not cond:
FAILURES.append(f"[{SECTION}] {msg}")
if len(FAILURES) <= 20:
print("FAIL:", SECTION, msg)
# ---------------------------------------------------------------- models
class EvalError(Exception):
pass
def maxcut_eval(n, edges, config):
"""MaxCut<SimpleGraph, One>::evaluate."""
if len(config) != n:
raise EvalError("cut assignment length does not match the graph vertices")
return sum(1 for (u, v) in edges if config[u] != config[v])
def literal_true(lit, assignment):
var = abs(lit) - 1
value = assignment[var] if var < len(assignment) else False
return value if lit > 0 else not value
def m2s_valid(num_vars, clauses):
"""Maximum2Satisfiability::try_new acceptance."""
if num_vars > 2**63 - 1:
return False
for c in clauses:
for lit in c:
if lit == 0 or lit == -(2**63) or abs(lit) > num_vars:
return False
return all(len(c) == 2 for c in clauses)
def m2s_eval(num_vars, clauses, assignment):
"""Maximum2Satisfiability::evaluate."""
if len(assignment) != num_vars:
raise EvalError("assignment length does not match the formula variables")
return sum(1 for c in clauses if any(literal_true(l, assignment) for l in c))
# ---------------------------------------------------------------- reduction
def reduce(n, edges):
clauses = []
for (u, v) in edges:
clauses.append([u + 1, v + 1])
clauses.append([-(u + 1), -(v + 1)])
return n, clauses
def extract(n, target_config):
if len(target_config) != n:
raise EvalError("target assignment length does not match the source vertices")
return list(target_config)
# ---------------------------------------------------------------- instances
def all_pairs(n):
return list(itertools.combinations(range(n), 2))
def simple_graphs(n):
pairs = all_pairs(n)
for mask in range(1 << len(pairs)):
yield [pairs[i] for i in range(len(pairs)) if mask >> i & 1]
def configs(n):
return [list(bits) for bits in itertools.product([False, True], repeat=n)]
def multigraphs(n, max_edges):
"""All edge multisets (loops and parallel edges allowed) of size <= max_edges,
every ordering-insensitive multiset once, plus a reversed-endpoint variant."""
slots = [(u, v) for u in range(n) for v in range(u, n)]
for k in range(max_edges + 1):
for combo in itertools.combinations_with_replacement(slots, k):
yield list(combo)
yield [(v, u) for (u, v) in combo]
def brute_opt(values):
return max(values) if values else None
# ================================================================ section 1
section("1 symbolic overhead")
n_s, m_s = sp.symbols("num_vertices num_edges", integer=True, nonnegative=True)
i = sp.symbols("i", integer=True)
num_vars_formula = n_s
num_clauses_formula = 2 * m_s
# per-edge clause count summed over the edge list = 2 m
check(sp.simplify(sp.summation(2, (i, 1, m_s)) - num_clauses_formula) == 0,
"sum_{e in E} 2 == 2*num_edges")
# one variable per vertex
check(sp.simplify(sp.summation(1, (i, 1, n_s)) - num_vars_formula) == 0,
"sum_{v in V} 1 == num_vertices")
# per-edge contribution: [a or b] + [not a or not b] == 1 + [a xor b] on {0,1}
a, b = sp.symbols("a b")
pos = a + b - a * b # indicator of (a or b) on 0/1 values
neg = 1 - a * b # indicator of (not a or not b)
xor = a + b - 2 * a * b # indicator of a != b
check(sp.expand(pos + neg - (1 + xor)) == 0, "polynomial identity pos+neg = 1+xor")
for av, bv in itertools.product([0, 1], repeat=2):
check(pos.subs({a: av, b: bv}) == int(av or bv), f"pos indicator at {av},{bv}")
check(neg.subs({a: av, b: bv}) == int((not av) or (not bv)), f"neg indicator at {av},{bv}")
check(xor.subs({a: av, b: bv}) == int(av != bv), f"xor indicator at {av},{bv}")
# boolean-logic form: with a==b exactly one clause holds, with a!=b both hold
A, B = sp.symbols("A B")
check(sp.satisfiable(~((A | B) | (~A | ~B))) is False, "never both clauses false")
check(sp.satisfiable((A | B) & (~A | ~B) & sp.Equivalent(A, B)) is False,
"a == b never satisfies both")
check(sp.satisfiable(sp.Xor(A, B) & ~((A | B) & (~A | ~B))) is False,
"a != b always satisfies both")
# affine map is strictly increasing => maximizers coincide; threshold map k -> m+k
k_s = sp.symbols("k", integer=True)
check(sp.diff(m_s + k_s, k_s) == 1, "d(m+k)/dk = 1 > 0")
# ================================================================ section 2
section("2 exhaustive forward/backward")
EXH = {} # (n, tuple(edges)) -> data, reused by section 3/4/5
for n in range(0, 6):
for edges in simple_graphs(n):
m = len(edges)
tn, cl = reduce(n, edges)
cs = configs(n)
src = [maxcut_eval(n, edges, c) for c in cs]
tgt = [m2s_eval(tn, cl, c) for c in cs]
for c, s, t in zip(cs, src, tgt):
check(t == m + s, f"identity n={n} E={edges} x={c}: sat={t}, m+cut={m + s}")
opt_s, opt_t = brute_opt(src), brute_opt(tgt)
check(opt_t == m + opt_s, f"optimum n={n} E={edges}")
# decision form, every threshold k in [0, m+1]: cut>=k feasible <=> sat>=m+k feasible
for k in range(0, m + 2):
check((opt_s >= k) == (opt_t >= m + k), f"threshold k={k} n={n} E={edges}")
EXH[(n, tuple(edges))] = (tn, cl, cs, src, tgt)
# n = 6, every simple graph (32768) and every configuration (64), via edge bitmasks.
# Per configuration and per possible edge slot, the indicator of each clause is
# computed by the clause semantics above; a graph is a mask over the 15 slots.
n6 = 6
pairs6 = all_pairs(n6)
cs6 = configs(n6)
cutmask, posmask, negmask = [], [], []
for c in cs6:
cm = pm = nm = 0
for j, (u, v) in enumerate(pairs6):
_, cl = reduce(n6, [(u, v)])
if maxcut_eval(n6, [(u, v)], c):
cm |= 1 << j
if literal_true(cl[0][0], c) or literal_true(cl[0][1], c):
pm |= 1 << j
if literal_true(cl[1][0], c) or literal_true(cl[1][1], c):
nm |= 1 << j
cutmask.append(cm)
posmask.append(pm)
negmask.append(nm)
pc = int.bit_count
n6_pairs = 0
for g in range(1 << len(pairs6)):
m = pc(g)
best_s = best_t = -1
ok = True
for ci in range(64):
s = pc(g & cutmask[ci])
t = pc(g & posmask[ci]) + pc(g & negmask[ci])
ok &= (t == m + s)
best_s = max(best_s, s)
best_t = max(best_t, t)
n6_pairs += 64
COUNTS[SECTION] += 63 # 64 pointwise checks, the last one recorded below
check(ok, f"n=6 identity graph mask {g}")
check(best_t == m + best_s, f"n=6 optimum graph mask {g}")
print(f" n=6: {1 << len(pairs6)} graphs x 64 configurations = {n6_pairs} pairs")
# multigraphs: loops and parallel edges (the construction is claimed for them)
MULTI = []
for n in range(1, 4):
for edges in multigraphs(n, 4 if n <= 2 else 3):
m = len(edges)
tn, cl = reduce(n, edges)
cs = configs(n)
src = [maxcut_eval(n, edges, c) for c in cs]
tgt = [m2s_eval(tn, cl, c) for c in cs]
for c, s, t in zip(cs, src, tgt):
check(t == m + s, f"multigraph identity n={n} E={edges} x={c}")
check(max(tgt) == m + max(src), f"multigraph optimum n={n} E={edges}")
MULTI.append((n, edges, tn, cl))
# hypothesis, strategy A: random simple graphs n <= 10, random assignment
@st.composite
def simple_graph_and_config(draw):
n = draw(st.integers(min_value=0, max_value=10))
pairs = all_pairs(n)
chosen = draw(st.lists(st.sampled_from(pairs), unique=True)) if pairs else []
edges = [(v, u) if draw(st.booleans()) else (u, v) for (u, v) in chosen]
config = draw(st.lists(st.booleans(), min_size=n, max_size=n))
return n, edges, config
# strategy B: multigraphs with loops/parallel edges, structured configurations
@st.composite
def multigraph_and_pattern(draw):
n = draw(st.integers(min_value=1, max_value=8))
edges = draw(st.lists(st.tuples(st.integers(0, n - 1), st.integers(0, n - 1)),
max_size=24))
pattern = draw(st.sampled_from(["zeros", "ones", "alternating", "random"]))
if pattern == "zeros":
config = [False] * n
elif pattern == "ones":
config = [True] * n
elif pattern == "alternating":
config = [v % 2 == 1 for v in range(n)]
else:
config = draw(st.lists(st.booleans(), min_size=n, max_size=n))
return n, edges, config
HSET = settings(max_examples=1500, derandomize=True, database=None, deadline=None,
suppress_health_check=list(HealthCheck))
@HSET
@given(simple_graph_and_config())
def hyp_simple(data):
n, edges, config = data
tn, cl = reduce(n, edges)
check(m2s_valid(tn, cl), f"hyp A valid {data}")
s = maxcut_eval(n, edges, config)
t = m2s_eval(tn, cl, config)
check(t == len(edges) + s, f"hyp A identity {data}")
check(maxcut_eval(n, edges, extract(n, config)) == t - len(edges), f"hyp A extract {data}")
@HSET
@given(multigraph_and_pattern())
def hyp_multi(data):
n, edges, config = data
tn, cl = reduce(n, edges)
check(m2s_valid(tn, cl), f"hyp B valid {data}")
s = maxcut_eval(n, edges, config)
t = m2s_eval(tn, cl, config)
check(t == len(edges) + s, f"hyp B identity {data}")
check(len(cl) == 2 * len(edges), f"hyp B size {data}")
hyp_simple()
hyp_multi()
# ================================================================ section 3
section("3 extraction")
for (n, edges), (tn, cl, cs, src, tgt) in EXH.items():
m = len(edges)
opt_t, opt_s = max(tgt), max(src)
for c, t in zip(cs, tgt):
x = extract(n, c)
check(len(x) == n and all(x[v] == c[v] for v in range(n)),
f"position-for-position n={n} x={c}")
check(maxcut_eval(n, edges, x) == t - m, f"extracted value n={n} E={edges} x={c}")
if t == opt_t: # every optimal target witness extracts to an optimal cut
check(maxcut_eval(n, edges, x) == opt_s, f"optimal witness n={n} E={edges} x={c}")
# wrong lengths are rejected, on both evaluations and extraction
for bad in (n + 1, n - 1):
if bad < 0:
continue
for fn in (lambda: extract(n, [False] * bad),
lambda: m2s_eval(tn, cl, [False] * bad),
lambda: maxcut_eval(n, edges, [False] * bad)):
try:
fn()
check(False, f"length {bad} accepted for n={n}")
except EvalError:
check(True, "")
for (n, edges, tn, cl) in MULTI:
tgt = [m2s_eval(tn, cl, c) for c in configs(n)]
opt = max(tgt)
for c, t in zip(configs(n), tgt):
if t == opt:
check(maxcut_eval(n, edges, extract(n, c)) == opt - len(edges),
f"multigraph optimal witness n={n} E={edges}")
# ================================================================ section 4
section("4 size vs formula")
# Derivation: the construction emits exactly one variable per vertex and a loop
# body of exactly two clauses per edge occurrence, with no branch, no omitted row
# and no normalization; so num_vars = n and num_clauses = 2m on the full domain.
for (n, edges), (tn, cl, *_rest) in EXH.items():
check(tn == num_vars_formula.subs(n_s, n), f"num_vars n={n}")
check(len(cl) == num_clauses_formula.subs(m_s, len(edges)), f"num_clauses E={edges}")
for (n, edges, tn, cl) in MULTI:
check(tn == n and len(cl) == 2 * len(edges), f"multigraph size n={n} E={edges}")
# ================================================================ section 5
section("5 structure")
def structure_ok(n, edges, tn, cl):
if not m2s_valid(tn, cl):
return False
if len(cl) != 2 * len(edges):
return False
for idx, (u, v) in enumerate(edges):
p, q = cl[2 * idx], cl[2 * idx + 1]
if p != [u + 1, v + 1] or q != [-(u + 1), -(v + 1)]:
return False
if q != [-l for l in p]: # (MCC): complementary pair
return False
if not all(1 <= abs(l) <= n for l in p + q):
return False
return True
for (n, edges), (tn, cl, *_rest) in EXH.items():
check(structure_ok(n, edges, tn, cl), f"structure n={n} E={edges}")
# positive literals precisely in even clauses, negative in odd
check(all((l > 0) == (j % 2 == 0) for j, c in enumerate(cl) for l in c), f"signs n={n}")
for (n, edges, tn, cl) in MULTI:
check(structure_ok(n, edges, tn, cl), f"multigraph structure n={n} E={edges}")
for idx, (u, v) in enumerate(edges):
if u == v: # loop: repeated literal in both clauses, still valid
check(len(cl) == 2 * len(edges) and cl[2 * idx] == [u + 1, u + 1]
and cl[2 * idx + 1] == [-(u + 1), -(u + 1)],
f"loop clauses {edges}")
# parallel edges: repeated clause pairs preserved with multiplicity
for e in set(edges):
mult = edges.count(e)
check(cl.count([e[0] + 1, e[1] + 1]) >= mult, f"parallel multiplicity {edges}")
# special cases named in the proof
tn, cl = reduce(0, [])
check(tn == 0 and cl == [] and m2s_eval(0, [], []) == 0 and maxcut_eval(0, [], []) == 0,
"empty graph: 0 vars, 0 clauses, value 0 = 0 + 0")
check(extract(0, []) == [], "empty graph extracts the empty configuration")
# isolated vertices in graphs with edges: flipping one changes neither value
for (n, edges), (tn, cl, cs, src, tgt) in EXH.items():
touched = {v for e in edges for v in e}
for w in (v for v in range(n) if v not in touched):
for c, s, t in zip(cs, src, tgt):
f = list(c)
f[w] = not f[w]
check(maxcut_eval(n, edges, f) == s and m2s_eval(tn, cl, f) == t,
f"isolated flip n={n} E={edges} w={w} x={c}")
iso_t = m2s_eval(*reduce(3, [(0, 1)]), [False, True, False])
iso_s = maxcut_eval(3, [(0, 1)], [False, True, False])
check(iso_s == 1 and iso_t == 2, "isolated vertex with an edge elsewhere: cut 1, sat 2")
for c in configs(3): # edgeless: every value is zero
check(m2s_eval(*reduce(3, []), c) == 0 == maxcut_eval(3, [], c), f"edgeless {c}")
# disconnected: two disjoint edges plus isolated vertex; value adds over components
dis = [(0, 1), (2, 3)]
for c in configs(5):
t = m2s_eval(*reduce(5, dis), c)
parts = m2s_eval(*reduce(5, [(0, 1)]), c) + m2s_eval(*reduce(5, [(2, 3)]), c)
check(t == parts == 2 + maxcut_eval(5, dis, c), f"disconnected {c}")
for c in configs(2): # self-loop contributes exactly one satisfied clause
check(m2s_eval(*reduce(2, [(1, 1)]), c) == 1, f"loop baseline {c}")
for c in configs(2): # parallel pair contributes 2*(1+[cut])
check(m2s_eval(*reduce(2, [(0, 1), (0, 1)]), c) == 2 * (1 + (c[0] != c[1])), f"parallel {c}")
# ================================================================ section 6
section("6 YES example")
yes_n, yes_e = 4, [(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]
ytn, ycl = reduce(yes_n, yes_e)
check(ytn == 4 and len(ycl) == 10, "4 variables, 10 clauses")
check(ycl == [[1, 2], [-1, -2], [2, 3], [-2, -3], [3, 4], [-3, -4],
[4, 1], [-4, -1], [1, 3], [-1, -3]], f"clause list {ycl}")
w = [False, True, False, True]
check(maxcut_eval(yes_n, yes_e, w) == 4, "cut([0,1,0,1]) = 4")
crossing = [e for e in yes_e if w[e[0]] != w[e[1]]]
check(crossing == [(0, 1), (1, 2), (2, 3), (3, 0)], "four cycle edges cross")
per_edge = [m2s_eval(4, ycl[2 * j:2 * j + 2], w) for j in range(5)]
check(per_edge == [2, 2, 2, 2, 1], f"per-edge satisfied {per_edge}")
check(m2s_eval(ytn, ycl, w) == 9, "sat([0,1,0,1]) = 9 = 5 + 4")
yall = [(maxcut_eval(4, yes_e, c), m2s_eval(4, ycl, c)) for c in configs(4)]
check(max(s for s, _ in yall) == 4, "MaxCut optimum 4")
check(max(t for _, t in yall) == 9, "Max2SAT optimum 9")
check(m2s_eval(4, ycl, [False] * 4) == 5 and m2s_eval(4, ycl, [True] * 4) == 5,
"all on one side: target 5 = m")
check(maxcut_eval(4, yes_e, extract(4, w)) == 4, "extraction returns the cut of value 4")
opt_witnesses = [c for c in configs(4) if m2s_eval(4, ycl, c) == 9]
check(sorted(map(tuple, opt_witnesses)) == [(False, True, False, True), (True, False, True, False)],
f"exactly two optimal assignments {opt_witnesses}")
dist = sorted(t for _, t in yall)
check(dist == [5] * 2 + [7] * 4 + [8] * 8 + [9] * 2, f"value distribution {dist}")
# ================================================================ section 7
section("7 NO example")
# issue: single edge, threshold cut >= 2 / target >= 3
no_n, no_e = 2, [(0, 1)]
ntn, ncl = reduce(no_n, no_e)
check(ncl == [[1, 2], [-1, -2]], "single-edge clauses")
check(all(maxcut_eval(2, no_e, c) < 2 for c in configs(2)), "no cut of value >= 2")
check(all(m2s_eval(ntn, ncl, c) < 3 for c in configs(2)), "no assignment with >= 3 satisfied")
check(max(m2s_eval(ntn, ncl, c) for c in configs(2)) == 2, "target optimum 2")
# >= 3 vertices: triangle, threshold cut >= 3 / target >= 6
tri_e = [(0, 1), (1, 2), (0, 2)]
ttn, tcl = reduce(3, tri_e)
tri = [(maxcut_eval(3, tri_e, c), m2s_eval(ttn, tcl, c)) for c in configs(3)]
check(all(s < 3 for s, _ in tri), "triangle: no cut of value >= 3")
check(all(t < 6 for _, t in tri), "triangle: no assignment with >= 6 satisfied")
check(max(s for s, _ in tri) == 2 and max(t for _, t in tri) == 5, "triangle optima 2 and 5")
check(sorted(t for _, t in tri) == [3, 3, 5, 5, 5, 5, 5, 5], "triangle value distribution")
for c in configs(3): # some edge of an odd cycle never crosses: one per-edge pair gives 1
per = [m2s_eval(3, tcl[2 * j:2 * j + 2], c) for j in range(3)]
check(1 in per, f"triangle: some edge pair contributes 1 at {c}")
# ================================================================ audit
print()
print("CHECK AUDIT")
for name, cnt in COUNTS.items():
print(f" {name}: {cnt}")
print()
print("CLAIM MAP (proof claim -> section)")
for claim, sec in [
("overhead num_vars = n, num_clauses = 2m", "1, 4"),
("per-edge lemma: 1 + [x_u != x_v] satisfied", "1, 5"),
("pointwise identity sat = m + cut", "2 (n<=6 exhaustive, multigraphs, hypothesis)"),
("(=>) cut >= k gives sat >= m + k; (<=) converse", "2 (thresholds)"),
("optimum m + OPT", "2"),
("extraction position-for-position, optimal -> optimal", "3"),
("wrong lengths rejected", "3"),
("literals in 1..n, clauses of length 2, complementary pairs", "5"),
("empty, edgeless, disconnected, loops, parallel edges", "2, 5"),
("flipping an isolated vertex changes neither value", "5"),
("YES example numbers", "6"),
("NO example numbers", "7"),
("checked arithmetic on 2m and v+1", "untestable here: Python integers are unbounded; Rust unit tests"),
]:
print(f" {claim}: {sec}")
print(f"seed={SEED}; hypothesis: derandomize=True, max_examples=1500 per strategy, 2 strategies")
total = sum(COUNTS.values())
print(f"TOTAL: {total} checks, {len(FAILURES)} failures")
sys.exit(1 if FAILURES else 0)Adversary script: attack.py#!/usr/bin/env python3
# /// script
# requires-python = ">=3.12"
# dependencies = ["hypothesis==6.155.7"]
# ///
"""Run with `uv run --script attack.py` (beside construction.py and instances.py). No constructor access."""
import json
import os
import tempfile
from collections import Counter
from itertools import product
from pathlib import Path
os.environ.setdefault("HYPOTHESIS_STORAGE_DIRECTORY", str(Path(tempfile.gettempdir()) / "maxcut-adversary"))
from hypothesis import given, seed, settings, strategies as st
from construction import (reduce, extract_solution, source_value, target_value,
source_feasible, target_feasible)
SEED = 846703
COUNTS = Counter()
FAMILIES = Counter()
def check(condition, section, detail):
COUNTS[section] += 1
if not condition:
raise AssertionError((section, detail))
from instances import simple_graphs, shared_instances
def audit(n, edges, target=None, extractor=extract_solution, exhaustive=True):
if target is None:
target = reduce(n, edges)
FAMILIES["instances"] += 1
FAMILIES["empty"] += n == 0
FAMILIES["edgeless"] += not edges
FAMILIES["loops"] += any(u == v for u, v in edges)
FAMILIES["parallel"] += len({tuple(sorted(e)) for e in edges}) < len(edges)
active = {v for edge in edges for v in edge}
FAMILIES["isolated_vertices"] += len(active) < n
reachable = {0} if n else set()
while True:
expanded = reachable | {v for edge in edges if reachable.intersection(edge) for v in edge}
if expanded == reachable:
break
reachable = expanded
FAMILIES["disconnected"] += n > 1 and len(reachable) < n
context = (n, edges)
check(target["num_vars"] == n, "overhead", context)
check(len(target["clauses"]) == 2 * len(edges), "overhead", context)
check(all(len(c) == 2 and all(0 < abs(lit) <= n for lit in c)
for c in target["clauses"]), "well_formed", context)
for j, (u, v) in enumerate(edges):
p, q = target["clauses"][2*j:2*j+2]
check(p == [u + 1, v + 1] and q == [-lit for lit in p], "edge_pairs", (context, j))
configs = list(product((0, 1), repeat=n)) if exhaustive else [
(0,) * n, (1,) * n, tuple(v % 2 for v in range(n)), tuple(1 - v % 2 for v in range(n))]
cuts, sats = [], []
for x in configs:
cut = source_value(n, edges, x)
sat = target_value(target, x)
cuts.append(cut)
sats.append(sat)
check(sat == len(edges) + cut, "pointwise", (context, x, cut, sat))
extracted = extractor(n, x)
check(extracted == x and source_value(n, edges, extracted) == sat - len(edges),
"extraction", (context, x, extracted))
if exhaustive:
check(max(sats) == len(edges) + max(cuts), "optimum", context)
for x, value in zip(configs, sats):
if value == max(sats):
check(source_value(n, edges, extractor(n, x)) == max(cuts), "optimal_extraction", (context, x))
for k in [-10**30, *range(-1, len(edges) + 2), 10**30]:
check(any(c >= k for c in cuts) == any(s >= len(edges) + k for s in sats),
"thresholds", (context, k))
for wrong in [(0,) * (n + 1)] + ([(0,) * (n - 1)] if n else []):
try:
extractor(n, wrong)
except ValueError:
check(True, "invalid_witness", context)
else:
check(False, "invalid_witness", (context, wrong))
@st.composite
def edge_lists(draw):
n = draw(st.integers(0, 8))
edges = [] if n == 0 else draw(st.lists(st.tuples(st.integers(0, n-1), st.integers(0, n-1)), max_size=30))
return n, edges
@st.composite
def disconnected_multigraphs(draw):
left = draw(st.integers(1, 4))
right = draw(st.integers(1, 4))
pair = st.one_of(st.tuples(st.integers(0, left-1), st.integers(0, left-1)),
st.tuples(st.integers(left, left+right-1), st.integers(left, left+right-1)))
edges = draw(st.lists(pair, max_size=15))
v = draw(st.integers(0, left-1))
# Force loops and multiplicity while the two components stay disconnected.
return left + right, edges + [(v, v), (v, v)]
@seed(SEED)
@settings(max_examples=400, database=None, deadline=None)
@given(edge_lists())
def arbitrary_property(instance):
audit(*instance)
@seed(SEED + 1)
@settings(max_examples=400, database=None, deadline=None)
@given(disconnected_multigraphs())
def disconnected_property(instance):
audit(*instance)
def mutation_checks():
n, edges = 4, [(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]
mutations = []
t = reduce(n, edges)
t["clauses"][1][0] *= -1
mutations.append((n, edges, t, extract_solution))
mutations.append((1, [(0, 0)], {"num_vars": 1, "clauses": []}, extract_solution))
mutations.append((2, [(0, 1), (0, 1)], reduce(2, [(0, 1)]), extract_solution))
mutations.append((3, [(0, 1)], reduce(2, [(0, 1)]), extract_solution))
mutations.append((n, edges, reduce(n, edges), lambda n, y: tuple(reversed(y))))
for args in mutations:
try:
audit(*args)
except AssertionError:
pass
else:
raise AssertionError("attack failed to detect a deliberately wrong target/extractor")
return len(mutations)
def main():
import unittest
from test_attack import ProofExamples
result = unittest.TextTestRunner().run(unittest.defaultTestLoader.loadTestsFromTestCase(ProofExamples))
if not result.wasSuccessful():
raise SystemExit(1)
killed = mutation_checks()
COUNTS.clear()
FAMILIES.clear()
shared_count = 0
for n, edges in shared_instances():
audit(n, edges)
shared_count += 1
# Identity risk probes on every six-vertex simple graph, four extremal configurations.
six_count = 0
for n, edges in simple_graphs(6):
if n == 6:
audit(n, edges, exhaustive=False)
six_count += 1
arbitrary_property()
disconnected_property()
# Independent existential checkers, including thresholds outside the value range.
for n, edges in [(0, []), (2, [(0, 1)]), (3, [(0, 1), (1, 2), (0, 2)])]:
for k in range(-1, len(edges) + 3):
check(source_feasible(n, edges, k) == target_feasible(reduce(n, edges), len(edges) + k),
"existential_checkers", (n, edges, k))
summary = {"sections": dict(COUNTS), "families": dict(FAMILIES),
"shared_instances": shared_count, "six_vertex_extreme_instances": six_count,
"hypothesis_examples_per_strategy": 400, "seeds": [SEED, SEED + 1],
"mutations_detected": killed, "checks": sum(COUNTS.values()), "failures": 0}
print(json.dumps(summary, indent=2))
Path(__file__).with_name("results.json").write_text(json.dumps(summary, indent=2) + "\n")
if __name__ == "__main__":
main()Adversary script: construction.py"""Independent implementation of the definitions in proof.typ; no constructor import."""
def reduce(num_vertices, edges):
clauses = []
for edge in edges:
positive = [vertex + 1 for vertex in edge]
clauses.extend((positive, [-literal for literal in positive]))
return {"num_vars": num_vertices, "clauses": clauses}
def extract_solution(num_vertices, assignment):
result = tuple(assignment)
if len(result) != num_vertices or any(bit not in (0, 1) for bit in result):
raise ValueError("expected one Boolean per vertex")
return result
def source_value(num_vertices, edges, assignment):
assignment = extract_solution(num_vertices, assignment)
side = {v for v, bit in enumerate(assignment) if bit}
return sum((u in side) != (v in side) for u, v in edges)
def target_value(target, assignment):
assignment = extract_solution(target["num_vars"], assignment)
# A clause fails precisely when every variable has its literal's false value.
return sum(not all(assignment[abs(lit) - 1] == (lit < 0) for lit in clause)
for clause in target["clauses"])
def source_feasible(num_vertices, edges, threshold):
from itertools import product
return any(source_value(num_vertices, edges, x) >= threshold
for x in product((0, 1), repeat=num_vertices))
def target_feasible(target, threshold):
from itertools import product
return any(target_value(target, y) >= threshold
for y in product((0, 1), repeat=target["num_vars"]))Adversary script: instances.py"""Deterministic shared simple-graph and multigraph inputs."""
from itertools import combinations, combinations_with_replacement
def simple_graphs(max_n=5):
for n in range(max_n + 1):
possible = list(combinations(range(n), 2))
for mask in range(1 << len(possible)):
yield n, [edge for i, edge in enumerate(possible) if mask & (1 << i)]
def shared_instances():
yield from simple_graphs()
# Preserve noncanonical endpoint and edge order, and explicitly include multigraphs.
yield 4, [(0, 1), (1, 2), (2, 3), (3, 0), (0, 2)]
yield 5, [(4, 3), (1, 0)]
for n in range(1, 4):
possible = list(combinations_with_replacement(range(n), 2))
for m in range(1, 5):
for edges in combinations_with_replacement(possible, m):
yield n, list(edges) |
Collaborator
Author
Agentic Review ReportPR: #1227 — (a) Structural and semantic
Hand trace on the issue example. The source is the 4-cycle plus the diagonal Per edge, a crossing edge satisfies both clauses and a non-crossing edge exactly one. So Paper proof. The proof is sound. It gives the per-edge case split, then the pointwise identity, then both threshold directions, then the bijection that shifts the objective by the constant Issue compliance.
(b) Quality
(c) Feature test (
|
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1227 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151798 +240
========================================
+ Hits 147308 147548 +240
Misses 4250 4250 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Address review: the pointwise sat = m + cut test now covers every simple graph through five vertices, as in the issue's validation plan, and the paper entry carries the source/target marker comment used by its neighbours. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
|
Thanks for the review. Both Minor findings are addressed in a919268:
|
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.
Fixes #1102
Summary
Adds the direct reduction
MaxCut/SimpleGraph/One → Maximum2Satisfiability(Gramm, Hirsch, Niedermeier, Rossmanith, Discrete Applied Mathematics 130(2), 2003, Section 5).vbecomes the variablex_v(literalv + 1); its truth value is the side of the cut.(u, v), in edge order, becomes the clauses[u+1, v+1]and[-(u+1), -(v+1)].satisfied(x) = m + cut(x)for every assignment. Maximum cuts are exactly the optimal assignments, and extraction returns the assignment unchanged.num_vars = num_vertices,num_clauses = 2 * num_edges.Changes
src/rules/maxcut_maximum2satisfiability.rs: the rule, built throughMaximum2Satisfiability::try_new(errors kept viatarget_construction), with checked arithmetic for the literalv + 1and the clause count2m. Extraction validates once and returns the assignment. Canonical example: the 4-cycle01, 12, 23, 30plus the diagonal02, witness[0, 1, 0, 1](cut 4, 9 satisfied clauses).src/unit_tests/rules/maxcut_maximum2satisfiability.rs: 14 tests covering:src/rules/mod.rs: module and example registration.docs/paper/reductions.typ,docs/paper/references.bib: areduction-ruleentry with the construction, both directions, extraction, and YES and NO examples. Every number in the examples is computed from the loaded fixture, including both optima by enumerating all assignments. Adds thegramm2003citation.Notes
SimpleGraphadmits self-loops and parallel edges, but on currentmainSimpleGraph::try_newand its deserializer reject both. The construction is still correct for multigraphs (each loop contributes exactly one satisfied clause; each parallel occurrence contributes its own clause pair), and the verification below covers that case mathematically. The rule never receives such graphs, and a test confirms the source rejects them.AggregateReductionResult::extract_valueis infallible, and the maptarget − mwould have to panic or clamp on an arbitrary input. Witness extraction covers the optimization workflow;pred solvethrough the existing Maximum2Satisfiability → ILP route recovers the optimal cut.Verification
make checkandmake paperpass locally; the paper shows no completeness warnings.pred reduceon 1,110 simple graphs produces exactly the targets of two independently written Python encoders (0 mismatches).🤖 Generated with Claude Code