Repository navigation
Add Phase 3 conditional direct QUBO reductions - #1216
Merged
GiggleLiu merged 28 commits intoOct 29, 2026
Merged
Conversation
Collaborator
Author
Verification certificate — Phase 3 constructor and cross-comparisonVERIFIED for the seven implemented constructions, before Rust implementation, with finite testing limitations below. Phase 2 base: Type resolution against actual model impls in The three proof-only adversaries were fresh-context agents, supplied the corresponding proof but no constructor/Rust implementation. Independent targets were then cross-compared. Constructor checks: 12,000 size/structure instances, 111,461 expanded-vs-scalar checks; semantic runner: 6 symbolic groups, 12,174 cross-comparisons, 29,161 target assignments, 325 successful extractions, 144 complete forward/backward instances and 7 YES/7 NO worked examples. No final disagreements. Initial comparison found a self-precedence bug in the Python constructor (extra cross terms versus the proof's diagonal term); corrected before Rust, and both constructor runs repeated with zero failures. Enumeration covers explicitly bounded families, not all unbounded constructor domains. Larger cases use deterministic samples and Hypothesis. Exact family counts, seeds and settings follow in three adversary certificates. Python unbounded integers do not establish Rust range safety; native source-prefix/product, coefficient, count and allocation tests plus checked helper contracts address that separately. The two processing-bit size bounds cannot be expressed by the current registry's constant-integer-exponent contract; metadata is explicitly unavailable rather than a false polynomial bound. Run with Python + sympy + hypothesis, save constructor files together, run adversaries to create their shared-case files, then constructor_check.py and constructor_semantics.py. Paths in scripts refer to the session scratch directory and may be relocated together. Only read-only access is needed to any repository evidence. No external corpus is needed for this mathematical certificate. constructor-report.json{
"size_structure": 12000,
"expanded_vs_scalar": 111461,
"tardiness": 1800,
"weighted": 1800,
"release": 1800,
"storage": 1500,
"register": 1800,
"supersequence": 1800,
"betweenness": 1500
}constructor-semantics-report.json{
"symbolic": 6,
"cross_comparison": 12174,
"target_assignments": 29161,
"extraction": 325,
"forward_backward": 144,
"worked_yes": 7,
"worked_no": 7
}constructor.pyfrom collections import defaultdict
from itertools import combinations,product,permutations
class Poly:
def __init__(self,n):self.n=n;self.e=defaultdict(int);self.c=0
def add(self,i,j,v):self.e[min(i,j),max(i,j)]+=v
def square(self,terms,r=1,p=1):
self.c+=p*r*r
for k,(i,w) in enumerate(terms):
self.add(i,i,p*(w*w-2*r*w))
for j,v in terms[k+1:]:self.add(i,j,2*p*w*v)
def literal_product(self,u,v,p=1):
i,rev=u;j,rev2=v
self.c+=p*rev*rev2
self.add(i,i,p*(1-2*rev)*rev2);self.add(j,j,p*(1-2*rev2)*rev)
self.add(i,j,p*(1-2*rev)*(1-2*rev2))
def result(self):return self.n,{k:v for k,v in self.e.items() if v},self.c
def build(kind,d):
if kind in ('betweenness','register'):
n=d['n'];pairs=list(combinations(range(n),2));ix={p:i for i,p in enumerate(pairs)};q=Poly(len(pairs))
def lit(i,j):return ix[min(i,j),max(i,j)],int(i>j)
for i,j,k in combinations(range(n),3):
a,b,c=ix[i,j],ix[i,k],ix[j,k]
q.add(b,b,1);q.add(a,c,1);q.add(a,b,-1);q.add(b,c,-1)
if kind=='betweenness':
for a,b,c in d['triples']:
(i,r),(j,s)=lit(a,b),lit(b,c);q.square([(i,1-2*r),(j,2*s-1)],s-r)
else:
for v,u in d['arcs']:
i,r=lit(u,v);q.c+=1-r;q.add(i,i,2*r-1)
for w in range(n):
if w!=u and w!=v and d['registers'][w]==d['registers'][u]:q.literal_product(lit(u,w),lit(w,v))
return q.result()
if kind=='supersequence':
a=d['alphabet_size'];ss=d['strings'];L=sum(map(len,ss));k=a+1;off=L*k;q=Poly(off+L*L);P=L+1
q.c+=L
for p in range(L):q.add(p*k+a,p*k+a,-1);q.square([(p*k+s,1) for s in range(k)],p=P)
gc=0
for s in ss:
for j,ch in enumerate(s):
row=[off+gc*L+p for p in range(L)];q.square([(i,1) for i in row],p=P)
for p,i in enumerate(row):
q.add(i,i,P)
if ch<a:q.add(i,p*k+ch,-P)
if j+1<len(s):
for t in range(p+1):q.add(i,off+(gc+1)*L+t,P)
gc+=1
for p in range(L-1):q.add(p*k+a,p*k+a,P);q.add(p*k+a,(p+1)*k+a,-P)
return q.result()
slots=[];rows=[];cost=[]
if kind=='storage':
for i,(r,e,s) in enumerate(d['items']):
row=[]
for t in range(d['memory_size']-s+1):row.append(len(slots));slots.append((i,t,t+s));cost.append(0)
rows.append(row)
else:
H=sum(d['lengths'])
for i,p in enumerate(d['lengths']):
lo=d['release_times'][i] if kind=='release' else 0
hi=d['deadlines'][i]-p if kind=='release' else H-p
row=[]
for t in range(lo,hi+1):
row.append(len(slots));slots.append((i,t,t+p));cost.append(int(t+p>d['deadlines'][i]) if kind=='tardiness' else d['weights'][i]*max(0,t+p-d['deadlines'][i]) if kind=='weighted' else 0)
rows.append(row)
q=Poly(len(slots));P=sum(cost)+1
for i,v in enumerate(cost):q.add(i,i,v)
for row in rows:q.square([(i,1) for i in row],p=P)
for a,(i,s,e) in enumerate(slots):
for b,(j,t,f) in enumerate(slots[a+1:],a+1):
lifetime=kind!='storage' or (d['items'][i][0]<d['items'][j][1] and d['items'][j][0]<d['items'][i][1])
if i!=j and lifetime and not(e<=t or f<=s):q.add(a,b,P)
if kind=='tardiness':
for i,j in d.get('precedences',[]):
if i==j:
for a in rows[i]:q.add(a,a,P)
continue
for a in rows[i]:
for b in rows[j]:
if slots[a][1]>=slots[b][1]:q.add(a,b,P)
return q.result()
def energy(poly,bits):return poly[2]+sum(c*bits[i]*bits[j] for (i,j),c in poly[1].items())
CASES={
'tardiness':('MinimumTardinessSequencing/i64',{'lengths':[1,1,2],'deadlines':[1,2,3],'precedences':[]}),
'weighted':('SequencingToMinimizeWeightedTardiness',{'lengths':[1,0,1],'weights':[1,2,1],'deadlines':[0,0,1],'bound':2}),
'release':('SequencingWithReleaseTimesAndDeadlines',{'lengths':[1,2,1],'release_times':[0,0,2],'deadlines':[3,3,4]}),
'storage':('DynamicStorageAllocation',{'items':[[0,1,1],[1,2,1],[0,2,1]],'memory_size':2}),
'register':('FeasibleRegisterAssignment',{'n':3,'arcs':[[1,0],[2,1]],'registers':[0,0,0]}),
'supersequence':('ShortestCommonSupersequence',{'alphabet_size':2,'strings':[[0],[1]]}),
'betweenness':('Betweenness',{'n':3,'triples':[[0,1,2]]}),
}
def envelope(kind,d):
name=CASES[kind][0];d=dict(d)
if kind=='register':d={'num_vertices':d['n'],'arcs':d['arcs'],'assignment':d['registers'],'num_registers':max(d['registers'],default=-1)+1}
if kind=='betweenness':d={'num_elements':d['n'],'triples':d['triples']}
return {'type':name.split('/')[0],'variant':{'weight':'i64'} if kind=='tardiness' else {},'data':d}constructor_check.pyfrom constructor import *
import random,json
from pathlib import Path
rng=random.Random(73921);counts=defaultdict(int)
def scalar(kind,d,b):
if kind in ('betweenness','register'):
n=d['n'];pairs=list(combinations(range(n),2));ix={p:i for i,p in enumerate(pairs)}
def before(i,j):return b[ix[i,j]] if i<j else 1-b[ix[j,i]]
v=sum(before(i,j)==before(j,k) and before(i,k)!=before(i,j) for i,j,k in combinations(range(n),3))
if kind=='betweenness':return v+sum(before(a,c)!=before(c,e) for a,c,e in d['triples'])
v+=sum(not before(u,v) for v,u in d['arcs'])
v+=sum(before(u,w) and before(w,v) for v,u in d['arcs'] for w in range(n) if w not in (u,v) and d['registers'][u]==d['registers'][w])
return v
if kind=='supersequence':
a=d['alphabet_size'];ss=d['strings'];L=sum(map(len,ss));k=a+1;off=L*k;P=L+1
v=sum((sum(b[p*k:(p+1)*k])-1)**2 for p in range(L));g=0
for s in ss:
for j,ch in enumerate(s):
row=b[off+g*L:off+(g+1)*L];v+=(sum(row)-1)**2
v+=sum(row[p]*(1-b[p*k+ch] if ch<a else 1) for p in range(L))
if j+1<len(s):v+=sum(row[p]*b[off+(g+1)*L+t] for p in range(L) for t in range(p+1))
g+=1
v+=sum(b[p*k+a]*(1-b[(p+1)*k+a]) for p in range(L-1))
return L-sum(b[p*k+a] for p in range(L))+P*v
slots=[];rows=[];cost=[]
for i in range(len(d['items']) if kind=='storage' else len(d['lengths'])):
if kind=='storage':p=d['items'][i][2];lo=0;hi=d['memory_size']-p
else:p=d['lengths'][i];lo=d['release_times'][i] if kind=='release' else 0;hi=(d['deadlines'][i] if kind=='release' else sum(d['lengths']))-p
row=[]
for t in range(lo,hi+1):
row.append(len(slots));slots.append((i,t,t+p));cost.append(int(t+p>d['deadlines'][i]) if kind=='tardiness' else d['weights'][i]*max(0,t+p-d['deadlines'][i]) if kind=='weighted' else 0)
rows.append(row)
v=sum((sum(b[j] for j in row)-1)**2 for row in rows)
for x,(i,s,e) in enumerate(slots):
for y,(j,t,f) in enumerate(slots[x+1:],x+1):
overlap=kind!='storage' or (d['items'][i][0]<d['items'][j][1] and d['items'][j][0]<d['items'][i][1])
if i!=j and overlap and s<f and t<e:v+=b[x]*b[y]
if kind=='tardiness':
for i,j in d.get('precedences',[]):v+=sum(b[x] for x in rows[i]) if i==j else sum(b[x]*b[y] for x in rows[i] for y in rows[j] if slots[x][1]>=slots[y][1])
return sum(x*c for x,c in zip(b,cost))+(sum(cost)+1)*v
for kind in CASES:
for n in range(6):
if kind=='betweenness' and n==0:continue
if kind=='storage' and n==0:continue
for rep in range(300):
if kind in ('betweenness','register'):
d={'n':n}
if kind=='betweenness':d['triples']=[rng.sample(range(n),3) for _ in range(rng.randrange(7))] if n>=3 else []
else:d.update(arcs=[(i,j) for i in range(n) for j in range(n) if i!=j and rng.random()<.2],registers=[rng.randrange(3) for _ in range(n)])
elif kind=='supersequence':d={'alphabet_size':rng.randrange(1,3),'strings':[[rng.randrange(3)] for _ in range(n)] or [[]]}
elif kind=='storage':d={'items':[(r:=rng.randrange(3),r+rng.randrange(1,3),rng.randrange(1,3)) for _ in range(n)],'memory_size':2}
else:
d={'lengths':[rng.randrange(1 if kind=='tardiness' else 0,3) for _ in range(n)],'deadlines':[rng.randrange(-2 if kind=='tardiness' else 0,6) for _ in range(n)]}
if kind=='tardiness':d['precedences']=[(rng.randrange(n),rng.randrange(n)) for _ in range(rng.randrange(3))] if n else []
if kind=='weighted':d.update(weights=[rng.randrange(3) for _ in range(n)],bound=rng.randrange(6))
if kind=='release':d['release_times']=[rng.randrange(3) for _ in range(n)]
q=build(kind,d);N=q[0]
assert all(0<=i<=j<N and c!=0 for (i,j),c in q[1].items());assert len([1 for i,j in q[1] if i!=j])<=N*(N-1)//2;counts['size_structure']+=1
vectors=list(product((0,1),repeat=N)) if N<=5 else [[rng.randrange(2) for _ in range(N)] for _ in range(12)]
for b in vectors:
assert energy(q,b)==scalar(kind,d,b),(kind,d,b,energy(q,b),scalar(kind,d,b));counts['expanded_vs_scalar']+=1
counts[kind]+=1
out=Path(__file__).parent/'constructor-report.json';out.write_text(json.dumps(dict(counts),indent=2));print(dict(counts))constructor_semantics.pyfrom constructor import *
from pathlib import Path
import json,random,importlib.util,sympy as s
base=Path(__file__).parent
counts=defaultdict(int)
def module(path):
spec=importlib.util.spec_from_file_location(path.stem,path);m=importlib.util.module_from_spec(spec);import sys;sys.modules[path.stem]=m;spec.loader.exec_module(m);return m
adv_order=module(base/'order-adversary/check.py');adv_grid=module(base/'grid-adversary/grid_adversary.py');adv_scs=module(base/'supersequence-adversary/adversary.py')
def other(kind,d):
if kind in ('register','betweenness'):return adv_order.build(kind,d)
if kind=='supersequence':return adv_scs.build(kind,d)
d=dict(d)
if kind=='tardiness':kind='minimum'
if kind=='weighted':d['K']=d['bound']
if kind=='release':d['releases']=d['release_times']
if kind=='storage':d['D']=d['memory_size']
return adv_grid.build(kind,d)
def source(kind,d,x):
n=len(x)
if kind in ('register','betweenness'):
if sorted(x)!=list(range(n)):return None
if kind=='betweenness':return 0 if all((x[a]<x[b]<x[c]) or (x[c]<x[b]<x[a]) for a,b,c in d['triples']) else None
computed=set()
for v in sorted(range(n),key=lambda i:x[i]):
if any(u not in computed for w,u in d['arcs'] if w==v):return None
for u in computed:
if d['registers'][u]==d['registers'][v] and any(w!=v and w not in computed for w,z in d['arcs'] if z==u):return None
computed.add(v)
return 0
if kind=='storage':
if any(not 0<=x[i]<=d['memory_size']-z[2] for i,z in enumerate(d['items'])):return None
for i,j in combinations(range(n),2):
a,b=d['items'][i],d['items'][j]
if a[0]<b[1] and b[0]<a[1] and x[i]<x[j]+b[2] and x[j]<x[i]+a[2]:return None
return 0
if kind=='supersequence':
a=d['alphabet_size'];prefix=[];padding=False
for z in x:
if z==a:padding=True
elif z>a or padding:return None
else:prefix.append(z)
for st in d['strings']:
it=iter(prefix)
if not all(any(c==z for c in it) for z in st):return None
return len(prefix)
if sorted(x)!=list(range(n)):return None
ranks={j:i for i,j in enumerate(x)}
if kind=='tardiness' and any(ranks[a]>=ranks[b] for a,b in d.get('precedences',[])):return None
t=cost=0
for i in x:
if kind=='release':t=max(t,d['release_times'][i])
t+=d['lengths'][i]
if kind=='release' and t>d['deadlines'][i]:return None
if kind=='tardiness':cost+=t>d['deadlines'][i]
if kind=='weighted':cost+=d['weights'][i]*max(0,t-d['deadlines'][i])
return cost if kind!='weighted' or cost<=d['bound'] else None
def decode(kind,d,b):
if kind in ('register','betweenness'):
n=d['n'];r=[0]*n
for bit,(i,j) in zip(b,combinations(range(n),2)):r[j if bit else i]+=1
return r
if kind=='supersequence':
a=d['alphabet_size'];L=sum(map(len,d['strings']));return [b[p*(a+1):(p+1)*(a+1)].index(1) for p in range(L)]
vals=[];off=0
for i in range(len(d['items']) if kind=='storage' else len(d['lengths'])):
lo=0;hi=d['memory_size']-d['items'][i][2] if kind=='storage' else sum(d['lengths'])-d['lengths'][i]
if kind=='release':lo=d['release_times'][i];hi=d['deadlines'][i]-d['lengths'][i]
size=max(0,hi-lo+1);vals.append(lo+b[off:off+size].index(1));off+=size
return vals if kind=='storage' else sorted(range(len(vals)),key=lambda i:(vals[i],d['lengths'][i],i))
def check(kind,d):
q=build(kind,d);assert q==other(kind,d),(kind,d,q,other(kind,d));counts['cross_comparison']+=1
N=q[0]
if N>12:return
if kind in ('register','betweenness'):xs=permutations(range(d['n']))
elif kind=='storage':xs=product(*(range(d['memory_size']-z[2]+1) for z in d['items']))
elif kind=='supersequence':xs=product(range(d['alphabet_size']+1),repeat=sum(map(len,d['strings'])))
else:xs=permutations(range(len(d['lengths'])))
truth=[v for x in xs if (v:=source(kind,d,x)) is not None];best=min(truth,default=None)
# Exact accepted interval: nonnegative linear objective's full Boolean upper bound.
if kind=='supersequence':U=sum(map(len,d['strings']))
elif kind in ('tardiness','weighted'):
H=sum(d['lengths']);U=sum(int(t+p>d['deadlines'][i]) if kind=='tardiness' else d['weights'][i]*max(0,t+p-d['deadlines'][i]) for i,p in enumerate(d['lengths']) for t in range(H-p+1))
else:U=0
cap=min(U,d['bound']) if kind=='weighted' else U
feasible=[]
for b in product((0,1),repeat=N):
e=energy(q,b)
if e<=cap:
x=decode(kind,d,list(b));v=source(kind,d,x);assert v is not None,(kind,d,b,x,e)
if kind in ('tardiness','supersequence'):assert e==v
feasible.append(e);counts['extraction']+=1
counts['target_assignments']+=1
assert bool(feasible)==(best is not None),(kind,d,best)
if kind in ('tardiness','supersequence'):assert min(feasible,default=None)==best
counts['forward_backward']+=1
# Algebraic derivations of declared variable bounds and square coupling bounds.
n,h,T,D,L,a=s.symbols('n h T D L a',nonnegative=True)
for actual,bound in [(n*(n*2**h),n**2*2**h),(n*(n*2**h+1),n*(n*2**h+1)),(n*(T+1),n*(T+1)),(n*D,n*D),(L*(a+1)+L**2,L*(a+1)+L**2),(n*(n-1)/2,n*(n-1)/2)]:assert s.expand(actual-bound)==0;counts['symbolic']+=1
for kind,(_,d) in CASES.items():check(kind,d);counts['worked_yes']+=1
no={
'tardiness':dict(lengths=[1,1,1],deadlines=[3]*3,precedences=[(0,1),(1,2),(2,0)]),
'weighted':dict(lengths=[1,0,1],weights=[1,2,1],deadlines=[0,0,1],bound=0),
'release':dict(lengths=[1]*3,release_times=[0]*3,deadlines=[1]*3),
'storage':dict(items=[(0,1,1)]*3,memory_size=2),
'register':dict(n=3,arcs=[(1,0),(2,0)],registers=[0]*3),
'betweenness':dict(n=3,triples=[(0,1,2),(0,2,1)]),
'supersequence':dict(alphabet_size=1,strings=[[1]])}
for kind,d in no.items():check(kind,d);counts['worked_no']+=1
# All constructor-generated cases are cross-compared, with semantic exhaustive
# target/source checks on a bounded representative subset to keep costs explicit.
import runpy
scope=runpy.run_path(str(base/'constructor_check.py'))
# Replay its deterministic generator by instrumenting only the final build call.
text=(base/'constructor_check.py').read_text();text=text[:text.index("out=Path")];text=text.replace('q=build(kind,d);N=q[0]',"q=build(kind,d);N=q[0]\n assert q==other(kind,d), (kind,d);semantic_counts['cross_comparison']+=1\n if rep<4:check(kind,d)")
exec(compile(text,str(base/'constructor_check.py'),'exec'),dict(globals(),semantic_counts=counts))
(base/'constructor-semantics-report.json').write_text(json.dumps(dict(counts),indent=2));print(dict(counts)) |
Collaborator
Author
Verification certificate — Phase 3 grid independent adversaryVERIFIED, together with the constructor/cross-comparison certificate. Proof-only independent implementation; no production imports. Proof formatting was escaped for Typst compilation afterward; mathematical polynomials did not change. Machine-range guard clarifications were added after the fresh reviewer reproduced two boundary failures, each covered by a red-then-green Rust regression. All three proof PDFs compile. Finite coverage and untested machine/resource limits are stated in the report. The constructor script is in the companion certificate; this comment contains the independent script and full proof. Independent report
The public interface is Schemas:
Executed checksAll 10,241 instances passed independent source-versus-target aggregate recovery. Source minima were computed by all order permutations; source decision values used permutations or all legal address assignments. Target accepted assignments were solved by complete row enumeration and pruning using polynomial coefficients alone. The nonnegative penalty gap rules out all other bit vectors; 67 instances additionally enumerated the full Boolean cube, recovered the actual unrestricted QUBO/decision optimum, and compared it with the source result. The run checked 62,217 Boolean target configurations, including 7,327 accepted and 54,890 rejected configurations. Each configuration compared the sparse polynomial energy against a separately expanded sum of row and conflict penalties. Accepted configurations were decoded and re-evaluated at the source. Minimum tardiness recovered its exact count; weighted tardiness recovered the exact selected cost as well as the decision result. Rejected configurations were confirmed to return no extracted witness. There are 300 random instances for every size n=1,...,5 in each of the four families: 6,000 total. The following finite subfamilies were exhausted for every n=1,...,5:
Two independently generated Hypothesis strategies each completed 350 examples: weighted instances forced to contain zero-duration tasks, and release instances containing arbitrary nonnegative windows including empty/reversed windows. Both generate n=1,...,5 and disable timing deadlines, with deterministic generation. All eight theorem examples were reproduced by full Boolean-cube enumeration: minimum optimum 1 and cyclic infeasibility; weighted YES at K=2 and NO at K=0; release YES/NO; storage YES/NO. Extra shared examples cover negative deadlines, self and duplicate precedences, multiple zero ties, all-zero durations, empty rows, reversed release windows, release boundary zeros, and storage items filling the entire capacity. Symbolic and structural auditRow identity and penalty gap. SymPy verified the Boolean multilinear identity Exact horizon and optimization recovery. For either full-horizon construction, Zero-duration ties. A zero at an interior point of a positive interval fails both disjunctive inequalities and is penalized. At a shared boundary it is permitted. Sorting Release extraction. The same ordering guarantees that the preceding selected finish is no greater than the next selected start. Inductively, earliest execution starts at Precedence infeasibility. Positive processing makes ordering by start equivalent to ordering by permutation position. A directed cycle cannot satisfy strict increasing starts. A self edge contributes P to every selected option in its row: an empty row selection costs P, and a nonempty one also costs at least P. Duplicate precedence edges only increase nonnegative penalties. The tests include both cases. Storage endpoints. Strict lifetime overlap permits touching lifetimes to reuse an address; strict address overlap permits adjacent occupied intervals. Legal choices imply address+size<=D, so decoded address endpoints are representable whenever D is. A full-capacity item has exactly one address choice. Pairwise exclusion is sufficient because simultaneous storage feasibility is defined pairwise. Integer guards. Independent big-integer boundary checks establish that (1) two processing lengths may overflow an i64 horizon even when each is valid; (2) the weighted source upper bound may overflow; (3) U may exceed the source upper bound because it sums costs of alternative choices; (4) U may fit while U+1 does not; and (5) comparing completion with i64::MIN is safe mathematically while subtracting that deadline would overflow. A one-task weighted instance with p=1,w=i64::MAX,d=0 has U=i64::MAX and P=i64::MAX+1, so the stated construction correctly requires rejection. The independent builder deliberately uses arbitrary precision and does not implement rejection as a substitute for validating these necessary guards. For any stored target polynomial, if the sum of positive coefficients is at most i64::MAX and the sum of negative coefficients is at least i64::MIN, every partial sum of active coefficients lies in that interval, regardless of accumulation order. The additional constant and decision-bound checks are still necessary: safe E alone does not establish safe E+c or min(K,U)-c. The proof explicitly requires those checks. If implementation computes E+c in i64, the mapping must handle overflow as an out-of-interval result or use wider/checked arithmetic; this review does not inspect that implementation. Coefficient and size bounds. With q precedence occurrences, each off-diagonal coefficient accumulates at most LimitsThe finite tests exhaust the specified subfamilies, not all unbounded integer inputs. Full Boolean cubes were exhausted only for 67 small cases; larger cases used complete accepted-row search plus the independently checked nonnegative penalty proof. Huge horizons/capacities were assessed by symbolic bounds without allocation. Repository implementations, runtime overflow handling, reduction registration, and external artifacts were not inspected or verified by this proof-only adversary. Typst proof= Direct start and address choices
Theorem. Three scheduling constructions and one storage construction below preserve their exact endpoint semantics. All witnesses use Boolean target choices. MinimumTardinessSequencing<i64> has positive lengths, signed deadlines, arbitrary in-range precedences, Min<i64> objective counting late tasks, and order-permutation witness. WeightedTardiness has nonnegative i64 lengths, weights, deadlines and bound K, Or value and order-permutation witness. Release/deadline sequencing has nonnegative i64 data, Or value and order witness interpreted by earliest-start execution. Storage has nonempty items (arrival,departure,size) with departure>arrival and 1<=size<=positive usize D; Or value, address vector witness.
_Construction._ 1. For minimum tardiness and weighted tardiness set H=sum p_j. Check H fits i64. Task j has one choice per integer start t=0,...,H-p_j. Cost is [t+p_j>d_j] for minimum tardiness, and w_j max(0,t+p_j-d_j) for weighted tardiness. For the latter check sum_j w_j max(0,H-d_j) fits i64, bounding all source products and prefix sums. For minimum tardiness all elapsed times are bounded by H and cost by n.
2. For release/deadline sequencing first check max release + sum lengths fits i64 (empty maximum zero). This bounds every source finish addition, even for infeasible permutations; otherwise return typed IntegerOverflow. Choices are t=r_j,...,d_j-p_j; the row is empty when r_j>d_j or p_j>d_j-r_j. Its cost is zero. Endpoints use subtraction before addition to avoid overflow. For storage, item i has addresses 0,...,D-size_i, cost zero. All counts and totals are checked before allocation.
3. Each row receives (sum x-1)^2. For schedules add x_jt*x_ku for each pair of distinct tasks with neither t+p_j<=u nor u+p_k<=t. This excludes a zero-duration task strictly inside a positive task, and permits equal-time zero tasks. For minimum tardiness also add conflicts for each precedence (j,k) and choices with t>=u; self precedences add their row's diagonal choices, guaranteeing infeasibility. For storage add conflicts only if lifetimes overlap strictly and the two chosen address intervals overlap strictly.
4. Let F be the linear cost and U the sum of all nonnegative choice costs. Compute U and P=U+1 with checked arithmetic. Multiply all row/conflict penalties by P; zero-cost feasibility uses P=1. Let Q=F+P V, where V is their sum. Drop constant c to get E. Minimum tardiness target is QUBO; source value is E+c if 0<=E+c<=U, otherwise Min(None). Weighted tardiness target is DecisionQUBO with bound min(K,U)-c. Release and storage use DecisionQUBO bound -c. Check constant, bounds, every coefficient and sums of positive and negative target coefficients in i64.
_Correctness, forward._ A permutation of positive/nonnegative tasks gives prefix starts in [0,H-p_j], no disjunctive conflicts, and exactly its source cost. Minimum tardiness precedences imply strict starts because all lengths are positive. A feasible release schedule's earliest starts satisfy its windows and conflicts. A source storage witness chooses each legal address and no simultaneous address overlap. All row penalties vanish.
_Correctness, backward._ V is a nonnegative integer. If a row or conflict is violated, Q>=P>U. Every target within the accepted cost interval therefore chooses exactly one legal option per row and avoids every conflict. A minimum tardiness schedule fills all H units with total positive processing H, so there is no idle time: sorting starts gives exact prefix completion times, precedences and cost. Weighted tardiness permits zero-length tasks; sort by (start,length,index), so zero tasks precede positive tasks at equal starts. No zero task lies strictly inside a positive task. Positive intervals fill H, and zeros occur at their boundaries, hence source completion times and cost equal the selected costs. Release schedules sorted the same way have earliest execution no later than the selected starts by induction; release/deadline feasibility follows. Each reconstructed source finish is bounded by its selected finish<=deadline, so the source's unchecked addition is representable on decoded witnesses. Storage row choices give endpoints<=D, preventing address overflow, and all simultaneous overlaps were penalized.
_Extraction and aggregate recovery._ Validate target once against its value predicate, decode one start/address per row, sort starts for scheduling and return task indices; storage returns addresses. Minimum tardiness maps completed optimum through the omitted constant and infeasibility interval. Feasibility maps Or identically. Cyclic/self precedence sources have no zero-penalty assignment, and their optimum lies above U, recovering Min(None). Target configurations outside the predicate are rejected, never repaired.
_Overhead._ Let S be total choices. Exactly S bits, at most S(S-1)/2 couplings, no auxiliary bits. Minimum tardiness S<=n^2*2^h for processing magnitude bits h (positive lengths); weighted tardiness S<=n*(n*2^h+1); release S<=n*(T+1), T=max deadline; storage S<=nD. Use these squared upper bounds for couplings. Construction O(S^2 + q*S^2) in a simple precedence loop with q precedences, or O(S^2) without precedences, and sparse accumulation logarithms. Scheduling grids and address grids are pseudopolynomial in numeric H,T,D, exponential in their bit lengths. No universal saving over compact binary arithmetic. Extraction O(S+n log n), or O(S) storage. Coefficients are bounded by accumulated penalties and U; their bit lengths depend on input magnitudes and number of repeated constraints.
_Examples._ Minimum tardiness: lengths [1,1,2], deadlines [1,2,3], no precedences. H=4, row lengths [4,4,3], S=11. Order [0,1,2] completes [1,2,4], cost 1, optimal because all tasks cannot be on time. Adding precedences [(0,1),(1,2),(2,0)] is NO (Min(None)); no strict total order respects the cycle.
Weighted tardiness: lengths [1,0,1], weights [1,2,1], deadlines [0,0,1], K=2. H=2, counts [2,3,2], S=7. Order [1,0,2] costs 0+1+1=2. K=0 is NO because first positive completion already costs at least one.
Release: lengths [1,2,1], releases [0,0,2], deadlines [3,3,4]. Choices [0,1,2], [0,1], [2,3], S=7. Starts [0,1,3], order [0,1,2] give finishes [1,3,4], YES. Three unit tasks each with release 0 and deadline 1 yield three bits, all chosen; every pair conflicts, so NO.
Storage: items [(0,1,1),(1,2,1),(0,2,1)], D=2. S=6. Addresses [0,0,1] are YES: the first two lifetimes touch, allowing reuse. Three unit items all alive [0,1) in D=2 are NO by the pigeonhole principle. All cases have at least three source variables.
Complexity clarification: the stated extraction costs describe decoding after validation; include O(N+E_count) for evaluating the target once. Alphabet symbols and all indices are intrinsically unsigned usize.
Registry clarification: the two processing-horizon rules expose unavailable parameter transforms because the registry contract accepts constant integer exponents only. The exponential-in-h bounds above remain mathematical bounds, not registered polynomial metadata. Release/deadline and storage bounds retain their explicit numeric horizon/capacity parameters.
Independent adversary"""Independent executable reconstruction of proof-grid.typ (no repository imports).
Public build(kind, data) -> (N, {(i,j): integer coefficient}, integer constant).
Indices are zero-based; only i <= j are present and zero coefficients are omitted.
E(bits) = sum(a[i,j] * bits[i] * bits[j]); Q = E + constant.
Kinds/schema:
minimum: {lengths: [positive int], deadlines: [signed int], precedences: [[j,k], ...]}
weighted: {lengths: [nonnegative int], weights: [nonnegative int], deadlines: [nonnegative int], K: nonnegative int}
release: {lengths: [nonnegative int], releases: [nonnegative int], deadlines: [nonnegative int]}
storage: {items: [[arrival, departure, size], ...], D: positive int}
Rows follow input item order; each row's starts/addresses ascend. Arbitrary precision
integers are intentional; this verifier separately checks the stated i64 guards.
"""
from collections import defaultdict
from itertools import combinations, permutations, product
import json
import random
from pathlib import Path
KINDS = ('minimum', 'weighted', 'release', 'storage')
OUT = Path(__file__).parent
COUNTS = defaultdict(int)
def grids(kind, data):
if kind in ('minimum', 'weighted'):
horizon = sum(data['lengths'])
return [list(range(horizon - p + 1)) for p in data['lengths']]
if kind == 'release':
return [list(range(r, d - p + 1)) for p, r, d in zip(data['lengths'], data['releases'], data['deadlines'])]
if kind == 'storage':
return [list(range(data['D'] - item[2] + 1)) for item in data['items']]
raise ValueError(kind)
def option_cost(kind, data, j, start):
if kind == 'minimum':
return int(start + data['lengths'][j] > data['deadlines'][j])
if kind == 'weighted':
return data['weights'][j] * max(0, start + data['lengths'][j] - data['deadlines'][j])
return 0
def build(kind, data):
rows = grids(kind, data)
variables = []
indices = []
for j, row in enumerate(rows):
indices.append(list(range(len(variables), len(variables) + len(row))))
variables.extend((j, t) for t in row)
costs = [option_cost(kind, data, j, t) for j, t in variables]
penalty = sum(costs) + 1
entries = defaultdict(int)
for row in indices:
for i in row:
entries[i, i] -= penalty
for i, k in combinations(row, 2):
entries[i, k] += 2 * penalty
for i, cost in enumerate(costs):
entries[i, i] += cost
for a, (j, t) in enumerate(variables):
for b in range(a + 1, len(variables)):
k, u = variables[b]
if j == k:
continue
if kind == 'storage':
aj, dj, sj = data['items'][j]
ak, dk, sk = data['items'][k]
forbidden = max(aj, ak) < min(dj, dk) and max(t, u) < min(t + sj, u + sk)
else:
forbidden = not (t + data['lengths'][j] <= u or u + data['lengths'][k] <= t)
if forbidden:
entries[a, b] += penalty
if kind == 'minimum':
for j, k in data.get('precedences', []):
if j == k:
for a in indices[j]:
entries[a, a] += penalty
else:
for a in indices[j]:
for b in indices[k]:
if variables[a][1] >= variables[b][1]:
entries[min(a, b), max(a, b)] += penalty
return len(variables), {pair: value for pair, value in sorted(entries.items()) if value}, len(rows) * penalty
def energy(polynomial, bits):
n, entries, _ = polynomial
assert len(bits) == n and all(b in (0, 1) for b in bits)
return sum(coefficient * bits[a] * bits[b] for (a, b), coefficient in entries.items())
def source(kind, data, witness):
n = len(data['items']) if kind == 'storage' else len(data['lengths'])
if kind == 'storage':
if len(witness) != n:
return False
for addr, item in zip(witness, data['items']):
if addr < 0 or addr + item[2] > data['D']:
return False
for j, k in combinations(range(n), 2):
aj, dj, sj = data['items'][j]
ak, dk, sk = data['items'][k]
if aj < dk and ak < dj:
if witness[j] < witness[k] + sk and witness[k] < witness[j] + sj:
return False
return True
if sorted(witness) != list(range(n)):
return None if kind == 'minimum' else False
if kind == 'minimum':
positions = {j: k for k, j in enumerate(witness)}
if any(positions[j] >= positions[k] for j, k in data.get('precedences', [])):
return None
elapsed = 0
cost = 0
for j in witness:
if kind == 'release':
elapsed = max(elapsed, data['releases'][j])
elapsed += data['lengths'][j]
if kind == 'release' and elapsed > data['deadlines'][j]:
return False
if kind == 'minimum':
cost += elapsed > data['deadlines'][j]
if kind == 'weighted':
cost += data['weights'][j] * max(0, elapsed - data['deadlines'][j])
if kind == 'minimum':
return cost
if kind == 'weighted':
return cost <= data['K']
return True
def weighted_cost(data, order):
elapsed = result = 0
for j in order:
elapsed += data['lengths'][j]
result += data['weights'][j] * max(0, elapsed - data['deadlines'][j])
return result
def upper(kind, data):
return sum(option_cost(kind, data, j, t) for j, row in enumerate(grids(kind, data)) for t in row)
def predicate(kind, data, polynomial, bits):
q = energy(polynomial, bits) + polynomial[2]
u = upper(kind, data)
if kind == 'minimum':
return 0 <= q <= u
if kind == 'weighted':
return q <= min(data['K'], u)
return q <= 0
def extract(kind, data, polynomial, bits):
if not predicate(kind, data, polynomial, bits):
return None
chosen = []
offset = 0
for row in grids(kind, data):
selected = [value for i, value in enumerate(row, offset) if bits[i]]
assert len(selected) == 1
chosen.append(selected[0])
offset += len(row)
if kind == 'storage':
return chosen
return sorted(range(len(chosen)), key=lambda j: (chosen[j], data['lengths'][j], j))
def direct_q(kind, data, bits):
rows = grids(kind, data)
selections = []
offset = 0
violation = 0
cost = 0
for j, row in enumerate(rows):
selected = [t for i, t in enumerate(row, offset) if bits[i]]
selections.append(selected)
violation += (len(selected) - 1) ** 2
cost += sum(option_cost(kind, data, j, t) for t in selected)
offset += len(row)
for j, k in combinations(range(len(rows)), 2):
for t, u in product(selections[j], selections[k]):
if kind == 'storage':
a, b, size = data['items'][j]
c, d, other = data['items'][k]
if a < d and c < b and t < u + other and u < t + size:
violation += 1
elif t + data['lengths'][j] > u and u + data['lengths'][k] > t:
violation += 1
if kind == 'minimum':
for j, k in data.get('precedences', []):
if j == k:
violation += len(selections[j])
else:
violation += sum(t >= u for t, u in product(selections[j], selections[k]))
return cost + (upper(kind, data) + 1) * violation, cost, violation
def source_optimum(kind, data):
if kind == 'storage':
return any(source(kind, data, addr) for addr in product(*grids(kind, data)))
n = len(data['lengths'])
if kind == 'minimum':
values = [value for p in permutations(range(n)) if (value := source(kind, data, p)) is not None]
return min(values) if values else None
return any(source(kind, data, p) for p in permutations(range(n)))
def target_row_optimum(kind, data, polynomial):
"""Solve valid rows using polynomial entries only, not source feasibility logic.
Row enumeration is exhaustive. The nonnegative penalty proof excludes all
other bit vectors from acceptance; separate small instances enumerate every
bit vector and verify this exclusion directly.
"""
rows = grids(kind, data)
offsets = []
offset = 0
for row in rows:
offsets.append(list(range(offset, offset + len(row))))
offset += len(row)
penalty = upper(kind, data) + 1
entries = polynomial[1]
best = None
best_bits = None
def visit(j, selected, subtotal):
nonlocal best, best_bits
if j == len(rows):
q = subtotal + polynomial[2]
if best is None or q < best:
best = q
best_bits = [int(a in selected) for a in range(polynomial[0])]
return
for a in offsets[j]:
diag = entries.get((a, a), 0)
if diag >= 0: # With self penalties; every ordinary cost is < P.
continue
couplings = sum(entries.get((b, a), 0) for b in selected)
if couplings >= penalty:
continue
visit(j + 1, selected + [a], subtotal + diag + couplings)
visit(0, [], 0)
if kind == 'minimum':
return best, best_bits
if kind == 'weighted':
return best is not None and best <= min(data['K'], upper(kind, data)), best_bits
return best is not None and best <= 0, best_bits
def check_bits(kind, data, polynomial, bits):
q, cost, v = direct_q(kind, data, bits)
assert energy(polynomial, bits) + polynomial[2] == q, (kind, data, bits, 'polynomial expansion')
if v:
assert q > upper(kind, data), (kind, data, bits, 'penalty gap')
accepted = predicate(kind, data, polynomial, bits)
witness = extract(kind, data, polynomial, bits)
assert (witness is not None) == accepted
if accepted:
assert v == 0
value = source(kind, data, witness)
if kind == 'minimum':
assert value == q
else:
assert value is True
if kind == 'weighted':
assert weighted_cost(data, witness) == cost
COUNTS['accepted_witnesses'] += 1
else:
COUNTS['rejected_witnesses'] += 1
COUNTS['bit_vectors'] += 1
def check_instance(kind, data, rng, exhaustive_bits=False):
polynomial = build(kind, data)
actual, bits = target_row_optimum(kind, data, polynomial)
expected = source_optimum(kind, data)
assert actual == expected, (kind, data, actual, expected)
COUNTS['instances'] += 1
COUNTS['instances_' + kind] += 1
if bits is not None:
check_bits(kind, data, polynomial, bits)
nbits = polynomial[0]
if exhaustive_bits:
assert nbits <= 16
values = []
for candidate in product((0, 1), repeat=nbits):
check_bits(kind, data, polynomial, candidate)
values.append(energy(polynomial, candidate) + polynomial[2])
qmin = min(values)
if kind == 'minimum':
recovered = qmin if 0 <= qmin <= upper(kind, data) else None
elif kind == 'weighted':
recovered = qmin <= min(data['K'], upper(kind, data))
else:
recovered = qmin <= 0
assert recovered == expected
COUNTS['full_cube_instances'] += 1
else:
for candidate in ([0] * nbits, [1] * nbits, [rng.randrange(2) for _ in range(nbits)]):
check_bits(kind, data, polynomial, candidate)
return polynomial
def examples():
return [
('minimum_yes', 'minimum', dict(lengths=[1, 1, 2], deadlines=[1, 2, 3], precedences=[]), 1),
('minimum_no', 'minimum', dict(lengths=[1, 1, 2], deadlines=[1, 2, 3], precedences=[[0, 1], [1, 2], [2, 0]]), None),
('weighted_yes', 'weighted', dict(lengths=[1, 0, 1], weights=[1, 2, 1], deadlines=[0, 0, 1], K=2), True),
('weighted_no', 'weighted', dict(lengths=[1, 0, 1], weights=[1, 2, 1], deadlines=[0, 0, 1], K=0), False),
('release_yes', 'release', dict(lengths=[1, 2, 1], releases=[0, 0, 2], deadlines=[3, 3, 4]), True),
('release_no', 'release', dict(lengths=[1, 1, 1], releases=[0, 0, 0], deadlines=[1, 1, 1]), False),
('storage_yes', 'storage', dict(items=[[0, 1, 1], [1, 2, 1], [0, 2, 1]], D=2), True),
('storage_no', 'storage', dict(items=[[0, 1, 1]] * 3, D=2), False),
('minimum_negative', 'minimum', dict(lengths=[1, 2, 1], deadlines=[-3, -1, 2], precedences=[]), 2),
('minimum_self', 'minimum', dict(lengths=[1], deadlines=[1], precedences=[[0, 0]]), None),
('minimum_duplicate_edges', 'minimum', dict(lengths=[1, 1], deadlines=[0, 2], precedences=[[0, 1], [0, 1]]), 1),
('weighted_zero_ties', 'weighted', dict(lengths=[2, 0, 0, 1], weights=[1, 3, 4, 2], deadlines=[0, 0, 0, 1], K=6), True),
('weighted_all_zero', 'weighted', dict(lengths=[0, 0, 0], weights=[0, 5, 1], deadlines=[0, 0, 4], K=0), True),
('release_empty_row', 'release', dict(lengths=[2, 1], releases=[1, 0], deadlines=[2, 2]), False),
('release_reverse_window', 'release', dict(lengths=[0], releases=[3], deadlines=[2]), False),
('release_zero_boundary', 'release', dict(lengths=[2, 0, 1], releases=[0, 2, 2], deadlines=[2, 2, 3]), True),
('storage_full_size', 'storage', dict(items=[[0, 2, 3], [2, 3, 3]], D=3), True),
]
def random_instance(kind, n, rng):
if kind == 'minimum':
lengths = [rng.randrange(1, 3) for _ in range(n)]
h = sum(lengths)
return dict(lengths=lengths, deadlines=[rng.randrange(-2, h + 2) for _ in range(n)],
precedences=[[j, k] for j in range(n) for k in range(n) if rng.random() < .10])
if kind == 'weighted':
lengths = [rng.randrange(0, 3) for _ in range(n)]
h = sum(lengths)
return dict(lengths=lengths, weights=[rng.randrange(4) for _ in range(n)],
deadlines=[rng.randrange(h + 2) for _ in range(n)], K=rng.randrange(3 * h * n + 2))
if kind == 'release':
return dict(lengths=[rng.randrange(3) for _ in range(n)], releases=[rng.randrange(4) for _ in range(n)],
deadlines=[rng.randrange(6) for _ in range(n)])
d = rng.randrange(1, 4)
items = []
for _ in range(n):
a = rng.randrange(4)
items.append([a, a + rng.randrange(1, 4), rng.randrange(1, d + 1)])
return dict(items=items, D=d)
def exhaustive_families(rng):
# Exhaust every member of these finite families at each n <= 5.
for n in range(1, 6):
edgesets = [[]] + [[[j, k]] for j in range(n) for k in range(n)]
if n > 1:
edgesets += [[[j, (j + 1) % n] for j in range(n)]]
for ds, edges in product(product((0, n), repeat=n), edgesets):
check_instance('minimum', dict(lengths=[1] * n, deadlines=list(ds), precedences=edges), rng)
COUNTS['exhaustive_minimum_n' + str(n)] += 1
for ps in product((0, 1), repeat=n):
for bound in range(n * (n + 1) // 2 + 1):
check_instance('weighted', dict(lengths=list(ps), weights=[1] * n, deadlines=[0] * n, K=bound), rng)
COUNTS['exhaustive_weighted_n' + str(n)] += 1
for ps, ds in product(product((0, 1), repeat=n), product((0, 1), repeat=n)):
check_instance('release', dict(lengths=list(ps), releases=[0] * n, deadlines=list(ds)), rng)
COUNTS['exhaustive_release_n' + str(n)] += 1
for starts, d in product(product((0, 1), repeat=n), (1, 2)):
check_instance('storage', dict(items=[[a, a + 1, 1] for a in starts], D=d), rng)
COUNTS['exhaustive_storage_n' + str(n)] += 1
def hypothesis_checks():
from hypothesis import given, settings, strategies as st, HealthCheck
@st.composite
def zero_tie_instances(draw):
n = draw(st.integers(1, 5))
ps = draw(st.lists(st.integers(0, 2), min_size=n, max_size=n))
ps[draw(st.integers(0, n - 1))] = 0
return dict(lengths=ps, weights=draw(st.lists(st.integers(0, 4), min_size=n, max_size=n)),
deadlines=draw(st.lists(st.integers(0, sum(ps) + 1), min_size=n, max_size=n)), K=draw(st.integers(0, 25)))
@st.composite
def window_instances(draw):
n = draw(st.integers(1, 5))
ps = draw(st.lists(st.integers(0, 3), min_size=n, max_size=n))
rs = draw(st.lists(st.integers(0, 4), min_size=n, max_size=n))
ds = draw(st.lists(st.integers(0, 5), min_size=n, max_size=n))
return dict(lengths=ps, releases=rs, deadlines=ds)
@settings(max_examples=350, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow])
@given(zero_tie_instances())
def zeros(data):
check_instance('weighted', data, random.Random(901))
COUNTS['hypothesis_zero_ties'] += 1
@settings(max_examples=350, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow])
@given(window_instances())
def windows(data):
check_instance('release', data, random.Random(902))
COUNTS['hypothesis_windows'] += 1
zeros()
windows()
def symbolic_checks():
import sympy as s
a, b, c = s.symbols('a b c')
expanded = s.expand((a + b + c - 1) ** 2)
boolean = expanded.xreplace({a**2: a, b**2: b, c**2: c})
assert s.expand(boolean - (1 - a - b - c + 2*a*b + 2*a*c + 2*b*c)) == 0
u, f, excess = s.symbols('U F excess', integer=True, nonnegative=True)
assert s.expand(f + (u + 1) * (1 + excess) - u) == f + u*excess + excess + 1
n, h, total = s.symbols('n h H', integer=True, nonnegative=True)
assert s.expand(n * (total + 1) - total - ((n-1)*total+n)) == 0
# sum(H-p_j+1)=(n-1)H+n. This verifies the exact choice count,
# stronger than the stated bound once H<=n*2^h is substituted.
COUNTS['symbolic_identities'] = 3
def boundaries(rng):
maximum = 2**63 - 1
# Small grids with large numeric costs/deadlines: arithmetic is checked
# symbolically using Python integers, not by allocating huge grids.
data = dict(lengths=[1, 1], deadlines=[-2**63, maximum], precedences=[])
check_instance('minimum', data, rng, exhaustive_bits=True)
assert sum([maximum, 1]) > maximum
assert maximum * max(0, 2 - 0) > maximum
data = dict(lengths=[1], weights=[maximum], deadlines=[0], K=maximum)
n, entries, constant = build('weighted', data)
assert n == 1 and constant == maximum + 1
assert upper('weighted', data) <= maximum < upper('weighted', data) + 1
# U may exceed the source upper bound: guards for both are necessary.
data = dict(lengths=[1, 1], weights=[1, 1], deadlines=[0, 0], K=3)
assert upper('weighted', data) == 6 > sum(w * max(0, sum(data['lengths']) - d) for w, d in zip(data['weights'], data['deadlines'])) == 4
# Signed minimum deadlines must use comparison, never subtract MIN from H.
assert 1 > -2**63 and 1 - (-2**63) > maximum
# A gap in a selected release schedule disappears under earliest execution.
data = dict(lengths=[1, 1], releases=[0, 0], deadlines=[4, 4])
poly = build('release', data)
bits = [0, 1, 0, 0, 0, 0, 0, 1] # starts 1 and 3 -> earliest starts 0 and 1
assert extract('release', data, poly, bits) == [0, 1]
check_bits('release', data, poly, bits)
# A zero task strictly inside a positive task is forbidden; boundaries work.
data = dict(lengths=[2, 0], weights=[1, 1], deadlines=[0, 0], K=4)
poly = build('weighted', data)
for zero, expected in [(0, [1, 0]), (1, None), (2, [0, 1])]:
bits = [1] + [int(t == zero) for t in range(3)]
assert extract('weighted', data, poly, bits) == expected
check_bits('weighted', data, poly, bits)
# Empty scheduling instances: one empty permutation, zero objective.
for kind, data in [('minimum', dict(lengths=[], deadlines=[], precedences=[])),
('weighted', dict(lengths=[], weights=[], deadlines=[], K=0)),
('release', dict(lengths=[], releases=[], deadlines=[]))]:
check_instance(kind, data, rng, exhaustive_bits=True)
COUNTS['boundary_groups'] = 9
def main():
rng = random.Random(20261022)
shared = []
for name, kind, data, expected in examples():
assert source_optimum(kind, data) == expected, (name, 'example source mismatch')
poly = check_instance(kind, data, rng, exhaustive_bits=True)
shared.append(dict(name=name, kind=kind, data=data, expected=expected,
N=poly[0], constant=poly[2], entries=[[a, b, value] for (a, b), value in poly[1].items()]))
for kind in KINDS:
for n in range(1, 6):
for sample in range(300):
data = random_instance(kind, n, rng)
poly = check_instance(kind, data, rng, exhaustive_bits=(sample < 3 and sum(map(len, grids(kind, data))) <= 12))
COUNTS['random_' + kind + '_n' + str(n)] += 1
if sample < 3:
shared.append(dict(name=f'{kind}_n{n}_sample{sample}', kind=kind, data=data,
expected=source_optimum(kind, data), N=poly[0], constant=poly[2],
entries=[[a, b, value] for (a, b), value in poly[1].items()]))
print(kind, n, 'random complete', flush=True)
exhaustive_families(rng)
print('exhaustive families complete', flush=True)
hypothesis_checks()
symbolic_checks()
boundaries(rng)
(OUT / 'shared_cases.json').write_text(json.dumps(shared, indent=2) + '\n')
(OUT / 'results.json').write_text(json.dumps(dict(COUNTS), indent=2, sort_keys=True) + '\n')
print(json.dumps(dict(COUNTS), sort_keys=True), flush=True)
if __name__ == '__main__':
main() |
Collaborator
Author
Verification certificate — Phase 3 order independent adversaryVERIFIED, together with the constructor/cross-comparison certificate. Proof-only independent implementation; no production imports. Proof formatting was escaped for Typst compilation afterward; mathematical polynomials did not change. Machine-range guard clarifications were added after the fresh reviewer reproduced two boundary failures, each covered by a red-then-green Rust regression. All three proof PDFs compile. Finite coverage and untested machine/resource limits are stated in the report. The constructor script is in the companion certificate; this comment contains the independent script and full proof. Independent reportDependencies: Python 3.12.14, SymPy 1.14.0, Hypothesis 6.170.5. The supplied phase2 environment initially lacked the packages; they were installed with Import
Independent semanticsBetweenness is evaluated by the strict inequalities For every instance, all source permutations and all Coverage and counts82,738 instances passed, with zero failures:
Exhaustive finite families:
For all Unbounded duplicate multiplicities make literal exhaustive enumeration of all legal instances impossible even for fixed small Symbolic derivation and proof-claim mapThere is one comparison bit per unordered pair, so Triangle blocks have coefficient absolute sum 4. A squared difference of two Boolean literals has absolute coefficient sum at most 6. Thus the full betweenness polynomial has absolute coefficient sum at most For an individual coefficient, triangles contribute at most There are
For a general tournament, the proof's shortest-cycle chord argument establishes triangle-free implies transitive beyond tested sizes. The operational source oracle confirms the register interpretation, but compatibility with the repository's concrete model evaluator remains a parent responsibility because repository code was intentionally excluded. Worked examplesWriting
All four examples were reproduced by the independent source and target evaluators. No Rust compilation, implementation inspection, corpus access, repository edit, Git operation, or GitHub action was performed. Concrete i64 overflow rejection and allocation behavior are unverified; Python arithmetic is exact and unbounded. Cross-comparison with the constructor is pending outside this isolated adversary audit. Typst proof#set page(width: 210mm, height: 297mm)
= Direct integer order encodings
Theorem. The following constructions preserve feasibility and completed Or values, from position-permutation witnesses to Decision\<QUBO\<i64\>\> Boolean witnesses, subject to checked representability of coefficients, constant, threshold and all sums of positive/negative target coefficients. Betweenness requires n\>=1, distinct in-range triple elements, duplicates allowed. FeasibleRegisterAssignment permits n=0, duplicate arcs and cycles but no self arcs; registers are fixed, never chosen. Source numeric work uses indices, not signed objective arithmetic.
_Construction._ 1. For each i\<j use bit x_ij meaning i precedes j. Write b(i,j)=x_ij if i\<j and 1-x_ji otherwise. Layout is lexicographic unordered pairs. For each i\<j\<k add C=x_ik+x_ij\*x_jk-x_ij\*x_ik-x_ik\*x_jk. The resulting T is the number of directed triangles.
2. Betweenness: add (b(a,b)-b(b,c))^2 for each ordered triple (a,b,c). Expansion uses Boolean idempotence; no auxiliary variables. Call total P.
3. Register feasibility: for arc (v,u) meaning v depends on u, add 1-b(u,v). For every ordered pair (w,v) of distinct vertices sharing a register and every arc (d,w) with d!=v, add b(w,v)\*b(v,d). Add these to T to obtain P. Duplicate arcs contribute duplicate penalties.
4. Drop the constant c from P, obtaining E; decision bound is -c.
_Correctness, forward._ A source position permutation orients all comparisons and has no triangle. A satisfied betweenness triple has b(a,b)=b(b,c) (both one or both zero), so its square vanishes. A feasible register schedule respects each dependency and does not overwrite w before another consumer d executes; hence no w\<v\<d conflict term is one. The target has E=-c.
_Correctness, backward._ Each triangle term is zero or one by the eight-case Boolean truth table. All added terms are nonnegative squares or products of Boolean literals. E\<=-c therefore means every term vanishes. A tournament without directed triangles is transitive: a shortest directed cycle of length greater than three has a chord producing a shorter directed cycle. Ranks are distinct and range from zero to n-1. Under these ranks, equality of the two comparisons in a betweenness triple is exactly either a\<b\<c or c\<b\<a. For registers, dependencies hold. If an earlier same-register w were live at overwrite v, some uncomputed consumer d!=v would follow v, producing a positive b(w,v)\*b(v,d), contradiction. This includes cycles, shared consumers, duplicate arcs, and consumption during the overwrite itself.
_Extraction and aggregate recovery._ Evaluate the target once and reject if false or malformed. Return the number of predecessors of each vertex. Completed Or is identical, including false for unsatisfiable sources. No auxiliary decoding occurs.
_Overhead._ Both targets have exactly N=n(n-1)/2 variables and at most N^2 off-diagonal terms. Construction enumerates O(n^3+q) blocks for q betweenness triples, and O(n^3+n\*m) for m register arcs. Index/allocation arithmetic is checked. Coefficients are O(n+q) or O(n+m); accumulation and all evaluation prefixes must fit i64. Time includes integer arithmetic in those coefficient bits. Extraction takes O(n^2+n log n). No numeric horizon.
_Examples._ Betweenness YES: n=3, [(0,1,2)], ranks [0,1,2], x=[1,1,1]. T=0 and square=(1-1)^2=0. Thus E=x02+x01+x12-x01\*x12-x01\*x02-x02\*x12, c=0, energy=0. NO: add (0,2,1); no element can simultaneously be the middle in both triples. All eight target assignments have positive total penalty.
Register YES: n=3, arcs [(1,0),(2,1)], fixed registers [0,0,0], ranks [0,1,2]. Consuming 0 while overwriting it at 1 is allowed; then consuming 1 at 2 is allowed; every penalty is zero. NO: arcs [(1,0),(2,0)] with registers [0,0,0]. Whichever of 1 and 2 overwrites 0 first leaves the other uncomputed; the corresponding conflict contributes one. All eight assignments violate a dependency, transitivity or overwrite rule. Empty n=0 maps to an empty zero-energy target and empty positions.
Complexity clarification: the stated extraction costs describe decoding after validation; include O(N+E_count) for evaluating the target once. Alphabet symbols and all indices are intrinsically unsigned usize.
Independent adversary"""Independent proof-only audit. Run with the phase2 venv Python.
build(kind,data) -> (N, {(i,j): coefficient}, constant), i <= j.
kind='betweenness': {'n': n, 'triples': [[a,b,c], ...]}.
kind='register': {'n': n, 'arcs': [[dependent,dependency], ...],
'registers': [fixed register identifier per vertex]}.
Entries are upper-triangular monomial coefficients (no factor of two).
"""
from collections import Counter
from functools import lru_cache
from itertools import combinations, permutations, product
from pathlib import Path
import json
import random
import sympy as sp
from hypothesis import given, settings, strategies as st
ROOT = Path(__file__).parent
COUNTS = Counter()
FAMILIES = Counter()
SHARED = []
SEED = 6201022
def add(p, q, scale=1):
for mon, coefficient in q.items():
p[mon] = p.get(mon, 0) + scale * coefficient
def mul(p, q):
result = {}
for left, a in p.items():
for right, b in q.items():
mon = tuple(sorted(set(left + right)))
result[mon] = result.get(mon, 0) + a * b
return result
def build(kind, data):
n = data['n']
pairs = list(combinations(range(n), 2))
indices = {pair: k for k, pair in enumerate(pairs)}
def b(i, j):
assert i != j
k = indices[tuple(sorted((i, j)))]
return {(k,): 1} if i < j else {(): 1, (k,): -1}
penalty = {}
for i, j, k in combinations(range(n), 3):
add(penalty, b(i, k))
add(penalty, mul(b(i, j), b(j, k)))
add(penalty, mul(b(i, j), b(i, k)), -1)
add(penalty, mul(b(i, k), b(j, k)), -1)
if kind == 'betweenness':
for a, middle, c in data['triples']:
difference = dict(b(a, middle))
add(difference, b(middle, c), -1)
add(penalty, mul(difference, difference))
elif kind == 'register':
for v, u in data['arcs']:
add(penalty, {(): 1})
add(penalty, b(u, v), -1)
for w, v in permutations(range(n), 2):
if data['registers'][w] == data['registers'][v]:
for d, dependency in data['arcs']:
if dependency == w and d != v:
add(penalty, mul(b(w, v), b(v, d)))
else:
raise ValueError(kind)
entries = {(mon[0], mon[-1]): value for mon, value in penalty.items()
if mon and value}
return len(pairs), entries, penalty.get((), 0)
def source(kind, data, ranks):
n = data['n']
if sorted(ranks) != list(range(n)):
return False
if kind == 'betweenness':
return all(min(ranks[a], ranks[c]) < ranks[b] < max(ranks[a], ranks[c])
for a, b, c in data['triples'])
contents = {}
for v in sorted(range(n), key=lambda vertex: ranks[vertex]):
for dependent, dependency in data['arcs']:
if dependent == v and contents.get(data['registers'][dependency]) != dependency:
return False
contents[data['registers'][v]] = v
return True
def energy(target, bits):
N, entries, _ = target
if len(bits) != N or any(type(x) is not int or x not in (0, 1) for x in bits):
raise ValueError('malformed Boolean witness')
return sum(c * bits[i] * bits[j] for (i, j), c in entries.items())
def extract(data, target, bits):
if energy(target, bits) > -target[2]:
raise ValueError('target is false')
ranks = [0] * data['n']
for x, (i, j) in zip(bits, combinations(range(data['n']), 2)):
ranks[j if x else i] += 1
return ranks
@lru_cache(None)
def geometry(n):
pairs = tuple(combinations(range(n), 2))
configs = tuple(product((0, 1), repeat=len(pairs)))
rank_masks = []
for ranks in permutations(range(n)):
mask = sum((ranks[i] < ranks[j]) << (len(pairs) - k - 1)
for k, (i, j) in enumerate(pairs))
rank_masks.append((ranks, mask))
active = {(i, j): tuple(k for k, bits in enumerate(configs) if bits[i] and bits[j])
for i in range(len(pairs)) for j in range(i, len(pairs))}
return configs, rank_masks, active
def direct_penalty(kind, data, bits):
comparisons = dict(zip(combinations(range(data['n']), 2), bits))
def before(i, j):
return comparisons[(i, j)] if i < j else 1 - comparisons[(j, i)]
total = 0
# Count directed cycles directly instead of repeating the polynomial.
for i, j, k in combinations(range(data['n']), 3):
total += int(before(i, j) == before(j, k) == before(k, i))
if kind == 'betweenness':
total += sum(before(a, b) != before(b, c) for a, b, c in data['triples'])
else:
total += sum(not before(u, v) for v, u in data['arcs'])
total += sum(before(w, v) and before(v, d)
for w, v in permutations(range(data['n']), 2)
if data['registers'][w] == data['registers'][v]
for d, u in data['arcs'] if u == w and d != v)
return total
def check(kind, data, family, save=False):
target = build(kind, data)
N, entries, constant = target
configs, rank_masks, active = geometry(data['n'])
expected = {mask for ranks, mask in rank_masks if source(kind, data, ranks)}
totals = [constant] * len(configs)
for pair, coefficient in entries.items():
for mask in active[pair]:
totals[mask] += coefficient
found = {mask for mask, total in enumerate(totals) if total <= 0}
assert found == expected, (kind, data, found ^ expected)
assert min(totals) >= 0
COUNTS['forward_backward_target_witnesses'] += len(configs)
COUNTS['source_permutations'] += len(rank_masks)
COUNTS['completed_or'] += 1
for mask in found:
ranks = extract(data, target, configs[mask])
assert source(kind, data, ranks), (kind, data, configs[mask], ranks)
COUNTS['extraction_feasible'] += 1
for invalid in ([0] * (N + 1), [2] * max(N, 1)):
try:
extract(data, target, invalid)
except ValueError:
COUNTS['extraction_malformed'] += 1
else:
raise AssertionError('malformed target accepted')
rejected = next((k for k, total in enumerate(totals) if total > 0), None)
if rejected is not None:
try:
extract(data, target, configs[rejected])
except ValueError:
COUNTS['extraction_false'] += 1
else:
raise AssertionError('false target accepted')
assert N == data['n'] * (data['n'] - 1) // 2
assert sum(i != j for i, j in entries) <= N * (N - 1) // 2 <= N * N
assert all(0 <= i <= j < N and type(c) is int and c for (i, j), c in entries.items())
n = data['n']
triangle_absolute = 4*n*(n-1)*(n-2)//6
if kind == 'betweenness':
count = len(data['triples'])
absolute_bound = triangle_absolute + 6*count
else:
count = len(data['arcs'])
absolute_bound = triangle_absolute + 2*count + 4*count*max(n-2, 0)
assert abs(constant) + sum(abs(c) for c in entries.values()) <= absolute_bound
assert all(abs(c) <= max(n-2, 0) + 2*count for c in entries.values())
COUNTS['size'] += 2
COUNTS['coefficient_bounds'] += 2
COUNTS['structure'] += 1
# Independently check all configurations on tiny instances; boundary and
# alternating configurations on larger instances supplement exact YES sets.
probes = range(len(configs)) if N <= 3 else {0, len(configs)-1, len(configs)//3, 2*len(configs)//3}
for mask in probes:
assert totals[mask] == direct_penalty(kind, data, configs[mask])
COUNTS['exact_polynomial'] += 1
FAMILIES[family] += 1
if save:
SHARED.append({'kind': kind, 'data': data, 'N': N,
'entries': [[i, j, c] for (i, j), c in sorted(entries.items())],
'constant': constant, 'bound': -constant,
'feasible': bool(found), 'minimum_penalty': min(totals),
'accepted_witnesses': len(found)})
def partitions(n):
if n == 0:
yield []
return
def extend(prefix):
if len(prefix) == n:
yield prefix
else:
for color in range(max(prefix) + 2):
yield from extend(prefix + [color])
yield from extend([0])
def symbolic():
n, q, m, N = sp.symbols('n q m N', integer=True, nonnegative=True)
assert sp.simplify(n*(n-1)/2 - sp.binomial(n, 2).expand(func=True)) == 0
assert sp.simplify(N**2 - N*(N-1)/2 - N*(N+1)/2) == 0
assert sp.simplify(4*sp.binomial(n, 3).expand(func=True) - 2*n*(n-1)*(n-2)/3) == 0
# Sum of absolute coefficients before cancellation: triangle <=4,
# square of two literals <=6; dependency <=2; conflict <=4.
absolute_between = 4*sp.binomial(n, 3) + 6*q
absolute_register = 4*sp.binomial(n, 3) + 2*m + 4*m*sp.Max(n-2, 0)
assert absolute_between.subs({n: 3, q: 1}) == 10
assert absolute_register.subs({n: 3, m: 2}) == 16
COUNTS['symbolic'] += 5
# Independent truth-table verification of triangle indicator.
for a, b, c in product((0, 1), repeat=3):
assert b + a*c - a*b - b*c == int(a == c == 1-b)
COUNTS['symbolic'] += 1
def examples():
yes_b = {'n': 3, 'triples': [[0, 1, 2]]}
no_b = {'n': 3, 'triples': [[0, 1, 2], [0, 2, 1]]}
yes_r = {'n': 3, 'arcs': [[1, 0], [2, 1]], 'registers': [0, 0, 0]}
no_r = {'n': 3, 'arcs': [[1, 0], [2, 0]], 'registers': [0, 0, 0]}
for kind, data, feasible in [('betweenness', yes_b, True), ('betweenness', no_b, False),
('register', yes_r, True), ('register', no_r, False)]:
check(kind, data, 'worked_examples', save=True)
target = build(kind, data)
assert min(energy(target, bits) + target[2] for bits in geometry(3)[0]) == (0 if feasible else 1)
if feasible:
assert source(kind, data, [0, 1, 2])
assert energy(target, [1, 1, 1]) == -target[2]
COUNTS['yes_examples' if feasible else 'no_examples'] += 1
assert build('betweenness', yes_b) == (3, {(0,0):1, (1,1):1, (2,2):1,
(0,1):-1, (0,2):-1, (1,2):-1}, 0)
COUNTS['yes_examples'] += 1
def exhaustive():
for n in range(1, 5):
canonical = [(a, middle, c) for triple in combinations(range(n), 3)
for middle in triple for a, c in [tuple(x for x in triple if x != middle)]]
for flags in product((0, 1), repeat=len(canonical)):
data = {'n': n, 'triples': [list(t) for t, f in zip(canonical, flags) if f]}
check('betweenness', data, f'betweenness_exhaustive_n{n}')
for n in range(5):
arcs = list(permutations(range(n), 2))
for registers in partitions(n):
for flags in product((0, 1), repeat=len(arcs)):
data = {'n': n, 'arcs': [list(a) for a, f in zip(arcs, flags) if f], 'registers': registers}
check('register', data, f'register_exhaustive_n{n}')
n = 5
canonical = [(a, middle, c) for triple in combinations(range(n), 3)
for middle in triple for a, c in [tuple(x for x in triple if x != middle)]]
for count in range(3):
for triples in combinations(canonical, count):
check('betweenness', {'n': n, 'triples': triples}, f'betweenness_exhaustive_n5_q{count}')
arcs = list(permutations(range(n), 2))
for registers in partitions(n):
for count in range(2):
for selected in combinations(arcs, count):
check('register', {'n': n, 'arcs': selected, 'registers': registers},
f'register_exhaustive_n5_m{count}')
def samples():
rng = random.Random(SEED)
for n in range(1, 6):
triples = list(permutations(range(n), 3))
for q in sorted({0, 1, 2, n, 2*n, 6*n, 12*n} if triples else {0}):
for sample in range(300):
data = {'n': n, 'triples': [list(rng.choice(triples)) for _ in range(q)]}
check('betweenness', data, f'betweenness_sample_n{n}_q{q}', save=sample == 0)
for n in range(6):
arcs = list(permutations(range(n), 2))
for m in sorted({0, 1, n-1, n, 2*n, n*(n-1), 2*n*(n-1)} if arcs else {0}):
for sample in range(300):
if sample % 3 == 0:
registers = [0] * n
elif sample % 3 == 1:
registers = list(range(n))
else:
registers = [rng.randrange(n) for _ in range(n)]
data = {'n': n, 'arcs': [list(rng.choice(arcs)) for _ in range(m)], 'registers': registers}
check('register', data, f'register_sample_n{n}_m{m}', save=sample < 3)
@st.composite
def between_instances(draw):
n = draw(st.integers(1, 5))
triples = list(permutations(range(n), 3))
values = draw(st.lists(st.sampled_from(triples), max_size=35)) if triples else []
return {'n': n, 'triples': values}
@st.composite
def register_instances(draw):
n = draw(st.integers(0, 5))
arcs = list(permutations(range(n), 2))
values = draw(st.lists(st.sampled_from(arcs), max_size=30)) if arcs else []
registers = draw(st.lists(st.integers(0, max(n, 1)), min_size=n, max_size=n))
return {'n': n, 'arcs': values, 'registers': registers}
@settings(max_examples=300, deadline=None, derandomize=True, database=None)
@given(between_instances())
def hypothesis_between(data):
check('betweenness', data, 'hypothesis_betweenness')
@settings(max_examples=300, deadline=None, derandomize=True, database=None)
@given(register_instances())
def hypothesis_register(data):
check('register', data, 'hypothesis_register')
if __name__ == '__main__':
symbolic()
examples()
print('symbolic and worked examples PASS', flush=True)
exhaustive()
print('exhaustive families PASS', dict(COUNTS), flush=True)
samples()
print('stratified samples PASS', dict(COUNTS), flush=True)
hypothesis_between()
hypothesis_register()
report = {'status': 'PASS', 'seed': SEED, 'hypothesis': {'max_examples_per_strategy': 300,
'derandomize': True, 'deadline': None, 'database': None},
'checks': dict(COUNTS), 'families': dict(FAMILIES), 'shared_cases': len(SHARED)}
(ROOT / 'summary.json').write_text(json.dumps(report, indent=2) + '\n')
(ROOT / 'shared_cases.json').write_text(json.dumps(SHARED, indent=2) + '\n')
print(json.dumps(report, indent=2), flush=True) |
Collaborator
Author
Verification certificate — Phase 3 supersequence independent adversaryVERIFIED, together with the constructor/cross-comparison certificate. Proof-only independent implementation; no production imports. Proof formatting was escaped for Typst compilation afterward; mathematical polynomials did not change. Machine-range guard clarifications were added after the fresh reviewer reproduced two boundary failures, each covered by a red-then-green Rust regression. All three proof PDFs compile. Finite coverage and untested machine/resource limits are stated in the report. The constructor script is in the companion certificate; this comment contains the independent script and full proof. Independent reportExact counts / settings{
"status": "PASS",
"counts": {
"symbolic_identities": 11,
"exhaustive_target_assignments": 96588,
"exhaustive_instances": 60,
"sampled_arbitrary_targets": 2450,
"sampled_instances_L_3": 350,
"sampled_optimal_lifts": 1421,
"sampled_mutated_lifts": 2842,
"sampled_concatenation_lifts": 1421,
"sampled_instances_L_4": 350,
"sampled_instances_L_5": 350,
"sampled_instances_L_6": 350,
"sampled_instances_L_7": 350,
"sampled_instances_L_8": 350,
"sampled_instances_L_9": 350,
"hypothesis_arbitrary_targets": 1300,
"hypothesis_contained_lifts": 1300,
"explicit_examples": 3,
"example_target_enumerations": 524305,
"rejected_empty_lists": 3
},
"examples": [
{
"data": {
"alphabet_size": 2,
"strings": [
[
0
],
[
1
],
[
0
]
]
},
"N": 18,
"constant": 27,
"source_optimum": 2,
"target_minimum": -25,
"witness": [
0,
1,
null
]
},
{
"data": {
"alphabet_size": 2,
"strings": [
[
0
],
[
1
],
[
2
]
]
},
"N": 18,
"constant": 27,
"source_optimum": null,
"target_minimum": -21,
"witness": null
},
{
"data": {
"alphabet_size": 2,
"strings": [
[],
[
0
],
[
0,
1
],
[
0,
1
]
]
},
"N": 40,
"constant": 65,
"source_optimum": 2,
"target_minimum": null,
"witness": [
0,
1,
null,
null,
null
]
},
{
"data": {
"alphabet_size": 0,
"strings": [
[],
[]
]
},
"N": 0,
"constant": 0,
"source_optimum": 0,
"target_minimum": 0,
"witness": []
},
{
"data": {
"alphabet_size": 2,
"strings": [
[
-1
]
]
},
"N": 4,
"constant": 5,
"source_optimum": null,
"target_minimum": -3,
"witness": null
}
],
"limitations": [
"Finite enumeration covers only listed small domains; larger instances are sampled.",
"No repository, production constructor, Rust, machine overflow, or allocation behavior inspected.",
"Negative-symbol case is an extra mathematical check outside the confirmed usize production domain.",
"Revised proof correctly charges O(N+nnz) for energy validation and decoding."
]
}
Typst proof= Direct shortest common supersequence
Theorem. A nonempty list of strings over declared alphabet 0,...,a-1 (constructor also accepts invalid symbols) with total length L has source value Min\<i64\> and a witness of L optional symbols, a nonpadding prefix followed by None. The construction targets QUBO\<i64\>, with Boolean witness, preserving optimum, infeasibility, and completed value.
_Construction._ 1. Use x[p,s] for p=0,...,L-1 and s=0,...,a, where s=a is padding, row-major. Use y[g,p] for each input character indexed globally in input-string order g=0,...,L-1 and each output position p; y bits follow all x bits. No containment or duplicate preprocessing. N=L(a+1)+L^2.
2. Objective F=sum_p(1-x[p,a]); on arbitrary bitstrings 0\<=F\<=L. P=L+1. Each output symbol row and each character embedding row gets P(sum bits-1)^2. For a valid character s\<a add P\*y[g,p]\*(1-x[p,s]) for every p. For any invalid character add P\*y[g,p] instead, making its row impossible without ever indexing outside x.
3. For consecutive characters g,g+1 in each individual input string, add P\*y[g,p]\*y[g+1,q] for all p\>=q. For each adjacent output pair add P\*x[p,a]\*(1-x[p+1,a]). These enforce strictly increasing embeddings and contiguous padding. Let Q=F+PV. Drop its constant c and call resulting energy E. Accept energies -c\<=E\<=L-c for witness extraction, map completed optimum to E+c in this interval, otherwise Min(None).
_Correctness forward._ Every accepted source sequence admits increasing embeddings of each input string. Choose its output symbols and one such embedding per character. Every penalty vanishes, so Q is exactly sequence length. Empty strings need no embedding, duplicates use independent rows, and contained strings use ordinary embeddings. Concatenation witnesses feasibility for valid symbols and has length L.
_Correctness backward._ Every penalty is a nonnegative integer (a square or product of literals). F is nonnegative even if the x rows are malformed. Thus V\>0 implies Q\>=P\>L. A target in the accepted interval has exactly one symbol per output and one position per source character; consistency and increasing embeddings prove every input is a subsequence. Padding implication gives a contiguous suffix. F is its prefix length. An invalid alphabet symbol forces its embedding row nonempty and simultaneously penalizes every selected bit, so no accepted target exists, matching source infeasibility.
_Extraction and aggregate recovery._ Validate once against the energy interval. Decode output symbol rows; symbol a becomes None. Return exactly L entries. Decode no embedding choices beyond target validation. Completed Min maps through constant and interval; all optima represent valid minimum-length strings whenever source feasible. All-empty inputs have L=0, no bits, c=0 and optimum 0 even if a=0. Empty input lists are constructor-rejected, outside domain.
_Overhead and arithmetic._ Exact N=L(a+1)+L^2. Upper E_count\<=N^2; quadratic construction work O(L(a+1)^2+L^3), sparse accumulation logarithms; O(N) extraction. Alphabet magnitude a is explicit, and allocation is pseudopolynomial in binary a. Coefficients are O(L^2) with no signed source objectives. Check a+1, all dimensions, total N, L to i64, P, constants and target coefficient positive/negative sums. Source length conversion bounded by checked L. Integer arithmetic bit costs remain logarithmic in coefficients. No claim of universal savings over alternative encodings.
_Examples._ Three nonempty source strings [0], [1], [0], alphabet a=2, total L=3: output [0,1,None] has length two, embedding positions [0,1,0], all penalties zero, and optimum two since both symbols are required. There are N=3\*3+9=18 bits. NO: alphabet a=2, three strings [0], [1], [2]. The third symbol is constructor-accepted but cannot occur in any source witness; its embedding row must choose a bit yet every such bit is penalized. No target within the valid energy interval exists. Empty/duplicate/contained example [[],[0],[0,1],[0,1]] can use [0,1,None,None,None], length two.
Complexity clarification: the stated extraction costs describe decoding after validation; include O(N+E_count) for evaluating the target once. Alphabet symbols and all indices are intrinsically unsigned usize.
Machine representation clarification: when L is nonzero, the allocated row length max(a+1,L) times sizeof(usize) must fit isize before allocating either symbol or embedding rows. Count arithmetic alone does not establish an allocatable layout. Fail with typed IntegerOverflow otherwise.
Independent adversary"""Independent implementation from proof-supersequence.typ only; upper-triangle QUBO."""
from collections import defaultdict, deque
from itertools import product
import json
import random
from pathlib import Path
from hypothesis import given, settings, strategies as st
import sympy as sp
HERE = Path(__file__).parent
COUNTS = defaultdict(int)
def build(kind, data):
if kind not in ('supersequence', 'shortest_common_supersequence'):
raise ValueError(kind)
a, strings = data['alphabet_size'], data['strings']
if a < 0 or not strings:
raise ValueError('nonnegative alphabet and nonempty input list required')
L = sum(map(len, strings))
P = L + 1
N = L * (a + 1) + L * L
q = defaultdict(int)
c = L
def add(i, j, v):
q[min(i, j), max(i, j)] += v
def onehot(row):
nonlocal c
c += P
for ii, i in enumerate(row):
add(i, i, -P)
for j in row[ii + 1:]:
add(i, j, 2 * P)
def x(p, s):
return p * (a + 1) + s
def y(g, p):
return L * (a + 1) + g * L + p
for p in range(L):
add(x(p, a), x(p, a), -1)
onehot([x(p, s) for s in range(a + 1)])
g = 0
for string in strings:
for h, s in enumerate(string):
onehot([y(g, p) for p in range(L)])
for p in range(L):
add(y(g, p), y(g, p), P)
if 0 <= s < a:
add(y(g, p), x(p, s), -P)
if h:
for p in range(L):
for r in range(p + 1):
add(y(g - 1, p), y(g, r), P)
g += 1
for p in range(L - 1):
add(x(p, a), x(p, a), P)
add(x(p, a), x(p + 1, a), -P)
return N, {k: v for k, v in sorted(q.items()) if v}, c
def source_value(data, witness):
a = data['alphabet_size']
L = sum(map(len, data['strings']))
if len(witness) != L:
return None
prefix = []
padded = False
for symbol in witness:
if symbol is None:
padded = True
elif padded or not 0 <= symbol < a:
return None
else:
prefix.append(symbol)
for string in data['strings']:
progress = 0
for symbol in prefix:
if progress < len(string) and symbol == string[progress]:
progress += 1
if progress != len(string):
return None
return len(prefix)
def source_optimum(data):
"""BFS on string progress, independent of positions and QUBO embeddings."""
strings, a = data['strings'], data['alphabet_size']
if any(not 0 <= s < a for string in strings for s in string):
return None, None
start = tuple(0 for _ in strings)
goal = tuple(map(len, strings))
queue = deque([(start, [])])
seen = {start}
while queue:
state, word = queue.popleft()
if state == goal:
L = sum(map(len, strings))
return len(word), word + [None] * (L - len(word))
for s in range(a):
new = tuple(p + int(p < len(t) and t[p] == s) for p, t in zip(state, strings))
if new not in seen:
seen.add(new)
queue.append((new, word + [s]))
raise AssertionError('valid strings must have concatenation witness')
def evaluate(q, bits):
return sum(v * bits[i] * bits[j] for (i, j), v in q.items())
def direct_terms(data, bits):
"""Literal proof expression, independent of coefficient accumulator."""
a = data['alphabet_size']
L = sum(map(len, data['strings']))
width = a + 1
xs = [bits[p * width:(p + 1) * width] for p in range(L)]
ys = [bits[L * width + g * L:L * width + (g + 1) * L] for g in range(L)]
F = sum(1 - row[a] for row in xs)
V = sum((sum(row) - 1) ** 2 for row in xs + ys)
g = 0
for string in data['strings']:
for h, symbol in enumerate(string):
V += sum(ys[g][p] * (1 - xs[p][symbol] if 0 <= symbol < a else 1) for p in range(L))
if h:
V += sum(ys[g - 1][p] * ys[g][r] for p in range(L) for r in range(L) if p >= r)
g += 1
V += sum(xs[p][a] * (1 - xs[p + 1][a]) for p in range(L - 1))
return F, V
def extract(data, bits, energy, constant):
L, a = sum(map(len, data['strings'])), data['alphabet_size']
if not -constant <= energy <= L - constant:
return None
out = []
for p in range(L):
row = bits[p * (a + 1):(p + 1) * (a + 1)]
assert sum(row) == 1
s = row.index(1)
out.append(None if s == a else s)
return out
def lift(data, witness):
assert source_value(data, witness) is not None
a, L = data['alphabet_size'], len(witness)
bits = [0] * (L * (a + 1) + L * L)
for p, s in enumerate(witness):
bits[p * (a + 1) + (a if s is None else s)] = 1
g = 0
for string in data['strings']:
p = 0
for s in string:
while witness[p] != s:
p += 1
bits[L * (a + 1) + g * L + p] = 1
p += 1
g += 1
return bits
def check_bits(data, built, bits, category):
N, q, c = built
assert len(bits) == N
L = sum(map(len, data['strings']))
F, V = direct_terms(data, bits)
E = evaluate(q, bits)
assert E + c == F + (L + 1) * V
assert 0 <= F <= L and V >= 0
out = extract(data, bits, E, c)
assert (out is not None) == (V == 0)
if out is not None:
assert source_value(data, out) == E + c
else:
assert E + c >= L + 1
COUNTS[category] += 1
return E
def exhaustive():
cases = []
for a in range(3):
for L in range(3):
for chars in product(range(a + 1), repeat=L):
# Each split includes empty strings; one-string case also checks ordering.
for split in range(L + 1):
cases.append({'alphabet_size': a, 'strings': [list(chars[:split]), list(chars[split:])]})
cases.extend([
{'alphabet_size': 1, 'strings': [[0, 0, 0]]},
{'alphabet_size': 1, 'strings': [[0], [0], [0]]},
{'alphabet_size': 0, 'strings': [[], [], []]},
])
shared = []
for data in cases:
built = build('supersequence', data)
N, q, c = built
minimum = min(check_bits(data, built, list(bits), 'exhaustive_target_assignments') for bits in product((0, 1), repeat=N))
L, a = sum(map(len, data['strings'])), data['alphabet_size']
expected, witness = source_optimum(data)
mapped = minimum + c if 0 <= minimum + c <= L else None
assert expected == mapped
candidates = [source_value(data, word) for word in product([*range(a), None], repeat=L)]
valid = [v for v in candidates if v is not None]
assert expected == (min(valid) if valid else None)
COUNTS['exhaustive_instances'] += 1
shared.append({'kind': 'supersequence', 'data': data, 'N': N,
'entries': [[i, j, v] for (i, j), v in q.items()],
'constant': c, 'source_optimum': expected, 'target_minimum': minimum})
return shared
def symbolic():
# Multilinear one-hot square identity, checked symbolically before numeric checks.
for width in range(1, 9):
xs = sp.symbols(f'x:{width}')
poly = sp.Poly(sp.expand((sum(xs) - 1) ** 2), *xs)
boolean = sum(coeff * sp.prod(x ** min(e, 1) for x, e in zip(xs, powers)) for powers, coeff in poly.terms())
explicit = 1 - sum(xs) + 2 * sum(xs[i] * xs[j] for i in range(width) for j in range(i + 1, width))
assert sp.expand(boolean - explicit) == 0
L = sp.symbols('L', integer=True, nonnegative=True)
assert sp.expand((L + 1) - L) == 1
assert sp.expand(L + 2 * L * (L + 1) - (2 * L ** 2 + 3 * L)) == 0
t = sp.symbols('t', integer=True, nonnegative=True)
assert sp.expand((t - 1) ** 2 + t - (t * (t - 1) + 1)) == 0
# t(t-1)>=0 on nonnegative integers, including t=0,1; hence invalid row costs >=1.
COUNTS['symbolic_identities'] += 11
def sampled():
rng = random.Random(510831)
shared = []
for L in range(3, 10):
for trial in range(350):
a = rng.randrange(4)
chars = [rng.randrange(a + int(trial % 4 == 0)) if a else 0 for _ in range(L)]
cuts = sorted([0, L] + [rng.randrange(L + 1) for _ in range(rng.randrange(4))])
data = {'alphabet_size': a, 'strings': [chars[i:j] for i, j in zip(cuts, cuts[1:])]}
built = build('supersequence', data)
N, q, c = built
assert c == 2 * L * L + 3 * L
assert max(map(abs, q.values()), default=0) <= 2 * (L + 1)
assert len(q) <= N * (N + 1) // 2
check_bits(data, built, [rng.randrange(2) for _ in range(N)], 'sampled_arbitrary_targets')
optimum, witness = source_optimum(data)
if witness is not None:
bits = lift(data, witness)
assert check_bits(data, built, bits, 'sampled_optimal_lifts') + c == optimum
for _ in range(2):
changed = bits.copy()
i = rng.randrange(N)
changed[i] ^= 1
check_bits(data, built, changed, 'sampled_mutated_lifts')
concatenation = [s for string in data['strings'] for s in string]
assert check_bits(data, built, lift(data, concatenation), 'sampled_concatenation_lifts') + c == L
COUNTS[f'sampled_instances_L_{L}'] += 1
if trial < 5:
shared.append({'kind': 'supersequence', 'data': data, 'N': N,
'entries': [[i, j, v] for (i, j), v in q.items()], 'constant': c,
'source_optimum': optimum})
return shared
@st.composite
def arbitrary_instances(draw):
a = draw(st.integers(0, 3))
strings = draw(st.lists(st.lists(st.integers(0, a + 1), max_size=3), min_size=1, max_size=3).filter(lambda ss: sum(map(len, ss)) <= 6))
data = {'alphabet_size': a, 'strings': strings}
N = sum(map(len, strings)) * (a + 1 + sum(map(len, strings)))
return data, draw(st.lists(st.integers(0, 1), min_size=N, max_size=N))
@given(arbitrary_instances())
@settings(max_examples=1300, deadline=None, derandomize=True, database=None)
def arbitrary_property(case):
data, bits = case
check_bits(data, build('supersequence', data), bits, 'hypothesis_arbitrary_targets')
@st.composite
def subsequences_of_word(draw):
a = draw(st.integers(1, 3))
word = draw(st.lists(st.integers(0, a - 1), min_size=1, max_size=5))
masks = draw(st.lists(st.lists(st.booleans(), min_size=len(word), max_size=len(word)), min_size=1, max_size=4))
strings = [[s for s, keep in zip(word, mask) if keep] for mask in masks]
# Include full word to make its independently known optimum exactly len(word).
strings.append(word)
return {'alphabet_size': a, 'strings': strings}, word
@given(subsequences_of_word())
@settings(max_examples=1300, deadline=None, derandomize=True, database=None)
def contained_property(case):
data, word = case
L = sum(map(len, data['strings']))
built = build('supersequence', data)
witness = word + [None] * (L - len(word))
assert check_bits(data, built, lift(data, witness), 'hypothesis_contained_lifts') + built[2] == len(word)
assert source_optimum(data)[0] == len(word)
def examples():
items = [
({'alphabet_size': 2, 'strings': [[0], [1], [0]]}, 2),
({'alphabet_size': 2, 'strings': [[0], [1], [2]]}, None),
({'alphabet_size': 2, 'strings': [[], [0], [0, 1], [0, 1]]}, 2),
({'alphabet_size': 0, 'strings': [[], []]}, 0),
({'alphabet_size': 2, 'strings': [[-1]]}, None),
]
results = []
for data, expected in items:
built = build('supersequence', data)
optimum, witness = source_optimum(data)
assert optimum == expected
if witness is not None:
assert check_bits(data, built, lift(data, witness), 'explicit_examples') + built[2] == expected
# Exhaust both 18-bit YES/NO targets, independently confirming supplied examples.
minimum = None
if built[0] <= 18:
minimum = min(evaluate(built[1], bits) for bits in product((0, 1), repeat=built[0]))
mapped = minimum + built[2] if 0 <= minimum + built[2] <= sum(map(len, data['strings'])) else None
assert mapped == expected
COUNTS['example_target_enumerations'] += 2 ** built[0]
results.append({'data': data, 'N': built[0], 'constant': built[2], 'source_optimum': optimum, 'target_minimum': minimum, 'witness': witness})
for a in (0, 1, 2):
try:
build('supersequence', {'alphabet_size': a, 'strings': []})
except ValueError:
COUNTS['rejected_empty_lists'] += 1
else:
raise AssertionError('empty list accepted')
return results
if __name__ == '__main__':
symbolic()
shared = exhaustive()
shared += sampled()
arbitrary_property()
contained_property()
example_results = examples()
(HERE / 'shared-cases.json').write_text(json.dumps(shared, indent=2) + '\n')
report = {'status': 'PASS', 'counts': dict(COUNTS), 'examples': example_results,
'limitations': ['Finite enumeration covers only listed small domains; larger instances are sampled.',
'No repository, production constructor, Rust, machine overflow, or allocation behavior inspected.',
'Negative-symbol case is an extra mathematical check outside the confirmed usize production domain.',
'Revised proof correctly charges O(N+nnz) for energy validation and decoding.']}
(HERE / 'results.json').write_text(json.dumps(report, indent=2) + '\n')
print(json.dumps(report, indent=2)) |
Collaborator
Author
Existing-route measured baselines and composed contractsAll candidate routes were discovered on the Phase 2 head before Rust implementation. Unavailable and failed/timeout routes are not treated as correctness or dominance evidence. measurements/baseline-results.json[
{
"source": "MinimumTardinessSequencing/i64",
"kind": "proposed",
"variables": 11,
"couplings": 31,
"max_coefficient": 14,
"coefficient_bits": 4
},
{
"source": "MinimumTardinessSequencing/i64",
"kind": "existing",
"path": [
{
"from": {
"name": "MinimumTardinessSequencing",
"variant": {
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + max_processing_time_bits + num_tasks",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_precedences + 2 * num_tasks + num_tasks^2",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "(num_precedences + 2 * num_tasks + num_tasks^2) * (num_tasks + num_tasks^2)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_tasks + num_tasks^2",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_tasks + (1 + max_processing_time_bits + num_tasks) * (num_precedences + 2 * num_tasks + num_tasks^2) + (num_precedences + 2 * num_tasks + num_tasks^2) * (num_tasks + num_tasks^2) + num_tasks^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + max_processing_time_bits + num_tasks) * (num_precedences + 2 * num_tasks + num_tasks^2) * (num_tasks + num_tasks^2) + 2 * (1 + max_processing_time_bits + num_tasks) * (num_tasks + num_tasks^2) * (num_precedences + 2 * num_tasks + num_tasks^2)^2 + 2 * (num_precedences + 2 * num_tasks + num_tasks^2) * (num_tasks + num_tasks^2)^2 + (1 + max_processing_time_bits + num_tasks)^2 * (num_precedences + 2 * num_tasks + num_tasks^2)^2 + (num_precedences + 2 * num_tasks + num_tasks^2)^2 * (num_tasks + num_tasks^2)^2 + (num_tasks + num_tasks^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 38.45283389091492,
"variables": 48,
"couplings": 291,
"max_coefficient": 8737,
"coefficient_bits": 14
},
{
"source": "SequencingToMinimizeWeightedTardiness",
"kind": "proposed",
"variables": 7,
"couplings": 7,
"max_coefficient": 22,
"coefficient_bits": 5
},
{
"source": "SequencingToMinimizeWeightedTardiness",
"kind": "existing",
"path": [
{
"from": {
"name": "SequencingToMinimizeWeightedTardiness",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "max_numeric_magnitude_bits + num_tasks",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "1 + 2 * num_tasks^2 + 3 * num_tasks",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "(1 + 2 * num_tasks^2 + 3 * num_tasks) * (2 * num_tasks + num_tasks^2)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "2 * num_tasks + num_tasks^2",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vars + 2 * max_constraint_magnitude_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_constraints",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_nonzeros * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "2 * num_tasks + (1 + 2 * num_tasks + 2 * (max_numeric_magnitude_bits + num_tasks) + num_tasks^2) * (1 + 2 * num_tasks^2 + 3 * num_tasks) + (1 + 2 * num_tasks^2 + 3 * num_tasks) * (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2) + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + 2 * num_tasks + 2 * (max_numeric_magnitude_bits + num_tasks) + num_tasks^2) * (1 + 2 * num_tasks^2 + 3 * num_tasks) * (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2) + 2 * (1 + 2 * num_tasks + 2 * (max_numeric_magnitude_bits + num_tasks) + num_tasks^2) * (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2) * (1 + 2 * num_tasks^2 + 3 * num_tasks)^2 + 2 * (1 + 2 * num_tasks^2 + 3 * num_tasks) * (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2)^2 + (1 + 2 * num_tasks + 2 * (max_numeric_magnitude_bits + num_tasks) + num_tasks^2)^2 * (1 + 2 * num_tasks^2 + 3 * num_tasks)^2 + (1 + 2 * num_tasks^2 + 3 * num_tasks)^2 * (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2)^2 + (2 * num_tasks + (max_numeric_magnitude_bits + num_tasks) * (2 * num_tasks + num_tasks^2) + num_tasks^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 38.34375005681068,
"variables": 53,
"couplings": 204,
"max_coefficient": 240,
"coefficient_bits": 8
},
{
"source": "SequencingWithReleaseTimesAndDeadlines",
"kind": "proposed",
"variables": 7,
"couplings": 11,
"max_coefficient": 2,
"coefficient_bits": 2
},
{
"source": "SequencingWithReleaseTimesAndDeadlines",
"kind": "existing",
"path": [
{
"from": {
"name": "SequencingWithReleaseTimesAndDeadlines",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "time_horizon_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "1 + num_tasks * (-1 + num_tasks)",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "num_tasks * (-1 + num_tasks) * (1 + 2 * time_horizon_bits)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1 + time_horizon_bits * (1 + num_tasks * (-1 + num_tasks)) + (1 + num_tasks * (-1 + num_tasks)) * (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * time_horizon_bits * (1 + num_tasks * (-1 + num_tasks)) * (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1) + 2 * time_horizon_bits * (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1) * (1 + num_tasks * (-1 + num_tasks))^2 + 2 * (1 + num_tasks * (-1 + num_tasks)) * (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1)^2 + time_horizon_bits^2 * (1 + num_tasks * (-1 + num_tasks))^2 + (1 + num_tasks * (-1 + num_tasks))^2 * (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1)^2 + (num_tasks * time_horizon_bits + num_tasks * (-1 + num_tasks) * 2^-1)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.79283300880343,
"variables": 19,
"couplings": 64,
"max_coefficient": 308,
"coefficient_bits": 9
},
{
"source": "DynamicStorageAllocation",
"kind": "proposed",
"variables": 6,
"couplings": 7,
"max_coefficient": 2,
"coefficient_bits": 2
},
{
"source": "FeasibleRegisterAssignment",
"kind": "proposed",
"variables": 3,
"couplings": 3,
"max_coefficient": 3,
"coefficient_bits": 2
},
{
"source": "FeasibleRegisterAssignment",
"kind": "existing",
"path": [
{
"from": {
"name": "FeasibleRegisterAssignment",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vertices",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "2 * num_same_register_pairs + num_arcs * num_vertices",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "3 * num_arcs * num_vertices + 6 * num_same_register_pairs",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_same_register_pairs + num_vertices",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vars + 2 * max_constraint_magnitude_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_constraints",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_nonzeros * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_same_register_pairs + num_vertices + (1 + num_same_register_pairs + num_vertices + 2 * (1 + num_vertices)) * (2 * num_same_register_pairs + num_arcs * num_vertices) + (1 + num_vertices) * (num_same_register_pairs + num_vertices) + (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices)) * (2 * num_same_register_pairs + num_arcs * num_vertices)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + num_same_register_pairs + num_vertices + 2 * (1 + num_vertices)) * (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices)) * (2 * num_same_register_pairs + num_arcs * num_vertices) + 2 * (1 + num_same_register_pairs + num_vertices + 2 * (1 + num_vertices)) * (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices)) * (2 * num_same_register_pairs + num_arcs * num_vertices)^2 + 2 * (2 * num_same_register_pairs + num_arcs * num_vertices) * (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices))^2 + (1 + num_same_register_pairs + num_vertices + 2 * (1 + num_vertices))^2 * (2 * num_same_register_pairs + num_arcs * num_vertices)^2 + (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices))^2 * (2 * num_same_register_pairs + num_arcs * num_vertices)^2 + (num_same_register_pairs + num_vertices + (1 + num_vertices) * (num_same_register_pairs + num_vertices))^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 37.6287919934839,
"variables": 35,
"couplings": 183,
"max_coefficient": 360,
"coefficient_bits": 9
},
{
"source": "ShortestCommonSupersequence",
"kind": "proposed",
"variables": 10,
"couplings": 13,
"max_coefficient": 6,
"coefficient_bits": 3
},
{
"source": "ShortestCommonSupersequence",
"kind": "existing",
"path": [
{
"from": {
"name": "ShortestCommonSupersequence",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + max_length * 2^-1",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "2 * max_length + 2 * total_length + max_length * total_length",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "5 * max_length * total_length + max_length * (3 + alphabet_size)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "max_length * total_length + max_length * (1 + alphabet_size)",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "max_length * total_length + max_length * (1 + alphabet_size) + (1 + max_length * 2^-1) * (2 * max_length + 2 * total_length + max_length * total_length) + (2 * max_length + 2 * total_length + max_length * total_length) * (max_length * total_length + max_length * (1 + alphabet_size))",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + max_length * 2^-1) * (2 * max_length + 2 * total_length + max_length * total_length) * (max_length * total_length + max_length * (1 + alphabet_size)) + 2 * (1 + max_length * 2^-1) * (max_length * total_length + max_length * (1 + alphabet_size)) * (2 * max_length + 2 * total_length + max_length * total_length)^2 + 2 * (2 * max_length + 2 * total_length + max_length * total_length) * (max_length * total_length + max_length * (1 + alphabet_size))^2 + (1 + max_length * 2^-1)^2 * (2 * max_length + 2 * total_length + max_length * total_length)^2 + (2 * max_length + 2 * total_length + max_length * total_length)^2 * (max_length * total_length + max_length * (1 + alphabet_size))^2 + (max_length * total_length + max_length * (1 + alphabet_size))^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.8722080020234,
"variables": 15,
"couplings": 23,
"max_coefficient": 14,
"coefficient_bits": 4
},
{
"source": "Betweenness",
"kind": "proposed",
"variables": 3,
"couplings": 3,
"max_coefficient": 1,
"coefficient_bits": 1
},
{
"source": "Betweenness",
"kind": "existing",
"path": [
{
"from": {
"name": "Betweenness",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "num_elements",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "4 * num_triples",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "12 * num_triples",
"relation": "exact"
},
{
"field": "num_vars",
"formula": "num_elements + num_triples",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vars + 2 * max_constraint_magnitude_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_constraints",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_nonzeros * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_elements + num_triples + 4 * num_triples * (1 + num_triples + 3 * num_elements) + 4 * num_triples * (num_elements + num_triples + num_elements * (num_elements + num_triples)) + num_elements * (num_elements + num_triples)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + num_triples + 3 * num_elements) * (num_elements + num_triples + num_elements * (num_elements + num_triples)) * (4 * num_triples)^2 + 8 * num_triples * (1 + num_triples + 3 * num_elements) * (num_elements + num_triples + num_elements * (num_elements + num_triples)) + 8 * num_triples * (num_elements + num_triples + num_elements * (num_elements + num_triples))^2 + (1 + num_triples + 3 * num_elements)^2 * (4 * num_triples)^2 + (num_elements + num_triples + num_elements * (num_elements + num_triples))^2 * (4 * num_triples)^2 + (num_elements + num_triples + num_elements * (num_elements + num_triples))^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 37.9136250121519,
"variables": 19,
"couplings": 87,
"max_coefficient": 168,
"coefficient_bits": 8
}
]deferred/measurements.json[
{
"source": "SequencingToMinimizeTardyTaskWeight",
"route": [
{
"from": {
"name": "SequencingToMinimizeTardyTaskWeight",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "2 + max_processing_time_bits + num_tasks",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "2 * num_tasks + 2 * num_tasks^2",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "(num_tasks + num_tasks^2) * (2 * num_tasks + 2 * num_tasks^2)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_tasks + num_tasks^2",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_tasks + (2 + max_processing_time_bits + num_tasks) * (2 * num_tasks + 2 * num_tasks^2) + (num_tasks + num_tasks^2) * (2 * num_tasks + 2 * num_tasks^2) + num_tasks^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (2 + max_processing_time_bits + num_tasks) * (num_tasks + num_tasks^2) * (2 * num_tasks + 2 * num_tasks^2) + 2 * (2 + max_processing_time_bits + num_tasks) * (num_tasks + num_tasks^2) * (2 * num_tasks + 2 * num_tasks^2)^2 + 2 * (2 * num_tasks + 2 * num_tasks^2) * (num_tasks + num_tasks^2)^2 + (2 + max_processing_time_bits + num_tasks)^2 * (2 * num_tasks + 2 * num_tasks^2)^2 + (num_tasks + num_tasks^2)^2 * (2 * num_tasks + 2 * num_tasks^2)^2 + (num_tasks + num_tasks^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 45.64625001512468,
"variables": 212,
"couplings": 3297,
"max_coefficient": 417792,
"coefficient_bits": 19
},
{
"source": "MultiprocessorScheduling",
"route": [
{
"from": {
"name": "MultiprocessorScheduling",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "max_numeric_magnitude_bits",
"relation": "exact"
},
{
"field": "num_constraints",
"formula": "num_processors + num_tasks",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_processors * num_tasks * (num_processors + num_tasks)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_processors * num_tasks",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "max_numeric_magnitude_bits * (num_processors + num_tasks) + num_processors * num_tasks + num_processors * num_tasks * (num_processors + num_tasks)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * max_numeric_magnitude_bits * num_processors * num_tasks * (num_processors + num_tasks) + 2 * max_numeric_magnitude_bits * num_processors * num_tasks * (num_processors + num_tasks)^2 + 2 * (num_processors + num_tasks) * (num_processors * num_tasks)^2 + max_numeric_magnitude_bits^2 * (num_processors + num_tasks)^2 + (num_processors + num_tasks)^2 * (num_processors * num_tasks)^2 + (num_processors * num_tasks)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.9144999422133,
"variables": 18,
"couplings": 77,
"max_coefficient": 2496,
"coefficient_bits": 12
},
{
"source": "ResourceConstrainedScheduling",
"route": [
{
"from": {
"name": "ResourceConstrainedScheduling",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "max_resource_bits + num_tasks",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_tasks * (2 + num_resources)",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "(2 + num_resources) * num_tasks^3",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_tasks^2",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_tasks * (2 + num_resources) * (max_resource_bits + num_tasks) + (2 + num_resources) * num_tasks^3 + num_tasks^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * num_tasks * (2 + num_resources) * (num_tasks^2)^2 + 2 * (2 + num_resources) * (max_resource_bits + num_tasks) * num_tasks^3 + 2 * (max_resource_bits + num_tasks) * num_tasks^2 * (num_tasks * (2 + num_resources))^2 + (max_resource_bits + num_tasks)^2 * (num_tasks * (2 + num_resources))^2 + (num_tasks * (2 + num_resources))^2 * (num_tasks^2)^2 + (num_tasks^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.78837500046939,
"variables": 26,
"couplings": 142,
"max_coefficient": 20352,
"coefficient_bits": 15
},
{
"source": "BinPacking/i64",
"route": [
{
"from": {
"name": "BinPacking",
"variant": {
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "max_numeric_magnitude_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "2 * num_items",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "2 * num_items * (num_items + num_items^2)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_items + num_items^2",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_items + 2 * max_numeric_magnitude_bits * num_items + 2 * num_items * (num_items + num_items^2) + num_items^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * max_numeric_magnitude_bits * (num_items + num_items^2) * (2 * num_items)^2 + 4 * max_numeric_magnitude_bits * num_items * (num_items + num_items^2) + 4 * num_items * (num_items + num_items^2)^2 + max_numeric_magnitude_bits^2 * (2 * num_items)^2 + (num_items + num_items^2)^2 * (2 * num_items)^2 + (num_items + num_items^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.81933297775686,
"variables": 21,
"couplings": 72,
"max_coefficient": 392,
"coefficient_bits": 9
},
{
"source": "CapacityAssignment",
"route": [
{
"from": {
"name": "CapacityAssignment",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "max_delay_bits",
"relation": "exact"
},
{
"field": "num_constraints",
"formula": "1 + num_links",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_capacities * num_links * (1 + num_links)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_capacities * num_links",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "max_delay_bits * (1 + num_links) + num_capacities * num_links + num_capacities * num_links * (1 + num_links)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * max_delay_bits * num_capacities * num_links * (1 + num_links) + 2 * max_delay_bits * num_capacities * num_links * (1 + num_links)^2 + 2 * (1 + num_links) * (num_capacities * num_links)^2 + max_delay_bits^2 * (1 + num_links)^2 + (1 + num_links)^2 * (num_capacities * num_links)^2 + (num_capacities * num_links)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 36.64658300112933,
"variables": 13,
"couplings": 78,
"max_coefficient": 6062,
"coefficient_bits": 13
},
{
"source": "LongestCommonSubsequence",
"route": [
{
"from": {
"name": "LongestCommonSubsequence",
"variant": {}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "cross_frequency_product^2",
"relation": "upper_bound"
},
{
"field": "num_vertices",
"formula": "cross_frequency_product",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "num_edges",
"relation": "exact"
},
{
"field": "num_vertices",
"formula": "num_vertices",
"relation": "exact"
}
],
"step": 2,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "-1 * num_edges + num_vertices * (-1 + num_vertices) * 2^-1",
"relation": "exact"
},
{
"field": "num_vertices",
"formula": "num_vertices",
"relation": "exact"
}
],
"step": 3,
"to": {
"name": "MaximumClique",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumClique",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_vertices^2",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "num_vertices^3",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vertices",
"relation": "upper_bound"
}
],
"step": 4,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 5,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "cross_frequency_product + cross_frequency_product^2 + cross_frequency_product^3",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * cross_frequency_product * (cross_frequency_product^2)^2 + 2 * cross_frequency_product^3 + 2 * cross_frequency_product^4 + cross_frequency_product^2 * (cross_frequency_product^2)^2 + cross_frequency_product^2 + (cross_frequency_product^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 10130.698291934095,
"error": "construction timeout after 10 seconds"
},
{
"source": "LongestCommonSubsequence",
"route": [
{
"from": {
"name": "LongestCommonSubsequence",
"variant": {}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "cross_frequency_product^2",
"relation": "upper_bound"
},
{
"field": "num_vertices",
"formula": "cross_frequency_product",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "num_edges",
"relation": "exact"
},
{
"field": "num_vertices",
"formula": "num_vertices",
"relation": "exact"
}
],
"step": 2,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "num_sets",
"formula": "num_vertices",
"relation": "upper_bound"
},
{
"field": "universe_size",
"formula": "num_edges",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "universe_size",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "num_sets * universe_size",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_sets",
"relation": "exact"
}
],
"step": 4,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 5,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "cross_frequency_product + cross_frequency_product^2 + cross_frequency_product^3",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * cross_frequency_product * (cross_frequency_product^2)^2 + 2 * cross_frequency_product^3 + 2 * cross_frequency_product^4 + cross_frequency_product^2 * (cross_frequency_product^2)^2 + cross_frequency_product^2 + (cross_frequency_product^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 10149.037042050622,
"error": "construction timeout after 10 seconds"
},
{
"source": "LongestCommonSubsequence",
"route": [
{
"from": {
"name": "LongestCommonSubsequence",
"variant": {}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "cross_frequency_product^2",
"relation": "upper_bound"
},
{
"field": "num_vertices",
"formula": "cross_frequency_product",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
},
"parameter_contract": [
{
"field": "num_sets",
"formula": "num_vertices",
"relation": "upper_bound"
},
{
"field": "universe_size",
"formula": "num_edges",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "MaximumSetPacking",
"variant": {
"weight": "One"
}
}
},
{
"from": {
"name": "MaximumSetPacking",
"variant": {
"weight": "One"
}
},
"parameter_contract": [
{
"field": "num_sets",
"formula": "num_sets",
"relation": "exact"
},
{
"field": "universe_size",
"formula": "universe_size",
"relation": "exact"
}
],
"step": 3,
"to": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "universe_size",
"relation": "upper_bound"
},
{
"field": "num_nonzeros",
"formula": "num_sets * universe_size",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_sets",
"relation": "exact"
}
],
"step": 4,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 5,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "cross_frequency_product + cross_frequency_product^2 + cross_frequency_product^3",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * cross_frequency_product * (cross_frequency_product^2)^2 + 2 * cross_frequency_product^3 + 2 * cross_frequency_product^4 + cross_frequency_product^2 * (cross_frequency_product^2)^2 + cross_frequency_product^2 + (cross_frequency_product^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 10161.585541907698,
"error": "construction timeout after 10 seconds"
},
{
"source": "LongestCommonSubsequence",
"route": [
{
"from": {
"name": "LongestCommonSubsequence",
"variant": {}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1",
"relation": "exact"
},
{
"field": "num_constraints",
"formula": "max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "2 * num_transitions * (1 + sum_triangular_lengths) + max_length * (1 + alphabet_size + num_strings + 3 * total_length)",
"relation": "exact"
},
{
"field": "num_vars",
"formula": "max_length * total_length + max_length * (1 + alphabet_size)",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "max_length + num_transitions + 2 * max_length * total_length + max_length * num_strings + max_length * (1 + alphabet_size) + num_transitions * sum_triangular_lengths + (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths) * (max_length * total_length + max_length * (1 + alphabet_size))",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths) * (max_length * total_length + max_length * (1 + alphabet_size)) + 2 * (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths) * (max_length * total_length + max_length * (1 + alphabet_size))^2 + 2 * (max_length * total_length + max_length * (1 + alphabet_size)) * (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths)^2 + (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths)^2 * (max_length * total_length + max_length * (1 + alphabet_size))^2 + (max_length + num_transitions + max_length * num_strings + max_length * total_length + num_transitions * sum_triangular_lengths)^2 + (max_length * total_length + max_length * (1 + alphabet_size))^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 183.9643750572577,
"variables": 1085,
"couplings": 3327,
"max_coefficient": 11644,
"coefficient_bits": 14
},
{
"source": "MinimumGraphBandwidth/SimpleGraph",
"route": [
{
"from": {
"name": "MinimumGraphBandwidth",
"variant": {
"graph": "SimpleGraph"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vertices",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "1 + 2 * num_edges + 4 * num_vertices + num_vertices^2",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "(1 + num_vertices + num_vertices^2) * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "1 + num_vertices + num_vertices^2",
"relation": "exact"
}
],
"step": 1,
"to": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "bounded",
"coefficient": "i64",
"variable": "i64"
}
},
"parameter_contract": [
{
"field": "max_constraint_magnitude_bits",
"formula": "1 + num_vars + 2 * max_constraint_magnitude_bits",
"relation": "upper_bound"
},
{
"field": "num_constraints",
"formula": "num_constraints",
"relation": "exact"
},
{
"field": "num_nonzeros",
"formula": "num_nonzeros * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars * (1 + max_constraint_magnitude_bits)",
"relation": "upper_bound"
}
],
"step": 2,
"to": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
}
},
{
"from": {
"name": "ILP",
"variant": {
"bounds": "general",
"coefficient": "i64",
"variable": "bool"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "(num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars))^2",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_vars + num_constraints * (max_constraint_magnitude_bits + num_vars)",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "QUBO",
"variant": {
"weight": "i64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2) * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2) + (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2) * (2 + num_vertices + 2 * (1 + num_vertices) + num_vertices^2) + num_vertices^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2) * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2) * (2 + num_vertices + 2 * (1 + num_vertices) + num_vertices^2) + 2 * (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2) * (2 + num_vertices + 2 * (1 + num_vertices) + num_vertices^2) * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2)^2 + 2 * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2) * (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2)^2 + (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2)^2 * (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2)^2 + (1 + 2 * num_edges + 4 * num_vertices + num_vertices^2)^2 * (2 + num_vertices + 2 * (1 + num_vertices) + num_vertices^2)^2 + (1 + num_vertices + (1 + num_vertices) * (1 + num_vertices + num_vertices^2) + num_vertices^2)^2",
"relation": "upper_bound"
}
]
},
"cli_ms": 40.91674997471273,
"variables": 70,
"couplings": 256,
"max_coefficient": 1376,
"coefficient_bits": 11
}
] |
Collaborator
Author
Measurement and external-validation certificateActual targets, not symbolic upper bounds, determine the support comparisons. Couplings exclude diagonal terms and zero coefficients; coefficient bit lengths are Corpus coverage is explicitly split: coefficient equivalence; oracle-witness lift/target acceptance/actual CLI extraction/source evaluation/completed-value recovery; and unhinted raw CP-SAT target solving. Independent corpus truth is never regenerated or overwritten. 700/700 pass the first two applicable classes; raw50/70 pass,20timeouts. NO coefficient checks alone do not claim a raw solve. Every file in the read-only corpus, including hidden/environment files, was SHA-256 checked: 32,372 unchanged. Corpus-specific files are exclusively in the outside-repository scratch directory. See companion reproducibility comment for scripts. cli/results.json[
{
"source": "MinimumTardinessSequencing/i64",
"variables": 11,
"couplings": 31,
"max_coefficient": 14,
"coefficient_bits": 4,
"cli_ms": 35.7602919684723,
"composed": {
"fields": [
{
"field": "num_vars",
"reason": "reduction `MinimumTardinessSequencing -> QUBO` target field `num_vars` is unavailable: Start-grid size depends exponentially on processing magnitude bits; the contract supports only constant integer exponents",
"relation": "unavailable"
},
{
"field": "num_quadratic_terms",
"reason": "reduction `MinimumTardinessSequencing -> QUBO` target field `num_quadratic_terms` is unavailable: Start-grid size depends exponentially on processing magnitude bits; the contract supports only constant integer exponents",
"relation": "unavailable"
}
]
},
"source_result": {
"evaluation": "Min(1)",
"problem": "MinimumTardinessSequencing",
"solution": [
0,
1,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Min(1)",
"intermediate": {
"evaluation": "Min(-20)",
"problem": "QUBO",
"solution": [
false,
false,
false,
true,
true,
false,
false,
false,
false,
true,
false
],
"status": "optimal"
},
"problem": "MinimumTardinessSequencing",
"solution": [
1,
2,
0
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "SequencingToMinimizeWeightedTardiness",
"variables": 7,
"couplings": 7,
"max_coefficient": 22,
"coefficient_bits": 5,
"cli_ms": 35.63162498176098,
"composed": {
"fields": [
{
"field": "num_vars",
"reason": "reduction `SequencingToMinimizeWeightedTardiness -> DecisionQUBO` target field `num_vars` is unavailable: Start-grid size depends exponentially on processing magnitude bits; the contract supports only constant integer exponents",
"relation": "unavailable"
},
{
"field": "num_quadratic_terms",
"reason": "reduction `SequencingToMinimizeWeightedTardiness -> DecisionQUBO` target field `num_quadratic_terms` is unavailable: Start-grid size depends exponentially on processing magnitude bits; the contract supports only constant integer exponents",
"relation": "unavailable"
}
]
},
"source_result": {
"evaluation": "Or(true)",
"problem": "SequencingToMinimizeWeightedTardiness",
"solution": [
1,
0,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Or(true)",
"intermediate": {
"evaluation": "Or(true)",
"problem": "DecisionQUBO",
"solution": [
false,
true,
true,
false,
false,
true,
false
],
"status": "optimal"
},
"problem": "SequencingToMinimizeWeightedTardiness",
"solution": [
1,
2,
0
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "SequencingWithReleaseTimesAndDeadlines",
"variables": 7,
"couplings": 11,
"max_coefficient": 2,
"coefficient_bits": 2,
"cli_ms": 35.6483330251649,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_tasks * (1 + time_horizon)",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "(num_tasks * (1 + time_horizon))^2",
"relation": "upper_bound"
}
]
},
"source_result": {
"evaluation": "Or(true)",
"problem": "SequencingWithReleaseTimesAndDeadlines",
"solution": [
0,
1,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Or(true)",
"intermediate": {
"evaluation": "Or(true)",
"problem": "DecisionQUBO",
"solution": [
false,
false,
true,
true,
false,
false,
true
],
"status": "optimal"
},
"problem": "SequencingWithReleaseTimesAndDeadlines",
"solution": [
1,
0,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "DynamicStorageAllocation",
"variables": 6,
"couplings": 7,
"max_coefficient": 2,
"coefficient_bits": 2,
"cli_ms": 35.42050009127706,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "memory_size * num_items",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "(memory_size * num_items)^2",
"relation": "upper_bound"
}
]
},
"source_result": {
"evaluation": "Or(true)",
"problem": "DynamicStorageAllocation",
"solution": [
0,
0,
1
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Or(true)",
"intermediate": {
"evaluation": "Or(true)",
"problem": "DecisionQUBO",
"solution": [
false,
true,
false,
true,
true,
false
],
"status": "optimal"
},
"problem": "DynamicStorageAllocation",
"solution": [
1,
1,
0
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "FeasibleRegisterAssignment",
"variables": 3,
"couplings": 3,
"max_coefficient": 3,
"coefficient_bits": 2,
"cli_ms": 35.89008399285376,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_vertices * (-1 + num_vertices) * 2^-1",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "(num_vertices * (-1 + num_vertices) * 2^-1)^2",
"relation": "upper_bound"
}
]
},
"source_result": {
"evaluation": "Or(true)",
"problem": "FeasibleRegisterAssignment",
"solution": [
0,
1,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Or(true)",
"intermediate": {
"evaluation": "Or(true)",
"problem": "DecisionQUBO",
"solution": [
true,
true,
true
],
"status": "optimal"
},
"problem": "FeasibleRegisterAssignment",
"solution": [
0,
1,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "ShortestCommonSupersequence",
"variables": 10,
"couplings": 13,
"max_coefficient": 6,
"coefficient_bits": 3,
"cli_ms": 35.453291959129274,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "max_length * total_length + max_length * (1 + alphabet_size)",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "(max_length * total_length + max_length * (1 + alphabet_size))^2",
"relation": "upper_bound"
}
]
},
"source_result": {
"evaluation": "Min(2)",
"problem": "ShortestCommonSupersequence",
"solution": [
0,
1
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Min(2)",
"intermediate": {
"evaluation": "Min(-12)",
"problem": "QUBO",
"solution": [
false,
true,
false,
true,
false,
false,
false,
true,
true,
false
],
"status": "optimal"
},
"problem": "ShortestCommonSupersequence",
"solution": [
1,
0
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
},
{
"source": "Betweenness",
"variables": 3,
"couplings": 3,
"max_coefficient": 1,
"coefficient_bits": 1,
"cli_ms": 35.67558398935944,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_elements * (-1 + num_elements) * 2^-1",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "(num_elements * (-1 + num_elements) * 2^-1)^2",
"relation": "upper_bound"
}
]
},
"source_result": {
"evaluation": "Or(true)",
"problem": "Betweenness",
"solution": [
0,
1,
2
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
},
"recovered_result": {
"evaluation": "Or(true)",
"intermediate": {
"evaluation": "Or(true)",
"problem": "DecisionQUBO",
"solution": [
false,
false,
false
],
"status": "optimal"
},
"problem": "Betweenness",
"solution": [
2,
1,
0
],
"solver": {
"kind": "brute-force"
},
"status": "optimal"
}
}
]tradeoffs/results.json[
{
"source": "MinimumTardinessSequencing/i64",
"kind": "direct",
"variables": 130,
"couplings": 8383,
"max_coefficient": 130,
"coefficient_bits": 8,
"cli_ms": 48.6214580014348,
"instance": {
"type": "MinimumTardinessSequencing",
"variant": {
"weight": "i64"
},
"data": {
"lengths": [
64,
64
],
"deadlines": [
64,
128
],
"precedences": []
}
}
},
{
"source": "MinimumTardinessSequencing/i64",
"kind": "existing",
"variables": 42,
"couplings": 264,
"max_coefficient": 84803585,
"coefficient_bits": 27,
"cli_ms": 38.19420805666596,
"instance": {
"type": "MinimumTardinessSequencing",
"variant": {
"weight": "i64"
},
"data": {
"lengths": [
64,
64
],
"deadlines": [
64,
128
],
"precedences": []
}
}
},
{
"source": "SequencingToMinimizeWeightedTardiness",
"kind": "direct",
"variables": 130,
"couplings": 8383,
"max_coefficient": 4162,
"coefficient_bits": 13,
"cli_ms": 49.79908396489918,
"instance": {
"type": "SequencingToMinimizeWeightedTardiness",
"variant": {},
"data": {
"lengths": [
64,
64
],
"weights": [
1,
1
],
"deadlines": [
64,
128
],
"bound": 0
}
}
},
{
"source": "SequencingToMinimizeWeightedTardiness",
"kind": "existing",
"variables": 98,
"couplings": 1388,
"max_coefficient": 29491200,
"coefficient_bits": 25,
"cli_ms": 41.62600007839501,
"instance": {
"type": "SequencingToMinimizeWeightedTardiness",
"variant": {},
"data": {
"lengths": [
64,
64
],
"weights": [
1,
1
],
"deadlines": [
64,
128
],
"bound": 0
}
}
},
{
"source": "SequencingWithReleaseTimesAndDeadlines",
"kind": "direct",
"variables": 256,
"couplings": 16384,
"max_coefficient": 2,
"coefficient_bits": 2,
"cli_ms": 60.63058401923627,
"instance": {
"type": "SequencingWithReleaseTimesAndDeadlines",
"variant": {},
"data": {
"lengths": [
1,
1
],
"release_times": [
0,
0
],
"deadlines": [
128,
128
]
}
}
},
{
"source": "SequencingWithReleaseTimesAndDeadlines",
"kind": "existing",
"variables": 29,
"couplings": 350,
"max_coefficient": 3170304,
"coefficient_bits": 22,
"cli_ms": 38.17708301357925,
"instance": {
"type": "SequencingWithReleaseTimesAndDeadlines",
"variant": {},
"data": {
"lengths": [
1,
1
],
"release_times": [
0,
0
],
"deadlines": [
128,
128
]
}
}
},
{
"source": "FeasibleRegisterAssignment",
"kind": "direct",
"variables": 28,
"couplings": 168,
"max_coefficient": 6,
"coefficient_bits": 3,
"cli_ms": 38.42945792712271,
"instance": {
"type": "FeasibleRegisterAssignment",
"variant": {},
"data": {
"num_vertices": 8,
"arcs": [],
"num_registers": 8,
"assignment": [
0,
1,
2,
3,
4,
5,
6,
7
]
}
}
},
{
"source": "FeasibleRegisterAssignment",
"kind": "existing",
"variables": 24,
"couplings": 0,
"max_coefficient": 0,
"coefficient_bits": 0,
"cli_ms": 38.72587508521974,
"instance": {
"type": "FeasibleRegisterAssignment",
"variant": {},
"data": {
"num_vertices": 8,
"arcs": [],
"num_registers": 8,
"assignment": [
0,
1,
2,
3,
4,
5,
6,
7
]
}
}
},
{
"source": "LongestCommonSubsequence",
"kind": "existing_f64_match_MIS",
"variables": 6,
"couplings": 9,
"path": [
{
"from": {
"name": "LongestCommonSubsequence",
"variant": {}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "cross_frequency_product^2",
"relation": "upper_bound"
},
{
"field": "num_vertices",
"formula": "cross_frequency_product",
"relation": "upper_bound"
}
],
"step": 1,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "One"
}
},
"parameter_contract": [
{
"field": "num_edges",
"formula": "num_edges",
"relation": "exact"
},
{
"field": "num_vertices",
"formula": "num_vertices",
"relation": "exact"
}
],
"step": 2,
"to": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumIndependentSet",
"variant": {
"graph": "SimpleGraph",
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "num_sets",
"formula": "num_vertices",
"relation": "upper_bound"
},
{
"field": "universe_size",
"formula": "num_edges",
"relation": "upper_bound"
}
],
"step": 3,
"to": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
}
},
{
"from": {
"name": "MaximumSetPacking",
"variant": {
"weight": "i64"
}
},
"parameter_contract": [
{
"field": "num_sets",
"formula": "num_sets",
"relation": "exact"
},
{
"field": "universe_size",
"formula": "universe_size",
"relation": "exact"
}
],
"step": 4,
"to": {
"name": "MaximumSetPacking",
"variant": {
"weight": "f64"
}
}
},
{
"from": {
"name": "MaximumSetPacking",
"variant": {
"weight": "f64"
}
},
"parameter_contract": [
{
"field": "num_quadratic_terms",
"formula": "num_sets * (-1 + num_sets) * 2^-1",
"relation": "upper_bound"
},
{
"field": "num_vars",
"formula": "num_sets",
"relation": "exact"
}
],
"step": 5,
"to": {
"name": "QUBO",
"variant": {
"weight": "f64"
}
}
}
],
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "cross_frequency_product",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "0.5 * cross_frequency_product^2",
"relation": "upper_bound"
}
]
},
"max_coefficient": 2.0
}
]corpus/summary.json{
"total": 700,
"correct": 700,
"coverage": {
"coefficient_equivalence_and_oracle_witness_value_recovery": 446,
"coefficient_equivalence_with_independent_no_truth": 254
},
"by_source": {
"MinimumTardinessSequencing/i64": {
"total": 100,
"correct": 100
},
"Betweenness": {
"total": 100,
"correct": 100
},
"DynamicStorageAllocation": {
"total": 100,
"correct": 100
},
"ShortestCommonSupersequence": {
"total": 100,
"correct": 100
},
"SequencingWithReleaseTimesAndDeadlines": {
"total": 100,
"correct": 100
},
"SequencingToMinimizeWeightedTardiness": {
"total": 100,
"correct": 100
},
"FeasibleRegisterAssignment": {
"total": 100,
"correct": 100
}
}
}raw-targets/summary.json{
"total": 70,
"passed": 50,
"timeouts": 20,
"failures": 0,
"by_kind": {
"tardiness": {
"True": 10
},
"weighted": {
"None": 10
},
"release": {
"True": 10
},
"storage": {
"True": 10
},
"register": {
"True": 10
},
"supersequence": {
"None": 10
},
"betweenness": {
"True": 10
}
}
}upstream/results.json[
{
"source": "ThreePartition",
"via": "SequencingWithReleaseTimesAndDeadlines",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "-1 + num_elements + num_groups + (-1 + num_elements + num_groups) * (-1 + num_groups * (1 + bound))",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (-1 + num_groups * (1 + bound)) * (-1 + num_elements + num_groups)^2 + (-1 + num_elements + num_groups)^2 * (-1 + num_groups * (1 + bound))^2 + (-1 + num_elements + num_groups)^2",
"relation": "upper_bound"
}
]
},
"variables": 163,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "ThreePartition",
"value": true
},
"seconds": 0.8348919589770958
},
{
"source": "KSatisfiability/K3",
"via": "FeasibleRegisterAssignment",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "0.5 * (2 * num_vars + 12 * num_clauses)^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "0.25 * (2 * num_vars + 12 * num_clauses)^2 + 0.25 * (2 * num_vars + 12 * num_clauses)^4",
"relation": "upper_bound"
}
]
},
"variables": 435,
"status": "UNKNOWN",
"correct": false,
"error": "UNKNOWN",
"limitation": "Raw target solve unavailable",
"seconds": 20.501580332987942
},
{
"source": "SetSplitting",
"via": "Betweenness",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "0.5 * (1 + universe_size + num_subsets * (1 + 4 * universe_size))^2",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "0.25 * (1 + universe_size + num_subsets * (1 + 4 * universe_size))^2 + 0.25 * (1 + universe_size + num_subsets * (1 + 4 * universe_size))^4",
"relation": "upper_bound"
}
]
},
"variables": 45,
"status": "UNKNOWN",
"correct": false,
"error": "UNKNOWN",
"limitation": "Raw target solve unavailable",
"seconds": 20.438883082941175
}
]upstream/oracle-results.json[
{
"source": "KSatisfiability/K3",
"via": "FeasibleRegisterAssignment",
"coverage": "middle-model ILP oracle witness; actual QUBO evaluation and full-chain extraction/aggregate/source brute force",
"correct": true,
"variables": 435,
"middle_solution": [
8,
13,
0,
1,
2,
9,
26,
28,
25,
3,
14,
20,
10,
16,
11,
21,
4,
18,
12,
15,
5,
27,
19,
22,
17,
6,
24,
29,
23,
7
],
"source_solution": [
false,
false,
true
],
"aggregate": {
"problem": "KSatisfiability",
"value": true
}
},
{
"source": "SetSplitting",
"via": "Betweenness",
"coverage": "middle-model ILP oracle witness; actual QUBO evaluation and full-chain extraction/aggregate/source brute force",
"correct": true,
"variables": 45,
"middle_solution": [
8,
0,
9,
1,
2,
4,
3,
6,
7,
5
],
"source_solution": [
true,
false,
true,
false,
false
],
"aggregate": {
"problem": "SetSplitting",
"value": true
}
}
]upstream/inherited-direct-comparison.json{
"source": "ThreePartition",
"route": "Phase 2 direct",
"variables": 12,
"couplings": 36,
"max_coefficient": 150,
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "num_elements * num_groups",
"relation": "exact"
},
{
"field": "num_quadratic_terms",
"formula": "(num_elements * num_groups)^2",
"relation": "upper_bound"
}
]
}
}coverage-summary.json{
"files": [
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/betweenness_qubo.rs",
"covered": 47,
"lines": 47,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/dynamicstorageallocation_qubo.rs",
"covered": 66,
"lines": 66,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/feasibleregisterassignment_qubo.rs",
"covered": 57,
"lines": 57,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/minimumtardinesssequencingweighted_qubo.rs",
"covered": 45,
"lines": 46,
"percent": 97.82608695652173,
"uncovered": [
56
]
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/sequencingtominimizeweightedtardiness_qubo.rs",
"covered": 66,
"lines": 67,
"percent": 98.50746268656717,
"uncovered": [
68
]
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/sequencingwithreleasetimesanddeadlines_qubo.rs",
"covered": 50,
"lines": 50,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/shortestcommonsupersequence_qubo.rs",
"covered": 81,
"lines": 82,
"percent": 98.78048780487805,
"uncovered": [
75
]
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/start_time_qubo.rs",
"covered": 77,
"lines": 79,
"percent": 97.46835443037975,
"uncovered": [
98,
99
]
}
],
"total_covered": 489,
"total_lines": 494,
"percentage": 98.98785425101215
} |
Collaborator
Author
Reproducibility — measurement-runnersScripts run outside the repository/corpus. Use a scratch Python environment with OR-Tools for raw solving and the constructor from the mathematical certificate. Paths identify the local scratch, read-only corpus, and built CLI; relocate those roots when reproducing. No corpus file is written. baselines.pyimport json,subprocess,time,statistics
from pathlib import Path
from constructor import *
base=Path(__file__).parent;out=base/'measurements';out.mkdir(exist_ok=True)
pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def run(args):
t=time.perf_counter();p=subprocess.run([pred,*args,'--quiet','--json'],capture_output=True,text=True,timeout=60)
return (json.loads(p.stdout) if p.returncode==0 else None),p.stderr,(time.perf_counter()-t)*1000
rows=[]
for kind,(name,d) in CASES.items():
source=envelope(kind,d);f=out/(kind+'-source.json');f.write_text(json.dumps(source))
paths,err,_=run(['path',name,'QUBO/i64','--limit','all']);paths=paths or {'paths':[], 'error':err}
(out/(kind+'-paths.json')).write_text(json.dumps(paths,indent=2))
n,e,c=build(kind,d);rows.append(dict(source=name,kind='proposed',variables=n,couplings=sum(i!=j for i,j in e),max_coefficient=max(map(abs,e.values()),default=0),coefficient_bits=max(map(abs,e.values()),default=0).bit_length()))
# Measure all shortest alternatives and any paths using inherited direct rules, bounded to 5 steps.
steps=min((p['steps'] for p in paths['paths']),default=0)
choices=[p for p in paths['paths'] if p['steps']==steps or p['steps']<=5 and any(x['to']['name']=='DecisionQUBO' for x in p['path'])]
for i,p in enumerate(choices):
route=out/(kind+f'-baseline-route-{i}.json');route.write_text(json.dumps(p));timings=[]
for _ in range(3):
bundle,error,ms=run(['reduce',str(f),'--via',str(route)]);timings.append(ms)
if bundle is None:break
row=dict(source=name,kind='existing',path=p['path'],composed=p['overall_parameters'],cli_ms=statistics.median(timings))
if bundle is None:row['error']=error
else:
(out/(kind+f'-baseline-bundle-{i}.json')).write_text(json.dumps(bundle));q=bundle['target']['data'];q=q.get('inner',q);m=max((abs(c) for i,j,c in q['entries']),default=0);row.update(variables=q['num_vars'],couplings=sum(i!=j for i,j,c in q['entries']),max_coefficient=m,coefficient_bits=m.bit_length())
rows.append(row)
print(name,[(r['kind'],r.get('variables'),r.get('couplings'),r.get('error')) for r in rows if r['source']==name],flush=True)
(out/'baseline-results.json').write_text(json.dumps(rows,indent=2))cli_checks.pyimport json,subprocess,time,statistics
from pathlib import Path
from constructor import CASES,build
base=Path(__file__).parent;out=base/'cli';out.mkdir(exist_ok=True);pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--json','--quiet'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=30);assert p.returncode==0,p.stderr;return json.loads(p.stdout)
rows=[]
for kind,(name,d) in CASES.items():
target='QUBO/i64' if kind in ('tardiness','supersequence') else 'DecisionQUBO/i64'
source=cli(['create','--example',name,'--to',target]);f=out/(kind+'-source.json');f.write_text(json.dumps(source))
paths=cli(['path',name,target,'--limit','all']);route=next(p for p in paths['paths'] if p['steps']==1);rf=out/(kind+'-route.json');rf.write_text(json.dumps(route));ts=[]
for _ in range(3):
start=time.perf_counter();bundle=cli(['reduce',str(f),'--via',str(rf)]);ts.append((time.perf_counter()-start)*1000)
bf=out/(kind+'-bundle.json');bf.write_text(json.dumps(bundle))
solved=cli(['solve',str(bf),'--solver','brute-force']);direct=cli(['solve',str(f),'--solver','brute-force']);assert solved['evaluation']==direct['evaluation'],(solved,direct)
ev=cli(['evaluate',str(f),'--config',json.dumps(solved['solution'])]);assert ev['result']==direct['evaluation']
q=bundle['target']['data'];q=q.get('inner',q);N,e,c=build(kind,d);assert q['num_vars']==N and q['entries']==sorted([i,j,v] for (i,j),v in e.items())
row=dict(source=name,variables=N,couplings=sum(i!=j for i,j in e),max_coefficient=max(map(abs,e.values()),default=0),coefficient_bits=max(map(abs,e.values()),default=0).bit_length(),cli_ms=statistics.median(ts),composed=route['overall_parameters'],source_result=direct,recovered_result=solved)
rows.append(row);print(kind,row['variables'],row['couplings'],solved['evaluation'],flush=True)
(out/'results.json').write_text(json.dumps(rows,indent=2))
# Signed bin use is not represented by the existing capacity*y linking row.
s={'type':'BinPacking','variant':{'weight':'i64'},'data':{'sizes':[-1],'capacity':1}}
f=out/'signed-bin.json';f.write_text(json.dumps(s));direct=cli(['solve',str(f),'--solver','brute-force'])
r=next(p for p in cli(['path','BinPacking/i64','ILP/variable=bool','--limit','all'])['paths'] if p['steps']==1);rf=out/'signed-bin-route.json';rf.write_text(json.dumps(r));bundle=cli(['reduce',str(f),'--via',str(rf)])
wrong=cli(['evaluate','-','--config','[1,0]'],bundle['target']);(out/'signed-bin-evidence.json').write_text(json.dumps(dict(source=direct,target_evaluation=wrong,bundle=bundle),indent=2));print('signed-bin',direct['evaluation'],wrong['result'])tradeoffs.pyimport json,subprocess,time
from pathlib import Path
from constructor import build
base=Path(__file__).parent;out=base/'tradeoffs';out.mkdir(exist_ok=True);pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--quiet','--json'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=30);assert p.returncode==0,p.stderr;return json.loads(p.stdout)
rows=[]
for kind,name,d in [
('tardiness','MinimumTardinessSequencing/i64',dict(lengths=[64,64],deadlines=[64,128],precedences=[])),
('weighted','SequencingToMinimizeWeightedTardiness',dict(lengths=[64,64],weights=[1,1],deadlines=[64,128],bound=0)),
('release','SequencingWithReleaseTimesAndDeadlines',dict(lengths=[1,1],release_times=[0,0],deadlines=[128,128])),
('register','FeasibleRegisterAssignment',dict(num_vertices=8,arcs=[],num_registers=8,assignment=list(range(8))))]:
source=dict(type=name.split('/')[0],variant={'weight':'i64'} if kind=='tardiness' else {},data=d);f=out/(kind+'.json');f.write_text(json.dumps(source))
target='QUBO/i64' if kind=='tardiness' else 'DecisionQUBO/i64'
paths=cli(['path',name,target,'--limit','all'])['paths'];direct=next(p for p in paths if p['steps']==1)
baselinepaths=cli(['path',name,'QUBO/i64','--limit','all'])['paths'];baseline=min((p for p in baselinepaths if not any(e['from']['name']==name.split('/')[0] and e['to']['name'] in ['QUBO','DecisionQUBO'] for e in p['path'])),key=lambda p:p['steps'])
for label,p in [('direct',direct),('existing',baseline)]:
rf=out/(kind+'-'+label+'-route.json');rf.write_text(json.dumps(p));start=time.perf_counter();b=cli(['reduce',str(f),'--via',str(rf)]);ms=(time.perf_counter()-start)*1000;q=b['target']['data'];q=q.get('inner',q);M=max((abs(v) for i,j,v in q['entries']),default=0)
rows.append(dict(source=name,kind=label,variables=q['num_vars'],couplings=sum(i!=j for i,j,v in q['entries']),max_coefficient=M,coefficient_bits=M.bit_length(),cli_ms=ms,instance=source))
print(name,[(r['kind'],r['variables'],r['couplings']) for r in rows if r['source']==name],flush=True)
# Compare match-tuple support to the existing f64 MIS->set-packing chain.
name='LongestCommonSubsequence';source=cli(['create','--example',name,'--to','MaximumIndependentSet/SimpleGraph/One']);f=out/'lcs.json';f.write_text(json.dumps(source))
paths=cli(['path',name,'QUBO/f64','--limit','all'])['paths'];p=min((p for p in paths if any(e['to']['name']=='MaximumIndependentSet' for e in p['path']) and not any(e['to']['name'] in ['ILP','MinimumFeedbackArcSet','SpinGlass','MaximumClique'] for e in p['path'])),key=lambda p:p['steps']);rf=out/'lcs-route.json';rf.write_text(json.dumps(p));b=cli(['reduce',str(f),'--via',str(rf)]);q=b['target']['data'];rows.append(dict(source=name,kind='existing_f64_match_MIS',variables=q['num_vars'],couplings=sum(i!=j for i,j,v in q['entries']),path=p['path'],composed=p['overall_parameters'],max_coefficient=max(abs(v) for i,j,v in q['entries'])));print('LCS',rows[-1],flush=True)
(out/'results.json').write_text(json.dumps(rows,indent=2))deferred.pyimport json,subprocess,time
from pathlib import Path
base=Path(__file__).parent;out=base/'deferred';out.mkdir(exist_ok=True);pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
names=['SequencingToMinimizeTardyTaskWeight','MultiprocessorScheduling','ResourceConstrainedScheduling','BinPacking/i64','CapacityAssignment','LongestCommonSubsequence','MinimumGraphBandwidth/SimpleGraph'];rows=[]
def run(args):
try:p=subprocess.run([pred,*args,'--json','--quiet'],capture_output=True,text=True,timeout=10)
except subprocess.TimeoutExpired:return {'error':'construction timeout after 10 seconds'}
return json.loads(p.stdout) if p.returncode==0 else {'error':p.stderr}
for name in names:
s=run(['create','--example',name]);key=name.split('/')[0];f=out/(key+'.json');f.write_text(json.dumps(s));paths=run(['path',name,'QUBO/i64','--limit','all']);(out/(key+'-paths.json')).write_text(json.dumps(paths,indent=2))
if 'error' in paths:rows.append(dict(source=name,error=paths['error']));continue
steps=min(p['steps'] for p in paths['paths']);choices=[p for p in paths['paths'] if p['steps']==steps]
if name=='LongestCommonSubsequence':choices=[p for p in paths['paths'] if p['steps']<=5 and any(e['to']['name']=='MaximumIndependentSet' for e in p['path']) and not any(e['to']['name']=='MinimumFeedbackArcSet' for e in p['path'])][:3]+choices
for i,p in enumerate(choices):
route=out/(key+f'-route-{i}.json');route.write_text(json.dumps(p));t=time.perf_counter();bundle=run(['reduce',str(f),'--via',str(route)]);ms=(time.perf_counter()-t)*1000
row=dict(source=name,route=p['path'],composed=p['overall_parameters'],cli_ms=ms)
if 'error' in bundle:row.update(error=bundle['error'])
else:
(out/(key+f'-bundle-{i}.json')).write_text(json.dumps(bundle));q=bundle['target']['data'];q=q.get('inner',q);M=max((abs(c) for _,_,c in q['entries']),default=0);row.update(variables=q['num_vars'],couplings=sum(i!=j for i,j,c in q['entries']),max_coefficient=M,coefficient_bits=M.bit_length())
rows.append(row)
(out/'measurements.json').write_text(json.dumps(rows,indent=2))
print(name,[(r.get('variables'),r.get('couplings'),r.get('error')) for r in rows if r['source']==name],flush=True)
(out/'measurements.json').write_text(json.dumps(rows,indent=2)) |
Collaborator
Author
Reproducibility — corpus-runnersScripts run outside the repository/corpus. Use a scratch Python environment with OR-Tools for raw solving and the constructor from the mathematical certificate. Paths identify the local scratch, read-only corpus, and built CLI; relocate those roots when reproducing. No corpus file is written. corpus.pyimport sys
sys.dont_write_bytecode=True
import json,subprocess,time,collections,concurrent.futures
from pathlib import Path
from constructor import build,CASES
base=Path(__file__).parent;root=Path('/Users/xiweipan/Codes/pred-validation-corpus');out=base/'corpus';out.mkdir(exist_ok=True)
pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--quiet','--json'],input=json.dumps(data) if data is not None else None,capture_output=True,text=True,timeout=30)
if p.returncode:raise RuntimeError(p.stderr)
return json.loads(p.stdout)
def parse(v):
if isinstance(v,str):
v=v[v.index('(')+1:-1]
if v in ('None','none'):return None
return json.loads(v)
return v
routes={}
for kind,(name,_) in CASES.items():
target='QUBO/i64' if kind in ('tardiness','supersequence') else 'DecisionQUBO/i64'
route=next(p for p in cli(['path',name,target,'--limit','all'])['paths'] if p['steps']==1);f=out/(kind+'-route.json');f.write_text(json.dumps(route));routes[kind]=f
truth=collections.defaultdict(list)
for f in (root/'ground-truth').rglob('*.jsonl'):
for line in f.read_text().splitlines():
t=json.loads(line)
if t['problem'] in [v[0] for v in CASES.values()]:truth[t['problem']].append(t)
def schema(kind,d):
d=dict(d)
if kind=='register':d={'n':d['num_vertices'],'arcs':d['arcs'],'registers':d['assignment']}
if kind=='betweenness':d={'n':d['num_elements'],'triples':d['triples']}
return d
def lift(kind,d,w,N):
bits=[False]*N
if kind in ('register','betweenness'):
return [w.index(i)<w.index(j) for i in range(d['n']) for j in range(i+1,d['n'])]
if kind=='supersequence':
L=sum(map(len,d['strings']));a=d['alphabet_size'];k=a+1
for p in range(L):bits[p*k+(w[p] if p<len(w) else a)]=True
gc=0
for s in d['strings']:
start=0
for ch in s:
p=w.index(ch,start);bits[L*k+gc*L+p]=True;gc+=1;start=p+1
return bits
if kind=='storage':counts=[d['memory_size']-s+1 for _,_,s in d['items']];choices=w
else:
H=sum(d['lengths']);counts=[max(0,d['deadlines'][i]-d['release_times'][i]-p+1) if kind=='release' else H-p+1 for i,p in enumerate(d['lengths'])]
if kind=='release':choices=[s-r for s,r in zip(w,d['release_times'])]
else:
order=w['order'] if kind=='weighted' else w;choices=[0]*len(order);elapsed=0
for i in order:choices[i]=elapsed;elapsed+=d['lengths'][i]
offset=0
for count,choice in zip(counts,choices):bits[offset+choice]=True;offset+=count
return bits
def verify(kind,t):
r=dict(kind=kind,source=t['problem'],instance=t['instance'],expected=t['value']);start=time.monotonic()
try:
data=json.loads((root/t['instance']).read_text())['data'];d=schema(kind,data);N,e,c=build(kind,d)
bundle=cli(['reduce',str(root/t['instance']),'--via',str(routes[kind])]);td=bundle['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data']
assert N==q['num_vars'] and sorted([i,j,v] for (i,j),v in e.items())==q['entries'], 'polynomial mismatch'
if decision:
cap=0
if kind=='weighted':H=sum(d['lengths']);cap=min(d['bound'],sum(d['weights'][i]*max(0,t+p-d['deadlines'][i]) for i,p in enumerate(d['lengths']) for t in range(H-p+1)))
assert td['data']['bound']==cap-c
no=t['status'] in ('unsatisfiable','infeasible')
if no:r.update(correct=True,coverage='coefficient_equivalence_with_independent_no_truth')
else:
bits=lift(kind,d,t['witness'],N);E=sum(v*bits[i]*bits[j] for (i,j),v in e.items())
assert E<=td['data']['bound'] if decision else E+c==t['value']
x=cli(['extract','-','--config',json.dumps(bits)],bundle);assert parse(x['evaluation'])==t['value'],x
ev=cli(['evaluate',str(root/t['instance']),'--config',json.dumps(x['solution'])]);assert parse(ev['result'])==t['value']
value=cli(['extract','-','--value='+json.dumps(True if decision else E)],bundle);assert value['value']==t['value'],value
r.update(correct=True,coverage='coefficient_equivalence_and_oracle_witness_value_recovery')
r.update(variables=N,couplings=sum(i!=j for i,j in e),max_coefficient=max(map(abs,e.values()),default=0))
except Exception as ex:r.update(correct=False,error=str(ex))
r['seconds']=time.monotonic()-start;return r
if __name__=='__main__':
work=[(kind,t) for kind,(name,_) in CASES.items() for t in truth[name]];assert len(work)==700,[(k,len(truth[n])) for k,(n,_) in CASES.items()]
rows=[]
with (out/'results.jsonl').open('w') as f,concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
for r in pool.map(lambda x:verify(*x),work):
rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
if not r['correct'] or len(rows)%100==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['kind'])),flush=True)
summary=dict(total=len(rows),correct=sum(r['correct'] for r in rows),coverage=dict(collections.Counter(r.get('coverage','failure') for r in rows)),by_source={n:dict(total=sum(r['source']==n for r in rows),correct=sum(r['source']==n and r['correct'] for r in rows)) for n in truth})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary))raw_targets.pyimport corpus as c
from ortools.sat.python import cp_model
import json,time,collections
from pathlib import Path
base=Path(__file__).parent;out=base/'raw-targets';out.mkdir(exist_ok=True)
def verify(kind,t):
r=dict(kind=kind,source=t['problem'],instance=t['instance'],expected=t['value']);start=time.monotonic()
try:
b=c.cli(['reduce',str(c.root/t['instance']),'--via',str(c.routes[kind])]);td=b['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data']
m=cp_model.CpModel();xs=[m.new_bool_var('x'+str(i)) for i in range(q['num_vars'])];terms=[]
for i,j,v in q['entries']:
if i==j:terms.append(v*xs[i])
else:y=m.new_bool_var(f'y{i}_{j}');m.add_multiplication_equality(y,[xs[i],xs[j]]);terms.append(v*y)
if decision:m.add(sum(terms)<=td['data']['bound'])
else:m.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=3;status=solver.solve(m);r.update(status=solver.status_name(status),variables=q['num_vars'])
if status not in (cp_model.OPTIMAL,cp_model.INFEASIBLE):r.update(correct=None,limitation='raw target solve timeout');return r
no=t['status'] in ('infeasible','unsatisfiable')
if status==cp_model.INFEASIBLE:
assert decision and no;value=c.cli(['extract','-','--value=false'],b);assert value['value']==False
else:
bits=[bool(solver.value(x)) for x in xs];E=sum(v*bits[i]*bits[j] for i,j,v in q['entries']);value=c.cli(['extract','-','--value='+json.dumps(True if decision else E)],b);assert value['value']==t['value'],value
if not no:
ex=c.cli(['extract','-','--config',json.dumps(bits)],b);assert c.parse(ex['evaluation'])==t['value']
else:
try:c.cli(['extract','-','--config',json.dumps(bits)],b)
except RuntimeError:pass
else:raise AssertionError('invalid optimum decoded')
r.update(correct=True,aggregate=value)
except Exception as ex:r.update(correct=False,error=str(ex))
r['seconds']=time.monotonic()-start;return r
def size(kind,t):
d=c.schema(kind,json.loads((c.root/t['instance']).read_text())['data'])
if kind in ('register','betweenness'):return d['n']*(d['n']-1)//2
if kind=='supersequence':L=sum(map(len,d['strings']));return L*(L+d['alphabet_size']+1)
if kind=='storage':return sum(d['memory_size']-s+1 for _,_,s in d['items'])
if kind=='release':return sum(max(0,e-r-p+1) for e,r,p in zip(d['deadlines'],d['release_times'],d['lengths']))
H=sum(d['lengths']);return sum(H-p+1 for p in d['lengths'])
rows=[]
with (out/'results.jsonl').open('w') as f:
for kind,(name,_) in c.CASES.items():
for t in sorted(c.truth[name],key=lambda t:size(kind,t))[:10]:
r=verify(kind,t);rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
print(kind,collections.Counter(str(r['correct']) for r in rows if r['kind']==kind),flush=True)
summary=dict(total=len(rows),passed=sum(r['correct'] is True for r in rows),timeouts=sum(r['correct'] is None for r in rows),failures=sum(r['correct'] is False for r in rows),by_kind={k:dict(collections.Counter(str(r['correct']) for r in rows if r['kind']==k)) for k in c.CASES})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary))upstream.pyimport json,subprocess,time
from pathlib import Path
from ortools.sat.python import cp_model
base=Path(__file__).parent;out=base/'upstream';out.mkdir(exist_ok=True)
pred=Path('/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred')
def cli(args,data=None):
p=subprocess.run([str(pred),*args,'--quiet','--json'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=60)
assert p.returncode==0,p.stderr
return json.loads(p.stdout)
rows=[]
for a,b,target in [('ThreePartition','SequencingWithReleaseTimesAndDeadlines','DecisionQUBO/i64'),('KSatisfiability/K3','FeasibleRegisterAssignment','DecisionQUBO/i64'),('SetSplitting','Betweenness','DecisionQUBO/i64')]:
row=dict(source=a,via=b,target=target);label=a.replace('/','_')+'-'+b.replace('/','_');start=time.monotonic()
try:
source=cli(['create','--example',a,'--to',b]);f=out/(label+'.json');f.write_text(json.dumps(source))
paths=cli(['path',a,target,'--limit','all'])['paths'];route=next(p for p in paths if p['steps']==2 and p['path'][0]['to']['name']==b.split('/')[0]);rf=out/(label+'-route.json');rf.write_text(json.dumps(route));row['composed']=route['overall_parameters']
bundle=cli(['reduce',str(f),'--via',str(rf)]);(out/(label+'-bundle.json')).write_text(json.dumps(bundle));td=bundle['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data'];row['variables']=q['num_vars']
model=cp_model.CpModel();xs=[model.new_bool_var('x'+str(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)
if decision:model.add(sum(terms)<=td['data']['bound'])
else:model.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=20
status=solver.solve(model);row['status']=solver.status_name(status);assert status==cp_model.OPTIMAL,row['status']
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'])
extracted=cli(['extract','-','--config',json.dumps(bits)],bundle);aggregate=cli(['extract','-','--value='+json.dumps(True if decision else energy)],bundle)
direct=cli(['solve',str(f),'--solver','brute-force']);evaluated=cli(['evaluate',str(f),'--config',json.dumps(extracted['solution'])]);assert direct['evaluation']==evaluated['result'],(direct,evaluated)
row.update(correct=True,evaluation=evaluated['result'],aggregate=aggregate)
except Exception as e:row.update(correct=False,error=str(e),limitation='Raw target solve unavailable' if 'UNKNOWN' in str(e) else None)
row['seconds']=time.monotonic()-start;rows.append(row);(out/'results.json').write_text(json.dumps(rows,indent=2));print(json.dumps(row),flush=True)upstream_witness.pyimport json,subprocess,time
from pathlib import Path
from ortools.sat.python import cp_model
base=Path(__file__).parent;out=base/'upstream';pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--quiet','--json'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=60);assert p.returncode==0,p.stderr;return json.loads(p.stdout)
rows=[]
for a,b in [('KSatisfiability/K3','FeasibleRegisterAssignment'),('SetSplitting','Betweenness')]:
label=a.replace('/','_')+'-'+b;source=out/(label+'.json');bundle=json.loads((out/(label+'-bundle.json')).read_text())
route=next(p for p in cli(['path',a,b,'--limit','all'])['paths'] if p['steps']==1);rf=out/(label+'-first-route.json');rf.write_text(json.dumps(route));middle=cli(['reduce',str(source),'--via',str(rf)])['target']
# This is a witness oracle for the middle model, explicitly not a raw QUBO solve.
solved=cli(['solve','-','--solver','ilp'],middle);rank=solved['solution'];bits=[rank[i]<rank[j] for i in range(len(rank)) for j in range(i+1,len(rank))]
evaluated=cli(['evaluate','-','--config',json.dumps(bits)],bundle['target']);assert evaluated['result']=='Or(true)'
x=cli(['extract','-','--config',json.dumps(bits)],bundle);value=cli(['extract','-','--value=true'],bundle);direct=cli(['solve',str(source),'--solver','brute-force']);assert x['evaluation']==direct['evaluation']=='Or(true)';assert value['value']==True
rows.append(dict(source=a,via=b,coverage='middle-model ILP oracle witness; actual QUBO evaluation and full-chain extraction/aggregate/source brute force',correct=True,variables=len(bits),middle_solution=rank,source_solution=x['solution'],aggregate=value));print(a,'oracle round trip passed',flush=True)
(out/'oracle-results.json').write_text(json.dumps(rows,indent=2))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') |
Collaborator
Author
Agentic Review ReportFresh-context review of the uncommitted Phase 3 diff against Structural and semantic reviewAll seven exact endpoint edges, aggregate mappings, canonical examples, parameter declarations and manual proofs are present. No generated exports, model-domain changes, unrelated core changes or dependencies are added. Existing ILP changes only qualify trait methods whose target inference becomes ambiguous. Traced constructors and actual evaluators, sparse coefficient expansion, omitted constants, penalty separation, extraction and completed-value recovery. In particular, the start encoding correctly orders zero-duration tasks before positive tasks at shared starts; fixed register assignments remain fixed; invalid SCS alphabet symbols force infeasibility; and reversed Betweenness literals produce the intended squared comparison difference. The two processing-horizon transforms deliberately report unavailable metadata while their mathematical pseudopolynomial bounds remain documented. Quality and verificationNative tests reuse independent source/target brute-force helpers, enumerate small target bitstrings, verify recovered values, reject malformed lengths, and cover NO and boundary inputs. The red log records the seven original behavior tests failing because direct edges were absent. Existing registry-wide parameter validation discovers the canonical sources. Reviewed independent proof/adversary reports and route measurements. The measured benefits are conditional: examples improve over ILP routes, storage gains connectivity, while large horizons and sparse-register instances can favor existing encodings. Reports distinguish polynomial/oracle checks from raw target solves and explicit timeouts. Feature testsUsing the installed release CLI built from this checkout, independently completed 23 workflows: all seven canonical Scripts, inputs and outputs are in FindingsResolved Important — Release-time source arithmetic can overflow before a source witness reaches the new encoding. Initial location: For Resolved Important — SCS row allocation can panic despite representable index counts. Initial location: For Both findings are resolved. The coordinator first reproduced each in a failing native regression, then added the source-finish bound and SCS row-byte-capacity check. I reviewed both guards and rechecked the original inputs against both rebuilt debug and installed release CLIs: each now fails at reduction with typed integer overflow and produces no target. The release guard deliberately conservatively rejects instances whose source arithmetic cannot be certified; no model semantics were changed. The final installed release CLI also passes all 23 feature workflows again. Three additional extreme round trips pass: a zero-duration job at maximum i64 release, a maximum-i64-duration job starting at zero, and all-empty SCS with alphabet Final verdict: no unresolved Critical, Important, or Minor findings. This review does not approve merging or change draft status. The coordinator reports final Skipped duplicate Rust builds and direct corpus access; coordinator-owned full gates and corpus evidence must be attributed separately. No hardware embedding or annealer performance was checked, and large-target solve timeouts remain limitations. Reviewed-file hashes match committed head features.pyimport json,subprocess,pathlib,sys
out=pathlib.Path(__file__).parent
pred=sys.argv[1]
rows=[]
def cli(args,fail=False):
p=subprocess.run([pred,*args,'--json','--quiet'],capture_output=True,text=True,timeout=30)
if fail:
assert p.returncode != 0,(args,p.stdout);return {'code':p.returncode,'error':p.stderr}
assert p.returncode==0,(args,p.returncode,p.stderr)
return json.loads(p.stdout)
def save(name,value):
f=out/(name+'.json');f.write_text(json.dumps(value,indent=2));return str(f)
def target(name):return 'QUBO/i64' if name in ['MinimumTardinessSequencing/i64','ShortestCommonSupersequence'] else 'DecisionQUBO/i64'
names=['MinimumTardinessSequencing/i64','SequencingToMinimizeWeightedTardiness','SequencingWithReleaseTimesAndDeadlines','DynamicStorageAllocation','FeasibleRegisterAssignment','ShortestCommonSupersequence','Betweenness']
routes={}
for name in names:
t=target(name);stem=name.split('/')[0]
for command in [['list','--rules',name],['show',name]]:save(stem+'-'+command[0],cli(command))
source=cli(['create','--example',name,'--to',t]);f=save(stem+'-source',source)
save(stem+'-inspect',cli(['inspect',f]))
paths=cli(['path',name,t,f,'--limit','all']);save(stem+'-paths',paths)
route=next(p for p in paths['paths'] if p['steps']==1);rf=save(stem+'-route',route);routes[name]=rf
bundle=cli(['reduce',f,'--via',rf]);bf=save(stem+'-bundle',bundle)
original=cli(['solve',f,'--solver','brute-force']);recovered=cli(['solve',bf,'--solver','brute-force'])
assert original['evaluation']==recovered['evaluation'],(original,recovered)
bits=recovered['intermediate']['solution'];val=recovered['intermediate']['evaluation']
assert cli(['extract',bf,'--config',json.dumps(bits)])['solution']==recovered['solution']
av=val[val.index('(')+1:-1];value=cli(['extract',bf,'--value='+av]);save(stem+'-aggregate',value)
assert value['value']==json.loads(original['evaluation'].split('(',1)[1][:-1])
reject=cli(['extract',bf,'--config',json.dumps(bits+[False])],True)
rows.append(dict(case=stem+'-canonical',original=original,recovered=recovered,reject=reject))
cases=[
('MinimumTardinessSequencing/i64',{'lengths':[1,2],'deadlines':[-2,1],'precedences':[]}),
('MinimumTardinessSequencing/i64',{'lengths':[1,1],'deadlines':[2,2],'precedences':[[0,1],[1,0]]}),
('SequencingToMinimizeWeightedTardiness',{'lengths':[0,1,0],'weights':[3,0,5],'deadlines':[0,0,0],'bound':0}),
('SequencingToMinimizeWeightedTardiness',{'lengths':[1,0],'weights':[1,1],'deadlines':[0,0],'bound':0}),
('SequencingWithReleaseTimesAndDeadlines',{'lengths':[1,0,1,0,1],'release_times':[0,0,1,2,2],'deadlines':[1,0,2,2,3]}),
('SequencingWithReleaseTimesAndDeadlines',{'lengths':[0,0],'release_times':[2,1],'deadlines':[2,1]}),
('SequencingWithReleaseTimesAndDeadlines',{'lengths':[1,1],'release_times':[0,0],'deadlines':[1,1]}),
('DynamicStorageAllocation',{'items':[[0,2,2],[2,4,2],[1,3,1]],'memory_size':3}),
('DynamicStorageAllocation',{'items':[[0,2,2],[0,2,2]],'memory_size':3}),
('FeasibleRegisterAssignment',{'num_vertices':5,'arcs':[[1,0],[2,1],[3,2],[4,3],[4,3]],'num_registers':1,'assignment':[0]*5}),
('FeasibleRegisterAssignment',{'num_vertices':5,'arcs':[[1,0],[2,0],[3,1],[4,2]],'num_registers':1,'assignment':[0]*5}),
('ShortestCommonSupersequence',{'alphabet_size':2,'strings':[[1,0]]}),
('ShortestCommonSupersequence',{'alphabet_size':1,'strings':[[],[0],[0,0]]}),
('ShortestCommonSupersequence',{'alphabet_size':1,'strings':[[1]]}),
('Betweenness',{'num_elements':5,'triples':[[4,3,2],[2,1,0],[4,2,0],[4,2,0]]}),
('Betweenness',{'num_elements':5,'triples':[[4,3,2],[4,2,3]]}),
]
for i,(name,data) in enumerate(cases):
stem=f'adversarial-{i}-{name.split("/")[0]}'
source={'type':name.split('/')[0],'variant':{'weight':'i64'} if '/' in name else {},'data':data};f=save(stem+'-source',source)
bundle=cli(['reduce',f,'--via',routes[name]]);bf=save(stem+'-bundle',bundle)
a=cli(['solve',f,'--solver','brute-force']);b=cli(['solve',bf,'--solver','brute-force'])
assert a.get('evaluation')==b.get('evaluation') and a['status']==b['status'],(name,a,b)
rows.append(dict(case=stem,source=a,recovered=b))
print(stem,a.get('evaluation'),a['status'],flush=True)
save('feature-results',rows)
print('PASS',len(rows),flush=True)fixed_boundaries.pyimport json, pathlib, subprocess, sys
out=pathlib.Path(__file__).parent
pred=sys.argv[1]
rows=[]
def run(args):
p=subprocess.run([pred,*args,'--json','--quiet'],capture_output=True,text=True,timeout=20)
return dict(args=args,returncode=p.returncode,stdout=p.stdout,stderr=p.stderr)
for stem,route in [('release-overflow','SequencingWithReleaseTimesAndDeadlines-route'),('supersequence-allocation-overflow','ShortestCommonSupersequence-route')]:
r=run(['reduce',str(out/(stem+'.json')),'--via',str(out/(route+'.json'))]);assert r['returncode']==1 and 'integer overflow' in r['stderr'].lower(),r;rows.append(r)
# Both extremes have a single legal witness, so they distinguish numeric magnitude from allocation size.
for stem,name,data,expected in [
('release-max-zero','SequencingWithReleaseTimesAndDeadlines',{'lengths':[0],'release_times':[2**63-1],'deadlines':[2**63-1]},'Or(true)'),
('release-max-positive','SequencingWithReleaseTimesAndDeadlines',{'lengths':[2**63-1],'release_times':[0],'deadlines':[2**63-1]},'Or(true)'),
('supersequence-large-alphabet-empty','ShortestCommonSupersequence',{'alphabet_size':2**64-3,'strings':[[],[]]},'Min(0)'),
]:
source={'type':name,'variant':{},'data':data};f=out/(stem+'.json');f.write_text(json.dumps(source))
r=run(['reduce',str(f),'--via',str(out/(name+'-route.json'))]);assert r['returncode']==0,r
bf=out/(stem+'-bundle.json');bf.write_text(r['stdout']);rows.append(r)
for path in [f,bf]:
r=run(['solve',str(path),'--solver','brute-force']);assert r['returncode']==0 and json.loads(r['stdout'])['evaluation']==expected,r;rows.append(r)
(out/'fixed-boundary-results.json').write_text(json.dumps(rows,indent=2))
print('PASS two typed failures and three extreme source/target round trips')reviewed-file-hashes.json{
"docs/paper/reductions.typ": "5f635066a29bba7056abd2bdd8877480e018d3a8cd6b37e8fcc5d16bc8d979d4",
"src/rules/betweenness_ilp.rs": "3247d7aed82b26bb4d1c3ab96fb1ab828ad8cd5ce696414b1ff50a9dde5e08c4",
"src/rules/betweenness_qubo.rs": "a1ff9b89c61148305464279340196ee38aad85d5aabc5f61bda842596fc9c006",
"src/rules/dynamicstorageallocation_qubo.rs": "1d9c7909c86a13525490a5c70a3e5f548efdebd7366319d3c1ba3c4d44817c9a",
"src/rules/feasibleregisterassignment_ilp.rs": "5647292f1287c51c472faca6d3e2c9c2cbcb5a1613ee3d65f771d60d0c5e0a23",
"src/rules/feasibleregisterassignment_qubo.rs": "306bef0fe9767551d3532ebc582a11a575af5a9dbe7c791d79bf13cd260508c5",
"src/rules/minimumtardinesssequencing_ilp.rs": "2c0a1ebe65a3dd6a9993a5c5110a687c23d6fa0154abe633c8dac3e6faf2dcd2",
"src/rules/minimumtardinesssequencingweighted_qubo.rs": "1d5deb0af928cc4d1ff3742a541da8fabedf7b1263a8bcdb54f32d30ba758524",
"src/rules/mod.rs": "bea5a2102097b072b77e0b24b34025ba86441ad40e4542275623fe5977fb7d07",
"src/rules/sequencingtominimizeweightedtardiness_ilp.rs": "4e2b16004e2e55d89806742d633f0786cdaa1c7a917b8c89944b6ef4a4423385",
"src/rules/sequencingtominimizeweightedtardiness_qubo.rs": "e98fcd61aac02340cb2168ccf2b15eb51c450afc0c8a1f6eb0b0196162edf25f",
"src/rules/sequencingwithreleasetimesanddeadlines_qubo.rs": "c39d073f53742ba7c7d59dda385781a370799ba581f33259f8c3f0c61596279d",
"src/rules/shortestcommonsupersequence_ilp.rs": "9c0a6e57befae85ed43f416d949429f7e25927b62f4e5ef5df31399715729f24",
"src/rules/shortestcommonsupersequence_qubo.rs": "09c47f81ab213d97452b331dfc3c52a0bad39eed8e716094324964ed7d92995b",
"src/rules/start_time_qubo.rs": "5b8a80355dea1710d253e41e6ac709e243187f966dd5a0b347b5762c46020a2d",
"src/unit_tests/rules/direct_qubo_conditional.rs": "d4ec0d5407ff767eed3ac04c446b8926e872bfb8c4869bc99f6e46f2eb0680d3"
} |
Open
57 tasks
Collaborator
Author
Follow-up: timeout diagnosis on small source instancesThe source instances are small. Calling the incomplete validation “larger-instance” verification without measuring source dimensions was misleading. The original 3-second, one-worker CP-SAT budget and its default Boolean linearization were a validation shortcut; the timeout totals alone did not establish intrinsic problem size or hardness. No reduction code changed from Actual sizes of the 20 original timeouts
Controlled diagnosisThe original runner translates every QUBO product into a Boolean multiplication equality, then submits one weighted energy inequality (decision) or the expanded energy objective (optimization). It provides no scheduling, one-hot or subsequence constraints separately. Consequently the solver has to recover that structure from penalties. This is a raw-target check, not a source-model solve. CP-SAT defaults to
The first NO schedule explored 5.7 million branches in 30 seconds with the original settings; level 2 proved NO in 3.2 seconds. The first SCS case remained at length 5 after 30 seconds although its optimum is 4; level 2 proved length 4 in 0.12 seconds. These experiments establish a configuration effect, not merely a larger wall-clock budget. The remaining difficulty is not just configuration. Generic product linearization has a weak relaxation. In the first scheduling case, assigning every original bit 0.5 and every product auxiliary 0 satisfies the edgewise continuous product inequalities and gives energy -23,616.5, below threshold -3,263, despite selecting no integral schedule. For the first SCS instance, a feasible edgewise fractional point has energy -192 while the integer optimum is -86. LP cuts help but do not eliminate this gap automatically. This explains why encoding size and coefficient savings need not translate to faster generic solver performance. Follow-up resultWith
Combined with the original 50 completed raw solves, 66/70 distinct selected targets now have completed raw-target validation under the documented mixed configurations. This does not mean all 700 corpus instances have raw solves; the 700-instance coefficient/oracle evidence remains separate. The original 3-second results remain preserved as historical measurements. The diagnostic 30-second runs sometimes return FEASIBLE incumbents with nonoptimal cost or violated source penalties. Those are not correctness counterexamples or completed optimum checks. The objective interval correctly rejects penalty-violating incumbents, and only OPTIMAL/INFEASIBLE results count toward completed validation. All20 follow-up results[
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-020-chain-3216513949.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.690958980470896,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "INFEASIBLE",
"elapsed": 3.2181799589889124,
"branches": 94371,
"conflicts": 7603,
"objective": 0.0,
"best_bound": 0.0,
"matches_truth": true
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-031-sparse_constraints-3217665968.json",
"kind": "weighted",
"expected": true,
"source_ms": 6.568624987266958,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.10750895796809345,
"branches": 12286,
"conflicts": 289,
"objective": 0.0,
"best_bound": 0.0,
"recovered": true,
"matches_truth": true,
"witness_value": "Or(true)"
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-042-dense_constraints-3218817987.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.794333923608065,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "INFEASIBLE",
"elapsed": 3.9159795409068465,
"branches": 97786,
"conflicts": 9769,
"objective": 0.0,
"best_bound": 0.0,
"matches_truth": true
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-053-antichain-3219970006.json",
"kind": "weighted",
"expected": true,
"source_ms": 6.6720000468194485,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 3.2805030000163242,
"branches": 63031,
"conflicts": 7863,
"objective": 0.0,
"best_bound": 0.0,
"recovered": true,
"matches_truth": true,
"witness_value": "Or(true)"
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-064-loose_bounds-3221122025.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.986957974731922,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "INFEASIBLE",
"elapsed": 4.609663333976641,
"branches": 103630,
"conflicts": 11970,
"objective": 0.0,
"best_bound": 0.0,
"matches_truth": true
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-075-tight_bounds-3222274044.json",
"kind": "weighted",
"expected": true,
"source_ms": 6.7200419725850224,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 2.325153624988161,
"branches": 40621,
"conflicts": 6834,
"objective": 0.0,
"best_bound": 0.0,
"recovered": true,
"matches_truth": true,
"witness_value": "Or(true)"
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-009-uniform_small-3215361930.json",
"kind": "weighted",
"expected": true,
"source_ms": 6.90075010061264,
"source_evaluation": "Or(true)",
"qubo_variables": 149,
"couplings": 5624,
"solver_variables": 5773,
"linearization_level": 2,
"limit": 15,
"status": "UNKNOWN",
"elapsed": 14.999945124960504,
"branches": 141690,
"conflicts": 13566,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/special-00-minimum_legal-3215419372.json",
"kind": "weighted",
"expected": true,
"source_ms": 7.192625082097948,
"source_evaluation": "Or(true)",
"qubo_variables": 153,
"couplings": 5938,
"solver_variables": 6091,
"linearization_level": 2,
"limit": 15,
"status": "UNKNOWN",
"elapsed": 15.001240083947778,
"branches": 208890,
"conflicts": 16661,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-071-tight_bounds-3221855128.json",
"kind": "weighted",
"expected": true,
"source_ms": 7.973707979544997,
"source_evaluation": "Or(true)",
"qubo_variables": 221,
"couplings": 12710,
"solver_variables": 12931,
"linearization_level": 2,
"limit": 15,
"status": "UNKNOWN",
"elapsed": 15.001491708913818,
"branches": 139248,
"conflicts": 7756,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-082-planted_witness-3223007147.json",
"kind": "weighted",
"expected": false,
"source_ms": 8.79808294121176,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 229,
"couplings": 13606,
"solver_variables": 13835,
"linearization_level": 2,
"limit": 15,
"status": "UNKNOWN",
"elapsed": 15.000903374981135,
"branches": 143763,
"conflicts": 7481,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/ShortestCommonSupersequence/random-033-sparse_constraints-2511684564.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 8.677667006850243,
"source_evaluation": "Min(4)",
"qubo_variables": 54,
"couplings": 233,
"solver_variables": 287,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.12137058400548995,
"branches": 13388,
"conflicts": 580,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-057-antichain-2514198060.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 8.051666081883013,
"source_evaluation": "Min(4)",
"qubo_variables": 54,
"couplings": 233,
"solver_variables": 287,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.08509587496519089,
"branches": 15517,
"conflicts": 278,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-053-antichain-2513779144.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 9.926582919433713,
"source_evaluation": "Min(4)",
"qubo_variables": 60,
"couplings": 251,
"solver_variables": 311,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.28737779101356864,
"branches": 41894,
"conflicts": 1159,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-077-tight_bounds-2516292640.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 9.665334015153348,
"source_evaluation": "Min(4)",
"qubo_variables": 60,
"couplings": 251,
"solver_variables": 311,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.10681441600900143,
"branches": 17244,
"conflicts": 398,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-004-uniform_small-2508647423.json",
"kind": "supersequence",
"expected": 5,
"source_ms": 13.239374966360629,
"source_evaluation": "Min(5)",
"qubo_variables": 66,
"couplings": 275,
"solver_variables": 341,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.3035106670577079,
"branches": 31215,
"conflicts": 1326,
"objective": -85.0,
"best_bound": -85.0,
"recovered": 5,
"matches_truth": true,
"witness_value": "Min(5)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-013-bimodal-2509589984.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 11.273249983787537,
"source_evaluation": "Min(4)",
"qubo_variables": 66,
"couplings": 275,
"solver_variables": 341,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 0.27253183303400874,
"branches": 34840,
"conflicts": 1058,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-015-bimodal-2509799442.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 9.570667054504156,
"source_evaluation": "Min(4)",
"qubo_variables": 88,
"couplings": 535,
"solver_variables": 623,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 4.993010708014481,
"branches": 308645,
"conflicts": 12832,
"objective": -148.0,
"best_bound": -148.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-024-chain-2510742003.json",
"kind": "supersequence",
"expected": 5,
"source_ms": 9.869667002931237,
"source_evaluation": "Min(5)",
"qubo_variables": 88,
"couplings": 535,
"solver_variables": 623,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 5.95909512497019,
"branches": 349101,
"conflicts": 12532,
"objective": -147.0,
"best_bound": -147.0,
"recovered": 5,
"matches_truth": true,
"witness_value": "Min(5)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-044-dense_constraints-2512836583.json",
"kind": "supersequence",
"expected": 5,
"source_ms": 27.694374904967844,
"source_evaluation": "Min(5)",
"qubo_variables": 96,
"couplings": 559,
"solver_variables": 655,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 7.328958416939713,
"branches": 500737,
"conflicts": 11202,
"objective": -147.0,
"best_bound": -147.0,
"recovered": 5,
"matches_truth": true,
"witness_value": "Min(5)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-064-loose_bounds-2514931163.json",
"kind": "supersequence",
"expected": 6,
"source_ms": 116.24879098962992,
"source_evaluation": "Min(6)",
"qubo_variables": 104,
"couplings": 591,
"solver_variables": 695,
"linearization_level": 2,
"limit": 15,
"status": "OPTIMAL",
"elapsed": 7.913881457992829,
"branches": 415876,
"conflicts": 14393,
"objective": -146.0,
"best_bound": -146.0,
"recovered": 6,
"matches_truth": true,
"witness_value": "Min(6)"
}
]Controlled comparison results[
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-020-chain-3216513949.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.92950002849102,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 1,
"limit": 3,
"status": "UNKNOWN",
"elapsed": 3.000890624942258,
"branches": 515733,
"conflicts": 218398,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-020-chain-3216513949.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.92950002849102,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 1,
"limit": 30,
"status": "UNKNOWN",
"elapsed": 30.00001149997115,
"branches": 5718493,
"conflicts": 2333047,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-020-chain-3216513949.json",
"kind": "weighted",
"expected": false,
"source_ms": 6.92950002849102,
"source_evaluation": {
"problem": "SequencingToMinimizeWeightedTardiness",
"solver": {
"kind": "brute-force"
},
"status": "infeasible"
},
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 10,
"status": "INFEASIBLE",
"elapsed": 3.2018809160217643,
"branches": 94371,
"conflicts": 7603,
"objective": 0.0,
"best_bound": 0.0,
"matches_truth": true
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-031-sparse_constraints-3217665968.json",
"kind": "weighted",
"expected": true,
"source_ms": 7.134500076062977,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 1,
"limit": 3,
"status": "UNKNOWN",
"elapsed": 3.0001733329845592,
"branches": 390991,
"conflicts": 225261,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-031-sparse_constraints-3217665968.json",
"kind": "weighted",
"expected": true,
"source_ms": 7.134500076062977,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 1,
"limit": 30,
"status": "UNKNOWN",
"elapsed": 30.00425445800647,
"branches": 6435723,
"conflicts": 2289952,
"objective": 0.0,
"best_bound": 0.0
},
{
"instance": "instances/SequencingToMinimizeWeightedTardiness/random-031-sparse_constraints-3217665968.json",
"kind": "weighted",
"expected": true,
"source_ms": 7.134500076062977,
"source_evaluation": "Or(true)",
"qubo_variables": 73,
"couplings": 1246,
"solver_variables": 1319,
"linearization_level": 2,
"limit": 10,
"status": "OPTIMAL",
"elapsed": 0.10664054099470377,
"branches": 12286,
"conflicts": 289,
"objective": 0.0,
"best_bound": 0.0,
"recovered": true,
"matches_truth": true,
"witness_value": "Or(true)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-033-sparse_constraints-2511684564.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 7.073207991197705,
"source_evaluation": "Min(4)",
"qubo_variables": 54,
"couplings": 233,
"solver_variables": 287,
"linearization_level": 1,
"limit": 3,
"status": "FEASIBLE",
"elapsed": 3.000163041986525,
"branches": 418768,
"conflicts": 274241,
"objective": -85.0,
"best_bound": -384.0,
"recovered": 5,
"matches_truth": false,
"witness_value": "Min(5)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-033-sparse_constraints-2511684564.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 7.073207991197705,
"source_evaluation": "Min(4)",
"qubo_variables": 54,
"couplings": 233,
"solver_variables": 287,
"linearization_level": 1,
"limit": 30,
"status": "FEASIBLE",
"elapsed": 30.0001666250173,
"branches": 4290273,
"conflicts": 2704701,
"objective": -85.0,
"best_bound": -384.0,
"recovered": 5,
"matches_truth": false,
"witness_value": "Min(5)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-033-sparse_constraints-2511684564.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 7.073207991197705,
"source_evaluation": "Min(4)",
"qubo_variables": 54,
"couplings": 233,
"solver_variables": 287,
"linearization_level": 2,
"limit": 10,
"status": "OPTIMAL",
"elapsed": 0.12119883298873901,
"branches": 13388,
"conflicts": 580,
"objective": -86.0,
"best_bound": -86.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
},
{
"instance": "instances/ShortestCommonSupersequence/random-015-bimodal-2509799442.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 8.33304098341614,
"source_evaluation": "Min(4)",
"qubo_variables": 88,
"couplings": 535,
"solver_variables": 623,
"linearization_level": 1,
"limit": 3,
"status": "FEASIBLE",
"elapsed": 3.0009289169684052,
"branches": 322450,
"conflicts": 220371,
"objective": -122.0,
"best_bound": -800.0,
"recovered": null,
"matches_truth": false,
"incumbent_extraction_error": "Error: ShortestCommonSupersequence -> QUBO: QUBO penalties do not certify a feasible source assignment\n"
},
{
"instance": "instances/ShortestCommonSupersequence/random-015-bimodal-2509799442.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 8.33304098341614,
"source_evaluation": "Min(4)",
"qubo_variables": 88,
"couplings": 535,
"solver_variables": 623,
"linearization_level": 1,
"limit": 30,
"status": "FEASIBLE",
"elapsed": 30.000105915940367,
"branches": 3169142,
"conflicts": 2184947,
"objective": -136.0,
"best_bound": -800.0,
"recovered": null,
"matches_truth": false,
"incumbent_extraction_error": "Error: ShortestCommonSupersequence -> QUBO: QUBO penalties do not certify a feasible source assignment\n"
},
{
"instance": "instances/ShortestCommonSupersequence/random-015-bimodal-2509799442.json",
"kind": "supersequence",
"expected": 4,
"source_ms": 8.33304098341614,
"source_evaluation": "Min(4)",
"qubo_variables": 88,
"couplings": 535,
"solver_variables": 623,
"linearization_level": 2,
"limit": 10,
"status": "OPTIMAL",
"elapsed": 4.983681375044398,
"branches": 308645,
"conflicts": 12832,
"objective": -148.0,
"best_bound": -148.0,
"recovered": 4,
"matches_truth": true,
"witness_value": "Min(4)"
}
]Diagnostic/reproduction scriptimport corpus as c
from ortools.sat.python import cp_model
from ortools.linear_solver import pywraplp
import json,time,sys
from pathlib import Path
s=Path(__file__).parent;o=s/'timeout-analysis'
old=[json.loads(x) for x in (s/'raw-targets/results.jsonl').read_text().splitlines() if json.loads(x)['correct'] is None]
selected=[old[0],old[1],old[10],old[16]]
if len(sys.argv)>1 and sys.argv[1]=='all':selected=old
results_file=o/('results-all.json' if len(sys.argv)>1 else 'results.json')
rows=json.loads(results_file.read_text()) if results_file.exists() else []
for idx,r in enumerate(selected):
b=c.cli(['reduce',str(c.root/r['instance']),'--via',str(c.routes[r['kind']])]);td=b['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data'];N=q['num_vars'];edges=sum(i!=j for i,j,v in q['entries'])
(o/(Path(r['instance']).stem+'-bundle.json')).write_text(json.dumps(b))
t=time.perf_counter();source=c.cli(['solve',str(c.root/r['instance']),'--solver','brute-force']);source_ms=(time.perf_counter()-t)*1000
configs=[(1,3),(1,30),(2,10)] if len(sys.argv)==1 else [(2,15)]
for level,limit in configs:
if any(x['instance']==r['instance'] and x['linearization_level']==level and x['limit']==limit for x in rows):continue
m=cp_model.CpModel();xs=[m.new_bool_var('x'+str(i)) for i in range(N)];terms=[]
for i,j,v in q['entries']:
if i==j:terms.append(v*xs[i])
else:
y=m.new_bool_var(f'y{i}_{j}');m.add_multiplication_equality(y,[xs[i],xs[j]]);terms.append(v*y)
if decision:m.add(sum(terms)<=td['data']['bound'])
else:m.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=limit;solver.parameters.linearization_level=level;solver.parameters.log_search_progress=True;solver.parameters.log_to_stdout=False
logs=[];solver.log_callback=logs.append;t=time.perf_counter();status=solver.solve(m)
row=dict(instance=r['instance'],kind=r['kind'],expected=r['expected'],source_ms=source_ms,source_evaluation=source.get('evaluation',source),qubo_variables=N,couplings=edges,solver_variables=len(m.proto.variables),linearization_level=level,limit=limit,status=solver.status_name(status),elapsed=time.perf_counter()-t,branches=solver.num_branches,conflicts=solver.num_conflicts,objective=solver.objective_value,best_bound=solver.best_objective_bound)
if status in (cp_model.OPTIMAL,cp_model.FEASIBLE):
bits=[bool(solver.value(x)) for x in xs];E=sum(v*bits[i]*bits[j] for i,j,v in q['entries']);value=c.cli(['extract','-','--value='+json.dumps(True if decision else E)],b);row['recovered']=value['value'];row['matches_truth']=value['value']==r['expected']
try:
ex=c.cli(['extract','-','--config',json.dumps(bits)],b);row['witness_value']=ex['evaluation']
except RuntimeError as error:
if status==cp_model.OPTIMAL:raise
row['incumbent_extraction_error']=str(error)
elif status==cp_model.INFEASIBLE:row['matches_truth']=decision and r['expected'] is False
(o/(Path(r['instance']).stem+f'-L{level}-{limit}.log')).write_text('\n'.join(logs))
rows.append(row);(o/('results-all.json' if len(sys.argv)>1 else 'results.json')).write_text(json.dumps(rows,indent=2));print(json.dumps(row),flush=True)Upstream chains and integrityThe two upstream timeouts likewise start from small sources: 3-SAT has three variables and two clauses; SetSplitting has five elements and four subsets. Their targets expand to 435 QUBO bits/12,615 solver Booleans and 45 QUBO bits/405 solver Booleans respectively. Both remained UNKNOWN at 15 seconds with Boolean LP enabled. Their earlier oracle-witness checks are still distinct from raw target completion. All 32,372 corpus file hashes remain unchanged after this investigation. Scripts/results are outside the repository and corpus. The working tree and reduction commit remain unchanged. No source hints, corpus witnesses, source-specific constraints, or expected objective cutoffs were supplied to these raw target solvers. Expected corpus values are consulted only after each solve. Upstream raw follow-up[
{
"chain": "KSatisfiability_K3-FeasibleRegisterAssignment",
"variables": 435,
"solver_variables": 12615,
"status": "UNKNOWN",
"seconds": 15.003514750045724
},
{
"chain": "SetSplitting-Betweenness",
"variables": 45,
"solver_variables": 405,
"status": "UNKNOWN",
"seconds": 15.00022237491794
}
] |
Collaborator
Author
Current Phase 3 scope and verification certificateVerified commit: Four retained rules: MinimumTardinessSequencing, SequencingWithReleaseTimesAndDeadlines, DynamicStorageAllocation, ShortestCommonSupersequence. All target exact i64 QUBO/DecisionQUBO endpoints as documented in the PR. Three removed rules: SequencingToMinimizeWeightedTardiness (four unresolved five-task corpus targets); FeasibleRegisterAssignment (unresolved canonical 3SAT upstream chain); Betweenness (unresolved canonical SetSplitting upstream chain). Their new implementations, graph registrations, canonical examples, tests and manual entries are removed. Existing models and ILP routes remain. The three ILP files are byte-identical to the Phase 2 base. Timeout diagnosis and historical evidence remain available; passing oracle checks did not meet the revised shipping condition.
Verified commit: ReproductionRun every script below from a scratch directory outside both repository and corpus, with OR-Tools 9.15.6755 in a scratch environment. Corpus is Commands: corpus/summary.json{
"total": 400,
"correct": 400,
"coverage": {
"coefficient_equivalence_and_oracle_witness_value_recovery": 316,
"coefficient_equivalence_with_independent_no_truth": 84
},
"by_source": {
"MinimumTardinessSequencing/i64": {
"total": 100,
"correct": 100
},
"DynamicStorageAllocation": {
"total": 100,
"correct": 100
},
"ShortestCommonSupersequence": {
"total": 100,
"correct": 100
},
"SequencingWithReleaseTimesAndDeadlines": {
"total": 100,
"correct": 100
}
}
}raw-targets/summary.json{
"total": 40,
"passed": 40,
"timeouts": 0,
"failures": 0,
"by_kind": {
"tardiness": {
"True": 10
},
"release": {
"True": 10
},
"storage": {
"True": 10
},
"supersequence": {
"True": 10
}
}
}raw-targets/results.jsonl{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-041-dense_constraints-804800914.json", "expected": 0, "status": "OPTIMAL", "variables": 16, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12959158304147422}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-068-loose_bounds-807628597.json", "expected": 0, "status": "OPTIMAL", "variables": 19, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.11679933394771069}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-070-tight_bounds-807838055.json", "expected": 0, "status": "OPTIMAL", "variables": 19, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.11651637498289347}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-074-tight_bounds-808256971.json", "expected": 0, "status": "OPTIMAL", "variables": 19, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.11611391697078943}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-003-uniform_small-800821212.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12193804094567895}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-005-uniform_small-801030670.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12317233299836516}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-010-bimodal-801554315.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.122720165993087}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-014-bimodal-801973231.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12181629100814462}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-018-bimodal-802392147.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12149887497071177}
{"kind": "tardiness", "source": "MinimumTardinessSequencing/i64", "instance": "instances/MinimumTardinessSequencing-i64/random-022-chain-802811063.json", "expected": 0, "status": "OPTIMAL", "variables": 25, "correct": true, "aggregate": {"problem": "MinimumTardinessSequencing", "value": 0}, "seconds": 0.12477929191663861}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-057-antichain-3837941541.json", "expected": false, "status": "INFEASIBLE", "variables": 5, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07490483298897743}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-061-loose_bounds-3838360457.json", "expected": false, "status": "INFEASIBLE", "variables": 5, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07428570801857859}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-000-uniform_small-3831971988.json", "expected": true, "status": "OPTIMAL", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": true}, "seconds": 0.11221604107413441}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-007-uniform_small-3832705091.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07483491697348654}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-017-bimodal-3833752381.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07373958302196115}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-019-bimodal-3833961839.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07311054202727973}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-047-dense_constraints-3836894251.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07354804105125368}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-053-antichain-3837522625.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07490712497383356}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-063-loose_bounds-3838569915.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.07529691699892282}
{"kind": "release", "source": "SequencingWithReleaseTimesAndDeadlines", "instance": "instances/SequencingWithReleaseTimesAndDeadlines/random-069-loose_bounds-3839198289.json", "expected": false, "status": "INFEASIBLE", "variables": 6, "correct": true, "aggregate": {"problem": "SequencingWithReleaseTimesAndDeadlines", "value": false}, "seconds": 0.08168766694143414}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-003-uniform_small-268526178.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.0792880830122158}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-012-bimodal-269468739.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07570504199247807}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-021-chain-270411300.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07468866696581244}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-028-chain-271244394.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07716287497896701}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-030-sparse_constraints-271353861.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.0752135420916602}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-039-sparse_constraints-272296422.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07507487502880394}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-048-dense_constraints-273238983.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07541216700337827}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-057-antichain-274181544.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.0764838750474155}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-075-tight_bounds-276066666.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07556179095990956}
{"kind": "storage", "source": "DynamicStorageAllocation", "instance": "instances/DynamicStorageAllocation/random-084-planted_witness-277009227.json", "expected": false, "status": "INFEASIBLE", "variables": 9, "correct": true, "aggregate": {"problem": "DynamicStorageAllocation", "value": false}, "seconds": 0.07528629200533032}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-033-sparse_constraints-2511684564.json", "expected": 4, "status": "OPTIMAL", "variables": 54, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 0.23679174995049834}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-057-antichain-2514198060.json", "expected": 4, "status": "OPTIMAL", "variables": 54, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 0.19964870891999453}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-053-antichain-2513779144.json", "expected": 4, "status": "OPTIMAL", "variables": 60, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 0.40388462506234646}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-077-tight_bounds-2516292640.json", "expected": 4, "status": "OPTIMAL", "variables": 60, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 0.22168800001963973}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-004-uniform_small-2508647423.json", "expected": 5, "status": "OPTIMAL", "variables": 66, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 5}, "seconds": 0.41959912492893636}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-013-bimodal-2509589984.json", "expected": 4, "status": "OPTIMAL", "variables": 66, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 0.3878918749978766}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-015-bimodal-2509799442.json", "expected": 4, "status": "OPTIMAL", "variables": 88, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 4}, "seconds": 5.146429458050989}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-024-chain-2510742003.json", "expected": 5, "status": "OPTIMAL", "variables": 88, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 5}, "seconds": 6.093389375018887}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-044-dense_constraints-2512836583.json", "expected": 5, "status": "OPTIMAL", "variables": 96, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 5}, "seconds": 7.491199917043559}
{"kind": "supersequence", "source": "ShortestCommonSupersequence", "instance": "instances/ShortestCommonSupersequence/random-064-loose_bounds-2514931163.json", "expected": 6, "status": "OPTIMAL", "variables": 104, "correct": true, "aggregate": {"problem": "ShortestCommonSupersequence", "value": 6}, "seconds": 8.071643666015007}
upstream/results.json[
{
"source": "ThreePartition",
"via": "SequencingWithReleaseTimesAndDeadlines",
"target": "DecisionQUBO/i64",
"composed": {
"fields": [
{
"field": "num_vars",
"formula": "-1 + num_elements + num_groups + (-1 + num_elements + num_groups) * (-1 + num_groups * (1 + bound))",
"relation": "upper_bound"
},
{
"field": "num_quadratic_terms",
"formula": "2 * (-1 + num_groups * (1 + bound)) * (-1 + num_elements + num_groups)^2 + (-1 + num_elements + num_groups)^2 * (-1 + num_groups * (1 + bound))^2 + (-1 + num_elements + num_groups)^2",
"relation": "upper_bound"
}
]
},
"variables": 163,
"status": "OPTIMAL",
"correct": true,
"evaluation": "Or(true)",
"aggregate": {
"problem": "ThreePartition",
"value": true
},
"seconds": 1.054056708002463
}
]coverage-summary.json{
"files": [
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/dynamicstorageallocation_qubo.rs",
"covered": 66,
"lines": 66,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/minimumtardinesssequencingweighted_qubo.rs",
"covered": 45,
"lines": 46,
"percent": 97.82608695652173,
"uncovered": [
56
]
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/sequencingwithreleasetimesanddeadlines_qubo.rs",
"covered": 50,
"lines": 50,
"percent": 100.0,
"uncovered": []
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/shortestcommonsupersequence_qubo.rs",
"covered": 81,
"lines": 82,
"percent": 98.78048780487805,
"uncovered": [
75
]
},
{
"file": "/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/src/rules/start_time_qubo.rs",
"covered": 77,
"lines": 79,
"percent": 97.46835443037975,
"uncovered": [
98,
99
]
}
],
"total_covered": 319,
"total_lines": 323,
"percentage": 98.76160990712074
}runner-hashes.json{
"constructor.py": "2bc03c07267f74742a7c70d6d1b7f6845dd519311e1d4608fc219481daea9393",
"corpus.py": "aa7ca9334f54350984a06a2e0d031db434b6600d519b2867b0642d672b50a36b",
"raw_targets.py": "4756dae138bc4824601bd72d9722520c02213dadb6cfcf3cdf42715dfd93b37f",
"upstream.py": "594b07df5683050d89ff91418cd52d5e79fd91d6599b59d74627721fdcb47073",
"cli_checks.py": "9ce6afae16ec23df68af9a9e601a22afda65831cdef4fe19779f82e507ec29d7"
}unchanged-production-hashes.json{
"src/rules/dynamicstorageallocation_qubo.rs": "1d9c7909c86a13525490a5c70a3e5f548efdebd7366319d3c1ba3c4d44817c9a",
"src/rules/minimumtardinesssequencingweighted_qubo.rs": "1d5deb0af928cc4d1ff3742a541da8fabedf7b1263a8bcdb54f32d30ba758524",
"src/rules/sequencingwithreleasetimesanddeadlines_qubo.rs": "c39d073f53742ba7c7d59dda385781a370799ba581f33259f8c3f0c61596279d",
"src/rules/shortestcommonsupersequence_qubo.rs": "09c47f81ab213d97452b331dfc3c52a0bad39eed8e716094324964ed7d92995b",
"src/rules/start_time_qubo.rs": "5b8a80355dea1710d253e41e6ac709e243187f966dd5a0b347b5762c46020a2d"
}Current runner: corpus.pyimport sys
sys.dont_write_bytecode=True
import json,subprocess,time,collections,concurrent.futures
from pathlib import Path
from constructor import build,CASES
base=Path(__file__).parent;root=Path('/Users/xiweipan/Codes/pred-validation-corpus');out=base/'corpus';out.mkdir(exist_ok=True)
pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--quiet','--json'],input=json.dumps(data) if data is not None else None,capture_output=True,text=True,timeout=30)
if p.returncode:raise RuntimeError(p.stderr)
return json.loads(p.stdout)
def parse(v):
if isinstance(v,str):
v=v[v.index('(')+1:-1]
if v in ('None','none'):return None
return json.loads(v)
return v
routes={}
for kind,(name,_) in CASES.items():
target='QUBO/i64' if kind in ('tardiness','supersequence') else 'DecisionQUBO/i64'
route=next(p for p in cli(['path',name,target,'--limit','all'])['paths'] if p['steps']==1);f=out/(kind+'-route.json');f.write_text(json.dumps(route));routes[kind]=f
truth=collections.defaultdict(list)
for f in (root/'ground-truth').rglob('*.jsonl'):
for line in f.read_text().splitlines():
t=json.loads(line)
if t['problem'] in [v[0] for v in CASES.values()]:truth[t['problem']].append(t)
def schema(kind,d):
d=dict(d)
if kind=='register':d={'n':d['num_vertices'],'arcs':d['arcs'],'registers':d['assignment']}
if kind=='betweenness':d={'n':d['num_elements'],'triples':d['triples']}
return d
def lift(kind,d,w,N):
bits=[False]*N
if kind in ('register','betweenness'):
return [w.index(i)<w.index(j) for i in range(d['n']) for j in range(i+1,d['n'])]
if kind=='supersequence':
L=sum(map(len,d['strings']));a=d['alphabet_size'];k=a+1
for p in range(L):bits[p*k+(w[p] if p<len(w) else a)]=True
gc=0
for s in d['strings']:
start=0
for ch in s:
p=w.index(ch,start);bits[L*k+gc*L+p]=True;gc+=1;start=p+1
return bits
if kind=='storage':counts=[d['memory_size']-s+1 for _,_,s in d['items']];choices=w
else:
H=sum(d['lengths']);counts=[max(0,d['deadlines'][i]-d['release_times'][i]-p+1) if kind=='release' else H-p+1 for i,p in enumerate(d['lengths'])]
if kind=='release':choices=[s-r for s,r in zip(w,d['release_times'])]
else:
order=w['order'] if kind=='weighted' else w;choices=[0]*len(order);elapsed=0
for i in order:choices[i]=elapsed;elapsed+=d['lengths'][i]
offset=0
for count,choice in zip(counts,choices):bits[offset+choice]=True;offset+=count
return bits
def verify(kind,t):
r=dict(kind=kind,source=t['problem'],instance=t['instance'],expected=t['value']);start=time.monotonic()
try:
data=json.loads((root/t['instance']).read_text())['data'];d=schema(kind,data);N,e,c=build(kind,d)
bundle=cli(['reduce',str(root/t['instance']),'--via',str(routes[kind])]);td=bundle['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data']
assert N==q['num_vars'] and sorted([i,j,v] for (i,j),v in e.items())==q['entries'], 'polynomial mismatch'
if decision:
cap=0
if kind=='weighted':H=sum(d['lengths']);cap=min(d['bound'],sum(d['weights'][i]*max(0,t+p-d['deadlines'][i]) for i,p in enumerate(d['lengths']) for t in range(H-p+1)))
assert td['data']['bound']==cap-c
no=t['status'] in ('unsatisfiable','infeasible')
if no:r.update(correct=True,coverage='coefficient_equivalence_with_independent_no_truth')
else:
bits=lift(kind,d,t['witness'],N);E=sum(v*bits[i]*bits[j] for (i,j),v in e.items())
assert E<=td['data']['bound'] if decision else E+c==t['value']
x=cli(['extract','-','--config',json.dumps(bits)],bundle);assert parse(x['evaluation'])==t['value'],x
ev=cli(['evaluate',str(root/t['instance']),'--config',json.dumps(x['solution'])]);assert parse(ev['result'])==t['value']
value=cli(['extract','-','--value='+json.dumps(True if decision else E)],bundle);assert value['value']==t['value'],value
r.update(correct=True,coverage='coefficient_equivalence_and_oracle_witness_value_recovery')
r.update(variables=N,couplings=sum(i!=j for i,j in e),max_coefficient=max(map(abs,e.values()),default=0))
except Exception as ex:r.update(correct=False,error=str(ex))
r['seconds']=time.monotonic()-start;return r
if __name__=='__main__':
work=[(kind,t) for kind,(name,_) in CASES.items() for t in truth[name]];assert len(work)==400,[(k,len(truth[n])) for k,(n,_) in CASES.items()]
rows=[]
with (out/'results.jsonl').open('w') as f,concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
for r in pool.map(lambda x:verify(*x),work):
rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
if not r['correct'] or len(rows)%100==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['kind'])),flush=True)
summary=dict(total=len(rows),correct=sum(r['correct'] for r in rows),coverage=dict(collections.Counter(r.get('coverage','failure') for r in rows)),by_source={n:dict(total=sum(r['source']==n for r in rows),correct=sum(r['source']==n and r['correct'] for r in rows)) for n in truth})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary))Current runner: raw_targets.pyimport corpus as c
from ortools.sat.python import cp_model
import json,time,collections
from pathlib import Path
base=Path(__file__).parent;out=base/'raw-targets';out.mkdir(exist_ok=True)
def verify(kind,t):
r=dict(kind=kind,source=t['problem'],instance=t['instance'],expected=t['value']);start=time.monotonic()
try:
b=c.cli(['reduce',str(c.root/t['instance']),'--via',str(c.routes[kind])]);td=b['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data']
m=cp_model.CpModel();xs=[m.new_bool_var('x'+str(i)) for i in range(q['num_vars'])];terms=[]
for i,j,v in q['entries']:
if i==j:terms.append(v*xs[i])
else:y=m.new_bool_var(f'y{i}_{j}');m.add_multiplication_equality(y,[xs[i],xs[j]]);terms.append(v*y)
if decision:m.add(sum(terms)<=td['data']['bound'])
else:m.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=15;solver.parameters.linearization_level=2;status=solver.solve(m);r.update(status=solver.status_name(status),variables=q['num_vars'])
if status not in (cp_model.OPTIMAL,cp_model.INFEASIBLE):r.update(correct=None,limitation='raw target solve timeout');return r
no=t['status'] in ('infeasible','unsatisfiable')
if status==cp_model.INFEASIBLE:
assert decision and no;value=c.cli(['extract','-','--value=false'],b);assert value['value']==False
else:
bits=[bool(solver.value(x)) for x in xs];E=sum(v*bits[i]*bits[j] for i,j,v in q['entries']);value=c.cli(['extract','-','--value='+json.dumps(True if decision else E)],b);assert value['value']==t['value'],value
if not no:
ex=c.cli(['extract','-','--config',json.dumps(bits)],b);assert c.parse(ex['evaluation'])==t['value']
else:
try:c.cli(['extract','-','--config',json.dumps(bits)],b)
except RuntimeError:pass
else:raise AssertionError('invalid optimum decoded')
r.update(correct=True,aggregate=value)
except Exception as ex:r.update(correct=False,error=str(ex))
r['seconds']=time.monotonic()-start;return r
def size(kind,t):
d=c.schema(kind,json.loads((c.root/t['instance']).read_text())['data'])
if kind in ('register','betweenness'):return d['n']*(d['n']-1)//2
if kind=='supersequence':L=sum(map(len,d['strings']));return L*(L+d['alphabet_size']+1)
if kind=='storage':return sum(d['memory_size']-s+1 for _,_,s in d['items'])
if kind=='release':return sum(max(0,e-r-p+1) for e,r,p in zip(d['deadlines'],d['release_times'],d['lengths']))
H=sum(d['lengths']);return sum(H-p+1 for p in d['lengths'])
rows=[]
with (out/'results.jsonl').open('w') as f:
for kind,(name,_) in c.CASES.items():
for t in sorted(c.truth[name],key=lambda t:size(kind,t))[:10]:
r=verify(kind,t);rows.append(r);f.write(json.dumps(r)+'\n');f.flush()
print(kind,collections.Counter(str(r['correct']) for r in rows if r['kind']==kind),flush=True)
summary=dict(total=len(rows),passed=sum(r['correct'] is True for r in rows),timeouts=sum(r['correct'] is None for r in rows),failures=sum(r['correct'] is False for r in rows),by_kind={k:dict(collections.Counter(str(r['correct']) for r in rows if r['kind']==k)) for k in c.CASES})
(out/'summary.json').write_text(json.dumps(summary,indent=2));print(json.dumps(summary))Current runner: upstream.pyimport json,subprocess,time
from pathlib import Path
from ortools.sat.python import cp_model
base=Path(__file__).parent;out=base/'upstream';out.mkdir(exist_ok=True)
pred=Path('/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred')
def cli(args,data=None):
p=subprocess.run([str(pred),*args,'--quiet','--json'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=60)
assert p.returncode==0,p.stderr
return json.loads(p.stdout)
rows=[]
for a,b,target in [('ThreePartition','SequencingWithReleaseTimesAndDeadlines','DecisionQUBO/i64')]:
row=dict(source=a,via=b,target=target);label=a.replace('/','_')+'-'+b.replace('/','_');start=time.monotonic()
try:
source=cli(['create','--example',a,'--to',b]);f=out/(label+'.json');f.write_text(json.dumps(source))
paths=cli(['path',a,target,'--limit','all'])['paths'];route=next(p for p in paths if p['steps']==2 and p['path'][0]['to']['name']==b.split('/')[0]);rf=out/(label+'-route.json');rf.write_text(json.dumps(route));row['composed']=route['overall_parameters']
bundle=cli(['reduce',str(f),'--via',str(rf)]);(out/(label+'-bundle.json')).write_text(json.dumps(bundle));td=bundle['target'];decision=td['type']=='DecisionQUBO';q=td['data']['inner'] if decision else td['data'];row['variables']=q['num_vars']
model=cp_model.CpModel();xs=[model.new_bool_var('x'+str(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)
if decision:model.add(sum(terms)<=td['data']['bound'])
else:model.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.num_search_workers=1;solver.parameters.max_time_in_seconds=15;solver.parameters.linearization_level=2
status=solver.solve(model);row['status']=solver.status_name(status);assert status==cp_model.OPTIMAL,row['status']
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'])
extracted=cli(['extract','-','--config',json.dumps(bits)],bundle);aggregate=cli(['extract','-','--value='+json.dumps(True if decision else energy)],bundle)
direct=cli(['solve',str(f),'--solver','brute-force']);evaluated=cli(['evaluate',str(f),'--config',json.dumps(extracted['solution'])]);assert direct['evaluation']==evaluated['result'],(direct,evaluated)
row.update(correct=True,evaluation=evaluated['result'],aggregate=aggregate)
except Exception as e:row.update(correct=False,error=str(e),limitation='Raw target solve unavailable' if 'UNKNOWN' in str(e) else None)
row['seconds']=time.monotonic()-start;rows.append(row);(out/'results.json').write_text(json.dumps(rows,indent=2));print(json.dumps(row),flush=True)Current runner: cli_checks.pyimport json,subprocess,time,statistics
from pathlib import Path
from constructor import CASES,build
base=Path(__file__).parent;out=base/'cli';out.mkdir(exist_ok=True);pred='/Users/xiweipan/Codes/problem-reductions-worktrees/direct-qubo-phase3/target/debug/pred'
def cli(args,data=None):
p=subprocess.run([pred,*args,'--json','--quiet'],input=None if data is None else json.dumps(data),capture_output=True,text=True,timeout=30);assert p.returncode==0,p.stderr;return json.loads(p.stdout)
rows=[]
for kind,(name,d) in CASES.items():
target='QUBO/i64' if kind in ('tardiness','supersequence') else 'DecisionQUBO/i64'
source=cli(['create','--example',name,'--to',target]);f=out/(kind+'-source.json');f.write_text(json.dumps(source))
paths=cli(['path',name,target,'--limit','all']);route=next(p for p in paths['paths'] if p['steps']==1);rf=out/(kind+'-route.json');rf.write_text(json.dumps(route));ts=[]
for _ in range(3):
start=time.perf_counter();bundle=cli(['reduce',str(f),'--via',str(rf)]);ts.append((time.perf_counter()-start)*1000)
bf=out/(kind+'-bundle.json');bf.write_text(json.dumps(bundle))
solved=cli(['solve',str(bf),'--solver','brute-force']);direct=cli(['solve',str(f),'--solver','brute-force']);assert solved['evaluation']==direct['evaluation'],(solved,direct)
ev=cli(['evaluate',str(f),'--config',json.dumps(solved['solution'])]);assert ev['result']==direct['evaluation']
q=bundle['target']['data'];q=q.get('inner',q);N,e,c=build(kind,d);assert q['num_vars']==N and q['entries']==sorted([i,j,v] for (i,j),v in e.items())
row=dict(source=name,variables=N,couplings=sum(i!=j for i,j in e),max_coefficient=max(map(abs,e.values()),default=0),coefficient_bits=max(map(abs,e.values()),default=0).bit_length(),cli_ms=statistics.median(ts),composed=route['overall_parameters'],source_result=direct,recovered_result=solved)
rows.append(row);print(kind,row['variables'],row['couplings'],solved['evaluation'],flush=True)
(out/'results.json').write_text(json.dumps(rows,indent=2))Corpus integrity: |
Collaborator
Author
Agentic Review ReportFresh-context, read-only review of the final Phase 3 working diff against stacked base Structural and semantic reviewThe final scope has four direct rules: MinimumTardinessSequencing, SequencingWithReleaseTimesAndDeadlines, DynamicStorageAllocation, and ShortestCommonSupersequence. The direct weighted-tardiness, fixed-register, and Betweenness rules, registrations, examples, and theorems are removed. Their source models and existing ILP routes remain; the three affected ILP files exactly match the Phase 2 base. The two retained ILP changes only qualify otherwise-ambiguous trait methods. No generated exports, new dependencies, model-domain changes, or unrelated core changes appear. Read the retained constructors, extraction and aggregate mappings, source evaluators and domain checks, shared sparse builder and row decoder, registrations, tests, and manual changes. The proofs match the actual code: positive-duration schedules fill their horizon; release schedules correctly sort zero-duration jobs before positive jobs at a shared start; storage penalizes strict overlap in both time and address; and SCS enforces exact output/embedding choices, increasing embeddings, consistency, and contiguous padding. Invalid accepted source alphabet symbols force NO. Penalty separation and omitted-constant intervals protect witness and completed-value recovery. Checked arithmetic against accepted domains and allocation boundaries, including the conservative release-time source-finish bound and SCS row-byte-capacity guard. Canonical hand traces yield 11/7/6/10 variables respectively. The three available parameter transforms follow from full construction counts and are covered by registry-wide parameter validation; processing-bit-dependent MTS metadata is explicitly unavailable, with its pseudopolynomial mathematical bound documented. Quality and verificationThe retained native tests reuse independent source/target brute-force helpers, enumerate small target bitstrings, check every target optimum and recovered objective, reject malformed lengths, and cover empty, NO, cyclic/self-precedence, zero-duration, invalid-symbol, arithmetic, and allocation cases. The removal regression checks observable registry edges and preservation of the existing ILP routes. Historical constructor/proof-only adversary evidence remains useful for these unchanged retained polynomials, while its seven-rule totals must not be presented as fresh four-rule results. Feature testsUsing the final The installed registry confirms all three excluded direct QUBO/DecisionQUBO edges are absent and each existing ILP edge remains. Re-ran the earlier release-finish and SCS-allocation boundary reproductions: both exit with typed integer overflow, without a target. Three representable extreme source/target round trips also pass: maximum-i64 release with zero duration, maximum-i64 duration starting at zero, and empty SCS with alphabet Fresh scripts, inputs, outputs, and reviewed hashes are in Separately reviewed the coordinator's fresh retained-scope results: 400/400 corpus coefficient checks, of which 316 include oracle-witness/value recovery and 84 use independent NO truth; 40/40 selected raw targets completed correctly with zero timeouts under CP-SAT Boolean linearization level 2, one worker, no hints, and a 15-second budget; the retained ThreePartition → release/deadline → DecisionQUBO chain completed and recovered the correct witness/value. These are coordinator-run results, not additional reviewer runs. The coordinator reports 7,130 passing workspace tests/doctests, passing check/paper gates, and all 32,372 corpus file hashes unchanged. Final coverage is reported separately by the coordinator. FindingsFinal verdict: no unresolved Critical, Important, or Minor findings. The retained four-rule scope meets the requested timeout exclusion in the reviewed fresh samples. This review does not approve merging or change draft status. Skipped duplicate Rust builds and direct corpus access; full gate, coverage, and external-corpus results belong to the coordinator's evidence. No hardware embedding or annealer performance was checked. Numeric horizon/capacity expansion and finite test coverage remain limits. The reviewed file hashes were rechecked unchanged before committing as |
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 #1216: Add Phase 3 conditional direct QUBO reductions
Review date: 2026-10-29. Fresh-context read-only review of ecc0ad5ae72e9a19dc9ca1a69dcc700cd4f1bc1c...109985f4103d4c4785f60b8a34007580cd7f2434. Used the PR's own stack base, not origin/main. Local implementation evidence is diff-1216.patch; GitHub context is context-1216.txt in this directory.
Verdict: No new blocking finding in this diff. Hold stack integration until #1214 is fixed.
Structural and semantic review
Reviewed the four new encodings, StartChoices helper, source parameter support, registration, test changes, and manual proofs against the exact #1215 base.
For weighted MinimumTardinessSequencing, the horizon is the sum of positive job lengths. A feasible nonoverlapping assignment of all jobs fills that horizon, so sorting chosen starts produces a gap-free source order with the same completion times and tardiness. For SequencingWithReleaseTimesAndDeadlines, feasible chosen starts may contain gaps; greedy evaluation of the extracted chronological order only moves completions earlier. Sorting zero-duration jobs before positive-duration jobs at a shared start preserves that implication. For DynamicStorageAllocation, addresses range from zero through memory-size; conflicts require both intersecting lifetimes and intersecting address ranges. Touching endpoints are allowed.
ShortestCommonSupersequence uses symbol-or-padding positions, embeddings of each source character, matching and order penalties, a padding suffix constraint, and objective equal to nonpadding length. Checked empty/invalid-alphabet behavior and the exact embedding direction. This encoding is later removed by #1217 for runtime reasons; no mathematical defect was identified in its own diff.
StartChoices checks multiplication by tuple size before allocating. Derived size and support bounds are consistent with construction. The unavailable bound for weighted tardiness is explicitly justified by the missing representable exponent contract for magnitude bits. The implementation does not make an unsupported closed-form size claim.
Quality review
Tests exercise all target bitstrings on small cases, compare both source and target brute-force optima, and cover infeasible and malformed witnesses. Zero durations, duplicate/touching time intervals, empty item sets, storage boundary equality, and overflow paths were traced. The optional SCS candidate's later removal is a documented performance decision, not an unexplained deleted rule.
Feature tests and verification limits
Executed the retained Phase 3 tests through the #1218 descendant's direct_qubo suite (44 tests passed overall). CLI workflows through list/show/create/inspect/path/reduce and independent source and bundle brute-force solves passed for weighted tardiness, release/deadline sequencing, and dynamic storage allocation; the source optimum/feasibility matched extraction.
Original #1216 SCS was reviewed statically, including tests and proof, but was not compiled or exercised: the shared descendant removes it in #1217, and build resources were reserved for current supported code and concrete boundary reproductions. Native exact-head test compilation was skipped for that reason. This is a verification limitation, not a claim that the original SCS runtime gate passed.
Author-reported conditional acceptance and benchmark limits were reviewed; no GitHub CI check results were visible for this stacked branch.
Findings (severity order)
No new blocking finding. The #1214 interval allocation panic remains inherited and should block stack integration until fixed. No repeated finding is assigned to this diff.
GitHub PR Audit — #1216
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
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 5e137d38f6c297c367207870afede4ec3eed1424 for merging into issue-1213-direct-qubo-phase2 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 four conditional Phase 3 direct integer QUBO reductions from #1213, with exact witness extraction, completed-value recovery, canonical examples and manual proofs. Stacked on unmerged draft #1215 at
ecc0ad5a(itself on #1214). Keep this PR draft and the roadmap open.Only candidates with completed raw-target validation in the selected direct and affected upstream cases remain. The direct weighted-tardiness, fixed-register and Betweenness rules are deferred because raw solves still time out on small sources. Their new reducers, registrations, examples and manual entries are removed; their source models and existing ILP routes remain unchanged.
Implemented, in roadmap priority order
The two scheduling rules share the checked start-choice helper. Existing sparse QUBO, row-decoding and objective-offset helpers are reused. The only existing ILP edits disambiguate trait calls for the retained minimum-tardiness and supersequence edges. No dependency or model-domain change.
Measured logical benefit, not a symbolic-bound claim
Same canonical instances, actual normalized nonzero off-diagonal couplings. Existing routes were enumerated from the Phase 2 head, including inherited Phase 1/2 routes, then shortest alternatives and inherited direct-edge paths up to five steps were constructed. These are measured baselines, not a claim to have solved global route optimization. Debug CLI wall time includes process startup/JSON; it is not a kernel benchmark or annealer timing.
Regressions are real. Two 64-unit tasks give minimum-tardiness 130 variables/8,383 couplings versus 42/264 through binary ILP. Two unit jobs with deadline 128 give release/deadline 256/16,384 versus 29/350. Smaller coefficients can accompany larger targets; no universal size or speed improvement is claimed.
Bounds, arithmetic and recovery
Start grids use
H=sum processing times; address grids use numeric memoryD. Their size is pseudopolynomial in those magnitudes and exponential in input bit lengths. Exact startsS=sum(H-p_i+1), release windowsS=sum max(0,d_i-p_i-r_i+1), and storageS=sum(D-size_i+1)have at mostS(S-1)/2couplings. Construction enumerates quadratic candidate pairs (and precedence pairs); extraction includes oneO(N+nnz)target validation. SCS uses exactlyL(a+1)+L²variables, with explicit alphabet magnitude. Composed bounds and exact coefficients are in the measurement certificate.The incoming ThreePartition example also illustrates route choice: its inherited Phase 2 direct rule has 12 variables/36 couplings, whereas the new release/deadline chain has 163 variables/5,465 couplings. The chain check establishes recovery, not preference over the inherited direct edge.
The minimum-tardiness rule publishes unavailable size transforms: its exponential-in-processing-bits bound cannot be represented by the registry's constant-integer-exponent contract. It does not publish a false polynomial bound. Release/deadline and storage retain explicit numeric horizon/capacity metadata.
Construction checks source prefixes/finish additions before target cancellation, coefficients/constants/thresholds, positive/negative target coefficient sums, and allocation dimensions. Unrepresentable arithmetic returns typed
IntegerOverflow; this does not redefine constructors. The checkedmax release + sum lengthsguard bounds source finish arithmetic for every order; it can reject representationally unsafe instances even if some schedules terminate early. Symbol-row byte capacity is checked against isize even when the variable count fits usize. Both have red-before-fix regression tests. The source models themselves remain unchanged. Existing exact-i64 limits can still block composed routes. Optimization uses the omitted-constant interval to recoverMin(None)on infeasible sources; feasibility aggregates mapOridentically.Verification
linearization_level=2), 15-second limit. All optimization runs proved OPTIMAL; decision runs proved feasible or infeasible. The earlier ten SCS timeouts are resolved. Raw solves of the remaining 360 corpus targets were not attempted.make checkpassed: 7,130 tests/doctests, formatting and clippy.make paper,make cliandmake coveragepassed. New production coverage: 319/323 executable lines (98.76%); every new production file exceeds 95%./simplifycompleted before the required fresh-context review. Fresh structural/proof review and installed-CLI feature testing found no unresolved substantive findings. The four retained reducers and helper are byte-identical to the previously certified implementations; the final change removes the three excluded rules and their related artifacts.Verified commit:
109985f4103d4c4785f60b8a34007580cd7f2434. Finite corpus and exhaustive tests supplement the proofs; they establish no universal runtime guarantee. Detailed current verification and fresh review are linked in the latest PR comments.Explicitly deferred candidates
[-1], capacity1has source optimum 1 while ILP assignment/use[1,0]scores 0. Recorded, not silently used as a correctness baseline or fixed out of scope. Canonical positive baseline 21/72.Max<i64> → Min<i64>needs a separately specified aggregate/decision endpoint. Three exact-integer MIS paths timed out in construction at ten seconds; an ILP path gives 1,085/3,327. No unsupported integer-domination claim.Phase 2's weighted-completion scheduling, ExpectedRetrievalCost and BottleneckTravelingSalesman remain explicitly deferred. They are not folded into this PR. Existing Phase 2 aggregate-recovery gaps and exact-coefficient chain limits are not claimed fixed.
Primary formulation references consulted: time-indexed scheduling, assignment/conflict penalties, quadratic tournaments, and LCS match-clique formulation. Repository-specific proofs use the exact constructors and evaluators.
Retained mathematical evidence: constructor certificate, grid proof/adversary, supersequence proof/adversary, baselines and composed bounds. These earlier certificates include additional historical candidates; only the four rules listed above ship. The order certificate and earlier seven-rule verification totals are historical, not current package scope. Timeout diagnosis and controlled solver comparisons explain the three exclusions and resolved SCS cases.
CI/Codecov: the stacked base does not trigger workflows filtered to main/develop; no remote result is claimed. References #1213; does not close it. No generated exports or corpus artifacts are committed. Keep draft; never merge.
Current evidence: four-rule verification certificate, fresh-context review.