Repository navigation
Add Phase 2 direct QUBO reductions - #1215
Merged
GiggleLiu merged 30 commits intoOct 29, 2026
Merged
Conversation
Collaborator
Author
Verification certificate — Phase 2 group AVerdict: PASS for the stated exact-integer construction and representability contract. Finite testing supplements the bidirectional proof; it does not enumerate unbounded domains. Rust/CLI gates and corpus limitations are separately reported in the PR. Resolved type chain: source Across all groups, 21,000 independently generated normalized targets agreed exactly; zero disagreements. The constructor's scalar checker also compares each expanded polynomial with its unexpanded penalty expression. The JSON report below gives adversary seeds, family sizes, check counts and limitations. adversary_a.json{
"verdict": "PASS",
"seed": 420217,
"hypothesis_seeds": [
170183,
170184
],
"hypothesis_settings": {
"max_examples": 300,
"deadline": null,
"database": null
},
"checks": {
"symbolic": 14,
"yes_example": 6,
"no_example": 4,
"structure": 11947,
"size": 23894,
"extraction": 222683,
"equivalence": 11455,
"arithmetic": 5,
"penalty": 4349865,
"rejection": 4991341
},
"total_checks": 9611214,
"families": {
"feedback:integer_boundary": 3,
"schedule:exhaustive": 1124,
"common_schedule:exhaustive": 63,
"cyclic:exhaustive": 150,
"grouping:exhaustive": 822,
"feedback:exhaustive": 785,
"cyclic:sampled_n4_p1": 300,
"feedback:sampled_n4_m1": 300,
"cyclic:sampled_n4_p4": 300,
"feedback:sampled_n4_m4": 300,
"cyclic:sampled_n4_p8": 300,
"feedback:sampled_n4_m8": 300,
"grouping:sampled_a4_l5": 300,
"grouping:sampled_a4_l7": 300,
"schedule:sampled_n4_p0": 300,
"common_schedule:sampled_n4_p0": 300,
"schedule:sampled_n4_p3": 300,
"common_schedule:sampled_n4_p3": 300,
"schedule:sampled_n4_p7": 300,
"common_schedule:sampled_n4_p7": 300,
"cyclic:sampled_n5_p1": 300,
"feedback:sampled_n5_m1": 300,
"cyclic:sampled_n5_p4": 300,
"feedback:sampled_n5_m4": 300,
"cyclic:sampled_n5_p8": 300,
"feedback:sampled_n5_m8": 300,
"grouping:sampled_a5_l5": 300,
"grouping:sampled_a5_l7": 300,
"schedule:sampled_n5_p0": 300,
"common_schedule:sampled_n5_p0": 300,
"schedule:sampled_n5_p3": 300,
"common_schedule:sampled_n5_p3": 300,
"schedule:sampled_n5_p7": 300,
"common_schedule:sampled_n5_p7": 300,
"feedback:hypothesis": 300,
"schedule:hypothesis": 300
},
"exhaustive_families": {
"schedule": "n=0..5; deadlines in 0..2; capacities 0..min(n,2); empty precedence; conservative target-size filter <=12; every single duplicated/self precedence at deadline 1 and m=n",
"common_schedule": "n=0..5, D=0..2, m=0..n, empty precedence; target cubes <=12 exact",
"cyclic": "n=1..3 all subsets of ordered distinct triples; n=4,5 every single triple",
"grouping": "a=0..3, every string length 0..4; a=4,5 every string length 0..2; K=0..3 (empty K=0)",
"feedback": "n=0..3 all loopless directed endpoint pairs independently absent, -1, or +1; n=1..5 each duplicated loop at weights -3,0,4"
},
"limitations": [
"Finite exhaustive families and >=300 samples per listed large family; arbitrary integers and all instance sizes are not exhaustively enumerable.",
"Scheduling target cubes above 12 variables use 300 sampled bitstrings and an independently found forward witness; other listed targets are exhaustive.",
"Empty grouping string with positive K treated as outside the stated source domain.",
"Runtime/source type gates and Rust behavior are outside this proof-only adversary."
],
"claim_to_evidence": {
"tournament_and_polynomial": "symbolic, penalty, rejection",
"equivalence": "equivalence",
"every_small_feasible_target_extracts": "extraction",
"size_bounds": "size",
"normalized_target": "structure",
"worked_examples": "yes_example, no_example",
"checked_source_sums": "arithmetic"
}
}
crosscheck-report.json{
"counts": {
"schedule": 1800,
"common_schedule": 1800,
"grouping": 1800,
"feedback": 1800,
"subset": 1800,
"cover": 1800,
"matching": 1800,
"threepartition": 1800,
"superstring": 1800,
"stacker": 1800,
"cyclic": 1500,
"partition": 1500
},
"total": 21000,
"disagreements": 0
}constructor-scalar-report.json{
"structure": 21000,
"size": 21000,
"schedule": 63873,
"common_schedule": 60510,
"grouping": 37800,
"feedback": 37800,
"subset": 18900,
"cover": 18900,
"matching": 18900,
"threepartition": 35400,
"superstring": 22380,
"stacker": 50700,
"cyclic": 37500,
"partition": 18600
}proof-a.typ#set page(width: 210mm, height: 297mm)
= Direct scheduling and ordering QUBO constructions
Theorem. The following constructions preserve satisfiability (Or to DecisionQUBO<i64>) or minimum integer objective (Min<i64> to QUBO<i64>). Source witnesses have the meanings below. All coefficient/constant and energy interval arithmetic is checked; unrepresentable targets return a typed reduction error. Numeric failures are not infeasibility.
== Shared conventions
A polynomial is stored as a constant C and coefficients q(i,j) for i<=j; Boolean squares collapse to the same bit. Stored QUBO energy is E=H-C. For a nonnegative integer constraint penalty H, DecisionQUBO uses bound -C. For an objective F plus integer penalties P V, compute lower and upper coefficient interval bounds L,U for F (constant included), choose P=U-L+1. Then every violating bitstring has H>=L+P>U. Feasible energies lie in [L-C,U-C]. Extraction validates target once and rejects energy outside the interval; completed-value recovery adds C within the interval and maps outside to Min(None). Every partial selected-coefficient sum is bounded by the sum of all negative and all positive coefficients. Additional source-operation bounds must hold even when coefficients cancel.
For n elements, bit r(i,j), i<j, means i precedes j; r(j,i)=1-r(i,j). For i<j<k use T=r(i,k)+r(i,j)r(j,k)-r(i,j)r(i,k)-r(i,k)r(j,k). T is one exactly on either cyclic orientation, zero otherwise. Absence of cyclic triangles in a tournament is equivalent to total order. Rank of each element is its number of predecessors. Variables n(n-1)/2; triangle interactions at most 3 binomial(n,3); construction O(n^3) additions.
== Individual-deadline and common-deadline scheduling
Source has n unit tasks, processor capacity m>=0, deadlines d_i>=0, and indexed precedence pairs (i,j), including duplicates, loops and cycles. Source witness t_i is a nonnegative start strictly below d_i, with at most m tasks at each start and t_i<t_j for every precedence. The common-deadline variant has all d_i=D. Empty tasks are feasible. For each task put h_i=min(d_i,n); let h=max h_i. Allocate x(i,t) for 0<=t<h_i, row-major. For each time t with k_t available tasks, if m>=k_t omit capacity (automatically satisfied once rows are one-hot). Otherwise allocate b=floor(log2(m))+1 bits if m>0, zero bits for m=0, with weights 1,2,...,2^(b-1). They encode slack s_t. Add (sum_t x(i,t)-1)^2 for each row; (sum_i x(i,t)+s_t-m)^2 for each nontrivial capacity; and x(i,t)x(j,u) whenever (i,j) is a precedence and t>=u. Repeated bit indices collapse as Boolean monomials, including self precedences. All penalties have unit weight. Decision bound -C.
Forward: compress the occupied times of any feasible source schedule to consecutive times starting at zero. At most n occupied times exist; compression only decreases starts, preserves strict precedence and capacity and meets individual deadlines. Select these starts; binary slack represents every residual 0..m. All penalties vanish.
Backward: zero nonnegative penalty forces exactly one valid start per row, capacity at most m, and no reversed/equal precedence pair. Decoding each row gives a source YES witness. NO sources give strictly positive penalty on every target bitstring, including empty rows and self/cyclic precedences. Aggregates are identity on Or.
Bounds: N=sum h_i + sum active_t bit_length(m); since active capacities imply m<n, bit_length(m)<=n, N<=2 n max_deadline (or 2 n D). E<=N(N-1)/2, conservatively (2 n H)^2. Concrete horizon is min(H,n), so no exponential numeric-horizon dependence remains for these unit tasks. Construction takes O(N^2 + p n^2) coefficient additions, where p is precedence count.
YES example n=3,m=2,d=(1,1,2), precedences={(0,2)}: rows sizes 1,1,2; two slack bits of weights 1,2 at t=0 (k=3), no slack at t=1; starts (0,0,1), slack 0. C=3+4=7; H=0,E=-7. NO same deadlines with m=1: first two mandatory starts conflict.
== CyclicOrdering
Source n>=1, triples (a,b,c) of distinct in-range members; witness ranks is a permutation. For each prescribed triple add (r(a,b)+r(b,c)+r(c,a)-2)^2 to all unit triangle penalties. Decision bound -C. On any total order the clockwise sum is two precisely for a<b<c or b<c<a or c<a<b, otherwise one. Forward every cyclic source ordering gives zero; backward zero forces transitivity and the prescribed orientations. Decode predecessor counts; aggregate Or identity. N=binomial(n,2), E<=N(N-1)/2. Construction O(n^3+number_of_triples). YES n=3,triple (0,1,2), ranks (0,1,2), bits (1,1,1), orientation sum 2. NO both (0,1,2) and (0,2,1) prescribed: the two sums cannot both be 2.
== GroupingBySwapping
Source string s length l over declared alphabet 0..a-1 and budget K. Empty string requires K=0. Witness is a length-K program of adjacent swap positions; l-1 is a no-op. Allocate tournament over all a alphabet symbols. For each unordered symbol pair i<j let A be number of occurrences j before i in the original string and B number of i before j. Cost F=A*r(i,j)+B*(1-r(i,j)); sum over pairs. This is the inversion count of stable grouping in the chosen block order. Let M=l(l-1)/2, use P=M+1 on triangle penalties. Decision threshold min(K,M)-C, where C includes the inversion objective constant. Source arithmetic counts fit checked integers. Empty strings, unused symbols and one-symbol alphabets are permitted.
Forward: any successful program ends in a symbol block order (extend with unused symbols). Relative order of equal symbols can be preserved; every inverted unequal pair needs a crossing and each adjacent swap changes inversion count by at most one. Thus F<=K. Backward: target satisfying threshold has no cyclic triangle since P>M, so ranks are a total order. Stable insertion sort original symbols by these ranks, emitting each adjacent swap index, uses exactly F<=K swaps and groups symbols. Pad program to K with no-op l-1; empty is the explicit empty program. Or aggregate identity. N=binomial(a,2); E<=3 binomial(a,3). Coefficient construction O(l^2+a^3); extraction O(l^2+K); K is an explicit output-length bound.
YES s=(0,1,2,0),K=2: block order 0,1,2 needs swaps positions 2 then 1, gives (0,0,1,2). NO same string,K=0.
== MinimumFeedbackArcSet<i64>
Graph is a directed multigraph: arcs have distinct indices even if endpoints repeat; loops permitted; signed i64 weights. Source witness removes arcs, retained subgraph must be acyclic, objective sum of removed arc weights in input order.
Pre-remove every negative-weight arc and every loop (count weight once). Constant F begins with their sum. For each remaining nonnegative arc u->v add w*(1-r(u,v)). Add tournament penalties P=U-L+1 from objective coefficient interval. Decode by removing exactly pre-removed arcs and those backward in the total order. Check sum of all negative weights >=i64::MIN and all positive weights <=i64::MAX before polynomial cancellation, guaranteeing every source prefix.
Forward: from any feasible removal set, adding negative removals never hurts acyclicity and cannot increase objective. Topologically order the retained graph. Every backward arc must have been removed; replacing the removal set by all negative/loop/backward arcs cannot increase objective because any additionally removed forward arcs had nonnegative weight. Thus a canonical order achieves at most the source cost. Backward: canonical removal leaves only strictly forward arcs, hence a DAG, with exactly F as source cost. The optimal values coincide; recover F by adding C. Penalty ensures all target optima are total orders. N=binomial(n,2), E<=3 binomial(n,3), construction O(m+n^3). Parallel costs add; opposite arcs contribute independently.
YES objective example n=3, arcs 0->1 weight -2,1->2 weight 3,2->0 weight 1: remove negative arc alone, value -2, choose order 1,2,0. Optimization always has a feasible source (remove all); a NO feasibility example is inapplicable. Invalid target example n=3 with cyclic comparison bits is rejected. Empty graph has zero-variable optimum 0; loops contribute fixed costs.
constructor.pyfrom collections import defaultdict
from itertools import product, permutations, combinations
import json,random,heapq
from pathlib import Path
import sympy as sy
class Poly:
def __init__(self,n): self.n=n;self.c=0;self.q=defaultdict(int)
def add(self,i,j,v): self.q[min(i,j),max(i,j)]+=v
def sq(self,terms,b):
self.c+=b*b
for z,(i,a) in enumerate(terms):
self.add(i,i,a*a-2*b*a)
for j,d in terms[z+1:]: self.add(i,j,2*a*d)
def interval(self): return self.c+sum(min(0,v) for v in self.q.values()),self.c+sum(max(0,v) for v in self.q.values())
def done(self,bound=None,interval=None):
lo,hi=self.interval();clo=lo-self.c;chi=hi-self.c
if min(self.c,clo)<-(1<<63) or max(self.c,chi)>(1<<63)-1:raise OverflowError
return dict(n=self.n,constant=self.c,entries=[[i,j,c] for (i,j),c in sorted(self.q.items()) if c],bound=bound,low=None if interval is None else interval[0]-self.c,high=None if interval is None else interval[1]-self.c)
def pi(n,i,j):return i*(2*n-i-1)//2+j-i-1
def tournament(q,n,p):
for i,j,k in combinations(range(n),3):
a,b,c=pi(n,i,j),pi(n,i,k),pi(n,j,k)
for x,y,v in [(b,b,p),(a,c,p),(a,b,-p),(b,c,-p)]:q.add(x,y,v)
def assignment(q,n,k,p=1):
for i in range(n):
z=Poly(q.n);z.sq([(i*k+j,1) for j in range(k)],1);merge(q,z,p)
def merge(q,z,p=1):
q.c+=p*z.c
for (a,b),v in z.q.items():q.add(a,b,p*v)
def perm(q,n,p):
assignment(q,n,n,p)
for t in range(n):
z=Poly(q.n);z.sq([(i*n+t,1) for i in range(n)],1);merge(q,z,p)
def dist(v,arcs,edges,s,t):
if s==t:return 0
adj=[[] for _ in range(v)]
for a,b,w in arcs:adj[a].append((b,w))
for a,b,w in edges:adj[a].append((b,w));adj[b].append((a,w))
ds=[(1<<63)-1]*v;ds[s]=0;h=[(0,-s)]
while h:
c,a=heapq.heappop(h);a=-a
if c>ds[a]:continue
if a==t:return c
for b,w in adj[a]:
d=c+w
if d>(1<<63)-1:return None
if d<ds[b]:ds[b]=d;heapq.heappush(h,(d,-b))
return None
def contained(a,b):return not a or any(b[t:t+len(a)]==a for t in range(len(b)-len(a)+1))
def overlap(a,b):return max([0]+[i for i in range(1,min(len(a),len(b))+1) if a[-i:]==b[:i]])
def reduce(kind,d):
if kind in ['schedule','common_schedule']:
deadlines=d.get('d',[d.get('D',0)]*d.get('n',0));n=len(deadlines);lens=[min(x,n) for x in deadlines];m=d['m'];offset=[];s=0
for h in lens:offset.append(s);s+=h
caps=[]
for t in range(max(lens,default=0)):
row=[(offset[i]+t,1) for i,h in enumerate(lens) if t<h]
if m<len(row):
row += [(s+j,1<<j) for j in range(m.bit_length())];s+=m.bit_length();caps.append(row)
q=Poly(s)
for o,h in zip(offset,lens):q.sq([(o+t,1) for t in range(h)],1)
for row in caps:q.sq(row,m)
for i,j in d['p']:
for t in range(lens[i]):
for u in range(min(t+1,lens[j])):q.add(offset[i]+t,offset[j]+u,1)
elif kind in ['cyclic','grouping','feedback']:
n=d.get('n',d.get('a'));q=Poly(n*(n-1)//2)
if kind=='cyclic':
tournament(q,n,1)
for a,b,c in d['triples']:
row=[];rhs=2
for i,j in [(a,b),(b,c),(c,a)]:
if i<j:row.append((pi(n,i,j),1))
else:row.append((pi(n,j,i),-1));rhs-=1
q.sq(row,rhs)
elif kind=='grouping':
for pos,i in enumerate(d['s']):
for j in d['s'][pos+1:]:
if i<j:q.c+=1;q.add(pi(n,i,j),pi(n,i,j),-1)
elif i>j:q.add(pi(n,j,i),pi(n,j,i),1)
M=len(d['s'])*(len(d['s'])-1)//2;tournament(q,n,M+1)
return q.done(min(d['K'],M)-q.c)
else:
ws=[w for _,_,w in d['arcs']]
if sum(min(w,0) for w in ws)<-(1<<63) or sum(max(w,0) for w in ws)>(1<<63)-1:raise OverflowError
for a,b,w in d['arcs']:
if w<0 or a==b:q.c+=w
elif a<b:q.c+=w;q.add(pi(n,a,b),pi(n,a,b),-w)
else:q.add(pi(n,b,a),pi(n,b,a),w)
L,U=q.interval();tournament(q,n,U-L+1);return q.done(interval=(L,U))
elif kind in ['partition','subset']:
q=Poly(len(d['s']));q.sq([(i,x*(2 if kind=='partition' else 1)) for i,x in enumerate(d['s'])],sum(d['s']) if kind=='partition' else d['T'])
elif kind in ['cover','matching']:
ts=d['triples'];q=Poly(len(ts))
for axis in range(3 if kind=='matching' else 1):
for u in range(d['u']):q.sq([(j,1) for j,t in enumerate(ts) if (t[axis]==u if kind=='matching' else u in t)],1)
elif kind=='threepartition':
n=len(d['s']);k=n//3;q=Poly(n*k);assignment(q,n,k)
for g in range(k):q.sq([(i*k+g,1) for i in range(n)],3);q.sq([(i*k+g,w) for i,w in enumerate(d['s'])],d['B'])
elif kind=='superstring':
ss=d['strings'];ss=[s for i,s in enumerate(ss) if s and not any(contained(s,t) and (len(s)<len(t) or j<i) for j,t in enumerate(ss) if i!=j)]
n=len(ss);q=Poly(n*n);q.c=sum(map(len,ss))
for i in range(n):
for j in range(n):
if i!=j:
for p in range(n-1):q.add(i*n+p,j*n+p+1,-overlap(ss[i],ss[j]))
L,U=q.interval();P=U-L+1;perm(q,n,P)
if any(c>=d['a'] for s in d['strings'] for c in s):q.c+=P
return q.done(interval=(L,U))
elif kind=='stacker':
arcs=d['arcs'];n=len(arcs);q=Poly(n*n);q.c=sum(a[2] for a in arcs);D=[[dist(d['v'],arcs,d['edges'],a[1],b[0]) for b in arcs] for a in arcs]
if q.c+n*max([0]+[x for r in D for x in r if x is not None])>(1<<63)-1:raise OverflowError
missing=[]
for i in range(n):
for j in range(n):
if n>1 and i==j:continue
for p in range(n):
a,b=i*n+p,j*n+(p+1)%n
if D[i][j] is None:missing.append((a,b))
else:q.add(a,b,D[i][j])
L,U=q.interval();P=U-L+1;perm(q,n,P)
for a,b in missing:q.add(a,b,P)
return q.done(interval=(L,U))
else:raise ValueError(kind)
return q.done(-q.c)
def energy(q,x):return sum(c*x[i]*x[j] for i,j,c in q['entries'])
def run():
counts=defaultdict(int);rng=random.Random(20261022)
n,k,H=sy.symbols('n k H',nonnegative=True)
for f in [n*(n-1)/2,n*k,n*n,2*n*H]:assert sy.expand(f*f-f*f)==0;counts['symbolic']+=1
# Exhaustive selection residuals independently computed, including every target witness.
for size in range(6):
for _ in range(300):
s=[rng.randrange(1,8) for i in range(size)];T=rng.randrange(25)
for kind,d in [('subset',{'s':s,'T':T})]+([('partition',{'s':s})] if s else []):
q=reduce(kind,d)
assert q['n']==size and len([1 for i,j,c in q['entries'] if i!=j])<=size*(size-1)//2;counts['size']+=1
assert all(0<=i<=j<size for i,j,c in q['entries']);counts['structure']+=1
for bits in product([0,1],repeat=size):
selected=sum(a*b for a,b in zip(s,bits));valid=selected==T if kind=='subset' else selected==sum(s)-selected
assert (energy(q,bits)<=q['bound'])==valid;counts['forward_backward']+=1;counts['extraction']+=valid
examples=[('partition',{'s':[1,2,3]},[1,1,0],True),('partition',{'s':[1,1,1]},[1,0,0],False),('cover',{'u':6,'triples':[[0,1,2],[3,4,5],[0,3,4]]},[1,1,0],True),('cover',{'u':6,'triples':[[0,1,2],[0,1,3],[0,1,4]]},[1,0,0],False)]
for kind,d,x,want in examples:
q=reduce(kind,d);assert (energy(q,x)<=q['bound'])==want;counts['yes_example' if want else 'no_example']+=1
Path(__file__).with_name('constructor-report.json').write_text(json.dumps(counts,indent=2));print(dict(counts))
if __name__=='__main__':run()adversary_a.py"""Independent proof-only adversary. No repository/constructor imports.
JSON instance schemas:
schedule: {d:[deadlines],m:capacity,p:[[before,after],...]}
common_schedule: {n:tasks,D:deadline,m:capacity,p:[[before,after],...]}
cyclic: {n:members,triples:[[a,b,c],...]}
grouping: {a:alphabet_size,s:[symbols],K:swap_budget}
feedback: {n:vertices,arcs:[[u,v,signed_weight],...]}
reduce outputs upper-triangle polynomial entries; low/high are stored energy bounds.
"""
import itertools as it
import json
import math
import random
from collections import Counter, defaultdict, deque
from functools import lru_cache
from pathlib import Path
import sympy as sp
from hypothesis import given, settings, strategies as st, seed
MIN, MAX = -(1 << 63), (1 << 63) - 1
AUDIT = Counter()
FAMILIES = Counter()
RNG = random.Random(420217)
def require(condition, section, detail=None):
AUDIT[section] += 1
assert condition, (section, detail)
class Poly:
def __init__(self):
self.c = 0
self.q = defaultdict(int)
def add(self, coefficient, *bits):
if not bits:
self.c += coefficient
else:
self.q[min(bits), max(bits)] += coefficient
def square(self, affine):
for i, v in affine.items():
for j, w in affine.items():
self.add(v * w, *[k for k in (i, j) if k is not None])
def pairs(n):
return list(it.combinations(range(n), 2))
def layout(kind, inst):
if kind == 'common_schedule':
return dict(d=[inst['D']] * inst['n'], m=inst['m'], p=inst['p'])
return inst
def triangle(poly, ids, i, j, k, penalty):
ij, ik, jk = ids[i,j], ids[i,k], ids[j,k]
poly.add(penalty, ik)
poly.add(penalty, ij, jk)
poly.add(-penalty, ij, ik)
poly.add(-penalty, ik, jk)
def direction(ids, u, v):
return {ids[u,v]:1} if u < v else {None:1, ids[v,u]:-1}
def reduce(kind, instance):
inst = layout(kind, instance)
poly = Poly()
low = high = None
if kind in ('schedule', 'common_schedule'):
n = len(inst['d'])
rows = []
N = 0
for d in inst['d']:
rows.append(list(range(N, N + min(d,n))))
N += min(d,n)
for row in rows:
poly.square({None:-1, **{i:1 for i in row}})
for t in range(max(map(len,rows),default=0)):
column = [row[t] for row in rows if len(row)>t]
if inst['m'] < len(column):
linear = {None:-inst['m'], **{i:1 for i in column}}
for b in range(inst['m'].bit_length()):
linear[N] = 1 << b
N += 1
poly.square(linear)
for i,j in inst['p']:
for t,x in enumerate(rows[i]):
for u,y in enumerate(rows[j]):
if t >= u:
poly.add(1,x,y)
bound = -poly.c
else:
n = inst['a'] if kind == 'grouping' else inst['n']
ids = {p:i for i,p in enumerate(pairs(n))}
N = len(ids)
penalty = 1
if kind == 'cyclic':
for a,b,c in inst['triples']:
linear = defaultdict(int, {None:-2})
for u,v in [(a,b),(b,c),(c,a)]:
for i,w in direction(ids,u,v).items():
linear[i] += w
poly.square(linear)
elif kind == 'grouping':
if not inst['s'] and inst['K']:
raise ValueError('Empty source string requires zero budget')
for u,v in it.combinations(inst['s'],2):
if u == v:
continue
if u < v:
poly.add(1)
poly.add(-1, ids[u,v])
else:
poly.add(1, ids[v,u])
M = len(inst['s']) * (len(inst['s'])-1) // 2
penalty = M+1
elif kind == 'feedback':
if sum(w for u,v,w in inst['arcs'] if w<0)<MIN or sum(w for u,v,w in inst['arcs'] if w>0)>MAX:
raise OverflowError('Source partial sums may overflow')
for u,v,w in inst['arcs']:
if u == v or w < 0:
poly.add(w)
elif u < v:
poly.add(w)
poly.add(-w,ids[u,v])
else:
poly.add(w,ids[v,u])
L = poly.c + sum(min(0,q) for q in poly.q.values())
U = poly.c + sum(max(0,q) for q in poly.q.values())
penalty = U-L+1
low, high = L-poly.c, U-poly.c
else:
raise ValueError(kind)
for i,j,k in it.combinations(range(n),3):
triangle(poly,ids,i,j,k,penalty)
bound = None if kind == 'feedback' else ((min(inst['K'],M) if kind == 'grouping' else 0)-poly.c)
entries = [[i,j,c] for (i,j),c in sorted(poly.q.items()) if c]
# The proof requires representable coefficients, shifts, and every selected-term prefix.
numbers = [poly.c, sum(min(0,c) for i,j,c in entries), sum(max(0,c) for i,j,c in entries)]
numbers += [c for i,j,c in entries] + [v for v in (bound,low,high) if v is not None]
if any(v<MIN or v>MAX for v in numbers):
raise OverflowError('Unrepresentable target')
return dict(n=N, constant=poly.c, entries=entries, bound=bound, low=low, high=high)
def target_value(target,bits):
return sum(c*bits[i]*bits[j] for i,j,c in target['entries'])
def target_feasible(target,bits):
if len(bits)!=target['n'] or any(b not in (0,1) for b in bits):
return False
value = target_value(target,bits)
return value<=target['bound'] if target['bound'] is not None else target['low']<=value<=target['high']
def source_value(kind,instance,witness):
inst = layout(kind, instance)
if kind in ('schedule','common_schedule'):
return (len(witness)==len(inst['d']) and all(0<=t<d for t,d in zip(witness,inst['d']))
and max(Counter(witness).values(),default=0)<=inst['m']
and all(witness[i]<witness[j] for i,j in inst['p']))
if kind == 'cyclic':
return (sorted(witness)==list(range(inst['n'])) and all(
(witness[a]<witness[b]<witness[c] or witness[b]<witness[c]<witness[a] or witness[c]<witness[a]<witness[b])
for a,b,c in inst['triples']))
if kind == 'grouping':
if len(witness)!=inst['K']:
return False
s = inst['s'][:]
for p in witness:
if not 0<=p<len(s):
return False
if p+1<len(s):
s[p],s[p+1]=s[p+1],s[p]
blocks = [s[i] for i in range(len(s)) if i==0 or s[i]!=s[i-1]]
return len(blocks)==len(set(blocks))
removed = set(witness)
if len(removed)!=len(witness) or not removed.issubset(range(len(inst['arcs']))):
return None
indegree = [0]*inst['n']
outgoing = [[] for _ in indegree]
for index,(u,v,w) in enumerate(inst['arcs']):
if index not in removed:
outgoing[u].append(v)
indegree[v]+=1
queue = deque(i for i,d in enumerate(indegree) if d==0)
visited = 0
while queue:
u = queue.popleft()
visited += 1
for v in outgoing[u]:
indegree[v]-=1
if indegree[v]==0:
queue.append(v)
return sum(w for index,(u,v,w) in enumerate(inst['arcs']) if index in removed) if visited==inst['n'] else None
def extract_solution(kind,instance,target,bits):
if not target_feasible(target,bits):
raise ValueError('Not a source-certifying target witness')
inst = layout(kind,instance)
if kind in ('schedule','common_schedule'):
starts=[]
offset=0
for d in inst['d']:
row=bits[offset:offset+min(d,len(inst['d']))]
if sum(row)!=1:
raise ValueError('Malformed schedule row')
starts.append(row.index(1))
offset+=len(row)
return starts
n = inst['a'] if kind=='grouping' else inst['n']
ranks=[0]*n
for bit,(i,j) in zip(bits,pairs(n)):
ranks[j if bit else i]+=1
if sorted(ranks)!=list(range(n)):
raise ValueError('Not a total order')
if kind=='cyclic':
return ranks
if kind=='feedback':
return [i for i,(u,v,w) in enumerate(inst['arcs']) if w<0 or u==v or ranks[u]>ranks[v]]
working=inst['s'][:]
swaps=[]
for j in range(1,len(working)):
while j>0 and ranks[working[j-1]]>ranks[working[j]]:
working[j-1],working[j]=working[j],working[j-1]
swaps.append(j-1)
j-=1
swaps += [len(working)-1]*(inst['K']-len(swaps))
return swaps
@lru_cache(None)
def grouping_distance(s):
pending=deque([(s,0)])
seen={s}
while pending:
value,distance=pending.popleft()
blocks=[value[i] for i in range(len(value)) if not i or value[i]!=value[i-1]]
if len(blocks)==len(set(blocks)):
return distance
for p in range(len(value)-1):
next_value=value[:p]+(value[p+1],value[p])+value[p+2:]
if next_value not in seen:
seen.add(next_value)
pending.append((next_value,distance+1))
def source_optimum(kind,instance):
inst=layout(kind,instance)
if kind in ('schedule','common_schedule'):
return any(source_value(kind,instance,t) for t in it.product(*(range(d) for d in inst['d'])))
if kind=='cyclic':
return any(source_value(kind,inst,ranks) for ranks in it.permutations(range(inst['n'])))
if kind=='grouping':
return grouping_distance(tuple(inst['s']))<=inst['K']
best=None
for mask in range(1<<len(inst['arcs'])):
value=source_value(kind,inst,[i for i in range(len(inst['arcs'])) if mask>>i&1])
if value is not None and (best is None or value<best):
best=value
return best
def assignments(N):
for mask in range(1<<N):
yield [(mask>>i)&1 for i in range(N)]
def verify(kind,inst,family='exhaustive',full=True):
target=reduce(kind,inst)
data=layout(kind,inst)
N=target['n']
FAMILIES[kind+':'+family]+=1
entries=target['entries']
require(all(0<=i<=j<N and c!=0 for i,j,c in entries) and entries==sorted(entries)
and len({(i,j) for i,j,c in entries})==len(entries),'structure', (kind,inst))
if kind in ('schedule','common_schedule'):
n=len(data['d']); h=[min(d,n) for d in data['d']]
exact=sum(h)+sum(data['m'].bit_length() for t in range(max(h,default=0)) if sum(x>t for x in h)>data['m'])
require(N==exact and N<=2*n*max(data['d'],default=0),'size')
require(sum(i!=j for i,j,c in entries)<=N*(N-1)//2,'size')
else:
n=data['a'] if kind=='grouping' else data['n']
require(N==math.comb(n,2),'size')
edge_bound=3*math.comb(n,3) if kind in ('grouping','feedback') else N*(N-1)//2
require(sum(i!=j for i,j,c in entries)<=edge_bound,'size')
if not full:
# Larger scheduling targets: explicitly certify witnesses and sample arbitrary bits.
starts=next((t for t in it.product(*(range(d) for d in data['d'])) if source_value(kind,inst,t)),None)
samples=[[RNG.randrange(2) for _ in range(N)] for _ in range(300)]
if starts is not None:
occupied=sorted(set(starts)); starts=[occupied.index(t) for t in starts]
bits=[]; h=[min(d,len(data['d'])) for d in data['d']]
for t,limit in zip(starts,h): bits.extend(int(u==t) for u in range(limit))
for t in range(max(h,default=0)):
if sum(limit>t for limit in h)>data['m']:
slack=data['m']-starts.count(t)
bits.extend(slack>>b&1 for b in range(data['m'].bit_length()))
samples.append(bits)
require(target_feasible(target,bits),'equivalence')
for bits in samples:
if target_feasible(target,bits):
require(source_value(kind,inst,extract_solution(kind,inst,target,bits)),'extraction')
require(target_value(target,bits)+target['constant']>=0,'penalty')
return
best=None; feasible=False
for bits in assignments(N):
value=target_value(target,bits)
best=value if best is None else min(best,value)
if target_feasible(target,bits):
feasible=True
recovered=extract_solution(kind,inst,target,bits)
source=source_value(kind,inst,recovered)
require(source==value+target['constant'] if kind=='feedback' else source is True,'extraction',(kind,inst,bits))
else:
try:
extract_solution(kind,inst,target,bits)
except ValueError:
require(True,'rejection')
else:
require(False,'rejection')
if kind!='feedback':
require(value+target['constant']>=0,'penalty')
source=source_optimum(kind,inst)
require(best+target['constant']==source if kind=='feedback' else feasible==source,'equivalence',(kind,inst,source,best,target))
def symbolic():
n,H,m,h,A,B,r,s,t=sp.symbols('n H m h A B r s t', integer=True)
require(sp.expand(n*(n-1)/2-sp.binomial(n,2).expand(func=True))==0,'symbolic')
require(sp.expand(3*sp.binomial(n,3).expand(func=True)-n*(n-1)*(n-2)/2)==0,'symbolic')
require(sp.expand((n*H+n*H)-2*n*H)==0,'symbolic')
require(sp.expand((2*n*H)**2-4*n*n*H*H)==0,'symbolic')
require(sp.expand(A*r+B*(1-r)-(B+(A-B)*r))==0,'symbolic')
for bits in it.product((0,1),repeat=3):
ij,ik,jk=bits
value=ik+ij*jk-ij*ik-ik*jk
cyclic=bits in ((0,1,0),(1,0,1))
require(value==int(cyclic),'symbolic')
L,U=sp.symbols('L U', integer=True)
require(sp.expand(L+(U-L+1)-U)==1,'symbolic')
def examples():
yes={'d':[1,1,2],'m':2,'p':[[0,2]]}
q=reduce('schedule',yes); x=[1,1,0,1,0,0]
require(q['constant']==7 and q['n']==6 and target_value(q,x)==-7,'yes_example')
require(extract_solution('schedule',yes,q,x)==[0,0,1],'yes_example')
no=dict(yes,m=1)
require(not source_optimum('schedule',no) and not any(target_feasible(reduce('schedule',no),b) for b in assignments(reduce('schedule',no)['n'])),'no_example')
cyc={'n':3,'triples':[[0,1,2]]}; q=reduce('cyclic',cyc)
require(target_feasible(q,[1,1,1]) and extract_solution('cyclic',cyc,q,[1,1,1])==[0,1,2],'yes_example')
no={'n':3,'triples':[[0,1,2],[0,2,1]]}
require(not source_optimum('cyclic',no) and not any(target_feasible(reduce('cyclic',no),b) for b in assignments(3)),'no_example')
g={'a':3,'s':[0,1,2,0],'K':2};q=reduce('grouping',g)
require(extract_solution('grouping',g,q,[1,1,1])==[2,1] and target_feasible(q,[1,1,1]),'yes_example')
no=dict(g,K=0)
require(not source_optimum('grouping',no) and not any(target_feasible(reduce('grouping',no),b) for b in assignments(3)),'no_example')
f={'n':3,'arcs':[[0,1,-2],[1,2,3],[2,0,1]]};q=reduce('feedback',f)
require(source_optimum('feedback',f)==-2 and target_value(q,[0,0,1])+q['constant']==-2,'yes_example')
require(extract_solution('feedback',f,q,[0,0,1])==[0],'yes_example')
require(not target_feasible(q,[0,1,0]) and not target_feasible(q,[1,0,1]),'no_example')
def exhaustive():
for n in range(6):
for d in it.product(range(3),repeat=n):
for m in range(min(n+1,3)):
if sum(min(x,n) for x in d)+2*max(d,default=0)>12: continue
verify('schedule',{'d':list(d),'m':m,'p':[]})
for D in range(3):
for m in range(n+1):
inst={'n':n,'D':D,'m':m,'p':[]}
verify('common_schedule',inst,full=reduce('common_schedule',inst)['n']<=12)
if n:
for i,j in it.product(range(n),repeat=2):
verify('schedule',{'d':[1]*n,'m':n,'p':[[i,j],[i,j]]})
for n in range(1,6):
triples=list(it.permutations(range(n),3))
subsets=([t for i,t in enumerate(triples) if mask>>i&1] for mask in range(1<<len(triples))) if n<=3 else ([list(t)] for t in triples)
for ts in subsets: verify('cyclic',{'n':n,'triples':ts})
for a in range(6):
strings=it.chain.from_iterable(it.product(range(a),repeat=l) for l in range(0,5 if a<=3 else 3))
for s in strings:
for K in (range(4) if s else [0]): verify('grouping',{'a':a,'s':list(s),'K':K})
for n in range(4):
possible=list(it.permutations(range(n),2))
for labels in it.product((None,-1,1),repeat=len(possible)):
arcs=[[u,v,w] for (u,v),w in zip(possible,labels) if w is not None]
verify('feedback',{'n':n,'arcs':arcs})
for n in range(1,6):
for v in range(n):
for w in (-3,0,4): verify('feedback',{'n':n,'arcs':[[v,v,w],[v,v,w]]})
def random_families():
for n in (4,5):
for count in (1,4,8):
for _ in range(300):
verify('cyclic',{'n':n,'triples':[RNG.sample(range(n),3) for _ in range(count)]},f'sampled_n{n}_p{count}')
verify('feedback',{'n':n,'arcs':[[RNG.randrange(n),RNG.randrange(n),RNG.randrange(-4,5)] for _ in range(count)]},f'sampled_n{n}_m{count}')
for length in (5,7):
for _ in range(300):
verify('grouping',{'a':n,'s':[RNG.randrange(n) for _ in range(length)],'K':RNG.randrange(8)},f'sampled_a{n}_l{length}')
for count in (0,3,7):
for _ in range(300):
d=[RNG.randrange(4) for _ in range(n)]
inst={'d':d,'m':RNG.randrange(n+1),'p':[[RNG.randrange(n),RNG.randrange(n)] for _ in range(count)]}
verify('schedule',inst,f'sampled_n{n}_p{count}',full=reduce('schedule',inst)['n']<=12)
common={'n':n,'D':RNG.randrange(4),'m':inst['m'],'p':inst['p']}
verify('common_schedule',common,f'sampled_n{n}_p{count}',full=reduce('common_schedule',common)['n']<=12)
@st.composite
def signed_multigraphs(draw):
n=draw(st.integers(1,5))
arcs=draw(st.lists(st.tuples(st.integers(0,n-1),st.integers(0,n-1),st.integers(-6,6)),max_size=8))
return {'n':n,'arcs':[list(a) for a in arcs]}
@st.composite
def precedence_schedules(draw):
n=draw(st.integers(0,5))
d=draw(st.lists(st.integers(0,3),min_size=n,max_size=n))
p=draw(st.lists(st.tuples(st.integers(0,n-1),st.integers(0,n-1)),max_size=8)) if n else []
return {'d':d,'m':draw(st.integers(0,6)),'p':[list(a) for a in p]}
@seed(170183)
@settings(max_examples=300,deadline=None,database=None)
@given(signed_multigraphs())
def hypothesis_feedback(inst):
verify('feedback',inst,'hypothesis')
@seed(170184)
@settings(max_examples=300,deadline=None,database=None)
@given(precedence_schedules())
def hypothesis_scheduling(inst):
verify('schedule',inst,'hypothesis',full=reduce('schedule',inst)['n']<=12)
def numeric_boundaries():
for weight in (MIN,MAX,0):
inst={'n':1,'arcs':[[0,0,weight]]}
verify('feedback',inst,'integer_boundary')
for arcs in ([[0,0,MIN],[0,0,-1]],[[0,0,MAX],[0,0,1]],[[0,1,MAX],[1,0,MAX]]):
try: reduce('feedback',{'n':2,'arcs':arcs})
except OverflowError: require(True,'arithmetic')
else: require(False,'arithmetic')
# Deadlines above n change neither the actual horizon nor the polynomial.
for kind in ('schedule','common_schedule'):
small={'d':[3]*3,'m':2,'p':[]} if kind=='schedule' else {'n':3,'D':3,'m':2,'p':[]}
huge={'d':[10**30]*3,'m':2,'p':[]} if kind=='schedule' else {'n':3,'D':10**30,'m':2,'p':[]}
require(reduce(kind,small)==reduce(kind,huge),'arithmetic')
def main():
symbolic(); examples(); numeric_boundaries()
print('examples, symbolic and boundaries passed',flush=True)
exhaustive(); print('exhaustive families passed',dict(AUDIT),flush=True)
random_families(); print('sampled families passed',dict(AUDIT),flush=True)
hypothesis_feedback(); hypothesis_scheduling()
report={'verdict':'PASS','seed':420217,'hypothesis_seeds':[170183,170184],
'hypothesis_settings':{'max_examples':300,'deadline':None,'database':None},
'checks':dict(AUDIT),'total_checks':sum(AUDIT.values()),'families':dict(FAMILIES),
'exhaustive_families':{'schedule':'n=0..5; deadlines in 0..2; capacities 0..min(n,2); empty precedence; conservative target-size filter <=12; every single duplicated/self precedence at deadline 1 and m=n',
'common_schedule':'n=0..5, D=0..2, m=0..n, empty precedence; target cubes <=12 exact',
'cyclic':'n=1..3 all subsets of ordered distinct triples; n=4,5 every single triple',
'grouping':'a=0..3, every string length 0..4; a=4,5 every string length 0..2; K=0..3 (empty K=0)',
'feedback':'n=0..3 all loopless directed endpoint pairs independently absent, -1, or +1; n=1..5 each duplicated loop at weights -3,0,4'},
'limitations':['Finite exhaustive families and >=300 samples per listed large family; arbitrary integers and all instance sizes are not exhaustively enumerable.',
'Scheduling target cubes above 12 variables use 300 sampled bitstrings and an independently found forward witness; other listed targets are exhaustive.',
'Empty grouping string with positive K treated as outside the stated source domain.',
'Runtime/source type gates and Rust behavior are outside this proof-only adversary.'],
'claim_to_evidence':{'tournament_and_polynomial':'symbolic, penalty, rejection','equivalence':'equivalence',
'every_small_feasible_target_extracts':'extraction','size_bounds':'size','normalized_target':'structure',
'worked_examples':'yes_example, no_example','checked_source_sums':'arithmetic'}}
Path(__file__).with_suffix('.json').write_text(json.dumps(report,indent=2)+'\n')
print(json.dumps(report,indent=2))
if __name__=='__main__': main() |
Collaborator
Author
Verification certificate — Phase 2 group BVerdict: PASS for the stated exact-integer construction and representability contract. Finite testing supplements the bidirectional proof; it does not enumerate unbounded domains. Rust/CLI gates and corpus limitations are separately reported in the PR. Resolved type chain: source Across all groups, 21,000 independently generated normalized targets agreed exactly; zero disagreements. The constructor's scalar checker also compares each expanded polynomial with its unexpanded penalty expression. The JSON report below gives adversary seeds, family sizes, check counts and limitations. adversary_b_report.json{
"status": "PASSED",
"seed": 20261022,
"checks": {
"symbolic": 7,
"size": 23198,
"structure": 11599,
"algebra": 1437094,
"rejection": 1556215,
"equivalence": 203477,
"extraction": 15418,
"yes_example": 6,
"forward": 3927,
"optimum": 2024,
"no_example": 6,
"source_optimum": 1675,
"hypothesis_subset": 350,
"hypothesis_strings": 350,
"numeric_limits": 20,
"malformed": 12,
"audit": 1
},
"instances": {
"Partition": 365,
"SubsetSum": 4364,
"ExactCoverBy3Sets": 1809,
"ThreePartition": 392,
"ThreeDimensionalMatching": 2994,
"ShortestCommonSuperstring": 1675
},
"total_checks": 3255379,
"hypothesis": {
"strategies": 2,
"max_examples_each": 350,
"derandomize": true
},
"coverage": "All binary targets for N<=12, source assignments and permutations independently enumerated; larger targets sampled with all permutations. Exhaustive finite positive-size {1,2,3} algebraic n<=5; T=0..S+1. Set families q=1,2, U=0,3 exhaustive as noted in code, >=300 samples per larger selected q,m. ThreePartition n=0,3 exhaustive sizes<=8; n=6 300 samples. SCS bounded-word families n<=5 and 300 samples per n=4,5. Unbounded source domains cannot be exhaustively enumerated.",
"untested": "Rust implementation, real typed errors and usize allocation overflow; verification is mathematical and Python exact-integer only.",
"claims": {
"polynomial_expansion": "symbolic, algebra",
"iff": "equivalence,forward,optimum",
"extraction": "extraction,rejection",
"sizes": "symbolic,size,structure",
"examples": "yes_example,no_example",
"BigUint": "numeric_limits",
"SCS_optima": "source_optimum,optimum,forward"
}
}
crosscheck-report.json{
"counts": {
"schedule": 1800,
"common_schedule": 1800,
"grouping": 1800,
"feedback": 1800,
"subset": 1800,
"cover": 1800,
"matching": 1800,
"threepartition": 1800,
"superstring": 1800,
"stacker": 1800,
"cyclic": 1500,
"partition": 1500
},
"total": 21000,
"disagreements": 0
}constructor-scalar-report.json{
"structure": 21000,
"size": 21000,
"schedule": 63873,
"common_schedule": 60510,
"grouping": 37800,
"feedback": 37800,
"subset": 18900,
"cover": 18900,
"matching": 18900,
"threepartition": 35400,
"superstring": 22380,
"stacker": 50700,
"cyclic": 37500,
"partition": 18600
}proof-b.typ= Direct subset, assignment, and string QUBO constructions
All Boolean polynomials H=C+sum(i<=j)q(i,j)x_i x_j store energy E=H-C. Coefficients, constants, dimension products and positive/negative coefficient sums are checked for i64/usize representability; numeric failures return typed reduction errors. No floating-point arithmetic. Exact integer feasibility uses DecisionQUBO<i64> bound -C. Zero H iff all nonnegative squared constraints vanish; decode only a target satisfying this threshold, aggregate Or values map identically. Squaring affine sum a_i x_i-b gives C=b^2, diagonals a_i^2-2b a_i, off-diagonals 2a_i a_j. Duplicate indices are folded by Boolean identities.
== Partition
Source positive i64 sizes s_i, nonempty, total S fits i64; selection witness bools and Or. Use H=(2 sum s_i x_i-S)^2, one variable per item. Source selected subtotal and complement bounded by S, so source arithmetic safe. Forward equal halves give H=0; backward H=0 is equal halves, identity bit extraction. No parity precheck needed; odd S gives NO. N=n,E<=n(n-1)/2; O(n^2) coefficient additions. YES (1,2,3), bits (1,1,0): S=6,H=0,E=-36. NO (1,1,1): every residual odd, H>=1.
== SubsetSum
Source positive arbitrary-precision BigUint sizes (empty allowed), nonnegative BigUint target T. Witness bools, Or. H=(sum s_i x_i-T)^2, exactly n bits. Expand with arbitrary-precision signed arithmetic then check each derived coefficient, constant T^2, and coefficient-sum bounds for i64. Never convert inputs prematurely or silently truncate. Algebra gives both directions exactly; identity extraction, identity aggregate. Source uses BigUint and has no fixed-width overflow. N=n,E<=n(n-1)/2; arithmetic bit complexity depends on input magnitude bits. YES (1,2,4),T=3,bits (1,1,0),C=9,H=0. NO same sizes,T=8: maximal sum 7. Empty/T=0 is YES, empty/T>0 is NO whenever target polynomial representable; overflow is a typed construction failure.
== ExactCoverBy3Sets
Universe U divisible by 3, possibly empty; m indexed triples of distinct in-range elements, duplicate triples allowed. One bit per indexed triple. H=sum(u in U)(sum(j contains u)x_j-1)^2. Since every selected triple contributes exactly three incidences, zero penalty forces exactly |U|/3 selected triples and disjoint complete cover. Forward exact cover makes every term zero; backward each element covered exactly once proves source witness. Extract same bits. N=m,E<=m(m-1)/2; coefficients count intersection size, diagonal -3 for every triple; C=|U|. O(|U|+m^2) or incidence construction. YES U=6, triples 012,345,034 select (1,1,0),E=-6. NO U=6, triples 012,013,014 leave 5 uncovered. Empty U/no triples is YES.
== ThreePartition
n=3k positive sizes s_i, B>0, B/4<s_i<B/2, total kB fits i64. The constructor requires a nonempty item list. Source witness maps items to groups 0..k-1 and every group has exactly three items and sum B; Or. Allocate x(i,g), row-major n*k. H=sum_i(sum_g x(i,g)-1)^2 + sum_g(sum_i x(i,g)-3)^2 + sum_g(sum_i s_i x(i,g)-B)^2. All unit penalties, no slack. Forward valid groups zero every term; backward each item has one group and each group has required count and sum. Extract unique group from each row. Source group sums bounded by checked total. N=nk,E<=N(N-1)/2, O(nk^2+kn^2) coefficient additions. YES sizes (2,2,2), B=6,k=1, select all 3 bits,C=3+9+36=48,E=-48. NO sizes (4,4,4,6,6,6),B=15: no triple sums to 15, while all classical domain constraints hold. The formal empty extension has zero bits and energy, but is not in the constructor domain.
== ThreeDimensionalMatching
q>=0, m indexed triples of coordinates in 0..q-1, duplicates allowed. Exactly q selected triples with all coordinates distinct, witness bools, Or. H=sum over each of the 3 coordinate axes and u in 0..q (sum of triples having coordinate u x_j-1)^2. Zero iff perfect matching: each axis covered exactly once; selected count q follows by summing one axis. Forward/backward immediate from equations; extract identical bits. N=m,E<=m(m-1)/2,C=3q; O(q+m^2). YES q=3 triples (0,1,2),(1,0,1),(2,2,0), select all, E=-9. NO q=3 triples (0,0,0),(1,1,1),(1,2,2), coordinate 2 on first axis uncovered. Empty q and triples is YES.
== ShortestCommonSuperstring
Source is a nonempty list of symbol vectors, alphabet bound a, original total length L. Constructor accepts out-of-alphabet input symbols; such instances have no valid source witness and must map to infeasible optimization encoding. Source witness is L Option<usize> entries, a contiguous actual prefix followed by None padding; objective prefix length as Min<i64>.
Preprocess by removing empty strings, duplicates (keep first), and every proper contained string. Retain k strings in original index order. Define o(i,j) as maximum suffix-prefix overlap, i!=j. Allocate k^2 bits x(i,p), meaning string i occupies position p. Objective F=sum_i len(s_i) - sum_{p=0}^{k-2} sum_{i!=j} o(i,j)x(i,p)x(j,p+1). Add P times all row and column one-hot squares, P=U-Low+1 from the objective coefficient interval (use Low to distinguish the bound from original length L). For invalid source symbols add an unconditional P penalty. This guarantees every target energy outside the feasible objective interval; k=0 allowed.
Forward: take a shortest source superstring and list the retained strings by starting occurrence; containment-free implies their ending positions have the same strict order. Between consecutive starts, distance is at least len(previous)-max_overlap(previous,next), or larger if separated. Summing and including the last string yields source length >= path length F. Overlap concatenation of that order is a valid superstring length F, so the optimal values agree. Backward: any permutation can be reconstructed by taking its first string and appending each next string after deleting its prefix of length o(previous,next); the current concatenation ends with the previous string, so all are contained. Removed substrings/duplicates/empties are also contained. The length is exactly F, at most original L. Pad to L with None. All-empty inputs yield the empty prefix and L=0. Reject malformed assignment rows/columns; aggregate restores C on the interval and otherwise Min(None), validating exactly once before decode.
N=k^2<=n^2, E<=n^4; construction naive containment/overlap O(n^2 L^2), assignment interactions O(k^4); source length bounded by checked i64 conversion of L. YES strings 01,10,empty,01,0: retain 01,10, maximal overlap 1, output 010 plus None padding to L=7, objective 3. Infeasible example alphabet 2, strings [0],[1],[2], accepted constructor but no valid source superstring; unconditional penalty makes all target values map Min(None). Nonempty feasible inputs always have a concatenation, so ordinary NO example inapplicable.
constructor.pyfrom collections import defaultdict
from itertools import product, permutations, combinations
import json,random,heapq
from pathlib import Path
import sympy as sy
class Poly:
def __init__(self,n): self.n=n;self.c=0;self.q=defaultdict(int)
def add(self,i,j,v): self.q[min(i,j),max(i,j)]+=v
def sq(self,terms,b):
self.c+=b*b
for z,(i,a) in enumerate(terms):
self.add(i,i,a*a-2*b*a)
for j,d in terms[z+1:]: self.add(i,j,2*a*d)
def interval(self): return self.c+sum(min(0,v) for v in self.q.values()),self.c+sum(max(0,v) for v in self.q.values())
def done(self,bound=None,interval=None):
lo,hi=self.interval();clo=lo-self.c;chi=hi-self.c
if min(self.c,clo)<-(1<<63) or max(self.c,chi)>(1<<63)-1:raise OverflowError
return dict(n=self.n,constant=self.c,entries=[[i,j,c] for (i,j),c in sorted(self.q.items()) if c],bound=bound,low=None if interval is None else interval[0]-self.c,high=None if interval is None else interval[1]-self.c)
def pi(n,i,j):return i*(2*n-i-1)//2+j-i-1
def tournament(q,n,p):
for i,j,k in combinations(range(n),3):
a,b,c=pi(n,i,j),pi(n,i,k),pi(n,j,k)
for x,y,v in [(b,b,p),(a,c,p),(a,b,-p),(b,c,-p)]:q.add(x,y,v)
def assignment(q,n,k,p=1):
for i in range(n):
z=Poly(q.n);z.sq([(i*k+j,1) for j in range(k)],1);merge(q,z,p)
def merge(q,z,p=1):
q.c+=p*z.c
for (a,b),v in z.q.items():q.add(a,b,p*v)
def perm(q,n,p):
assignment(q,n,n,p)
for t in range(n):
z=Poly(q.n);z.sq([(i*n+t,1) for i in range(n)],1);merge(q,z,p)
def dist(v,arcs,edges,s,t):
if s==t:return 0
adj=[[] for _ in range(v)]
for a,b,w in arcs:adj[a].append((b,w))
for a,b,w in edges:adj[a].append((b,w));adj[b].append((a,w))
ds=[(1<<63)-1]*v;ds[s]=0;h=[(0,-s)]
while h:
c,a=heapq.heappop(h);a=-a
if c>ds[a]:continue
if a==t:return c
for b,w in adj[a]:
d=c+w
if d>(1<<63)-1:return None
if d<ds[b]:ds[b]=d;heapq.heappush(h,(d,-b))
return None
def contained(a,b):return not a or any(b[t:t+len(a)]==a for t in range(len(b)-len(a)+1))
def overlap(a,b):return max([0]+[i for i in range(1,min(len(a),len(b))+1) if a[-i:]==b[:i]])
def reduce(kind,d):
if kind in ['schedule','common_schedule']:
deadlines=d.get('d',[d.get('D',0)]*d.get('n',0));n=len(deadlines);lens=[min(x,n) for x in deadlines];m=d['m'];offset=[];s=0
for h in lens:offset.append(s);s+=h
caps=[]
for t in range(max(lens,default=0)):
row=[(offset[i]+t,1) for i,h in enumerate(lens) if t<h]
if m<len(row):
row += [(s+j,1<<j) for j in range(m.bit_length())];s+=m.bit_length();caps.append(row)
q=Poly(s)
for o,h in zip(offset,lens):q.sq([(o+t,1) for t in range(h)],1)
for row in caps:q.sq(row,m)
for i,j in d['p']:
for t in range(lens[i]):
for u in range(min(t+1,lens[j])):q.add(offset[i]+t,offset[j]+u,1)
elif kind in ['cyclic','grouping','feedback']:
n=d.get('n',d.get('a'));q=Poly(n*(n-1)//2)
if kind=='cyclic':
tournament(q,n,1)
for a,b,c in d['triples']:
row=[];rhs=2
for i,j in [(a,b),(b,c),(c,a)]:
if i<j:row.append((pi(n,i,j),1))
else:row.append((pi(n,j,i),-1));rhs-=1
q.sq(row,rhs)
elif kind=='grouping':
for pos,i in enumerate(d['s']):
for j in d['s'][pos+1:]:
if i<j:q.c+=1;q.add(pi(n,i,j),pi(n,i,j),-1)
elif i>j:q.add(pi(n,j,i),pi(n,j,i),1)
M=len(d['s'])*(len(d['s'])-1)//2;tournament(q,n,M+1)
return q.done(min(d['K'],M)-q.c)
else:
ws=[w for _,_,w in d['arcs']]
if sum(min(w,0) for w in ws)<-(1<<63) or sum(max(w,0) for w in ws)>(1<<63)-1:raise OverflowError
for a,b,w in d['arcs']:
if w<0 or a==b:q.c+=w
elif a<b:q.c+=w;q.add(pi(n,a,b),pi(n,a,b),-w)
else:q.add(pi(n,b,a),pi(n,b,a),w)
L,U=q.interval();tournament(q,n,U-L+1);return q.done(interval=(L,U))
elif kind in ['partition','subset']:
q=Poly(len(d['s']));q.sq([(i,x*(2 if kind=='partition' else 1)) for i,x in enumerate(d['s'])],sum(d['s']) if kind=='partition' else d['T'])
elif kind in ['cover','matching']:
ts=d['triples'];q=Poly(len(ts))
for axis in range(3 if kind=='matching' else 1):
for u in range(d['u']):q.sq([(j,1) for j,t in enumerate(ts) if (t[axis]==u if kind=='matching' else u in t)],1)
elif kind=='threepartition':
n=len(d['s']);k=n//3;q=Poly(n*k);assignment(q,n,k)
for g in range(k):q.sq([(i*k+g,1) for i in range(n)],3);q.sq([(i*k+g,w) for i,w in enumerate(d['s'])],d['B'])
elif kind=='superstring':
ss=d['strings'];ss=[s for i,s in enumerate(ss) if s and not any(contained(s,t) and (len(s)<len(t) or j<i) for j,t in enumerate(ss) if i!=j)]
n=len(ss);q=Poly(n*n);q.c=sum(map(len,ss))
for i in range(n):
for j in range(n):
if i!=j:
for p in range(n-1):q.add(i*n+p,j*n+p+1,-overlap(ss[i],ss[j]))
L,U=q.interval();P=U-L+1;perm(q,n,P)
if any(c>=d['a'] for s in d['strings'] for c in s):q.c+=P
return q.done(interval=(L,U))
elif kind=='stacker':
arcs=d['arcs'];n=len(arcs);q=Poly(n*n);q.c=sum(a[2] for a in arcs);D=[[dist(d['v'],arcs,d['edges'],a[1],b[0]) for b in arcs] for a in arcs]
if q.c+n*max([0]+[x for r in D for x in r if x is not None])>(1<<63)-1:raise OverflowError
missing=[]
for i in range(n):
for j in range(n):
if n>1 and i==j:continue
for p in range(n):
a,b=i*n+p,j*n+(p+1)%n
if D[i][j] is None:missing.append((a,b))
else:q.add(a,b,D[i][j])
L,U=q.interval();P=U-L+1;perm(q,n,P)
for a,b in missing:q.add(a,b,P)
return q.done(interval=(L,U))
else:raise ValueError(kind)
return q.done(-q.c)
def energy(q,x):return sum(c*x[i]*x[j] for i,j,c in q['entries'])
def run():
counts=defaultdict(int);rng=random.Random(20261022)
n,k,H=sy.symbols('n k H',nonnegative=True)
for f in [n*(n-1)/2,n*k,n*n,2*n*H]:assert sy.expand(f*f-f*f)==0;counts['symbolic']+=1
# Exhaustive selection residuals independently computed, including every target witness.
for size in range(6):
for _ in range(300):
s=[rng.randrange(1,8) for i in range(size)];T=rng.randrange(25)
for kind,d in [('subset',{'s':s,'T':T})]+([('partition',{'s':s})] if s else []):
q=reduce(kind,d)
assert q['n']==size and len([1 for i,j,c in q['entries'] if i!=j])<=size*(size-1)//2;counts['size']+=1
assert all(0<=i<=j<size for i,j,c in q['entries']);counts['structure']+=1
for bits in product([0,1],repeat=size):
selected=sum(a*b for a,b in zip(s,bits));valid=selected==T if kind=='subset' else selected==sum(s)-selected
assert (energy(q,bits)<=q['bound'])==valid;counts['forward_backward']+=1;counts['extraction']+=valid
examples=[('partition',{'s':[1,2,3]},[1,1,0],True),('partition',{'s':[1,1,1]},[1,0,0],False),('cover',{'u':6,'triples':[[0,1,2],[3,4,5],[0,3,4]]},[1,1,0],True),('cover',{'u':6,'triples':[[0,1,2],[0,1,3],[0,1,4]]},[1,0,0],False)]
for kind,d,x,want in examples:
q=reduce(kind,d);assert (energy(q,x)<=q['bound'])==want;counts['yes_example' if want else 'no_example']+=1
Path(__file__).with_name('constructor-report.json').write_text(json.dumps(counts,indent=2));print(dict(counts))
if __name__=='__main__':run()adversary_b.py"""Independent proof-only adversary. No constructor or Rust imports.
JSON schemas by kind:
Partition: {sizes:[positive int]}; SubsetSum: {sizes:[positive int],target:int};
ExactCoverBy3Sets: {universe:int,triples:[[int,int,int]]};
ThreePartition: {sizes:[positive int],bound:int};
ThreeDimensionalMatching: {q:int,triples:[[int,int,int]]};
ShortestCommonSuperstring: {alphabet:int,strings:[[int]]}.
All target entries upper triangular; energy excludes constant.
low/high bound stored energy, not restored source objective.
"""
import itertools as it
import json
import math
import random
from collections import Counter, defaultdict
from pathlib import Path
I64_MIN=-(1<<63); I64_MAX=(1<<63)-1
COUNTS=Counter(); INSTANCES=Counter(); rng=random.Random(20261022)
def contains(a,b):
return any(tuple(a[i:i+len(b)])==tuple(b) for i in range(len(a)-len(b)+1))
def retained(z):
strings=[tuple(s) for s in z['strings']]
unique=list(dict.fromkeys(s for s in strings if s))
return [s for s in unique if not any(len(t)>len(s) and contains(t,s) for t in unique)]
def overlap(a,b):
return max(d for d in range(min(len(a),len(b))+1) if a[len(a)-d:]==b[:d])
def reduce(kind,z):
q=defaultdict(int); C=0
def square(items,b,scale=1):
nonlocal C
folded=defaultdict(int)
for i,a in items: folded[i]+=a
C+=scale*b*b
for i,a in folded.items(): q[i,i]+=scale*(a*a-2*b*a)
for (i,a),(j,c) in it.combinations(folded.items(),2): q[min(i,j),max(i,j)]+=2*scale*a*c
low=high=None
if kind in ('Partition','SubsetSum'):
ss=z['sizes']; n=len(ss)
b=sum(ss) if kind=='Partition' else z['target']
multiplier=2 if kind=='Partition' else 1
square(enumerate([multiplier*s for s in ss]),b)
elif kind in ('ExactCoverBy3Sets','ThreeDimensionalMatching'):
ts=z['triples']; n=len(ts)
if kind=='ExactCoverBy3Sets':
for u in range(z['universe']): square(((i,1) for i,t in enumerate(ts) if u in t),1)
else:
for axis in range(3):
for u in range(z['q']): square(((i,1) for i,t in enumerate(ts) if t[axis]==u),1)
elif kind=='ThreePartition':
ss=z['sizes']; k=len(ss)//3; n=len(ss)*k
for i in range(len(ss)): square(((i*k+g,1) for g in range(k)),1)
for g in range(k):
square(((i*k+g,1) for i in range(len(ss))),3)
square(((i*k+g,s) for i,s in enumerate(ss)),z['bound'])
elif kind=='ShortestCommonSuperstring':
ss=retained(z); k=len(ss); n=k*k; C=sum(map(len,ss))
for p in range(k-1):
for i in range(k):
for j in range(k):
if i!=j:
a,b=i*k+p,j*k+p+1
q[min(a,b),max(a,b)]-=overlap(ss[i],ss[j])
low=C+sum(v for v in q.values() if v<0); high=C
penalty=high-low+1
for i in range(k): square(((i*k+p,1) for p in range(k)),1,penalty)
for p in range(k): square(((i*k+p,1) for i in range(k)),1,penalty)
if any(c<0 or c>=z['alphabet'] for s in z['strings'] for c in s): C+=penalty
low-=C; high-=C
else: raise ValueError(kind)
entries=[[i,j,v] for (i,j),v in sorted(q.items()) if v]
vals=[C]+[v for _,_,v in entries]+[sum(min(v,0) for _,_,v in entries),sum(max(v,0) for _,_,v in entries)]
bound=-C if low is None else None
vals += [v for v in (bound,low,high) if v is not None]
if any(v<I64_MIN or v>I64_MAX for v in vals): raise OverflowError('derived i64 bound')
return dict(n=n,constant=C,entries=entries,bound=bound,low=low,high=high)
def target_value(t,x):
if len(x)!=t['n'] or any(v not in (0,1) for v in x): raise ValueError('nonbinary target')
return sum(c*x[i]*x[j] for i,j,c in t['entries'])
def target_feasible(t,x):
e=target_value(t,x)
return e<=t['bound'] if t['bound'] is not None else t['low']<=e<=t['high']
def source_value(kind,z,w):
if kind in ('Partition','SubsetSum'):
if len(w)!=len(z['sizes']) or any(x not in (0,1) for x in w): return False
a=sum(s for s,x in zip(z['sizes'],w) if x)
return 2*a==sum(z['sizes']) if kind=='Partition' else a==z['target']
if kind in ('ExactCoverBy3Sets','ThreeDimensionalMatching'):
if len(w)!=len(z['triples']) or any(x not in (0,1) for x in w): return False
ts=[t for t,x in zip(z['triples'],w) if x]
if kind=='ExactCoverBy3Sets': return sorted(u for t in ts for u in t)==list(range(z['universe']))
return len(ts)==z['q'] and all(sorted(t[a] for t in ts)==list(range(z['q'])) for a in range(3))
if kind=='ThreePartition':
k=len(z['sizes'])//3
return len(w)==len(z['sizes']) and all(0<=g<k for g in w) and all(sum(g==h for g in w)==3 and sum(s for s,g in zip(z['sizes'],w) if g==h)==z['bound'] for h in range(k))
if len(w)!=sum(map(len,z['strings'])): return None
prefix=[]; ended=False
for c in w:
if c is None: ended=True
elif ended or c<0 or c>=z['alphabet']: return None
else: prefix.append(c)
return len(prefix) if all(contains(prefix,s) for s in z['strings']) else None
def extract_solution(kind,z,t,x):
if not target_feasible(t,x): raise ValueError('noncertifying target')
if kind=='ThreePartition':
k=len(z['sizes'])//3
return [next(g for g in range(k) if x[i*k+g]) for i in range(len(z['sizes']))]
if kind=='ShortestCommonSuperstring':
ss=retained(z); k=len(ss)
if not all(sum(x[i*k+p] for p in range(k))==1 for i in range(k)) or not all(sum(x[i*k+p] for i in range(k))==1 for p in range(k)): raise ValueError('bad permutation')
order=[next(i for i in range(k) if x[i*k+p]) for p in range(k)]
out=list(ss[order[0]]) if order else []
for i,j in zip(order,order[1:]): out.extend(ss[j][overlap(ss[i],ss[j]):])
return out+[None]*(sum(map(len,z['strings']))-len(out))
return list(x)
def residual(kind,z,x):
if kind=='Partition': return (2*sum(s*b for s,b in zip(z['sizes'],x))-sum(z['sizes']))**2
if kind=='SubsetSum': return (sum(s*b for s,b in zip(z['sizes'],x))-z['target'])**2
if kind=='ExactCoverBy3Sets': return sum((sum(x[j] for j,t in enumerate(z['triples']) if u in t)-1)**2 for u in range(z['universe']))
if kind=='ThreeDimensionalMatching': return sum((sum(x[j] for j,t in enumerate(z['triples']) if t[a]==u)-1)**2 for a in range(3) for u in range(z['q']))
k=len(z['sizes'])//3
return sum((sum(x[i*k+g] for g in range(k))-1)**2 for i in range(len(z['sizes'])))+sum((sum(x[i*k+g] for i in range(len(z['sizes'])))-3)**2+(sum(s*x[i*k+g] for i,s in enumerate(z['sizes']))-z['bound'])**2 for g in range(k))
def check(ok,section):
COUNTS[section]+=1
assert ok,section
def brute_source_opt(z):
if any(c>=z['alphabet'] or c<0 for s in z['strings'] for c in s): return None
for length in range(max(map(len,z['strings']),default=0),sum(map(len,z['strings']))+1):
for w in it.product(range(z['alphabet']),repeat=length):
if all(contains(tuple(w),tuple(s)) for s in z['strings']): return length
return None
def verify(kind,z,full=True):
t=reduce(kind,z); INSTANCES[kind]+=1; n=t['n']; es=t['entries']
expected=len(z['sizes']) if kind in ('Partition','SubsetSum') else len(z['triples']) if kind in ('ExactCoverBy3Sets','ThreeDimensionalMatching') else len(z['sizes'])**2//3 if kind=='ThreePartition' else len(retained(z))**2
check(n==expected,'size'); check(sum(i!=j for i,j,c in es)<=n*(n-1)//2,'size')
check(all(0<=i<=j<n and c!=0 for i,j,c in es) and len({(i,j) for i,j,c in es})==len(es),'structure')
exhaustive=full and n<=12
xs=it.product((0,1),repeat=n) if exhaustive else (tuple(rng.randrange(2) for _ in range(n)) for _ in range(30))
found=False; best=None
for x in xs:
e=target_value(t,x); yes=target_feasible(t,x)
if kind!='ShortestCommonSuperstring': check(e+t['constant']==residual(kind,z,x),'algebra')
if yes:
found=True; w=extract_solution(kind,z,t,x); val=source_value(kind,z,w)
check(val is not None and (val if kind!='ShortestCommonSuperstring' else val==e+t['constant']),'extraction')
if kind=='ShortestCommonSuperstring': best=val if best is None else min(best,val)
else:
try: extract_solution(kind,z,t,x)
except ValueError: check(True,'rejection')
else: check(False,'rejection')
if kind not in ('ThreePartition','ShortestCommonSuperstring'): check(yes==source_value(kind,z,x),'equivalence')
if kind=='ThreePartition':
k=len(z['sizes'])//3
possible=False
for w in it.product(range(k),repeat=len(z['sizes'])):
yes=source_value(kind,z,w)
if yes:
possible=True; x=[int(w[i]==g) for i in range(len(w)) for g in range(k)]
check(target_feasible(t,x),'forward')
if exhaustive: check(found==possible,'optimum')
if kind=='ShortestCommonSuperstring':
k=len(retained(z)); perm_best=None
for order in it.permutations(range(k)):
x=[int(order[p]==i) for i in range(k) for p in range(k)]
if target_feasible(t,x):
v=source_value(kind,z,extract_solution(kind,z,t,x))
check(v==target_value(t,x)+t['constant'],'forward')
perm_best=v if perm_best is None else min(perm_best,v)
if exhaustive: check(best==perm_best,'optimum')
if z['alphabet']<=2 and max(map(len,z['strings']),default=0)<=3: check(perm_best==brute_source_opt(z),'source_optimum')
return t
def examples():
cases=[('Partition',{'sizes':[1,2,3]},[1,1,0],36,-36),('SubsetSum',{'sizes':[1,2,4],'target':3},[1,1,0],9,-9),('ExactCoverBy3Sets',{'universe':6,'triples':[[0,1,2],[3,4,5],[0,3,4]]},[1,1,0],6,-6),('ThreePartition',{'sizes':[2,2,2],'bound':6},[1,1,1],48,-48),('ThreeDimensionalMatching',{'q':3,'triples':[[0,1,2],[1,0,1],[2,2,0]]},[1,1,1],9,-9)]
for kind,z,x,c,e in cases:
t=verify(kind,z); check(t['constant']==c and target_value(t,x)==e and target_feasible(t,x),'yes_example')
no=[('Partition',{'sizes':[1,1,1]}),('SubsetSum',{'sizes':[1,2,4],'target':8}),('ExactCoverBy3Sets',{'universe':6,'triples':[[0,1,2],[0,1,3],[0,1,4]]}),('ThreePartition',{'sizes':[4,4,4,6,6,6],'bound':15}),('ThreeDimensionalMatching',{'q':3,'triples':[[0,0,0],[1,1,1],[1,2,2]]}),('ShortestCommonSuperstring',{'alphabet':2,'strings':[[0],[1],[2]]})]
for kind,z in no:
t=verify(kind,z); check(not any(target_feasible(t,x) for x in it.product((0,1),repeat=t['n'])),'no_example')
z={'alphabet':2,'strings':[[0,1],[1,0],[],[0,1],[0]]}; t=verify('ShortestCommonSuperstring',z)
w=extract_solution('ShortestCommonSuperstring',z,t,[1,0,0,1]); check(w==[0,1,0,None,None,None,None] and source_value('ShortestCommonSuperstring',z,w)==3,'yes_example')
def main():
from hypothesis import given,settings,strategies as st
import sympy as sp
a,b,c,x,y=sp.symbols('a b c x y'); expanded=sp.expand((a*x+b*y-c)**2).subs(x*x,x).subs(y*y,y)
check(sp.expand(expanded-(c*c+(a*a-2*a*c)*x+(b*b-2*b*c)*y+2*a*b*x*y))==0,'symbolic')
n,k,m=sp.symbols('n k m',integer=True,nonnegative=True)
for lhs,rhs in [(n,n),(m,m),(3*k*k,(3*k)*k),(k*k,k**2),(n*(n-1)/2,sp.binomial(n,2)),(k**4,(k*k)**2)]: check(sp.simplify(sp.expand_func(lhs-rhs))==0,'symbolic')
examples()
for n in range(1,6):
for ss in it.product(range(1,4),repeat=n):
verify('Partition',{'sizes':ss})
for target in range(sum(ss)+2): verify('SubsetSum',{'sizes':ss,'target':target})
for target in range(4): verify('SubsetSum',{'sizes':[],'target':target})
for m in range(6): verify('ExactCoverBy3Sets',{'universe':3,'triples':[[0,1,2]]*m})
verify('ExactCoverBy3Sets',{'universe':0,'triples':[]}); verify('ThreeDimensionalMatching',{'q':0,'triples':[]})
for m in range(6): verify('ThreeDimensionalMatching',{'q':1,'triples':[[0,0,0]]*m})
triples=list(it.product(range(2),repeat=3))
for m in range(4):
for ts in it.product(triples,repeat=m): verify('ThreeDimensionalMatching',{'q':2,'triples':ts})
triples=list(it.combinations(range(6),3))
for m in range(6):
for _ in range(300): verify('ExactCoverBy3Sets',{'universe':6,'triples':[rng.choice(triples) for _ in range(m)]})
for q in range(2,6):
for m in range(4,6):
for _ in range(300): verify('ThreeDimensionalMatching',{'q':q,'triples':[[rng.randrange(q) for _ in range(3)] for _ in range(m)]})
verify('ThreePartition',{'sizes':[],'bound':1})
for ss in it.product(range(1,9),repeat=3):
B=sum(ss)
if all(B<4*s and 2*s<B for s in ss): verify('ThreePartition',{'sizes':ss,'bound':B})
for _ in range(300):
while True:
ss=[rng.randrange(3,8) for _ in range(6)]; B=sum(ss)//2
if sum(ss)==2*B and all(B<4*s and 2*s<B for s in ss): break
verify('ThreePartition',{'sizes':ss,'bound':B})
words=[(),(0,),(1,),(0,0),(0,1),(1,0),(1,1)]
for n in range(1,4):
for ss in it.product(words,repeat=n): verify('ShortestCommonSuperstring',{'alphabet':2,'strings':ss})
for n in (4,5):
for ss in it.product(words[:3],repeat=n): verify('ShortestCommonSuperstring',{'alphabet':2,'strings':ss})
for _ in range(300):
ss=[tuple(rng.randrange(3) for _ in range(rng.randrange(4))) for _ in range(n)]
verify('ShortestCommonSuperstring',{'alphabet':2,'strings':ss})
@settings(max_examples=350,deadline=None,derandomize=True,database=None)
@given(st.lists(st.integers(1,30),min_size=0,max_size=5),st.integers(0,160))
def subset_property(ss,T): verify('SubsetSum',{'sizes':ss,'target':T}); check(True,'hypothesis_subset')
@settings(max_examples=350,deadline=None,derandomize=True,database=None)
@given(st.lists(st.lists(st.integers(0,2),min_size=0,max_size=3),min_size=1,max_size=5))
def strings_property(ss): verify('ShortestCommonSuperstring',{'alphabet':2,'strings':ss}); check(True,'hypothesis_strings')
subset_property(); strings_property()
for huge in [1<<32,1<<63,1<<64,1<<128,1<<256]:
for z in [{'sizes':[huge],'target':0},{'sizes':[],'target':huge},{'sizes':[huge],'target':huge}]:
try: reduce('SubsetSum',z)
except OverflowError: check(True,'numeric_limits')
else: check(False,'numeric_limits')
cancellation=reduce('SubsetSum',{'sizes':[1<<32],'target':1<<31})
check(cancellation['entries']==[] and cancellation['constant']==1<<62,'numeric_limits')
for T in [0,2_000_000_000]:
try: reduce('SubsetSum',{'sizes':[1_000_000_000]*4,'target':T})
except OverflowError: check(True,'numeric_limits')
else: check(False,'numeric_limits')
for kind,z in [('Partition',{'sizes':[1,1]}),('SubsetSum',{'sizes':[1],'target':1}),('ExactCoverBy3Sets',{'universe':3,'triples':[[0,1,2]]}),('ThreePartition',{'sizes':[2,2,2],'bound':6}),('ThreeDimensionalMatching',{'q':1,'triples':[[0,0,0]]}),('ShortestCommonSuperstring',{'alphabet':2,'strings':[[0]]})]:
t=reduce(kind,z)
for x in [[0]*(t['n']+1),[2]*t['n']]:
try: extract_solution(kind,z,t,x)
except ValueError: check(True,'malformed')
else: check(False,'malformed')
root=math.isqrt(I64_MAX)
check(reduce('SubsetSum',{'sizes':[],'target':root})['constant']==root*root,'numeric_limits')
try: reduce('SubsetSum',{'sizes':[],'target':root+1})
except OverflowError: check(True,'numeric_limits')
else: check(False,'numeric_limits')
check(sum(COUNTS.values())>=10000 and COUNTS['algebra']>=10000,'audit')
report={'status':'PASSED','seed':20261022,'checks':dict(COUNTS),'instances':dict(INSTANCES),'total_checks':sum(COUNTS.values()),'hypothesis':{'strategies':2,'max_examples_each':350,'derandomize':True},'coverage':'All binary targets for N<=12, source assignments and permutations independently enumerated; larger targets sampled with all permutations. Exhaustive finite positive-size {1,2,3} algebraic n<=5; T=0..S+1. Set families q=1,2, U=0,3 exhaustive as noted in code, >=300 samples per larger selected q,m. ThreePartition n=0,3 exhaustive sizes<=8; n=6 300 samples. SCS bounded-word families n<=5 and 300 samples per n=4,5. Unbounded source domains cannot be exhaustively enumerated.','untested':'Rust implementation, real typed errors and usize allocation overflow; verification is mathematical and Python exact-integer only.','claims':{'polynomial_expansion':'symbolic, algebra','iff':'equivalence,forward,optimum','extraction':'extraction,rejection','sizes':'symbolic,size,structure','examples':'yes_example,no_example','BigUint':'numeric_limits','SCS_optima':'source_optimum,optimum,forward'}}
Path(__file__).with_name('adversary_b_report.json').write_text(json.dumps(report,indent=2)+'\n'); print(json.dumps(report,indent=2))
if __name__=='__main__': main() |
Collaborator
Author
Verification certificate — Phase 2 group CVerdict: PASS for the stated exact-integer construction and representability contract. Finite testing supplements the bidirectional proof; it does not enumerate unbounded domains. Rust/CLI gates and corpus limitations are separately reported in the PR. Resolved type chain: source Across all groups, 21,000 independently generated normalized targets agreed exactly; zero disagreements. The constructor's scalar checker also compares each expanded polynomial with its unexpanded penalty expression. The JSON report below gives adversary seeds, family sizes, check counts and limitations. adversary_c_run.json{
"status": "PASS",
"seed": 22102026,
"audit": {
"backward": 742060,
"examples": 5,
"extraction": 99543,
"forward": 170572,
"hypothesis_general": 500,
"hypothesis_repeated": 500,
"numeric_rejection": 3,
"numeric_semantics": 9,
"objective": 94074,
"optimum": 4234,
"size": 6409,
"structure": 12818,
"symbolic": 3,
"target_numeric_rejection": 1
},
"total_checks": 1130731,
"hypothesis_examples": 1000,
"random_instances": 5400,
"full_source_permutations_through_n": 5,
"full_target_configurations_through_n": 3,
"extra_full_target_n4_instances": 2
}
crosscheck-report.json{
"counts": {
"schedule": 1800,
"common_schedule": 1800,
"grouping": 1800,
"feedback": 1800,
"subset": 1800,
"cover": 1800,
"matching": 1800,
"threepartition": 1800,
"superstring": 1800,
"stacker": 1800,
"cyclic": 1500,
"partition": 1500
},
"total": 21000,
"disagreements": 0
}constructor-scalar-report.json{
"structure": 21000,
"size": 21000,
"schedule": 63873,
"common_schedule": 60510,
"grouping": 37800,
"feedback": 37800,
"subset": 18900,
"cover": 18900,
"matching": 18900,
"threepartition": 35400,
"superstring": 22380,
"stacker": 50700,
"cyclic": 37500,
"partition": 18600
}proof-c.typ= StackerCrane to QUBO<i64>
Source has n required directed arcs with nonnegative i64 lengths and optional nonnegative undirected travel edges, vertices 0..v-1. Parallel arcs/edges and directed loops are allowed. Source witness is a permutation of arc indices, not a list of traversed vertices; its objective visits each required arc in that order and inserts a connector between each consecutive pair, including wraparound. Connectors can traverse required directed arcs again and optional edges in either direction. Empty order has cost zero. Values Min<i64> on both endpoints.
Preprocess d(i,j), the connector distance from head(i) to tail(j), using the source's exact Dijkstra routine and adjacency order. Source routine has two representational details: distance i64::MAX is the unreached sentinel; any overflowing explored cost+edge returns None for that query, even if some other path is finite. Preserve these semantics by reusing that routine, rather than substituting another shortest-path algorithm. An unavailable d prohibits that transition; a None can mean source-defined overflow as well as disconnectedness. All lengths are nonnegative; no negative-cycle complication exists.
Let B=sum required lengths. Before target construction require B and B+n*max_available_connector to fit i64, guaranteeing every source route accumulation fits (even when source itself would return None on overflow, this reduction returns typed numeric failure instead of misclassifying it). Dijkstra query overflow still has its original None meaning. Allocate n^2 x(i,p) arc-position bits. Objective F=B+sum_p sum_i,j d(i,j)x(i,p)x(j,(p+1) mod n), omitting unavailable connectors and i=j when n>1. When n=1 use its single diagonal connector once; when n=0 F=0. Compute coefficient interval L,U for F and P=U-L+1. Add P times row/column one-hot squares and P*x(i,p)*x(j,next) for every unavailable connector (including diagonal for n=1). Store H-C. Feasible energy interval [L-C,U-C]. Every penalty is a nonnegative integer multiple of P, and invalid H>=L+P>U.
Forward: each feasible source arc permutation picks one bit per row/column and only available connector terms; F is exactly the source closed-walk evaluation in that order. Thus its target energy recovers the same objective. Backward: a target within the feasible interval has zero penalties, therefore gives an arc permutation and all connectors exist; the source route uses exactly the precomputed queries, and its checked accumulation equals F. Infeasible sources have all target values outside the interval. All target optima recover a source optimum when one exists; completed minima outside interval map to Min(None); otherwise add C. Extraction validates once, reads unique position from each row, inverts positions to arc sequence, and returns the source-native witness. Each connector query has a realizing walk under the same algorithm; concatenate those walks with required arcs if an explicit physical route is wanted, but the model's witness stores the arc sequence only.
N=n^2 exactly, E<=n^4. Building target O(n^4) additions; n^2 Dijkstra queries each O((v+e+n) log(v+e+n+1)), auxiliary preprocessing storage O(n^2+v+e), plus O(n^4) target coefficients. Reuse a single mixed adjacency. Source prefix safety follows nonnegative terms and the bound above.
YES n=3, arcs 0->1,1->2,2->0, each length 1, no optional edges: order (0,1,2), source cost 3, all connectors zero. Other orders have positive extra travel; minimum 3. NO n=3, vertices 6, required disjoint arcs 0->1,2->3,4->5 lengths 1 and no optional edges: no return connectors, all target configurations penalized. Empty source zero optimum. One arc 0->1 length 2 and undirected edge 0--1 length 3 gives cost 5; one loop length 2 gives cost 2.
Operational connector specification: build each adjacency list by appending required directed arcs in input order, then optional undirected edges in input order, appending u->v then v->u for each edge. source==target returns zero immediately. Distances initialize to i64::MAX; source=0. Heap minimizes distance and, on equal distances, pops the larger vertex index first (Rust BinaryHeap<(Reverse<i64>,usize)>). On pop, skip if cost>dist[node], then return cost if node==target, otherwise scan adjacency in append order. An overflowing cost+length immediately returns None for the entire query. Relax only if next_cost<dist[next], and push updated pair. Exhausted heap returns None. This specification is part of the exact source contract for this reduction.
For canonical target construction, omit i=j transitions in both objective and unavailable-connector penalties whenever n>1; two positions cannot select the same arc under assignment constraints. Check all target constants, coefficients, positive/negative energy sums and shifted feasible bounds independently for i64 representability, in addition to the source route-accumulation guard. An intermediate or final unrepresentable stored number returns typed numeric failure.
constructor.pyfrom collections import defaultdict
from itertools import product, permutations, combinations
import json,random,heapq
from pathlib import Path
import sympy as sy
class Poly:
def __init__(self,n): self.n=n;self.c=0;self.q=defaultdict(int)
def add(self,i,j,v): self.q[min(i,j),max(i,j)]+=v
def sq(self,terms,b):
self.c+=b*b
for z,(i,a) in enumerate(terms):
self.add(i,i,a*a-2*b*a)
for j,d in terms[z+1:]: self.add(i,j,2*a*d)
def interval(self): return self.c+sum(min(0,v) for v in self.q.values()),self.c+sum(max(0,v) for v in self.q.values())
def done(self,bound=None,interval=None):
lo,hi=self.interval();clo=lo-self.c;chi=hi-self.c
if min(self.c,clo)<-(1<<63) or max(self.c,chi)>(1<<63)-1:raise OverflowError
return dict(n=self.n,constant=self.c,entries=[[i,j,c] for (i,j),c in sorted(self.q.items()) if c],bound=bound,low=None if interval is None else interval[0]-self.c,high=None if interval is None else interval[1]-self.c)
def pi(n,i,j):return i*(2*n-i-1)//2+j-i-1
def tournament(q,n,p):
for i,j,k in combinations(range(n),3):
a,b,c=pi(n,i,j),pi(n,i,k),pi(n,j,k)
for x,y,v in [(b,b,p),(a,c,p),(a,b,-p),(b,c,-p)]:q.add(x,y,v)
def assignment(q,n,k,p=1):
for i in range(n):
z=Poly(q.n);z.sq([(i*k+j,1) for j in range(k)],1);merge(q,z,p)
def merge(q,z,p=1):
q.c+=p*z.c
for (a,b),v in z.q.items():q.add(a,b,p*v)
def perm(q,n,p):
assignment(q,n,n,p)
for t in range(n):
z=Poly(q.n);z.sq([(i*n+t,1) for i in range(n)],1);merge(q,z,p)
def dist(v,arcs,edges,s,t):
if s==t:return 0
adj=[[] for _ in range(v)]
for a,b,w in arcs:adj[a].append((b,w))
for a,b,w in edges:adj[a].append((b,w));adj[b].append((a,w))
ds=[(1<<63)-1]*v;ds[s]=0;h=[(0,-s)]
while h:
c,a=heapq.heappop(h);a=-a
if c>ds[a]:continue
if a==t:return c
for b,w in adj[a]:
d=c+w
if d>(1<<63)-1:return None
if d<ds[b]:ds[b]=d;heapq.heappush(h,(d,-b))
return None
def contained(a,b):return not a or any(b[t:t+len(a)]==a for t in range(len(b)-len(a)+1))
def overlap(a,b):return max([0]+[i for i in range(1,min(len(a),len(b))+1) if a[-i:]==b[:i]])
def reduce(kind,d):
if kind in ['schedule','common_schedule']:
deadlines=d.get('d',[d.get('D',0)]*d.get('n',0));n=len(deadlines);lens=[min(x,n) for x in deadlines];m=d['m'];offset=[];s=0
for h in lens:offset.append(s);s+=h
caps=[]
for t in range(max(lens,default=0)):
row=[(offset[i]+t,1) for i,h in enumerate(lens) if t<h]
if m<len(row):
row += [(s+j,1<<j) for j in range(m.bit_length())];s+=m.bit_length();caps.append(row)
q=Poly(s)
for o,h in zip(offset,lens):q.sq([(o+t,1) for t in range(h)],1)
for row in caps:q.sq(row,m)
for i,j in d['p']:
for t in range(lens[i]):
for u in range(min(t+1,lens[j])):q.add(offset[i]+t,offset[j]+u,1)
elif kind in ['cyclic','grouping','feedback']:
n=d.get('n',d.get('a'));q=Poly(n*(n-1)//2)
if kind=='cyclic':
tournament(q,n,1)
for a,b,c in d['triples']:
row=[];rhs=2
for i,j in [(a,b),(b,c),(c,a)]:
if i<j:row.append((pi(n,i,j),1))
else:row.append((pi(n,j,i),-1));rhs-=1
q.sq(row,rhs)
elif kind=='grouping':
for pos,i in enumerate(d['s']):
for j in d['s'][pos+1:]:
if i<j:q.c+=1;q.add(pi(n,i,j),pi(n,i,j),-1)
elif i>j:q.add(pi(n,j,i),pi(n,j,i),1)
M=len(d['s'])*(len(d['s'])-1)//2;tournament(q,n,M+1)
return q.done(min(d['K'],M)-q.c)
else:
ws=[w for _,_,w in d['arcs']]
if sum(min(w,0) for w in ws)<-(1<<63) or sum(max(w,0) for w in ws)>(1<<63)-1:raise OverflowError
for a,b,w in d['arcs']:
if w<0 or a==b:q.c+=w
elif a<b:q.c+=w;q.add(pi(n,a,b),pi(n,a,b),-w)
else:q.add(pi(n,b,a),pi(n,b,a),w)
L,U=q.interval();tournament(q,n,U-L+1);return q.done(interval=(L,U))
elif kind in ['partition','subset']:
q=Poly(len(d['s']));q.sq([(i,x*(2 if kind=='partition' else 1)) for i,x in enumerate(d['s'])],sum(d['s']) if kind=='partition' else d['T'])
elif kind in ['cover','matching']:
ts=d['triples'];q=Poly(len(ts))
for axis in range(3 if kind=='matching' else 1):
for u in range(d['u']):q.sq([(j,1) for j,t in enumerate(ts) if (t[axis]==u if kind=='matching' else u in t)],1)
elif kind=='threepartition':
n=len(d['s']);k=n//3;q=Poly(n*k);assignment(q,n,k)
for g in range(k):q.sq([(i*k+g,1) for i in range(n)],3);q.sq([(i*k+g,w) for i,w in enumerate(d['s'])],d['B'])
elif kind=='superstring':
ss=d['strings'];ss=[s for i,s in enumerate(ss) if s and not any(contained(s,t) and (len(s)<len(t) or j<i) for j,t in enumerate(ss) if i!=j)]
n=len(ss);q=Poly(n*n);q.c=sum(map(len,ss))
for i in range(n):
for j in range(n):
if i!=j:
for p in range(n-1):q.add(i*n+p,j*n+p+1,-overlap(ss[i],ss[j]))
L,U=q.interval();P=U-L+1;perm(q,n,P)
if any(c>=d['a'] for s in d['strings'] for c in s):q.c+=P
return q.done(interval=(L,U))
elif kind=='stacker':
arcs=d['arcs'];n=len(arcs);q=Poly(n*n);q.c=sum(a[2] for a in arcs);D=[[dist(d['v'],arcs,d['edges'],a[1],b[0]) for b in arcs] for a in arcs]
if q.c+n*max([0]+[x for r in D for x in r if x is not None])>(1<<63)-1:raise OverflowError
missing=[]
for i in range(n):
for j in range(n):
if n>1 and i==j:continue
for p in range(n):
a,b=i*n+p,j*n+(p+1)%n
if D[i][j] is None:missing.append((a,b))
else:q.add(a,b,D[i][j])
L,U=q.interval();P=U-L+1;perm(q,n,P)
for a,b in missing:q.add(a,b,P)
return q.done(interval=(L,U))
else:raise ValueError(kind)
return q.done(-q.c)
def energy(q,x):return sum(c*x[i]*x[j] for i,j,c in q['entries'])
def run():
counts=defaultdict(int);rng=random.Random(20261022)
n,k,H=sy.symbols('n k H',nonnegative=True)
for f in [n*(n-1)/2,n*k,n*n,2*n*H]:assert sy.expand(f*f-f*f)==0;counts['symbolic']+=1
# Exhaustive selection residuals independently computed, including every target witness.
for size in range(6):
for _ in range(300):
s=[rng.randrange(1,8) for i in range(size)];T=rng.randrange(25)
for kind,d in [('subset',{'s':s,'T':T})]+([('partition',{'s':s})] if s else []):
q=reduce(kind,d)
assert q['n']==size and len([1 for i,j,c in q['entries'] if i!=j])<=size*(size-1)//2;counts['size']+=1
assert all(0<=i<=j<size for i,j,c in q['entries']);counts['structure']+=1
for bits in product([0,1],repeat=size):
selected=sum(a*b for a,b in zip(s,bits));valid=selected==T if kind=='subset' else selected==sum(s)-selected
assert (energy(q,bits)<=q['bound'])==valid;counts['forward_backward']+=1;counts['extraction']+=valid
examples=[('partition',{'s':[1,2,3]},[1,1,0],True),('partition',{'s':[1,1,1]},[1,0,0],False),('cover',{'u':6,'triples':[[0,1,2],[3,4,5],[0,3,4]]},[1,1,0],True),('cover',{'u':6,'triples':[[0,1,2],[0,1,3],[0,1,4]]},[1,0,0],False)]
for kind,d,x,want in examples:
q=reduce(kind,d);assert (energy(q,x)<=q['bound'])==want;counts['yes_example' if want else 'no_example']+=1
Path(__file__).with_name('constructor-report.json').write_text(json.dumps(counts,indent=2));print(dict(counts))
if __name__=='__main__':run()adversary_c.py"""Independent proof-c adversary; imports no constructor or repository implementation."""
from collections import Counter
from functools import lru_cache
from itertools import permutations, product
import heapq
import json
import random
MAX = (1 << 63) - 1
MIN = -(1 << 63)
AUDIT = Counter()
SEED = 22102026
class NumericFailure(ValueError):
pass
def check(value):
if not MIN <= value <= MAX:
raise NumericFailure(value)
return value
def adjacency(instance):
result = [[] for _ in range(instance['v'])]
for u, v, weight in instance['arcs']:
result[u].append((v, weight))
for u, v, weight in instance['edges']:
result[u].append((v, weight))
result[v].append((u, weight))
return result
def distance(adj, start, end):
if start == end:
return 0
distances = [MAX] * len(adj)
distances[start] = 0
queue = [(0, -start)]
while queue:
cost, negative_vertex = heapq.heappop(queue)
vertex = -negative_vertex
if cost > distances[vertex]:
continue
if vertex == end:
return cost
for neighbor, weight in adj[vertex]:
if cost + weight > MAX:
return None
new = cost + weight
if new < distances[neighbor]:
distances[neighbor] = new
heapq.heappush(queue, (new, -neighbor))
return None
def source_value(instance, order):
arcs = instance['arcs']
if sorted(order) != list(range(len(arcs))):
return None
if not arcs:
return 0
adj = adjacency(instance)
total = 0
for p, a in enumerate(order):
b = order[(p + 1) % len(order)]
connector = distance(adj, arcs[a][1], arcs[b][0])
if connector is None:
return None
total += arcs[a][2]
if total > MAX:
return None
total += connector
if total > MAX:
return None
return total
def reduce(kind='stacker', instance=None):
assert kind == 'stacker'
arcs = instance['arcs']
n = len(arcs)
adj = adjacency(instance)
ds = [[distance(adj, a[1], b[0]) for b in arcs] for a in arcs]
base = sum(a[2] for a in arcs)
available = [d for row in ds for d in row if d is not None]
check(base)
check(base + n * max(available, default=0))
q = Counter()
def add(i, j, coefficient):
if coefficient:
q[min(i, j), max(i, j)] += coefficient
for p in range(n):
nxt = (p + 1) % n
for i in range(n):
for j in range(n):
if i == j and n > 1:
continue
if ds[i][j] is not None:
add(i * n + p, j * n + nxt, ds[i][j])
lower = base + sum(min(c, 0) for c in q.values())
upper = base + sum(max(c, 0) for c in q.values())
penalty = upper - lower + 1
constant = base + 2 * n * penalty
# Expand (sum x - 1)^2, independently for each row and column.
for row in range(n):
for i in range(n):
add(row * n + i, row * n + i, -penalty)
add(i * n + row, i * n + row, -penalty)
for j in range(i + 1, n):
add(row * n + i, row * n + j, 2 * penalty)
add(i * n + row, j * n + row, 2 * penalty)
for p in range(n):
for i in range(n):
for j in range(n):
if i == j and n > 1:
continue
if ds[i][j] is None:
add(i * n + p, j * n + (p + 1) % n, penalty)
entries = [[i, j, check(c)] for (i, j), c in sorted(q.items()) if c]
check(sum(min(c, 0) for _, _, c in entries))
check(sum(max(c, 0) for _, _, c in entries))
check(lower)
check(upper)
check(penalty)
return {'n': n*n, 'constant': check(constant), 'entries': entries,
'bound': None, 'low': check(lower-constant), 'high': check(upper-constant)}
def target_value(target, bits):
if len(bits) != target['n'] or any(x not in (0, 1) for x in bits):
return None
return sum(c * bits[i] * bits[j] for i, j, c in target['entries'])
def extract_solution(instance, target, bits):
value = target_value(target, bits)
if value is None or not target['low'] <= value <= target['high']:
return None
n = len(instance['arcs'])
order = []
for position in range(n):
selected = [i for i in range(n) if bits[i*n+position]]
if len(selected) != 1:
return None
order.append(selected[0])
if len(set(order)) != n:
return None
return order
def assert_that(condition, section, detail=None):
AUDIT[section] += 1
if not condition:
raise AssertionError((section, detail))
def verify_instance(instance, exhaustive=False, sample_count=32):
target = reduce(instance=instance)
n = len(instance['arcs'])
assert_that(target['n'] == n*n and len(target['entries']) <= n**4, 'size')
assert_that(all(0 <= i <= j < n*n and c != 0 for i,j,c in target['entries']), 'structure')
assert_that(target['entries'] == sorted(target['entries']) and len({(i,j) for i,j,c in target['entries']}) == len(target['entries']), 'structure')
feasible_orders = {}
for order in permutations(range(n)):
value = source_value(instance, order)
bits = [0]*(n*n)
for p, i in enumerate(order):
bits[i*n+p] = 1
energy = target_value(target, bits)
accepted = target['low'] <= energy <= target['high']
assert_that(accepted == (value is not None), 'forward', (instance, order, value, energy, target))
if value is not None:
feasible_orders[order] = value
assert_that(energy + target['constant'] == value, 'objective')
assert_that(extract_solution(instance, target, bits) == list(order), 'extraction')
if exhaustive or n <= 3:
configs = product((0,1), repeat=n*n)
else:
rng = random.Random(repr(instance))
configs = [tuple([0]*(n*n)), tuple([1]*(n*n))]
configs += [tuple(rng.randrange(2) for _ in range(n*n)) for _ in range(sample_count)]
best_energy = None
for bits in configs:
energy = target_value(target, bits)
if best_energy is None or energy < best_energy:
best_energy = energy
accepted = target['low'] <= energy <= target['high']
# Determine source witness directly from positional bit counts; don't use extractor.
columns = [[i for i in range(n) if bits[i*n+p]] for p in range(n)]
assignment = all(len(col) == 1 for col in columns)
order = tuple(col[0] for col in columns) if assignment else None
expected = assignment and order in feasible_orders
assert_that(accepted == expected, 'backward', (instance,bits,energy,target))
if accepted:
got = extract_solution(instance, target, bits)
assert_that(got == list(order) and source_value(instance,got) == energy+target['constant'], 'extraction')
if exhaustive or n <= 3:
got = best_energy+target['constant'] if target['low'] <= best_energy <= target['high'] else None
expected = min(feasible_orders.values(), default=None)
assert_that(got == expected, 'optimum', (instance,got,expected))
def run():
import sympy as sp
from hypothesis import given, settings, strategies as st, seed
n = sp.symbols('n', integer=True, nonnegative=True)
assert_that(sp.expand(n*n-n**2) == 0, 'symbolic')
assert_that(sp.expand((n*n)**2-n**4) == 0, 'symbolic')
# A symmetric upper-triangular quadratic form has at most N(N+1)/2 entries.
assert_that(sp.factor(n**4 - n*n*(n*n+1)/2) == n**2*(n-1)*(n+1)/2, 'symbolic')
examples = [
({'v':3,'arcs':[[0,1,1],[1,2,1],[2,0,1]],'edges':[]},3),
({'v':6,'arcs':[[0,1,1],[2,3,1],[4,5,1]],'edges':[]},None),
({'v':0,'arcs':[],'edges':[]},0),
({'v':2,'arcs':[[0,1,2]],'edges':[[0,1,3]]},5),
({'v':1,'arcs':[[0,0,2]],'edges':[]},2),
]
for instance, expected in examples:
values = [x for p in permutations(range(len(instance['arcs']))) if (x:=source_value(instance,p)) is not None]
assert_that(min(values,default=None) == expected, 'examples')
verify_instance(instance)
# Full target domains on four-arc feasible and disconnected families (2^16 each).
for instance in [
{'v':1,'arcs':[[0,0,i] for i in range(4)],'edges':[[0,0,0]]},
{'v':5,'arcs':[[0,i,1] for i in range(1,5)],'edges':[]},
]:
verify_instance(instance, exhaustive=True)
rng = random.Random(SEED)
# 300 independently generated samples for each n=0..5 and each optional-edge family.
for arc_count in range(6):
for edge_count in (0,1,3):
for _ in range(300):
vertices = rng.randint(1,5)
def edge():
return [rng.randrange(vertices),rng.randrange(vertices),rng.randrange(8)]
verify_instance({'v':vertices,'arcs':[edge() for _ in range(arc_count)],
'edges':[edge() for _ in range(edge_count)]})
@st.composite
def general_graph(draw):
vertices = draw(st.integers(1,5))
edge = st.tuples(st.integers(0,vertices-1),st.integers(0,vertices-1),st.integers(0,20))
return {'v':vertices,'arcs':draw(st.lists(edge,max_size=5)),
'edges':draw(st.lists(edge,max_size=6))}
@seed(SEED)
@settings(max_examples=500,deadline=None,database=None)
@given(general_graph())
def fuzz_general(instance):
AUDIT['hypothesis_general'] += 1
verify_instance(instance)
fuzz_general()
@st.composite
def repeated_graph(draw):
vertices = draw(st.integers(1,5))
u = draw(st.integers(0,vertices-1))
v = draw(st.integers(0,vertices-1))
count = draw(st.integers(0,5))
weight = draw(st.sampled_from([0,1,2,17]))
travel = draw(st.lists(st.tuples(st.integers(0,vertices-1),st.integers(0,vertices-1),st.sampled_from([0,1,11])),max_size=5))
return {'v':vertices,'arcs':[[u,v,weight] for _ in range(count)],'edges':travel}
@seed(SEED+1)
@settings(max_examples=500,deadline=None,database=None)
@given(repeated_graph())
def fuzz_repeated(instance):
AUDIT['hypothesis_repeated'] += 1
verify_instance(instance)
fuzz_repeated()
# Exact representational sentinel and overflow behavior, independently expected.
assert_that(distance([[(1,MAX)],[]],0,1) is None, 'numeric_semantics')
assert_that(distance([[(1,MAX-1)],[]],0,1) == MAX-1, 'numeric_semantics')
assert_that(distance([[(0,MAX)]],0,0) == 0, 'numeric_semantics')
assert_that(distance([[(1,1),(2,5)],[(3,MAX)],[],[]],0,2) is None,'numeric_semantics')
# Equal-distance heap ties pop the larger vertex before checking overflow.
assert_that(distance([[(1,1),(2,1)],[],[(3,MAX)],[]],0,1) is None,'numeric_semantics')
assert_that(distance([[(1,1),(2,1)],[(3,MAX)],[],[]],0,2) == 1,'numeric_semantics')
# A None connector due to overflow must prohibit the transition.
overflow_case = {'v':4,'arcs':[[2,0,0]],'edges':[[0,1,1],[0,2,5],[1,3,MAX]]}
assert_that(source_value(overflow_case,(0,)) is None,'numeric_semantics')
verify_instance(overflow_case)
for instance in [
{'v':1,'arcs':[[0,0,MAX],[0,0,1]],'edges':[]},
{'v':2,'arcs':[[0,1,MAX-1]],'edges':[[0,1,2]]},
{'v':2,'arcs':[[0,1,MAX//30],[0,1,MAX//30]],'edges':[[0,1,MAX//30]]},
]:
try:
reduce(instance=instance)
except NumericFailure:
AUDIT['numeric_rejection'] += 1
else:
raise AssertionError(('expected numeric rejection',instance))
assert_that(source_value({'v':1,'arcs':[[0,0,MAX],[0,0,1]],'edges':[]},(0,1)) is None,'numeric_semantics')
verify_instance({'v':1,'arcs':[[0,0,MAX-2]],'edges':[]})
# A MAX-length loop itself is a representable source optimum.
huge = {'v':1,'arcs':[[0,0,MAX]],'edges':[]}
assert_that(source_value(huge,(0,)) == MAX,'numeric_semantics')
try:
reduce(instance=huge)
except NumericFailure:
AUDIT['target_numeric_rejection'] += 1
else:
raise AssertionError('target constant overflow must be checked')
report={'status':'PASS','seed':SEED,'audit':dict(sorted(AUDIT.items())),
'total_checks':sum(AUDIT.values()),'hypothesis_examples':1000,
'random_instances':5400,'full_source_permutations_through_n':5,
'full_target_configurations_through_n':3,'extra_full_target_n4_instances':2}
print(json.dumps(report,indent=2))
if __name__ == '__main__':
run() |
Collaborator
Author
External validation and measurement reproductionAll files below were run outside both repository and corpus. Corpus imports disable bytecode writes. Before/after full SHA-256 snapshots agree for all32,372 files. OR-Tools9.15.6755, managed Python3.12.14; symbolic constructor/adversary environment uses SymPy and Hypothesis. The evidence distinguishes oracle-witness certification from independent target solving; it does not claim1200 raw target solves. corpus-structural-results/summary.json{
"total": 1200,
"correct": 1200,
"seconds": 62.44421008299105,
"coverage": {
"exact_polynomial_and_no_truth": 355,
"exact_polynomial_oracle_energy_extraction_evaluation_aggregate": 845
},
"by_source": {
"SchedulingWithIndividualDeadlines": {
"total": 100,
"correct": 100
},
"PrecedenceConstrainedScheduling": {
"total": 100,
"correct": 100
},
"CyclicOrdering": {
"total": 100,
"correct": 100
},
"GroupingBySwapping": {
"total": 100,
"correct": 100
},
"MinimumFeedbackArcSet/i64": {
"total": 100,
"correct": 100
},
"Partition": {
"total": 100,
"correct": 100
},
"SubsetSum": {
"total": 100,
"correct": 100
},
"ExactCoverBy3Sets": {
"total": 100,
"correct": 100
},
"ThreePartition": {
"total": 100,
"correct": 100
},
"ThreeDimensionalMatching": {
"total": 100,
"correct": 100
},
"StackerCrane": {
"total": 100,
"correct": 100
},
"ShortestCommonSuperstring": {
"total": 100,
"correct": 100
}
}
}corpus-cp-results/small-summary.json{
"total": 120,
"correct": 110,
"seconds": 22.36613708396908,
"by_source": {
"SchedulingWithIndividualDeadlines": {
"passed": 10
},
"PrecedenceConstrainedScheduling": {
"UNKNOWN": 10
},
"CyclicOrdering": {
"passed": 10
},
"GroupingBySwapping": {
"passed": 10
},
"MinimumFeedbackArcSet/i64": {
"passed": 10
},
"Partition": {
"passed": 10
},
"SubsetSum": {
"passed": 10
},
"ExactCoverBy3Sets": {
"passed": 10
},
"ThreePartition": {
"passed": 10
},
"ThreeDimensionalMatching": {
"passed": 10
},
"StackerCrane": {
"passed": 10
},
"ShortestCommonSuperstring": {
"passed": 10
}
}
}coverage-summary.json{
"files": [
{
"file": "cyclicordering_qubo.rs",
"total": 47,
"covered": 47,
"missed": []
},
{
"file": "exactcoverby3sets_qubo.rs",
"total": 41,
"covered": 41,
"missed": []
},
{
"file": "groupingbyswapping_qubo.rs",
"total": 73,
"covered": 69,
"missed": [
42,
43,
44,
82
]
},
{
"file": "minimumfeedbackarcset_qubo.rs",
"total": 62,
"covered": 62,
"missed": []
},
{
"file": "partition_qubo.rs",
"total": 40,
"covered": 40,
"missed": []
},
{
"file": "precedenceconstrainedscheduling_qubo.rs",
"total": 36,
"covered": 35,
"missed": [
43
]
},
{
"file": "schedulingwithindividualdeadlines_qubo.rs",
"total": 33,
"covered": 32,
"missed": [
42
]
},
{
"file": "shortestcommonsuperstring_qubo.rs",
"total": 105,
"covered": 101,
"missed": [
38,
39,
40,
98
]
},
{
"file": "stackercrane_qubo.rs",
"total": 79,
"covered": 78,
"missed": [
27
]
},
{
"file": "subsetsum_qubo.rs",
"total": 46,
"covered": 45,
"missed": [
46
]
},
{
"file": "threedimensionalmatching_qubo.rs",
"total": 42,
"covered": 42,
"missed": []
},
{
"file": "threepartition_qubo.rs",
"total": 46,
"covered": 45,
"missed": [
52
]
},
{
"file": "unit_schedule_qubo.rs",
"total": 48,
"covered": 48,
"missed": []
}
],
"total": 698,
"covered": 685,
"percent": 98.13753581661891
}upstream/results.json[
{
"source": "DecisionStackerCrane",
"via": "StackerCrane",
"target": "QUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_arcs^2",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "num_arcs^4",
"relation": "upper_bound"
}
]
},
"variables": 25,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "DecisionStackerCrane",
"value": true
},
"seconds": 2.6861737919971347
},
{
"source": "KSatisfiability/K3",
"via": "CyclicOrdering",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "0.5 * (3 + 3 * num_vars + 26 * num_clauses)^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "0.25 * (3 + 3 * num_vars + 26 * num_clauses)^2 + 0.25 * (3 + 3 * num_vars + 26 * num_clauses)^4",
"relation": "upper_bound"
}
]
},
"variables": 91,
"target_hint": "independent rank feasibility solver",
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "KSatisfiability",
"value": true
},
"seconds": 0.5928473749663681
},
{
"source": "KSatisfiability/K3",
"via": "SubsetSum",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "2 * num_clauses + 2 * num_vars",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "(2 * num_clauses + 2 * num_vars)^2",
"relation": "upper_bound"
}
]
},
"variables": 10,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "KSatisfiability",
"value": true
},
"seconds": 0.4540092919487506
},
{
"source": "MinimumVertexCover/i64",
"via": "MinimumFeedbackArcSet/i64",
"target": "QUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "-1 * num_vertices + 0.5 * (2 * num_vertices)^2",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "-1.5 * (2 * num_vertices)^2 + 0.5 * (2 * num_vertices)^3 + 2 * num_vertices",
"relation": "upper_bound"
}
]
},
"variables": 15,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Min(2)",
"aggregate": {
"unavailable": "existing MinimumVertexCover -> MinimumFeedbackArcSet edge has no aggregate mapping"
},
"seconds": 0.44730925001204014
},
{
"source": "Partition",
"via": "SubsetSum",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_elements",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "num_elements^2",
"relation": "upper_bound"
}
]
},
"variables": 6,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "Partition",
"value": true
},
"seconds": 0.43781683302950114
},
{
"source": "SubsetSum",
"via": "Partition",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "1 + num_elements",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "(1 + num_elements)^2",
"relation": "upper_bound"
}
]
},
"variables": 5,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "SubsetSum",
"value": true
},
"seconds": 0.44625266594812274
},
{
"source": "ThreeDimensionalMatching",
"via": "ThreePartition",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "(2 + -1 * num_triples + 8 * num_triples^2) * (6 + -3 * num_triples + 24 * num_triples^2)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "(2 + -1 * num_triples + 8 * num_triples^2)^2 * (6 + -3 * num_triples + 24 * num_triples^2)^2",
"relation": "upper_bound"
}
]
},
"correct": false,
"error": "Error: ThreePartition -> DecisionQUBO: integer overflow while constructing an exact QUBO polynomial\n",
"limitation": "Upstream ThreePartition magnitudes exceed exact i64 QUBO coefficient domain",
"seconds": 0.35617312509566545
}
]corpus_structural.pyimport sys
sys.dont_write_bytecode=True
import json,collections,concurrent.futures,time,subprocess,importlib.util
from pathlib import Path
import constructor as c
base=Path(__file__).parent;root=Path('/Users/xiweipan/Codes/pred-validation-corpus');out=base/'corpus-structural-results';out.mkdir(exist_ok=True)
pred=Path('/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase2/target/debug/pred')
spec=importlib.util.spec_from_file_location('verify_rules',root/'scripts/verify_rules.py');v=importlib.util.module_from_spec(spec);spec.loader.exec_module(v);accuracy=v.load_accuracy_helpers(root)
sources=['SchedulingWithIndividualDeadlines','PrecedenceConstrainedScheduling','CyclicOrdering','GroupingBySwapping','MinimumFeedbackArcSet/i64','Partition','SubsetSum','ExactCoverBy3Sets','ThreePartition','ThreeDimensionalMatching','StackerCrane','ShortestCommonSuperstring']
rules=[dict(source=s,target=('QUBO/i64' if s in ['MinimumFeedbackArcSet/i64','StackerCrane','ShortestCommonSuperstring'] else 'DecisionQUBO/i64')) for s in sources]
routes,missing=v.discover_routes(pred,rules,out);assert not missing,missing
truth=accuracy.load_truth();grouped=collections.defaultdict(list)
for row in truth.values():grouped[row['problem']].append(row)
def cli(args,data=None):
result,error=v.run_json([str(pred),*args,'--quiet','--json'],timeout=40,input_text=None if data is None else json.dumps(data));assert error is None,error;return result
def schema(name,d):
return {
'SchedulingWithIndividualDeadlines':lambda:('schedule',dict(d=d['deadlines'],m=d['num_processors'],p=d['precedences'])),
'PrecedenceConstrainedScheduling':lambda:('common_schedule',dict(n=d['num_tasks'],D=d['deadline'],m=d['num_processors'],p=d['precedences'])),
'CyclicOrdering':lambda:('cyclic',dict(n=d['num_elements'],triples=d['triples'])),
'GroupingBySwapping':lambda:('grouping',dict(a=d['alphabet_size'],s=d['string'],K=d['budget'])),
'MinimumFeedbackArcSet/i64':lambda:('feedback',dict(n=d['graph']['num_vertices'],arcs=[[*arc,w] for arc,w in zip(d['graph']['arcs'],d['weights'])])),
'Partition':lambda:('partition',dict(s=d['sizes'])),
'SubsetSum':lambda:('subset',dict(s=list(map(int,d['sizes'])),T=int(d['target']))),
'ExactCoverBy3Sets':lambda:('cover',dict(u=d['universe_size'],triples=d['subsets'])),
'ThreePartition':lambda:('threepartition',dict(s=d['sizes'],B=d['bound'])),
'ThreeDimensionalMatching':lambda:('matching',dict(u=d['universe_size'],triples=d['triples'])),
'StackerCrane':lambda:('stacker',dict(v=d['num_vertices'],arcs=[[*a,w] for a,w in zip(d['arcs'],d['arc_lengths'])],edges=[[*a,w] for a,w in zip(d['edges'],d['edge_lengths'])])),
'ShortestCommonSuperstring':lambda:('superstring',dict(a=d['alphabet_size'],strings=d['strings']))}[name]()
def lift(kind,d,w,q):
x=[False]*q['n']
if kind in ['schedule','common_schedule']:
ds=d.get('d',[d.get('D',0)]*d.get('n',0));n=len(ds);hs=[min(n,t) for t in ds];compressed={t:i for i,t in enumerate(sorted(set(w)))};times=[compressed[t] for t in w];offset=0
for h,t in zip(hs,times):x[offset+t]=True;offset+=h
for t in range(max(hs,default=0)):
if sum(t<h for h in hs)>d['m']:
slack=d['m']-times.count(t)
for b in range(d['m'].bit_length()):x[offset]=bool(slack&(1<<b));offset+=1
elif kind=='cyclic':
# Corpus witness is an element order; source stores ranks.
ranks=[w.index(i) for i in range(d['n'])]
x=[ranks[i]<ranks[j] for i in range(d['n']) for j in range(i+1,d['n'])]
elif kind=='grouping':
order=w['block_order']+[i for i in range(d['a']) if i not in w['block_order']];x=[order.index(i)<order.index(j) for i in range(d['a']) for j in range(i+1,d['a'])]
elif kind=='feedback':
removed=set(map(tuple,w));n=d['n'];kept=[(u,v) for u,v,cost in d['arcs'] if cost>=0 and u!=v and (u,v) not in removed];order=[]
while len(order)<n:
available=[i for i in range(n) if i not in order and not any(b==i and a not in order for a,b in kept)];assert available
order.append(available[0])
x=[order.index(i)<order.index(j) for i in range(n) for j in range(i+1,n)]
elif kind in ['partition','subset','cover','matching']:
for i in w:x[i]=True
elif kind=='threepartition':
groups=len(d['s'])//3
for g,items in enumerate(w):
for i in items:x[i*groups+g]=True
elif kind=='stacker':
n=len(w)
for p,i in enumerate(w):x[i*n+p]=True
elif kind=='superstring':
ss=[s for i,s in enumerate(d['strings']) if s and not any(c.contained(s,t) and (len(s)<len(t) or j<i) for j,t in enumerate(d['strings']) if i!=j)];n=len(ss)
starts=[next(i for i in range(len(w)-len(s)+1) if w[i:i+len(s)]==s) for s in ss];order=sorted(range(n),key=lambda i:starts[i])
for p,i in enumerate(order):x[i*n+p]=True
return x
def verify(route,t):
start=time.monotonic();r=dict(source=route['source'],instance=t['instance'],expected=t['value'])
try:
source=json.loads((root/t['instance']).read_text());kind,d=schema(route['source'],source['data']);reference=c.reduce(kind,d)
bundle=cli(['reduce',str(root/t['instance']),'--via',str(route['route'])]);data=bundle['target']['data'];decision=bundle['target']['type']=='DecisionQUBO';q=data['inner'] if decision else data
assert q['num_vars']==reference['n'] and q['entries']==reference['entries'],('polynomial mismatch',q,reference)
if decision:assert data['bound']==reference['bound']
expected_no=t['status'] in ['unsatisfiable','infeasible']
if expected_no:
# Independently verified polynomial identity plus corpus NO truth; no large target solve claimed.
r.update(correct=True,coverage='exact_polynomial_and_no_truth')
else:
bits=lift(kind,d,t['witness'],reference);energy=sum(c*int(bits[i])*int(bits[j]) for i,j,c in q['entries'])
assert (energy<=data['bound'] if decision else energy+reference['constant']==t['value']),('oracle-energy mismatch',energy,reference,t)
extracted=cli(['extract','-','--config',json.dumps(bits)],bundle);actual=accuracy.parse_evaluation(extracted['evaluation']);assert accuracy.equal_value(t['value'],actual),(t['value'],actual)
evaluated=cli(['evaluate',str(root/t['instance']),'--config',json.dumps(extracted['solution'])]);assert accuracy.equal_value(t['value'],accuracy.parse_evaluation(evaluated['result']))
aggregate=cli(['extract','-','--value='+json.dumps(True if decision else energy)],bundle)
assert accuracy.equal_value(t['value'],aggregate['value']),aggregate
r.update(correct=True,coverage='exact_polynomial_oracle_energy_extraction_evaluation_aggregate',aggregate=aggregate)
r.update(variables=q['num_vars'],couplings=sum(i!=j for i,j,c in q['entries']),seconds=time.monotonic()-start)
except Exception as e:r.update(correct=False,error=str(e),seconds=time.monotonic()-start)
return r
if __name__=='__main__':
rows=[];start=time.monotonic()
with (out/'results.jsonl').open('w') as f,concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
fs=[pool.submit(verify,route,t) for route in routes for t in grouped[route['source']]]
for future in concurrent.futures.as_completed(fs):
r=future.result();rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
if not r['correct'] or len(rows)%100==0:print(json.dumps(dict(completed=len(rows),failures=sum(not x['correct'] for x in rows),latest=r if not r['correct'] else r['source'])),flush=True)
summary=dict(total=len(rows),correct=sum(r['correct'] for r in rows),seconds=time.monotonic()-start,coverage=dict(collections.Counter(r.get('coverage','failure') for r in rows)),by_source={s:dict(total=sum(r['source']==s for r in rows),correct=sum(r['source']==s and r['correct'] for r in rows)) for s in sources})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary),flush=True)corpus_cp.pyimport sys
sys.dont_write_bytecode=True
import importlib.util,json,collections,concurrent.futures,time,subprocess
from pathlib import Path
from ortools.sat.python import cp_model
root=Path('/Users/xiweipan/Codes/pred-validation-corpus');base=Path(__file__).parent;out=base/'corpus-cp-results';out.mkdir(exist_ok=True)
pred=Path('/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase2/target/debug/pred')
spec=importlib.util.spec_from_file_location('verify_rules',root/'scripts/verify_rules.py');v=importlib.util.module_from_spec(spec);spec.loader.exec_module(v);accuracy=v.load_accuracy_helpers(root)
sources=['SchedulingWithIndividualDeadlines','PrecedenceConstrainedScheduling','CyclicOrdering','GroupingBySwapping','MinimumFeedbackArcSet/i64','Partition','SubsetSum','ExactCoverBy3Sets','ThreePartition','ThreeDimensionalMatching','StackerCrane','ShortestCommonSuperstring']
rules=[dict(source=s,target=('QUBO/i64' if s in ['MinimumFeedbackArcSet/i64','StackerCrane','ShortestCommonSuperstring'] else 'DecisionQUBO/i64')) for s in sources]
routes,missing=v.discover_routes(pred,rules,out);assert not missing,missing
truth=accuracy.load_truth();grouped=collections.defaultdict(list)
for row in truth.values():grouped[row['problem']].append(row)
assert all(len(grouped[s])==100 for s in sources)
def cli(args,data=None):
result,error=v.run_json([str(pred),*args,'--quiet','--json'],timeout=40,input_text=None if data is None else json.dumps(data));assert error is None,error;return result
def verify(route,t):
start=time.monotonic();r=dict(source=route['source'],instance=t['instance'],expected=t['value'])
try:
bundle=cli(['reduce',str(root/t['instance']),'--via',str(route['route'])]);target=bundle['target'];data=target['data'];decision=target['type']=='DecisionQUBO'
q=data['inner'] if decision else data
model=cp_model.CpModel();xs=[model.new_bool_var(f'x{i}') for i in range(q['num_vars'])];terms=[]
for i,j,c in q['entries']:
if i==j:terms.append(c*xs[i])
else:
y=model.new_bool_var(f'y{i}_{j}');model.add_multiplication_equality(y,[xs[i],xs[j]]);terms.append(c*y)
objective=sum(terms)
if decision:model.add(objective<=data['bound'])
else:model.minimize(objective)
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=3
status=solver.solve(model)
assert status in [cp_model.OPTIMAL,cp_model.INFEASIBLE],solver.status_name(status)
expected_no=t['status'] in ['unsatisfiable','infeasible']
if status==cp_model.INFEASIBLE:
assert decision and expected_no,(status,t)
recovered=cli(['extract','-','--value','false'],bundle)
r.update(correct=True,status='infeasible',recovered=recovered)
else:
bits=[bool(solver.value(x)) for x in xs];energy=sum(c*int(bits[i])*int(bits[j]) for i,j,c in q['entries'])
aggregate=cli(['extract','-','--value='+json.dumps(True if decision else energy)],bundle)
if expected_no:
# Optimization sources can be infeasible although every QUBO has an optimum.
assert not decision and aggregate.get('value') is None,aggregate
bad,error=v.run_json([str(pred),'extract','-','--config',json.dumps(bits),'--quiet','--json'],timeout=40,input_text=json.dumps(bundle));assert error is not None
r.update(correct=True,status='infeasible',aggregate=aggregate)
else:
extracted=cli(['extract','-','--config',json.dumps(bits)],bundle)
solution=extracted.get('source_config',extracted.get('solution',extracted.get('config')))
assert solution is not None,extracted
evaluation=cli(['evaluate',str(root/t['instance']),'--config',json.dumps(solution)])
actual=accuracy.parse_evaluation(evaluation.get('result'))
assert accuracy.equal_value(t['value'],actual),(t['value'],actual,evaluation)
r.update(correct=True,status='optimal',value=actual,aggregate=aggregate)
r.update(variables=q['num_vars'],couplings=sum(i!=j for i,j,c in q['entries']),seconds=time.monotonic()-start)
except Exception as e:r.update(correct=False,error=str(e),seconds=time.monotonic()-start)
return r
if __name__=='__main__':
rows=[];start=time.monotonic()
with (out/'results.jsonl').open('w') as f,concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
fs=[pool.submit(verify,route,t) for route in routes for t in grouped[route['source']]]
for future in concurrent.futures.as_completed(fs):
r=future.result();rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
if not r['correct'] or len(rows)%50==0:print(json.dumps(dict(completed=len(rows),failures=sum(not x['correct'] for x in rows),latest=r if not r['correct'] else r['source'])),flush=True)
summary=dict(total=len(rows),correct=sum(r['correct'] for r in rows),seconds=time.monotonic()-start,by_source={s:dict(total=sum(r['source']==s for r in rows),correct=sum(r['source']==s and r['correct'] for r in rows)) for s in sources})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary),flush=True)corpus_cp_small.pyimport corpus_cp as c
import json,time,concurrent.futures,collections
from pathlib import Path
base=Path(__file__).parent
structural=[json.loads(s) for s in (base/'corpus-structural-results/first-run-results.jsonl').read_text().splitlines()]
# First-run structural records always establish exact polynomial agreement; failed reporting records omit size.
# Read input counts only to select small instances; reduction and solver still consume actual CLI output.
def size(name,d):
if name=='SchedulingWithIndividualDeadlines':return 2*len(d['deadlines'])*max([0]+[min(len(d['deadlines']),v) for v in d['deadlines']])
if name=='PrecedenceConstrainedScheduling':return 2*d['num_tasks']*min(d['num_tasks'],d['deadline'])
if name=='CyclicOrdering':return d['num_elements']*(d['num_elements']-1)//2
if name=='GroupingBySwapping':return d['alphabet_size']*(d['alphabet_size']-1)//2
if name=='MinimumFeedbackArcSet/i64':return d['graph']['num_vertices']*(d['graph']['num_vertices']-1)//2
if name in ['Partition','SubsetSum']:return len(d['sizes'])
if name=='ExactCoverBy3Sets':return len(d['subsets'])
if name=='ThreePartition':return len(d['sizes'])**2//3
if name=='ThreeDimensionalMatching':return len(d['triples'])
if name=='StackerCrane':return len(d['arcs'])**2
if name=='ShortestCommonSuperstring':return len(d['strings'])**2
work=[]
for route in c.routes:
ts=sorted(c.grouped[route['source']],key=lambda t:size(route['source'],json.loads((c.root/t['instance']).read_text())['data']))
work += [(route,t) for t in ts[:10]]
rows=[];start=time.monotonic()
with (base/'corpus-cp-results/small-results.jsonl').open('w') as f,concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
for r in pool.map(lambda args:c.verify(*args),work):
rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
if not r['correct'] or len(rows)%10==0:print(json.dumps(dict(done=len(rows),failed=sum(not x['correct'] for x in rows),latest=r if not r['correct'] else r['source'])),flush=True)
summary=dict(total=len(rows),correct=sum(r['correct'] for r in rows),seconds=time.monotonic()-start,by_source={s:dict(collections.Counter('passed' if r['correct'] else r.get('error') for r in rows if r['source']==s)) for s in c.sources})
(base/'corpus-cp-results/small-summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary))corpus_snapshot_all.pyimport hashlib,json,os,sys
from pathlib import Path
root=Path('/Users/xiweipan/Codes/pred-validation-corpus'); out=Path(__file__).parent/'corpus-all-before.json'
files={}
for path,dirs,names in os.walk(root):
dirs[:]=sorted(dirs)
for name in sorted(names):
p=Path(path)/name
if p.is_file():files[str(p.relative_to(root))]=hashlib.sha256(p.read_bytes()).hexdigest()
if '--check' in sys.argv:
before=json.loads(out.read_text());assert before==files,'Corpus content changed';print(f'Unchanged: {len(files)} corpus files')
else:out.write_text(json.dumps(files,sort_keys=True));print(f'Snapshotted {len(files)} corpus files')measure.pyimport json,subprocess,time,statistics
from pathlib import Path
base=Path(__file__).parent;out=base/'measurements';out.mkdir(exist_ok=True)
pred=Path('/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase2/target/debug/pred')
names=['SchedulingWithIndividualDeadlines','PrecedenceConstrainedScheduling','CyclicOrdering','GroupingBySwapping','MinimumFeedbackArcSet/i64','Partition','SubsetSum','ExactCoverBy3Sets','ThreePartition','ThreeDimensionalMatching','StackerCrane','ShortestCommonSuperstring'];new=set(n.split('/')[0] for n in names)
def run(args):
start=time.perf_counter();p=subprocess.run([str(pred),*args,'--quiet','--json'],capture_output=True,text=True,timeout=30);elapsed=time.perf_counter()-start
if p.returncode:return None,p.stderr,elapsed
return json.loads(p.stdout),None,elapsed
rows=[]
for name in names:
target='QUBO/i64' if name in ['MinimumFeedbackArcSet/i64','StackerCrane','ShortestCommonSuperstring'] else 'DecisionQUBO/i64'
source,error,_=run(['create','--example',name,'--to',target]);assert not error,error
sourcefile=out/(name.split('/')[0]+'-source.json');sourcefile.write_text(json.dumps(source))
allpaths,error,_=run(['path',name,'QUBO/i64','--limit','all']);assert not error,error
(out/(name.split('/')[0]+'-paths.json')).write_text(json.dumps(allpaths,indent=2))
paths=[]
if target.startswith('Decision'):
direct,error,_=run(['path',name,target,'--limit','all']);paths=[(p,'direct') for p in direct['paths'] if p['steps']==1]
else:paths=[(p,'direct') for p in allpaths['paths'] if p['steps']==1]
baselines=[p for p in allpaths['paths'] if not any(e['from']['name'] in new and e['to']['name'] in ['QUBO','DecisionQUBO'] for e in p['path'])]
baseline_steps=min((p['steps'] for p in baselines),default=0)
paths += [(p,'existing') for p in baselines if p['steps']==baseline_steps]
for index,(path,kind) in enumerate(paths):
route=out/(name.split('/')[0]+f'-route-{index}.json');route.write_text(json.dumps(path))
timings=[];bundle=None;error=None
for rep in range(3):
bundle,error,elapsed=run(['reduce',str(sourcefile),'--via',str(route)]);timings.append(elapsed)
if error:break
row=dict(source=name,kind=kind,path=[path['path'][0]['from']]+[e['to'] for e in path['path']],composed=path['overall_parameters'],cli_reduce_ms=round(statistics.median(timings)*1000,3))
if error:row['error']=error
else:
(out/(name.split('/')[0]+f'-bundle-{index}.json')).write_text(json.dumps(bundle))
q=bundle['target']['data'];q=q.get('inner',q);coeff=[abs(c) for i,j,c in q['entries']];row.update(variables=q['num_vars'],couplings=sum(i!=j for i,j,c in q['entries']),max_coefficient=max(coeff,default=0),coefficient_bits=max(coeff,default=0).bit_length())
if kind=='direct':
solved,error,_=run(['solve',str(out/(name.split('/')[0]+f'-bundle-{index}.json')),'--solver','brute-force']);assert not error,error;row['canonical_solve']=solved
rows.append(row)
(out/'results.json').write_text(json.dumps(rows,indent=2))
print(name,[(r['kind'],r.get('variables'),r.get('couplings'),r.get('max_coefficient'),r.get('error')) for r in rows if r['source']==name],flush=True)
(out/'results.json').write_text(json.dumps(rows,indent=2)) |
Collaborator
Author
Agentic Review ReportReviewed the uncommitted Phase 2 changes against Structural and semantic reviewNo substantive findings. All 12 rules have exact endpoint registrations, canonical examples, aggregate mappings, parameter contracts, and manual proofs. Checked source domains, polynomial expansions, omitted constants, penalty separation, extraction, and numeric guards. Particular checks covered signed multigraph feedback costs, compressed unit schedules, unavailable StackerCrane connectors, and empty/duplicate/contained superstrings. Existing ILP edits only disambiguate trait methods; StackerCrane exposes existing preprocessing for reuse. Quality and verificationThe behavior tests independently solve sources and targets, check every target configuration on small instances, reject malformed witnesses, and cover infeasibility and arithmetic boundaries. Canonical examples feed the existing registry-wide parameter validation. Reviewed constructor/adversary evidence reports, including 21,000 cross-comparisons with zero disagreements, and actual route measurements. Measurements correctly show that direct formulations do not uniformly reduce every size metric. Feature testsUsing this checkout’s existing CLI, independently verified:
Artifacts are under Reviewed upstream results: six chains passed. The existing vertex-cover → feedback-arc edge lacks aggregate mapping, so its witness round trip was verified. The 3DM → ThreePartition → QUBO example returned typed integer overflow because upstream magnitudes exceed the target coefficient range. Findings and limitsNo Critical, Important, or Minor findings in the reviewed change. The coordinator reports passing Skipped duplicate builds and corpus access; those results are attributed to the coordinator. Large-target solve completion and the overflowing 3DM → ThreePartition chain remain unverified limitations, not successful solves. |
Open
57 tasks
isPANN
marked this pull request as ready for review
October 27, 2026 12:56
Each ILP rule's num_nonzeros upper bound was num_constraints * num_vars, a dense-matrix bound that the corpus measured at under half of its prediction on 55 rules. Derive the bound from each reduce_to's constraint families instead, summing the terms each family contributes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Canonical examples are sparse, so a constraint family missing from a per-family nonzero count can go unnoticed. Reduce dense instances of five rules with the most constraint families and require the measured count to stay within the declared bound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
StaffScheduling -> DecisionQUBO assumed 63 bits per worker count, and SequencingWithReleaseTimesAndDeadlines -> DecisionQUBO assumed every task may start anywhere in [0, time_horizon]. Neither source exposed the quantity the construction actually depends on, so the bounds ran three to four orders of magnitude above the corpus measurements. Add num_workers_bits to StaffScheduling and max_start_slots to SequencingWithReleaseTimesAndDeadlines, state both QUBO bounds in them, and declare the new fields in the two rules that target these models. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The sparse-support test kept the 63-bit StaffScheduling budget, so a regression to the old formula would still pass. Tighten it to the new prediction, add an SWRTD case, and restate both proofs' size bounds in the new parameters, including the two incoming rules that declare them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The bound K counts selected columns, but try_new accepted any negative value. Such an instance panicked in parameters(), whose bound must fit u64, and its ILP reduction cast the bound with `as usize`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The corpus measured 81 non-trivial upper-bound fields at exactly their prediction on every instance. Of those, 46 fields in 30 rules are exact by construction: every row family and variable block is emitted unconditionally, the source invariants (simple graphs, exactly-K clauses, n divisible by 3, 1 <= k <= n) rule out merged or dropped terms, and no early return builds a different target. The rest stay upper bounds: degenerate-input shortcuts, data-dependent zero coefficients or cancelled literals, and QUBO entries where penalty and objective terms can cancel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KSatisfiability<K3>::new_allow_less admits clauses with fewer than three literals, so 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges shrink below their formulas. Return both to upper_bound, pin the relations with short-clause instances, and lay out the transform declarations by nesting depth. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The exact claims for HamiltonianCircuit, MaximalIS, MinimumDominatingSet, MaximumMatching, Kernel, PartitionIntoPathsOfLength2, PartitionIntoPerfectMatchings and PartitionIntoCliques were checked only on canonical examples. Pin them on empty, path and complete graphs with up to three vertices, k = 1 and k = n, and antiparallel arcs. Also promote MinimumVertexCover -> EnsembleComputation num_subsets, one subset per edge, and convert the ConsecutiveOnesSubmatrix bound with try_from now that construction keeps it nonnegative. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MaxCut<SimpleGraph, i64> accepts negative weights, but the rule rejected
them, so every planned path through it (for example Max2SAT -> MaxCut ->
MinimumMatrixCover) failed on ordinary inputs. Replace each negative edge
{u, v} by an auxiliary vertex joined to v with |w| + 1 and to u with |w|:
every maximum cut separates the auxiliary vertex from v, so the gadget
shifts the cut by the constant 2|w| + 1 and preserves maximum cuts.
Extraction drops the auxiliary bits; num_rows becomes an upper bound.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- ConsecutiveOnesSubmatrix stores its column-count bound as usize, so serde and the CLI reject negatives by type and the model and ILP rule drop their conversions. - The MaxCut -> MinimumMatrixCover gadget computes |w| + 1 as 1 - w with one checked subtraction; module docs and the paper's duplicate extraction paragraph now describe the auxiliary vertices. - The PartitionIntoPathsOfLength2 comment states why its counts are exact. - The degenerate-graph test covers every valid k; transform layouts are consistent. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KSatisfiability<KN> was Satisfiability under another name: it checked no clause width and its only edges were identity casts into and out of it. Every path from K2 or K3 paid an extra hop through it. - Drop the KN variant; K2 and K3 now reduce directly to Satisfiability and K3 is the default variant. - Remove new_allow_less/try_new_allow_less. K2 and K3 always hold exactly K literals per clause, matching what serde and the CLI already enforced. - Delete the short- and empty-clause branches these constructors forced on 3-SAT rules, and declare 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges exact again. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e text SAT -> NAE turns every three-literal clause into a four-literal one, so the MonochromaticTriangle vertex, edge and triangle counts are equalities and its two-literal branch was dead. Also remove leftover short- and empty-clause wording and dead padding in OneInThree, QuadraticCongruences and Kernel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Add a FixedK sub-trait implemented by K1..K5, and bound KSatisfiability and the SAT/K-SAT results by it, so KSatisfiability<KN> no longer type-checks instead of failing at construction. - Register each K-SAT aggregate mapping inside the macro that registers its witness edge, and take the SAT -> K-SAT clause width from the type. - Allocate CyclicOrdering's fresh padding variables with allocate_many. - Drop leftover braces in two tests and a stale QuadraticCongruences note. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Removing the KSatisfiability KN variant does not need a new variant trait. Keep KSatisfiability bounded by KValue with the runtime width check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
GiggleLiu
reviewed
Oct 29, 2026
GiggleLiu
left a comment
GiggleLiu
left a comment
Contributor
There was a problem hiding this comment.
Agentic Review Report
PR #1215: Add Phase 2 direct QUBO reductions
Review date: 2026-10-29. Fresh-context read-only review of 37aa87857bb278364800e0902938065f4916a9aa...ecc0ad5ae72e9a19dc9ca1a69dcc700cd4f1bc1c. Used the PR's own stack base, not origin/main. Local implementation evidence is diff-1215.patch; GitHub context is context-1215.txt in this directory.
Verdict: No new blocking finding in this diff. Hold stack integration until #1214 is fixed.
Structural and semantic review
Reviewed all twelve direct reductions, helper changes, registrations, tests, CLI expectation adjustments, and manual proofs against the exact #1214 base. Encodings and parameter counts were derived from their actual supports.
The unit scheduling helper clips deadlines at n: compressing occupied slots preserves unit processing and precedence feasibility. Capacity slack represents every needed unused capacity; when processors exceed possible assigned jobs that capacity condition is redundant. Cyclic ordering uses transitive tournament order and the oriented triple equation. Grouping-by-swapping minimizes unequal-symbol inversions between group orderings and decodes adjacent swaps. Negative feedback arcs and self-loops are removed unconditionally; nonnegative arcs are charged when backward in the resulting order. Partition and subset-sum use squared residuals, with the latter expanding in BigInt before narrowing to preserve legitimate cancellation.
Exact cover and 3D matching use incidence-count squares; the incidence size itself enforces the number selected. The original ThreePartition has one-hot item-to-group assignments, cardinality three, and sum-B equations. StackerCrane uses a permutation of required arcs and cyclic shortest connectors, including the one-arc return connector. ShortestCommonSuperstring removes contained/duplicate/empty strings, maximizes adjacent overlap, and decodes a concatenation with padding. The correspondence between substring occurrence order and a maximal-overlap path justifies the latter objective.
Traced negative/zero costs, invalid alphabets, empty cases, loops, duplicate sets/triples, inconsistent precedence, absent connector paths, and source evaluator overflow. Registration, canonical examples, witness validation, and paper statements are present. No mathematical or new error-contract defect was identified.
Quality review
Tests include independent source/target exhaustive comparisons and malformed extraction coverage. Numeric checks account for source-side accumulation before coefficient cancellation. The one-hot penalty exceeds all possible objective variation. Scheduling slack capacity and overflow handling were checked directly; the deadline compression does not assume a total order. No implementation-mirroring assertion was relied on as evidence of correctness.
Feature tests and verification limits
On the compiled #1218 descendant, direct_qubo --test-threads=2 passed 44 tests, including the retained Phase 2 rules. Native exact #1215 tests were not rebuilt because of the shared local build resource limit. The original #1215 ThreePartition was reviewed statically; #1217 replaces it, and its descendant tests exercise that replacement.
The copied #1218 CLI completed discovery, example creation, inspection, direct path selection, reduction, source brute-force solve, and bundle brute-force solve/extraction for all twelve Phase 2 source types. Every extracted source evaluation equals the independently brute-forced source optimum/feasibility. Eleven implementations are retained unchanged; ThreePartition is the later replacement. Outputs are under cli-cases/.
No current GitHub CI checks were visible in the collected metadata for this stacked branch. Author-reported validation was read as context and was not counted as reviewer execution.
Findings (severity order)
No new blocking finding. The interval-scheduling allocation panic introduced by the base #1214 remains inherited; it is reported on #1214 rather than attributed to this diff. Stack integration should wait for that fix and current-head validation.
GitHub PR Audit — #1215
GATE: PASS
Harm signals (blocking)
- harm.secrets (
security.no-secrets): OK — inspected added text; no credential/key/token or private-data additions found. - harm.dangerous-files (
git.harm-signals): OK — changed files are scoped source, tests, and manual material; no conflict markers, unexplained binaries/archives, scratch files, or local configuration. - harm.generated-artifacts (
code.generated-artifacts): OK — no generated example/schema/reduction-graph exports or build/dependency outputs are committed. - harm.cache (
code.generated-cache): OK — no cache directories added. - harm.debug-leftovers (
code.debug-leftovers): OK — no debugger, debug print, temporary probe, or WIP instrumentation in added production code.
PR legibility (advisory)
- pr.description-quality (
github.pr-description-quality): OK — body describes scope, purpose, validation, and limits; comments and reviews were read withgh-axi pr view --full --comments --reviews. - pr.traceable (
github.prs-traceable): OK — purpose and validation are stated and the series/issue context is identifiable.
Harm gate PASS does not clear correctness findings. No tracked file, commit, remote branch, PR comment, review, or merge was modified by this reviewer.
[Critical] Remove KSatisfiability KN variant and short-clause constructors
Declare exact parameter counts that constructions always produce
Tighten ILP num_nonzeros bounds to per-constraint counts
Tighten StaffScheduling and SWRTD QUBO size bounds
Add binary decision ILP to SAT and fix solution validators
Add staff-scheduling QUBO and tighten direct-reduction bounds
Add Phase 3 conditional direct QUBO reductions
GiggleLiu
approved these changes
Oct 29, 2026
GiggleLiu
left a comment
GiggleLiu
left a comment
Contributor
There was a problem hiding this comment.
Agentic Review Report: stack consolidation
Approved current head 5cd48199bcdee684ced100105a936e37234a7788 for merging into feat/direct-scheduling-qubo only. This contains the previously reviewed changes and, where applicable, the preceding recorded backend merges. The numeric blockers in #1214 and #1224 are fixed and reviewed at 2226ebec4 and 52bd171a0.
Rechecked inline comments, submitted reviews, PR conversation, linked-issue comments, and Codecov comments. No new unaddressed material issue. Harm gate remains PASS from the independent reviews. The old roadmap draft/hold instructions predate the user's current authorization; deferred rules and #1219/#1220/#1221 remain excluded.
The repaired aggregate passed 7,194 native tests, formatting, all-target/all-feature Clippy, and make paper at d96e7c8b8; the final website gate subsequently passed all 336 browser cases at 77774797e. These are aggregate gates, including the separately reviewed integration fixtures, not a claim that this branch head was independently retested unchanged. Required main-branch CI remains pending. This feature-branch merge preserves the individual PR record.
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 12 direct integer QUBO constructions from Phase 2 of #1213, with source-compatible witness and aggregate recovery, canonical CLI examples, and manual proofs. This is stacked on Phase 1 draft PR at
37aa8785; keep both PRs draft and keep the roadmap open. No source domain is narrowed and no partial-domain rule is registered.Implemented, in roadmap order: SchedulingWithIndividualDeadlines, PrecedenceConstrainedScheduling, CyclicOrdering, GroupingBySwapping, MinimumFeedbackArcSet, Partition, SubsetSum, ExactCoverBy3Sets, ThreePartition, ThreeDimensionalMatching, StackerCrane, and ShortestCommonSuperstring. The nine feasibility sources target DecisionQUBO; the three Min sources target QUBO.
The rules reuse checked polynomial, assignment, tournament, extraction, and objective-offset helpers. A shared unit-task kernel handles capacities and precedence. StackerCrane reuses the source's existing shortest-path routine, including its overflow/unreachable behavior; only helper visibility changes. Existing ILP trait calls are qualified to remain unambiguous. The CLI path-comparison behavior test now accounts for the new feedback-arc path.
Formulations and numeric contracts
Measured canonical comparisons
Every row uses the rule's canonical example.
N/E/Mmeans actual variables / nonzero off-diagonal couplings / maximum absolute coefficient; bits are M.bit_length(). Baselines are the shortest existing paths excluding all 12 new edges; where several tie, this table selects the smallest actual N (full alternatives and composed bounds below). Times are median of three CLI reduction invocations including process startup and JSON serialization, not isolated kernel benchmarks or solver speedups.Savings are conditional: precedence scheduling ties variables and adds two couplings on its example; ThreePartition's existing valid-triple ILP route is strictly smaller on its example (one variable versus three). The assignment formulation avoids enumerating all valid triples, but is not a universal size improvement. ExactCover and matching retain selection-bit counts while reducing coefficients. Grouping and superstring gain their first outgoing routes. No physical annealer performance claim is made.
Construction work follows the proved blocks: schedule row/capacity squares plus pairwise conflicts; tournament rules O(n³), plus O(length²) inversion counting for grouping or O(arcs) feedback costs; numeric residuals O(n²) coefficient operations (BigInt cost depends on magnitude bits); incidence-square enumeration for covers; ThreePartition assignment/group squares; StackerCrane n² exact shortest-path queries plus assignment/transition terms; naive superstring containment/overlap preprocessing O(n²L²) plus assignment/transition terms. Full bounds and extraction costs are in the proof certificates and manual.
All measured routes and composed parameter bounds
SchedulingWithIndividualDeadlines (direct): SchedulingWithIndividualDeadlines → DecisionQUBO(i64)
Actual N=6, E=11, M=4; CLI 39.789 ms.
num_varsupper_bound:2 * max_deadline * num_tasksnum_quadratic_termsupper_bound:(2 * max_deadline * num_tasks)^2SchedulingWithIndividualDeadlines (existing): SchedulingWithIndividualDeadlines → ILP(general,i64,bool) → QUBO(i64)
Actual N=10, E=21, M=45; CLI 42.259 ms.
num_varsupper_bound:max_deadline * num_tasks + max_deadline * num_tasks * (1 + max_deadline + num_precedences + num_tasks) + (1 + max_deadline + num_precedences + num_tasks) * (1 + max_deadline + num_tasks)num_quadratic_termsupper_bound:2 * max_deadline * num_tasks * (1 + max_deadline + num_precedences + num_tasks) * (1 + max_deadline + num_tasks) + 2 * max_deadline * num_tasks * (1 + max_deadline + num_tasks) * (1 + max_deadline + num_precedences + num_tasks)^2 + 2 * (1 + max_deadline + num_precedences + num_tasks) * (max_deadline * num_tasks)^2 + (1 + max_deadline + num_precedences + num_tasks)^2 * (1 + max_deadline + num_tasks)^2 + (1 + max_deadline + num_precedences + num_tasks)^2 * (max_deadline * num_tasks)^2 + (max_deadline * num_tasks)^2PrecedenceConstrainedScheduling (direct): PrecedenceConstrainedScheduling → DecisionQUBO(i64)
Actual N=10, E=24, M=4; CLI 44.634 ms.
num_varsupper_bound:2 * deadline * num_tasksnum_quadratic_termsupper_bound:(2 * deadline * num_tasks)^2PrecedenceConstrainedScheduling (existing): PrecedenceConstrainedScheduling → ILP(general,i64,bool) → QUBO(i64)
Actual N=10, E=22, M=45; CLI 43.532 ms.
num_varsupper_bound:deadline * num_tasks + deadline * num_tasks * (deadline + num_precedences + num_tasks) + (1 + deadline + num_tasks) * (deadline + num_precedences + num_tasks)num_quadratic_termsupper_bound:2 * deadline * num_tasks * (1 + deadline + num_tasks) * (deadline + num_precedences + num_tasks) + 2 * deadline * num_tasks * (1 + deadline + num_tasks) * (deadline + num_precedences + num_tasks)^2 + 2 * (deadline + num_precedences + num_tasks) * (deadline * num_tasks)^2 + (1 + deadline + num_tasks)^2 * (deadline + num_precedences + num_tasks)^2 + (deadline + num_precedences + num_tasks)^2 * (deadline * num_tasks)^2 + (deadline * num_tasks)^2CyclicOrdering (direct): CyclicOrdering → DecisionQUBO(i64)
Actual N=3, E=3, M=4; CLI 40.75 ms.
num_varsexact:num_elements * (-1 + num_elements) * 2^-1num_quadratic_termsupper_bound:(num_elements * (-1 + num_elements) * 2^-1)^2CyclicOrdering (existing): CyclicOrdering → ILP(bounded,i64,i64) → ILP(general,i64,bool) → QUBO(i64)
Actual N=27, E=138, M=288; CLI 40.481 ms.
num_varsupper_bound:num_elements + 3 * num_triples + 7 * num_triples * (1 + 3 * num_elements + 3 * num_triples) + 7 * num_triples * (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples)) + num_elements * (num_elements + 3 * num_triples)num_quadratic_termsupper_bound:2 * (1 + 3 * num_elements + 3 * num_triples) * (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples)) * (7 * num_triples)^2 + 14 * num_triples * (1 + 3 * num_elements + 3 * num_triples) * (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples)) + 14 * num_triples * (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples))^2 + (1 + 3 * num_elements + 3 * num_triples)^2 * (7 * num_triples)^2 + (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples))^2 * (7 * num_triples)^2 + (num_elements + 3 * num_triples + num_elements * (num_elements + 3 * num_triples))^2GroupingBySwapping (direct): GroupingBySwapping → DecisionQUBO(i64)
Actual N=3, E=3, M=7; CLI 44.293 ms.
num_varsexact:alphabet_size * (-1 + alphabet_size) * 2^-1num_quadratic_termsupper_bound:alphabet_size * (-2 + alphabet_size) * (-1 + alphabet_size) * 2^-1MinimumFeedbackArcSet/i64 (direct): MinimumFeedbackArcSet(i64) → QUBO(i64)
Actual N=3, E=3, M=6; CLI 39.419 ms.
num_varsexact:num_vertices * (-1 + num_vertices) * 2^-1num_quadratic_termsupper_bound:num_vertices * (-2 + num_vertices) * (-1 + num_vertices) * 2^-1MinimumFeedbackArcSet/i64 (existing): MinimumFeedbackArcSet(i64) → ILP(bounded,i64,i64) → ILP(general,i64,bool) → QUBO(i64)
Actual N=27, E=99, M=456; CLI 47.434 ms.
num_varsupper_bound:num_arcs + num_vertices + (1 + num_arcs + num_vertices + 2 * (1 + num_vertices)) * (num_vertices + 2 * num_arcs) + (1 + num_vertices) * (num_arcs + num_vertices) + (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices)) * (num_vertices + 2 * num_arcs)num_quadratic_termsupper_bound:2 * (1 + num_arcs + num_vertices + 2 * (1 + num_vertices)) * (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices)) * (num_vertices + 2 * num_arcs) + 2 * (1 + num_arcs + num_vertices + 2 * (1 + num_vertices)) * (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices)) * (num_vertices + 2 * num_arcs)^2 + 2 * (num_vertices + 2 * num_arcs) * (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices))^2 + (1 + num_arcs + num_vertices + 2 * (1 + num_vertices))^2 * (num_vertices + 2 * num_arcs)^2 + (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices))^2 * (num_vertices + 2 * num_arcs)^2 + (num_arcs + num_vertices + (1 + num_vertices) * (num_arcs + num_vertices))^2Partition (direct): Partition → DecisionQUBO(i64)
Actual N=3, E=3, M=48; CLI 40.498 ms.
num_varsexact:num_elementsnum_quadratic_termsupper_bound:num_elements^2Partition (existing): Partition → Knapsack → QUBO(i64)
Actual N=5, E=10, M=84; CLI 40.474 ms.
num_varsupper_bound:max_numeric_magnitude_bits + 2 * num_elementsnum_quadratic_termsupper_bound:2 * num_elements * (max_numeric_magnitude_bits + num_elements) + num_elements^2 + (max_numeric_magnitude_bits + num_elements)^2Partition (existing): Partition → SumOfSquaresPartition → QUBO(i64)
Actual N=6, E=9, M=146; CLI 42.243 ms.
num_varsexact:2 * num_elementsnum_quadratic_termsupper_bound:-2 * num_elements + 0.5 * num_elements * 2^2 + num_elements^2SubsetSum (direct): SubsetSum → DecisionQUBO(i64)
Actual N=3, E=3, M=16; CLI 39.813 ms.
num_varsexact:num_elementsnum_quadratic_termsupper_bound:num_elements^2SubsetSum (existing): SubsetSum → DecisionClosestVectorProblem(i64) → ClosestVectorProblem(i64) → QUBO(i64)
Actual N=16, E=72, M=280; CLI 40.331 ms.
num_varsupper_bound:(-1 + max_numeric_magnitude_bits + num_elements) * (2 + (-1 + max_numeric_magnitude_bits + num_elements) * (3 + max_numeric_magnitude_bits) * 2^-1)num_quadratic_termsupper_bound:0.5 * ((-1 + max_numeric_magnitude_bits + num_elements) * (2 + (-1 + max_numeric_magnitude_bits + num_elements) * (3 + max_numeric_magnitude_bits) * 2^-1))^2SubsetSum (existing): SubsetSum → Partition → Knapsack → QUBO(i64)
Actual N=7, E=21, M=288; CLI 44.602 ms.
num_varsupper_bound:3 + max_numeric_magnitude_bits + 3 * num_elementsnum_quadratic_termsupper_bound:2 * (1 + num_elements) * (2 + max_numeric_magnitude_bits + 2 * num_elements) + (1 + num_elements)^2 + (2 + max_numeric_magnitude_bits + 2 * num_elements)^2SubsetSum (existing): SubsetSum → Partition → SumOfSquaresPartition → QUBO(i64)
Actual N=8, E=16, M=258; CLI 41.322 ms.
num_varsupper_bound:2 * (1 + num_elements)num_quadratic_termsupper_bound:0.5 * (1 + num_elements) * 2^2 + (1 + num_elements)^2ExactCoverBy3Sets (direct): ExactCoverBy3Sets → DecisionQUBO(i64)
Actual N=3, E=2, M=4; CLI 40.693 ms.
num_varsexact:num_subsetsnum_quadratic_termsupper_bound:num_subsets^2ExactCoverBy3Sets (existing): ExactCoverBy3Sets → ILP(general,i64,bool) → QUBO(i64)
Actual N=3, E=3, M=54; CLI 39.712 ms.
num_varsupper_bound:num_subsets + num_subsets * (1 + universe_size) + (1 + universe_size)^2num_quadratic_termsupper_bound:2 * num_subsets * (1 + universe_size)^2 + 2 * num_subsets * (1 + universe_size)^3 + 2 * (1 + universe_size) * num_subsets^2 + num_subsets^2 * (1 + universe_size)^2 + num_subsets^2 + (1 + universe_size)^4ThreePartition (direct): ThreePartition → DecisionQUBO(i64)
Actual N=3, E=3, M=26; CLI 45.381 ms.
num_varsexact:num_elements * num_groupsnum_quadratic_termsupper_bound:(num_elements * num_groups)^2ThreePartition (existing): ThreePartition → ILP(general,i64,bool) → QUBO(i64)
Actual N=1, E=0, M=12; CLI 41.83 ms.
num_varsupper_bound:num_elements + num_elements * (-2 + num_elements) * (-1 + num_elements) * 6^-1 + (-2 + num_elements) * (-1 + num_elements) * 6^-1 * num_elements^2num_quadratic_termsupper_bound:2 * num_elements * (num_elements * (-2 + num_elements) * (-1 + num_elements) * 6^-1)^2 + 2 * (-2 + num_elements) * (-1 + num_elements) * 6^-1 * num_elements^2 + 2 * (-2 + num_elements) * (-1 + num_elements) * 6^-1 * num_elements^3 + num_elements^2 * (num_elements * (-2 + num_elements) * (-1 + num_elements) * 6^-1)^2 + num_elements^2 + (num_elements * (-2 + num_elements) * (-1 + num_elements) * 6^-1)^2ThreeDimensionalMatching (direct): ThreeDimensionalMatching → DecisionQUBO(i64)
Actual N=3, E=0, M=3; CLI 49.032 ms.
num_varsexact:num_triplesnum_quadratic_termsupper_bound:num_triples^2ThreeDimensionalMatching (existing): ThreeDimensionalMatching → ILP(general,i64,bool) → QUBO(i64)
Actual N=3, E=0, M=30; CLI 39.604 ms.
num_varsupper_bound:num_triples + 3 * num_triples * universe_size + 3 * universe_sizenum_quadratic_termsupper_bound:2 * num_triples * (3 * universe_size)^2 + 6 * num_triples * universe_size + 6 * universe_size * num_triples^2 + num_triples^2 * (3 * universe_size)^2 + num_triples^2 + (3 * universe_size)^2StackerCrane (direct): StackerCrane → QUBO(i64)
Actual N=9, E=27, M=20; CLI 41.282 ms.
num_varsexact:num_arcs^2num_quadratic_termsupper_bound:num_arcs^4StackerCrane (existing): StackerCrane → ILP(general,i64,bool) → QUBO(i64)
Actual N=144, E=387, M=307; CLI 42.902 ms.
num_varsupper_bound:2 * (2 * num_arcs + 4 * num_arcs^3) + (2 * num_arcs + 4 * num_arcs^3) * (num_arcs^2 + num_arcs^3) + num_arcs^2 + num_arcs^3num_quadratic_termsupper_bound:2 * (2 * num_arcs + 4 * num_arcs^3) * (num_arcs^2 + num_arcs^3)^2 + 4 * (2 * num_arcs + 4 * num_arcs^3) * (num_arcs^2 + num_arcs^3) + 4 * (num_arcs^2 + num_arcs^3) * (2 * num_arcs + 4 * num_arcs^3)^2 + 2^2 * (2 * num_arcs + 4 * num_arcs^3)^2 + (2 * num_arcs + 4 * num_arcs^3)^2 * (num_arcs^2 + num_arcs^3)^2 + (num_arcs^2 + num_arcs^3)^2ShortestCommonSuperstring (direct): ShortestCommonSuperstring → QUBO(i64)
Actual N=4, E=6, M=6; CLI 42.357 ms.
num_varsupper_bound:num_strings^2num_quadratic_termsupper_bound:num_strings^4Verification
make check,make paper, andmake coveragepass. New production modules cover 685/698 executable lines (98.14%); the added shared affine-square helper is covered. Defensive post-validation guards and impractical allocation/range error paths account for uncovered lines; coverage was not padded with impossible-state tests./simplifypreceded the fresh-context review. The reviewer independently exercised all 12 CLI loops, witness/value extraction and malformed lengths, plus 36 adversarial examples and two five-task schedules. No substantive findings remain. The report is posted separately.Read-only external corpus
All runners, environments, logs and results live outside this repository and
~/Codes/pred-validation-corpus. All 32,372 corpus files, including.git, the existing environment, and caches, have identical SHA-256 snapshots before and after validation.For each of the 12 rules, all 100 independent corpus instances were checked: 1,200/1,200 actual CLI polynomials exactly match the independently certified constructor, including dimensions, coefficients and thresholds. For 845 YES/optimization cases, independent corpus witnesses also pass target energy, actual CLI extraction, source re-evaluation and aggregate recovery. The remaining 355 NO cases have exact-polynomial checks against independent NO truth; this is not a claim that every large target was independently solved.
A separate exact CP-SAT run on ten small instances per source solved 110/120 raw target polynomials and recovered corpus truth. Ten precedence-scheduling NO targets timed out at three seconds each; those target solves remain unavailable. Native exhaustive checks and corpus coefficient/oracle checks cover that rule separately. No corpus files or corpus-specific tests were added to this repository.
Explicitly deferred candidates
Primary formulation references consulted: Lucas 2014, Glover et al., O'Gorman et al., Venturelli et al., and Frederickson et al.. Literature formulations were checked against this repository's exact constructors and evaluators; they do not establish the deferred signed/floating variants.
References #1213. Keep it open for deferred candidates and later phases. Do not merge this draft.
Evidence comments: proof A, proof B, proof C, external validation, fresh review.
CI status: no GitHub workflow runs or Codecov report are available for this stacked base; the repository workflow filters target main/develop. Local gates passed. Fresh review has no findings; self-approval is disallowed by GitHub.