Repository navigation
Conversation
Verification certificateVERIFIED — eight Phase 1 direct QUBO rules. Exact integer mathematics was checked independently before Rust implementation. The simplification changes allocation and redundant stored dimensions only. Fresh review additionally found source overflow hidden by algebraic cancellation; regression tests reproduced it before adding conservative source-arithmetic guards for weighted completion and QAP. Type resolution: the six optimization sources have Source evidence for concrete value types{
"SequencingToMinimizeWeightedCompletionTime": "Min<i64>; src/models/misc/sequencing_to_minimize_weighted_completion_time.rs:228",
"MinimumTardinessSequencing<One>": "Min<i64>; src/models/misc/minimum_tardiness_sequencing.rs:258",
"MaximumLikelihoodRanking": "Min<i64>; src/models/misc/maximum_likelihood_ranking.rs:151",
"QuadraticAssignment": "Min<i64>; src/models/algebraic/quadratic_assignment.rs:141",
"SumOfSquaresPartition": "Min<i64>; src/models/misc/sum_of_squares_partition.rs:173",
"OptimalLinearArrangement<SimpleGraph>": "Min<i64>; src/models/graph/optimal_linear_arrangement.rs:151",
"SequencingWithinIntervals": "Or; src/models/misc/sequencing_within_intervals.rs:189",
"TimetableDesign": "Or; src/models/misc/timetable_design.rs:249",
"QUBO<i64>": "Min<W::Sum>, W=i64, Sum=i64; src/models/algebraic/qubo.rs:299; src/types.rs:182",
"Decision<QUBO<i64>>": "Or; src/models/decision.rs"
}Constructor audit: 12,000 instances, 616,923 target strings, 29,999 successful extractions, 12,000 structural checks, 12,000 count checks, and 5 symbolic identities. Cross-comparison additionally checks 504,623 feasible source encodings. Constructor random seed: 2681. Independent adversary audit: 16,007 instances, 576,784 feasible witnesses, 751,462 target strings, 13,041 exhaustive small instances, and 15 symbolic identities. Two Hypothesis strategies each ran 10,000 examples ( Both cover dimensions 1 through 5 with at least 300 samples per dimension/family, plus small exhaustive families and empty boundaries. Target bitstrings are exhaustive through 9 bits; larger targets use every valid assignment and sampled invalid strings. This is not exhaustive enumeration of unbounded integer domains. Eight worked YES examples and four legitimate source-NO examples were reproduced. Ranking, QAP, sum-of-squares partition and linear arrangement are always feasible under their constructors, so rejected target configurations replace nonexistent source-NO examples. Cross-comparison: 12,000 identical canonical target polynomials and bounds, 0 disagreements. Arithmetic implementation limits are additionally exercised by Rust overflow tests; the Python mathematical checks use unbounded integers. The separate read-only corpus run passed 800/800 cases; after the source-arithmetic fix, the two affected rules passed 200/200 cases again and all 26,137 snapshotted corpus files remained unchanged. The corpus runner and corpus-specific tests are deliberately absent from this PR and this certificate. proof.typ= Eight direct integer QUBO reductions
== Type and arithmetic contract
Sources WeightedCompletion = SequencingToMinimizeWeightedCompletionTime,
Tardy = MinimumTardinessSequencing<One>, Ranking = MaximumLikelihoodRanking,
QAP = QuadraticAssignment, Squares = SumOfSquaresPartition,
Arrangement = OptimalLinearArrangement<SimpleGraph> all have Value Min<i64>.
Intervals = SequencingWithinIntervals and Timetable = TimetableDesign have Value Or.
Optimization targets are QUBO<i64> (Min<i64>); feasibility targets are
Decision<QUBO<i64>> (Or). All witnesses are binary vectors; all coefficients
are exact signed integers. Inputs outside representable derived i64 coefficients,
constants, penalty bounds or total energy bounds return typed overflow, never
saturation. This is a partial computational encoding under the existing numeric
contract, not an assertion that every arbitrary integer instance fits i64.
Source evaluation safety is checked before objective expansion: for weighted
completion, let a=sum(min(p_i,0)), b=sum(max(p_i,0)). Every elapsed prefix is
in [a,b]. Task i completes in [a+max(p_i,0), b+min(p_i,0)]; multiplying both
endpoints by w_i bounds its weighted cost. Checked sums of negative lower
bounds and positive upper bounds certify all source objective prefixes.
For QAP, check every directed A_ij D_pq product in i64, find each facility
pair's extrema over locations, and accumulate negative minima and positive
maxima. Thus neither polynomial expansion nor opposite-pair cancellation
can hide source overflow. These bounds conservatively reject uncertifiable
instances; they do not widen the source evaluator's numeric domain.
== Shared penalty lemma
1. Define a quadratic objective f(x)=c+sum(q_ab x_a x_b), with a<=b and
x_a^2=x_a. Combine repeated coefficients, omit zero coefficients.
2. Set L=c+sum(min(q_ab,0)), U=c+sum(max(q_ab,0)), and P=U-L+1.
3. Let g(x) be the sum of the nonnegative integer constraint penalties below.
Expand F=f+P*g, combine coefficients, and remove its constant C to obtain Q.
For feasibility use f=0 and P=1. Decision bound is -C.
Forward: A valid source witness encodes to bits with g=0. Then Q+C equals
its objective, in [L,U], or is zero for feasibility.
Backward: An invalid bitstring has g>=1, so F>=L+P=U+1. It cannot beat a
valid witness, or meet the feasibility threshold. If there is no valid source
witness, every target energy is above U-C. A completed target minimum e maps
to e+C if L<=e+C<=U and otherwise to Min(None); target Min(None) also maps
to Min(None). Decode only after validating length and this energy certificate.
This includes optimal infeasible-source recovery despite QUBO itself always
having bitstrings. Arbitrary penalized bitstrings must be rejected.
== Tournament construction (WeightedCompletion and Ranking)
1. There are N=n(n-1)/2 variables x_ij for i<j in lexicographic pair order;
x_ij=1 means item i precedes j. For every i<j<k add to g
x_ik+x_ij*x_jk-x_ij*x_ik-x_jk*x_ik. This equals 1 exactly for the two cyclic
orientations and 0 otherwise. Precedence (a,b) adds 1-x_ab if a<b, x_ba
if a>b, and constant 1 if a=b. Duplicate precedences are retained.
2. WeightedCompletion permits signed processing p_i and weights w_i. Set
c=sum_i(p_i*w_i)+sum_(i<j)(p_j*w_i),
f=c+sum_(i<j)((p_i*w_j-p_j*w_i)*x_ij).
3. Ranking has signed matrix M with M_ij+M_ji constant. Set
c=sum_(i<j) M_ij, f=c+sum_(i<j)(M_ji-M_ij)*x_ij. No precedence penalties.
Forward: Any ordered permutation defines an acyclic tournament. Each pair
contributes the earlier processing time times the later weight in completion
cost, in addition to each task's own p_i*w_i. Ranking pays M_ji exactly when
i precedes j, which is its definition using rank_j>rank_i.
Backward: A tournament with no directed triangle is transitive: any shortest
directed cycle of length >3 has a chord giving a shorter directed cycle.
Thus zero triangle penalties give a total order. Zero precedence penalties
make this order admissible. The two objectives then match term by term.
Extraction: Count incoming tournament arcs to get rank[item]. Reject duplicate
ranks. Ranking returns ranks; WeightedCompletion returns items sorted by rank.
Overhead: exact N bits; at most 3*binomial(n,3)=n(n-1)(n-2)/2 couplings.
Each triple supplies three pairs of distinct comparison bits, and a pair of
such bits determines its triple. Precedence contributes no couplings.
== Assignment constructions
For r rows and k columns use bit x_ip at index i*k+p. Every row adds
(1-sum_p x_ip)^2 to g. For permutations every column also adds
(1-sum_i x_ip)^2; for injective rectangular assignments each column instead
adds sum_(i<j) x_ip*x_jp. Squares needs only row penalties.
Tardy: r=k=n. f=sum_(i,p with p+1>d_i) x_ip, where signed d_i is deadline.
Every precedence (a,b) adds sum_(p>=q) x_ap*x_bq to g, including self
precedences (diagonal bit-products become linear). Decode task->position
then invert to an ordered list of tasks. Objective counts late unit jobs.
QAP: r=n facilities, k=m locations, n<=m; f=sum_(i!=j,p,q)
C_ij*D_pq*x_ip*x_jq. Include p=q, which vanishes on injective assignments.
Source ignores i=j even if C_ii or D_pp nonzero. Matrices may be asymmetric
and signed. Decode facility->location.
Squares: r=n items, k groups, 1<=k<=n, sizes s_i>0;
f=sum_g(sum_i s_i*x_ig)^2. Empty groups are allowed. Decode item->group.
Arrangement: r=k=n vertices; f=sum_((u,v) in E,p,q)
abs(p-q)*x_up*x_vq. Use the model's edge list (including multiplicity or
self edges if supplied); decode vertex->position.
Forward: Put a single 1 at each source-assigned column. Its row, column and
precedence penalties vanish. Substituting these bits reduces each displayed
objective to its source definition.
Backward: Vanishing squared row penalties ensure exactly one column for each
row; column penalties give a permutation or injection when required.
Precedence penalties prohibit every inverted or equal-position pair. Hence
the resulting assignment is admissible and substitution yields the objective.
Extraction: Select the unique set bit in each row, reject zero/multiple bits;
validate unique columns for injective variants and precedence for Tardy.
Overhead: Tardy and Arrangement exactly n^2 bits, at most n^2(n^2-1)/2
couplings. QAP exactly n*m bits, at most n*m*(n*m-1)/2 couplings.
Squares exactly n*k bits, at most n*k*(k-1)/2+k*n*(n-1)/2 couplings
(row one-hot pairs and same-group pairs of distinct items are disjoint).
== Intervals
1. Task i has nonnegative release r_i, deadline d_i, length l_i.
Its allowed starts are r_i+t for 0<=t<s_i=max(0,d_i-r_i-l_i+1).
Allocate S=sum_i s_i bits in task/start order, including no bits for empty rows.
2. Add (1-sum_t x_it)^2 to g for every task, including empty rows.
For different tasks, add x_it*x_ju whenever neither chosen execution interval
finishes before the other starts: not(end_i<=start_j or end_j<=start_i).
This is also the source predicate for zero-length tasks.
Forward: Every schedule has one allowed start per task and no conflicts, g=0.
Backward: g=0 gives exactly one start in every row and no selected conflict.
Each row domain already guarantees release/deadline constraints.
Extraction: Return the index t of the unique bit within each task's row.
Overhead: exactly S bits; at most S(S-1)/2 couplings. Constant C=n,
Decision bound -n. Empty domains make g>=1 and certify NO.
== Timetable
1. There are c craftsmen, t tasks, h periods; availability matrices a_ch,b_th
are boolean and requirements R_ct are signed integers.
Allocate A bits for triples (c,t,h) in that lexicographic order with R_ct>0
and both availabilities true. All other source tensor cells decode to false.
2. If any R_ct<0 or R_ct exceeds its eligible period count, construct the
zero polynomial on the same A bits with Decision bound -1. No source is
feasible, because a sum of eligible boolean cells cannot equal R_ct.
Otherwise g=sum_(c,t)(sum_h x_cth-R_ct)^2 plus one product for every pair
of eligible triples sharing a period and either craftsman or task. Count a
conflict pair once even if both resources coincide. C=sum_(c,t)R_ct^2.
Forward: A timetable satisfying demand and resource exclusivity yields g=0.
Backward: Each demand square must vanish and no exclusive resource conflict
can be selected; unavailable and zero-demand cells are false by construction.
Extraction: Fill a false tensor of shape c*t*h and place the selected bits
at their eligible coordinates. Validate the Decision certificate first.
Overhead: exactly A bits; at most A(A-1)/2 couplings, also for the NO sentinel.
== Worked examples (at least three variables)
WeightedCompletion: p=[1,1,1],w=[1,2,3], no precedences. c=10,
linear=[1,2,1], L=10,U=14,P=5. Order [2,1,0] has x=[0,0,0], g=0,
Q=0,C=10, recovered cost10. Adding (0,1),(1,2),(2,0) forces a cycle:
every assignment has g>=1; none certifies a source witness.
Ranking: M=[[0,1,2],[3,0,1],[2,3,0]], c=4,linear=[2,0,2],
L=4,U=8,P=5. Ranks [2,1,0] give x=000,cost4. There is no infeasible
source of this type; the cyclic x=101 has g=1,f=8,F=13>U, rejected.
Tardy: n=3,d=[1,2,3], precedence(0,1). Diagonal assignment has objective0.
The three late cells give L=0,U=3 (late cells: row0 positions1,2; row1 position2),
P=4; six one-hot squares yield C=24 and Q=-24. Adding (1,0) makes every
permutation violate precedence and every nonpermutation violate one-hot.
QAP: n=m=3,C_ij=1 for i!=j,C_ii=0; D_pq=1 for p!=q,D_pp=0.
There are36 unit quadratic products before combining ordered duplicates,
L=0,U=36,P=37. Identity assignment cost6; C=3P=111; Q=-105.
Every injective assignment costs6. All-zero bits give F=111>36, rejected.
This source type is always feasible, so source NO is unrepresentable.
Squares: s=[1,1,1],k=1, f=(x0+x1+x2)^2,L=0,U=9,P=10.
All-one has cost9,C=30,Q=-21. All-zero F=30>9 is rejected. Always feasible;
a source NO example cannot exist under positive sizes and k>=1.
Arrangement: three-vertex path edges(0,1),(1,2). Identity positions cost2.
For each edge sum_(p,q)|p-q|=8, so U=16,L=0,P=17,C=6P=102,Q=-100.
All-zero F=102>16 is rejected; this source type is always feasible.
Intervals YES: r=[0,1,2],d=[1,2,3],l=[1,1,1]. Three bits, Q=-sum x,
C=3,bound=-3, x=111 succeeds. NO: r=[0,0,0],d=[1,1,1],l=[1,1,1].
Three bits,Q=-sum x+sum_(i<j)x_i*x_j,minimum=-1>-3.
Timetable YES: c=3,t=1,h=3, each craftsman available only in their own period,
task available in all periods, each demand1. Three bits,Q=-sum x,C=3,
bound=-3,x=111 succeeds. NO: same but all craftsmen only available period0.
Three bits and conflict clique: Q=-sum x+sum_(i<j)x_i*x_j,min=-1>-3.
== Verification limits
Finite exhaustive enumeration of arbitrary signed integer matrices, times and
weights is impossible. Exhaust all bitstrings for bounded small instances;
for larger n through5 use sampled invalid strings plus all feasible assignments,
and at least300 generated instances per dimension family. Symbolically check
all count formulas and square/triangle expansions. Independently implemented
constructors must agree on sorted coefficient triples, constant, threshold,
and extracted objective. Negative-source examples apply only to source types
with infeasible instances; the four always-feasible types use rejected target
examples instead, with this explicit limitation.
constructor.pyimport itertools as it, random, json, collections
from pathlib import Path
import sympy as sp
class Poly:
def __init__(self): self.q=collections.defaultdict(int); self.c=0
def add(self,a,b,v): self.q[min(a,b),max(a,b)]+=v
def square(self,terms,b):
self.c+=b*b
for a,w in terms: self.add(a,a,w*w-2*b*w)
for (a,w),(d,v) in it.combinations(terms,2): self.add(a,d,2*w*v)
def reduce(kind,d):
f,g=Poly(),Poly(); bound=None
if kind in ['weighted','ranking']:
n=len(d['p'] if kind=='weighted' else d['M']); pairs=list(it.combinations(range(n),2)); ids={ij:k for k,ij in enumerate(pairs)}; N=len(pairs)
if kind=='weighted':
p,w=d['p'],d['w']; f.c=sum(a*b for a,b in zip(p,w))
for (i,j),v in ids.items(): f.c+=p[j]*w[i]; f.add(v,v,p[i]*w[j]-p[j]*w[i])
else:
for (i,j),v in ids.items(): f.c+=d['M'][i][j]; f.add(v,v,d['M'][j][i]-d['M'][i][j])
for i,j,k in it.combinations(range(n),3):
a,b,c=ids[i,j],ids[i,k],ids[j,k]
g.add(b,b,1);g.add(a,c,1);g.add(a,b,-1);g.add(c,b,-1)
for a,b in d.get('prec',[]):
if a==b:g.c+=1
elif a<b:g.c+=1;g.add(ids[a,b],ids[a,b],-1)
else:g.add(ids[b,a],ids[b,a],1)
elif kind in ['tardy','qap','squares','arrangement']:
n=len(d['d']) if kind=='tardy' else len(d['C']) if kind=='qap' else len(d['s']) if kind=='squares' else d['n']
k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else n;N=n*k
for i in range(n):g.square([(i*k+p,1) for p in range(k)],1)
if kind in ['tardy','arrangement']:
for p in range(k):g.square([(i*k+p,1) for i in range(n)],1)
if kind=='qap':
for p in range(k):
for i,j in it.combinations(range(n),2):g.add(i*k+p,j*k+p,1)
for i,j,p,q in it.product(range(n),range(n),range(k),range(k)):
if i!=j:f.add(i*k+p,j*k+q,d['C'][i][j]*d['D'][p][q])
if kind=='squares':
for p in range(k):f.square([(i*k+p,d['s'][i]) for i in range(n)],0)
if kind=='arrangement':
for u,v in d['edges']:
for p,q in it.product(range(k),repeat=2):f.add(u*k+p,v*k+q,abs(p-q))
if kind=='tardy':
for i,p in it.product(range(n),repeat=2):f.add(i*k+p,i*k+p,int(p+1>d['d'][i]))
for a,b in d['prec']:
for p in range(n):
for q in range(p+1):g.add(a*k+p,b*k+q,1)
elif kind=='intervals':
rows=[];N=0
for r,t,l in zip(d['r'],d['d'],d['l']):
row=list(range(N,N+max(0,t-r-l+1)));N+=len(row);rows.append(row);g.square([(v,1) for v in row],1)
for i,j in it.combinations(range(len(rows)),2):
for p,a in enumerate(rows[i]):
for q,b in enumerate(rows[j]):
si,sj=d['r'][i]+p,d['r'][j]+q
if not(si+d['l'][i]<=sj or sj+d['l'][j]<=si):g.add(a,b,1)
elif kind=='timetable':
R,a,b=d['R'],d['a'],d['b']; coords=[(i,j,h) for i in range(len(R)) for j in range(len(b)) for h in range(len(a[i])) if R[i][j]>0 and a[i][h] and b[j][h]];N=len(coords)
for i in range(len(R)):
for j in range(len(b)):
row=[(z,1) for z,(c,t,h) in enumerate(coords) if (c,t)==(i,j)]
if R[i][j]<0 or R[i][j]>len(row):return dict(n=N,q=[],constant=0,lower=0,upper=0,bound=-1)
g.square(row,R[i][j])
for (z,(i,j,h)),(v,(c,t,s)) in it.combinations(enumerate(coords),2):
if h==s and (i==c or j==t):g.add(z,v,1)
L=f.c+sum(min(0,q) for q in f.q.values()); U=f.c+sum(max(0,q) for q in f.q.values());P=U-L+1
for (a,b),q in g.q.items():f.add(a,b,P*q)
C=f.c+P*g.c
if kind in ['intervals','timetable']:bound=-C
return dict(n=N,q=[[a,b,q] for (a,b),q in sorted(f.q.items()) if q],constant=C,lower=L,upper=U,bound=bound)
def source(kind,d,z):
if kind=='weighted':
rank={v:i for i,v in enumerate(z)}
if any(rank[a]>=rank[b] for a,b in d['prec']):return None
time=0;v=0
for i in z:time+=d['p'][i];v+=time*d['w'][i]
return v
if kind=='ranking':return sum(d['M'][a][b] for a,b in it.permutations(range(len(z)),2) if z[a]>z[b])
if kind=='tardy':
rank={v:i for i,v in enumerate(z)}
return None if any(rank[a]>=rank[b] for a,b in d['prec']) else sum(rank[i]+1>d['d'][i] for i in range(len(z)))
if kind=='qap':return sum(d['C'][i][j]*d['D'][z[i]][z[j]] for i,j in it.permutations(range(len(z)),2))
if kind=='squares':return sum(sum(s for i,s in enumerate(d['s']) if z[i]==g)**2 for g in range(d['k']))
if kind=='arrangement':return sum(abs(z[u]-z[v]) for u,v in d['edges'])
if kind=='intervals':
t=[r+v for r,v in zip(d['r'],z)]
return 0 if all(t[i]+d['l'][i]<=t[j] or t[j]+d['l'][j]<=t[i] for i,j in it.combinations(range(len(z)),2)) else None
if kind=='timetable':
sel=z
if any(sum((i,j,h) in sel for h in range(len(d['a'][i])))!=v for i,row in enumerate(d['R']) for j,v in enumerate(row)):return None
if any(h==s and (i==c or j==t) for (i,j,h),(c,t,s) in it.combinations(sel,2)):return None
return 0
def decode(kind,d,x):
if kind in ['weighted','ranking']:
n=len(d['p'] if kind=='weighted' else d['M']);r=[0]*n
for a,(i,j) in enumerate(it.combinations(range(n),2)):r[j if x[a] else i]+=1
if sorted(r)!=list(range(n)):return None
return r if kind=='ranking' else sorted(range(n),key=r.__getitem__)
if kind=='timetable':
coords=[(i,j,h) for i,row in enumerate(d['R']) for j,v in enumerate(row) for h in range(len(d['a'][i])) if v>0 and d['a'][i][h] and d['b'][j][h]]
return [v for v,b in zip(coords,x) if b]
if kind=='intervals':lengths=[max(0,t-r-l+1) for r,t,l in zip(d['r'],d['d'],d['l'])]
else:
n=len(d['d']) if kind=='tardy' else len(d['C']) if kind=='qap' else len(d['s']) if kind=='squares' else d['n'];k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else n;lengths=[k]*n
rows=[];a=0
for size in lengths:
row=[p for p in range(size) if x[a+p]];a+=size
if len(row)!=1:return None
rows.append(row[0])
if kind in ['tardy','qap','arrangement'] and len(set(rows))<len(rows):return None
return sorted(range(len(rows)),key=rows.__getitem__) if kind=='tardy' else rows
def generate(kind,n,r):
prec=lambda:[(r.randrange(n),r.randrange(n)) for _ in range(r.randrange(3))] if n else []
if kind=='weighted':return dict(p=[r.randrange(-2,4) for _ in range(n)],w=[r.randrange(-2,4) for _ in range(n)],prec=prec())
if kind=='ranking':
M=[[0]*n for _ in range(n)]
for i,j in it.combinations(range(n),2):M[i][j]=r.randrange(-3,4);M[j][i]=2-M[i][j]
return dict(M=M)
if kind=='tardy':return dict(d=[r.randrange(-1,n+2) for _ in range(n)],prec=prec())
if kind=='qap':
k=n+(n<4);return dict(C=[[r.randrange(-2,3) for _ in range(n)] for _ in range(n)],D=[[r.randrange(-2,3) for _ in range(k)] for _ in range(k)])
if kind=='squares':return dict(s=[r.randrange(1,4) for _ in range(n)],k=max(1,r.randrange(1,n+1)))
if kind=='arrangement':return dict(n=n,edges=[p for p in it.combinations(range(n),2) if r.randrange(2)])
if kind=='intervals':
a=[r.randrange(3) for _ in range(n)];l=[r.randrange(3) for _ in range(n)];return dict(r=a,l=l,d=[v+w+r.randrange(-1,2) if v+w else r.randrange(2) for v,w in zip(a,l)])
if kind=='timetable':return dict(R=[[r.randrange(-1,3)] for _ in range(n)],a=[[bool(r.randrange(2)) for _ in range(3)] for _ in range(n)],b=[[True]*3])
def main():
r=random.Random(2681);audit=collections.Counter();cases=[]
n,k=sp.symbols('n k',integer=True,positive=True)
assert sp.expand(3*n*(n-1)*(n-2)/6-n*(n-1)*(n-2)/2)==0
assert sp.expand(n*k*(k-1)/2+k*n*(n-1)/2-n*k*(n+k-2)/2)==0
for N in [n*n,n*k,n*(n-1)/2]:assert sp.simplify(N*(N-1)/2-sp.binomial(N,2))==0
audit['symbolic']=5
for kind in ['weighted','ranking','tardy','qap','squares','arrangement','intervals','timetable']:
for n in range(1,6):
for iteration in range(300):
d=generate(kind,n,r);q=reduce(kind,d);N=q['n'];cases.append((kind,d,q));audit['instances']+=1
assert all(0<=a<=b<N and v for a,b,v in q['q']);audit['structure']+=1
assert sum(a!=b for a,b,v in q['q'])<=N*(N-1)//2;audit['counts']+=1
strings=it.product([0,1],repeat=N) if N<=9 else ([r.randrange(2) for _ in range(N)] for _ in range(30))
for x in strings:
F=q['constant']+sum(v*x[a]*x[b] for a,b,v in q['q']);z=decode(kind,d,x);val=None if z is None else source(kind,d,z)
certified=F==0 if q['bound'] is not None and q['bound']!=-1 else q['lower']<=F<=q['upper']
if kind=='timetable' and q['bound']==-1 and q['q']==[]:certified=False
if kind in ['intervals','timetable']:certified=sum(v*x[a]*x[b] for a,b,v in q['q'])<=q['bound']
assert certified==(val is not None),(kind,d,x,q,z,val,F)
if certified:assert F==val;audit['extraction']+=1
audit['backward']+=1
Path(__file__).with_name('constructor-cases.json').write_text(json.dumps(cases))
Path(__file__).with_name('constructor-report.json').write_text(json.dumps(audit,indent=2));print(audit)
if __name__=='__main__':main()adversary.py"""Independent executable reading only proof.typ. Protocol: see DATA_FIELDS below.
No constructor/repository imports. Integers are mathematical, not bounded i64.
Run with phase1/.venv/bin/python adversary.py; reports live beside this file.
"""
import itertools as it
import json
import math
import random
from collections import Counter, defaultdict
from pathlib import Path
DATA_FIELDS = {
'weighted':'p,w,prec(optional)', 'ranking':'M', 'tardy':'d,prec(optional)',
'qap':'C,D', 'squares':'s,k', 'arrangement':'n,edges',
'intervals':'r,d,l', 'timetable':'R,a,b'}
class Poly:
def __init__(self): self.c=0; self.q=defaultdict(int)
def add(self,i,j,v): self.q[tuple(sorted((i,j)))]+=v
def square(self,indices,target):
self.c+=target*target
for i in indices: self.add(i,i,1-2*target)
for i,j in it.combinations(indices,2): self.add(i,j,2)
def merge(self,other,scale):
self.c+=scale*other.c
for (i,j),v in other.q.items(): self.add(i,j,scale*v)
def pairs(n): return list(it.combinations(range(n),2))
def domain(d): return [list(range(max(0,b-a-l+1))) for a,b,l in zip(d['r'],d['d'],d['l'])]
def eligible(d):
return [(i,j,h) for i,row in enumerate(d['R']) for j,r in enumerate(row) for h in range(len(d['a'][i])) if r>0 and d['a'][i][h] and d['b'][j][h]]
def reduce(kind,d):
f,g=Poly(),Poly(); sentinel=False
if kind in ('weighted','ranking'):
n=len(d['p'] if kind=='weighted' else d['M']); ps=pairs(n); ids={p:i for i,p in enumerate(ps)}; N=len(ps)
for i,j,k in it.combinations(range(n),3):
a,b,c=ids[i,j],ids[i,k],ids[j,k]
g.add(b,b,1);g.add(a,c,1);g.add(a,b,-1);g.add(c,b,-1)
for a,b in d.get('prec',[]):
if a==b:g.c+=1
elif a<b:g.c+=1;g.add(ids[a,b],ids[a,b],-1)
else:g.add(ids[b,a],ids[b,a],1)
if kind=='weighted':
p,w=d['p'],d['w'];f.c=sum(a*b for a,b in zip(p,w))
for (i,j),v in ids.items():f.c+=p[j]*w[i];f.add(v,v,p[i]*w[j]-p[j]*w[i])
else:
M=d['M']
for (i,j),v in ids.items():f.c+=M[i][j];f.add(v,v,M[j][i]-M[i][j])
elif kind in ('tardy','qap','squares','arrangement'):
n=len(d['d']) if kind=='tardy' else len(d['C']) if kind=='qap' else len(d['s']) if kind=='squares' else d['n']
k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else n;N=n*k
for i in range(n):g.square([i*k+p for p in range(k)],1)
if kind in ('tardy','arrangement'):
for p in range(k):g.square([i*k+p for i in range(n)],1)
elif kind=='qap':
for p in range(k):
for i,j in pairs(n):g.add(i*k+p,j*k+p,1)
if kind=='tardy':
for i in range(n):
for p in range(k):f.add(i*k+p,i*k+p,int(p+1>d['d'][i]))
for a,b in d.get('prec',[]):
for p in range(k):
for q in range(p+1):g.add(a*k+p,b*k+q,1)
elif kind=='qap':
for i,j,p,q in it.product(range(n),range(n),range(k),range(k)):
if i!=j:f.add(i*k+p,j*k+q,d['C'][i][j]*d['D'][p][q])
elif kind=='squares':
for p in range(k):
for i in range(n):
f.add(i*k+p,i*k+p,d['s'][i]**2)
for j in range(i):f.add(i*k+p,j*k+p,2*d['s'][i]*d['s'][j])
else:
for i,j in d['edges']:
for p,q in it.product(range(k),repeat=2):f.add(i*k+p,j*k+q,abs(p-q))
elif kind=='intervals':
starts=domain(d);coords=[(i,t) for i,row in enumerate(starts) for t in row];N=len(coords)
for i in range(len(starts)):g.square([b for b,(j,_) in enumerate(coords) if i==j],1)
for a,b in pairs(N):
i,t=coords[a];j,u=coords[b];si=d['r'][i]+t;sj=d['r'][j]+u
if i!=j and not(si+d['l'][i]<=sj or sj+d['l'][j]<=si):g.add(a,b,1)
else:
assert kind=='timetable';coords=eligible(d);N=len(coords)
sentinel=any(r<0 or r>sum(x==i and y==j for x,y,h in coords) for i,row in enumerate(d['R']) for j,r in enumerate(row))
if not sentinel:
for i,row in enumerate(d['R']):
for j,r in enumerate(row):g.square([v for v,(a,b,h) in enumerate(coords) if (a,b)==(i,j)],r)
for a,b in pairs(N):
i,j,h=coords[a];x,y,t=coords[b]
if h==t and (i==x or j==y):g.add(a,b,1)
L=f.c+sum(min(v,0) for v in f.q.values());U=f.c+sum(max(v,0) for v in f.q.values())
f.merge(g,U-L+1)
return {'n':N,'q':[[i,j,v] for (i,j),v in sorted(f.q.items()) if v], 'constant':f.c,'lower':L,'upper':U,'bound':(-1 if sentinel else -f.c) if kind in ('intervals','timetable') else None}
def source(kind,d,w):
"""Return None for invalid, integer objective otherwise. Independent definitions."""
if kind in ('weighted','tardy'):
n=len(d['p'] if kind=='weighted' else d['d'])
if sorted(w)!=list(range(n)):return None
pos={a:i for i,a in enumerate(w)}
if any(pos[a]>=pos[b] for a,b in d.get('prec',[])):return None
if kind=='tardy':return sum(i+1>d['d'][a] for i,a in enumerate(w))
time=0;cost=0
for a in w:time+=d['p'][a];cost+=time*d['w'][a]
return cost
if kind in ('ranking','arrangement'):
n=len(d['M']) if kind=='ranking' else d['n']
if sorted(w)!=list(range(n)):return None
if kind=='arrangement':return sum(abs(w[a]-w[b]) for a,b in d['edges'])
return sum(d['M'][j][i] for i in range(n) for j in range(n) if w[j]>w[i])
if kind=='qap':
if len(w)!=len(d['C']) or len(set(w))!=len(w) or any(p<0 or p>=len(d['D']) for p in w):return None
return sum(d['C'][i][j]*d['D'][w[i]][w[j]] for i in range(len(w)) for j in range(len(w)) if i!=j)
if kind=='squares':
if len(w)!=len(d['s']) or any(p<0 or p>=d['k'] for p in w):return None
return sum(sum(s for s,p in zip(d['s'],w) if p==g)**2 for g in range(d['k']))
if kind=='intervals':
if len(w)!=len(d['r']):return None
starts=[r+t for r,t in zip(d['r'],w)]
if any(t<0 or s+l>deadline for t,s,l,deadline in zip(w,starts,d['l'],d['d'])):return None
for i,j in pairs(len(w)):
if not(starts[i]+d['l'][i]<=starts[j] or starts[j]+d['l'][j]<=starts[i]):return None
return 0
c,t,h=len(d['R']),len(d['b']),len(d['a'][0]) if d['a'] else 0
if len(w)!=c*t*h or any(x not in (0,1) for x in w):return None
def cell(i,j,p):return w[(i*t+j)*h+p]
for i,j in it.product(range(c),range(t)):
if sum(cell(i,j,p) for p in range(h))!=d['R'][i][j]:return None
for i,j,p in it.product(range(c),range(t),range(h)):
if cell(i,j,p) and not(d['a'][i][p] and d['b'][j][p]):return None
for p in range(h):
if any(sum(cell(i,j,p) for j in range(t))>1 for i in range(c)):return None
if any(sum(cell(i,j,p) for i in range(c))>1 for j in range(t)):return None
return 0
def raw_extract(kind,d,b):
if kind in ('weighted','ranking'):
n=len(d['p'] if kind=='weighted' else d['M']);rank=[0]*n
for v,(i,j) in zip(b,pairs(n)):rank[j if v else i]+=1
if len(set(rank))!=n:return None
return rank if kind=='ranking' else sorted(range(n),key=lambda i:rank[i])
if kind in ('tardy','qap','squares','arrangement','intervals'):
if kind=='intervals':sizes=list(map(len,domain(d)))
else:
n=len(d['d']) if kind=='tardy' else len(d['C']) if kind=='qap' else len(d['s']) if kind=='squares' else d['n']
k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else n;sizes=[k]*n
w=[];off=0
for k in sizes:
selected=[p for p in range(k) if b[off+p]];off+=k
if len(selected)!=1:return None
w.append(selected[0])
if kind=='tardy':return sorted(range(len(w)),key=lambda i:w[i]) if len(set(w))==len(w) else None
return w
t,h=len(d['b']),len(d['a'][0]) if d['a'] else 0;w=[0]*(len(d['R'])*t*h)
for x,(i,j,p) in zip(b,eligible(d)):w[(i*t+j)*h+p]=x
return w
def energy(q,b):return sum(v for i,j,v in q['q'] if b[i] and b[j])
def extract(kind,d,b,q=None):
q=q or reduce(kind,d)
if len(b)!=q['n'] or any(v not in (0,1) for v in b):return None
e=energy(q,b)
if q['bound'] is not None:
if e>q['bound']:return None
elif not(q['lower']<=e+q['constant']<=q['upper']):return None
w=raw_extract(kind,d,b)
return w if w is not None and source(kind,d,w) is not None else None
def witnesses(kind,d):
if kind in ('weighted','tardy','ranking','arrangement'):
n=len(d['p']) if kind=='weighted' else len(d['d']) if kind=='tardy' else len(d['M']) if kind=='ranking' else d['n']
return it.permutations(range(n))
if kind=='qap':return it.permutations(range(len(d['D'])),len(d['C']))
if kind=='squares':return it.product(range(d['k']),repeat=len(d['s']))
if kind=='intervals':return it.product(*domain(d))
coords=eligible(d);groups=[]
for i,row in enumerate(d['R']):
for j,r in enumerate(row):
if r<0:return iter(())
groups.append(it.combinations([v for v,(a,b,h) in enumerate(coords) if (a,b)==(i,j)],r))
def generate():
for selection in it.product(*groups):
b=[0]*len(coords)
for group in selection:
for v in group:b[v]=1
yield raw_extract(kind,d,b)
return generate()
COUNTS=Counter();BY_KIND=defaultdict(Counter)
def check(kind,d,rng):
q=reduce(kind,d);N=q['n'];valid=0;opt=None
if kind in ('weighted','ranking'):
n=len(d['p'] if kind=='weighted' else d['M']);assert N==n*(n-1)//2;limit=3*math.comb(n,3)
elif kind=='squares':
n,k=len(d['s']),d['k'];assert N==n*k;limit=n*k*(k-1)//2+k*n*(n-1)//2
else:
if kind=='qap':assert N==len(d['C'])*len(d['D'])
elif kind=='tardy':assert N==len(d['d'])**2
elif kind=='arrangement':assert N==d['n']**2
elif kind=='intervals':assert N==sum(map(len,domain(d)))
elif kind=='timetable':assert N==len(eligible(d))
limit=N*(N-1)//2
assert sum(i!=j for i,j,v in q['q'])<=limit,(kind,d,q,limit)
assert q['q']==sorted(q['q']) and all(0<=i<=j<N and v for i,j,v in q['q'])
for w in witnesses(kind,d):
obj=source(kind,d,w)
if obj is None:continue
valid+=1;opt=obj if opt is None else min(opt,obj)
# Encode directly without rebuilding polynomial for every witness.
b=encode_cached(kind,d,w,N)
actual=energy(q,b)+q['constant']
assert actual==obj,(kind,d,w,actual,obj)
assert extract(kind,d,b,q)==list(w),(kind,d,w,extract(kind,d,b,q))
COUNTS['valid_witnesses']+=1;BY_KIND[kind]['valid_witnesses']+=1
if N<=9:
bitstrings=it.product((0,1),repeat=N);COUNTS['exhaustive_instances']+=1
else:
bitstrings=it.chain(([0]*N,[1]*N),([rng.randrange(2) for _ in range(N)] for _ in range(20)))
best=None;accepted=0
for b in bitstrings:
e=energy(q,b);best=e if best is None else min(best,e)
w=raw_extract(kind,d,b);obj=None if w is None else source(kind,d,w)
accepted+=extract(kind,d,b,q) is not None
if obj is None:
if q['bound'] is None:assert e+q['constant']>q['upper'],(kind,d,b,e,q)
else:assert e>q['bound'],(kind,d,b,e,q)
else:
# An invalid tournament/row can decode coincidentally; equality certificate
# must still agree with exact reverse encoding.
canonical=encode_cached(kind,d,w,N)
if list(b)!=canonical:
assert extract(kind,d,b,q) is None,(kind,d,b,w)
else:assert e+q['constant']==obj,(kind,d,b,e,obj)
COUNTS['bitstrings']+=1;BY_KIND[kind]['bitstrings']+=1
if N<=9:
if q['bound'] is not None:assert (best<=q['bound'])==(valid>0)
else:assert (best+q['constant'] if q['lower']<=best+q['constant']<=q['upper'] else None)==opt
COUNTS['instances']+=1;BY_KIND[kind]['instances']+=1
return q
def encode_cached(kind,d,w,N):
# Same independently specified encoding, with cached allocation count.
if kind in ('weighted','ranking'):
pos=w if kind=='ranking' else [w.index(i) for i in range(len(w))]
return [int(pos[i]<pos[j]) for i,j in pairs(len(w))]
b=[0]*N
if kind in ('tardy','qap','squares','arrangement'):
pos=[w.index(i) for i in range(len(w))] if kind=='tardy' else w
k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else len(w)
for i,p in enumerate(pos):b[i*k+p]=1
elif kind=='intervals':
off=0
for row,p in zip(domain(d),w):b[off+p]=1;off+=len(row)
else:
t,h=len(d['b']),len(d['a'][0]) if d['a'] else 0
b=[w[(i*t+j)*h+p] for i,j,p in eligible(d)]
return b
def generated(kind,n,rng):
prec=lambda:[(rng.randrange(n),rng.randrange(n)) for _ in range(rng.randrange(4))] if n else []
matrix=lambda r,c:[[rng.randint(-3,3) for _ in range(c)] for _ in range(r)]
if kind=='weighted':return {'p':[rng.randint(-3,3) for _ in range(n)],'w':[rng.randint(-3,3) for _ in range(n)],'prec':prec()}
if kind=='ranking':
M=matrix(n,n);total=rng.randint(-3,3)
for i,j in pairs(n):M[j][i]=total-M[i][j]
return {'M':M}
if kind=='tardy':return {'d':[rng.randint(-1,n+1) for _ in range(n)],'prec':prec()}
if kind=='qap':
m=n+rng.randrange(2);return {'C':matrix(n,n),'D':matrix(m,m)}
if kind=='squares':return {'s':[rng.randint(1,5) for _ in range(n)],'k':rng.randint(1,n)}
if kind=='arrangement':return {'n':n,'edges':[(rng.randrange(n),rng.randrange(n)) for _ in range(rng.randrange(2*n+1))] if n else []}
if kind=='intervals':
r=[rng.randrange(4) for _ in range(n)];l=[rng.randrange(3) for _ in range(n)]
return {'r':r,'l':l,'d':[max(0,a+b+rng.randint(-2,1)) for a,b in zip(r,l)]}
c,t,h=(n,1,n) if rng.randrange(2) else (1,n,n)
return {'R':[[rng.choice([-1,0,1,1,1,2]) for _ in range(t)] for _ in range(c)],'a':[[bool(rng.randrange(2)) for _ in range(h)] for _ in range(c)],'b':[[bool(rng.randrange(2)) for _ in range(h)] for _ in range(t)]}
def symbolic():
import sympy as s
n,k,m,S,A=s.symbols('n k m S A',integer=True,nonnegative=True)
assert s.expand(3*n*(n-1)*(n-2)/6-n*(n-1)*(n-2)/2)==0
assert s.expand(n*k*(k-1)/2+k*n*(n-1)/2-n*k*(n+k-2)/2)==0
x,y,z=s.symbols('x y z')
triangle=z+x*y-x*z-y*z
assert [triangle.subs(dict(zip((x,y,z),b))) for b in it.product((0,1),repeat=3)]==[0,1,0,0,0,0,1,0]
for N in range(7):
xs=s.symbols('x:'+str(N));r=s.symbols('r');poly=s.Poly(s.expand((sum(xs)-r)**2),*xs,r)
actual=0
for exps,coef in poly.terms():actual+=coef*s.prod(v**min(e,1) for v,e in zip(xs,exps[:-1]))*r**exps[-1]
expected=r*r+(1-2*r)*sum(xs)+2*sum(a*b for a,b in it.combinations(xs,2))
assert s.expand(actual-expected)==0
for N in range(6):
ps=pairs(N);ids={p:i for i,p in enumerate(ps)};couplings=[]
for i,j,k in it.combinations(range(N),3):couplings.extend(pairs_of_three(ids[i,j],ids[i,k],ids[j,k]))
assert len(couplings)==len(set(couplings))==3*math.comb(N,3)
for bits in (n*n,n*m,n*k,S,A):
assert s.expand(bits*(bits-1)/2-s.binomial(bits,2).expand(func=True))==0
COUNTS['symbolic_identities']=15
def pairs_of_three(a,b,c):return [tuple(sorted(p)) for p in ((a,b),(a,c),(b,c))]
def hypothesis_checks():
from hypothesis import given,settings,strategies as st,HealthCheck
settings.register_profile('independent',max_examples=10000,deadline=None,database=None,derandomize=True,suppress_health_check=[HealthCheck.too_slow]);settings.load_profile('independent')
@given(st.lists(st.integers(-1000,1000),min_size=1,max_size=8),st.lists(st.booleans(),min_size=8,max_size=8),st.integers(-1000,1000))
def weighted_square(weights,bits,target):
bits=bits[:len(weights)];observed=(sum(w*b for w,b in zip(weights,bits))-target)**2
expanded=target**2+sum((w*w-2*target*w)*b for w,b in zip(weights,bits))+sum(2*weights[i]*weights[j]*bits[i]*bits[j] for i,j in pairs(len(weights)))
assert observed==expanded;COUNTS['hypothesis_square']=COUNTS['hypothesis_square']+1
@given(st.lists(st.tuples(st.integers(-1000,1000),st.integers(-1000,1000)),min_size=1,max_size=6),st.permutations(range(6)))
def completion_pair(data,order):
n=len(data);order=[i for i in order if i<n];p,w=zip(*data);pos={a:i for i,a in enumerate(order)}
direct=sum(w[a]*sum(p[b] for b in order[:i+1]) for i,a in enumerate(order))
expanded=sum(p[i]*w[i] for i in range(n))+sum(p[i]*w[j] if pos[i]<pos[j] else p[j]*w[i] for i,j in pairs(n))
assert direct==expanded;COUNTS['hypothesis_completion']=COUNTS['hypothesis_completion']+1
weighted_square();completion_pair()
def tiny_exhaustive(rng):
# Exhaust finite input alphabets, then every target bitstring (at most 4).
for pw in it.product((-1,0,1),repeat=4):
for ps in ([],[(0,1)],[(1,0)],[(0,0)],[(0,1),(1,0)],[(0,1),(0,1)]):check('weighted',{'p':list(pw[:2]),'w':list(pw[2:]),'prec':ps},rng)
for ds in it.product((-1,0,1,2,3),repeat=2):
for ps in ([],[(0,1)],[(1,0)],[(0,0)],[(0,1),(1,0)]):check('tardy',{'d':list(ds),'prec':ps},rng)
for total,a in it.product(range(-2,3),repeat=2):check('ranking',{'M':[[0,a],[total-a,0]]},rng)
for cv,dv in it.product(it.product((-1,0,1),repeat=2),repeat=2):check('qap',{'C':[[1,cv[0]],[cv[1],-1]],'D':[[1,dv[0]],[dv[1],-1]]},rng)
for sizes in it.product((1,2,3),repeat=2):
for k in (1,2):check('squares',{'s':list(sizes),'k':k},rng)
edges=[(0,0),(0,1),(1,1)]
for mult in it.product((0,1,2),repeat=3):check('arrangement',{'n':2,'edges':[e for e,c in zip(edges,mult) for _ in range(c)]},rng)
tasks=list(it.product((0,1),(0,1,2),(0,1)))
for rows in it.product(tasks,repeat=2):
r,d,l=zip(*rows);check('intervals',{'r':r,'d':d,'l':l},rng)
for av in it.product((False,True),repeat=4):
for req in range(-1,4):check('timetable',{'R':[[req]],'a':[list(av[:2])],'b':[list(av[2:])]},rng)
def guaranteed_feasible(rng):
# Exercise nonvacuous feasibility in each larger dimension, independently
# constructing source schedules first and deriving their requirements.
for n in range(1,6):
for _ in range(300):
lengths=[rng.randrange(3) for _ in range(n)];release=[];clock=0
for length in lengths:release.append(clock);clock+=length+1
check('intervals',{'r':release,'l':lengths,'d':[r+l+rng.randrange(2) for r,l in zip(release,lengths)]},rng)
c,t,h=(n,2,2) if _%3==0 else (2,n,2) if _%3==1 else (2,2,n)
a=[[bool(rng.randrange(2)) for p in range(h)] for i in range(c)]
b=[[bool(rng.randrange(2)) for p in range(h)] for j in range(t)]
R=[[0]*t for i in range(c)]
for p in range(h):
cs=[i for i in range(c) if a[i][p]];ts=[j for j in range(t) if b[j][p]];rng.shuffle(cs);rng.shuffle(ts)
for i,j in zip(cs,ts):
if rng.randrange(2):R[i][j]+=1
check('timetable',{'R':R,'a':a,'b':b},rng)
for kind,d in [('weighted',{'p':[],'w':[]}),('ranking',{'M':[]}),('tardy',{'d':[]}),('qap',{'C':[],'D':[]}),('arrangement',{'n':0,'edges':[]}),('intervals',{'r':[],'d':[],'l':[]}),('timetable',{'R':[],'a':[],'b':[]}),('timetable',{'R':[[0]],'a':[[]],'b':[[]]}),('timetable',{'R':[[1]],'a':[[]],'b':[[]]})]:check(kind,d,rng)
def examples(rng):
cases={
'weighted':{'p':[1,1,1],'w':[1,2,3]},
'ranking':{'M':[[0,1,2],[3,0,1],[2,3,0]]},
'tardy':{'d':[1,2,3],'prec':[(0,1)]},
'qap':{'C':[[int(i!=j) for j in range(3)] for i in range(3)],'D':[[int(i!=j) for j in range(3)] for i in range(3)]},
'squares':{'s':[1,1,1],'k':1},'arrangement':{'n':3,'edges':[(0,1),(1,2)]},
'intervals':{'r':[0,1,2],'d':[1,2,3],'l':[1,1,1]},
'timetable':{'R':[[1],[1],[1]],'a':[[True,False,False],[False,True,False],[False,False,True]],'b':[[True,True,True]]}}
expected={'weighted':(10,14,10,10),'ranking':(4,8,4,4),'tardy':(0,3,24,0),'qap':(0,36,111,6),'squares':(0,9,30,9),'arrangement':(0,16,102,2),'intervals':(0,0,3,0),'timetable':(0,0,3,0)}
result={}
for kind,d in cases.items():
q=check(kind,d,rng);L,U,C,opt=expected[kind];best=min(energy(q,b) for b in it.product((0,1),repeat=q['n']))
assert (q['lower'],q['upper'],q['constant'],best+C)==(L,U,C,opt)
result[kind]={'lower':L,'upper':U,'constant':C,'minimum_Q':best,'recovered':best+C}
for kind in ('weighted','tardy','intervals','timetable'):
d=json.loads(json.dumps(cases[kind]))
if kind=='weighted':d['prec']=[(0,1),(1,2),(2,0)]
elif kind=='tardy':d['prec'].append((1,0))
elif kind=='intervals':d['r']=[0]*3;d['d']=[1]*3
else:d['a']=[[True,False,False]]*3
q=check(kind,d,rng);assert not any(source(kind,d,w) is not None for w in witnesses(kind,d))
result[kind+'_NO']={'minimum_Q':min(energy(q,b) for b in it.product((0,1),repeat=q['n'])),'bound':q['bound'],'constant':q['constant']}
return result
def rejected_examples():
cases={'ranking':{'M':[[0,1,2],[3,0,1],[2,3,0]]},'qap':{'C':[[int(i!=j) for j in range(3)] for i in range(3)],'D':[[int(i!=j) for j in range(3)] for i in range(3)]},'squares':{'s':[1,1,1],'k':1},'arrangement':{'n':3,'edges':[(0,1),(1,2)]},'timetable_negative':{'R':[[-1,1]],'a':[[True]*3],'b':[[True]*3,[True]*3]},'timetable_excess':{'R':[[4,1]],'a':[[True]*3],'b':[[True]*3,[True]*3]}}
result={}
for name,d in cases.items():
kind=name.split('_')[0];q=reduce(kind,d);b=[1,0,1] if kind=='ranking' else [0]*q['n']
assert extract(kind,d,b,q) is None
assert extract(kind,d,b+[0],q) is None
assert extract(kind,d,[-1]+b[1:],q) is None
result[name]={'bits':b,'Q':energy(q,b),'F':energy(q,b)+q['constant'],'U':q['upper'],'bound':q['bound'],'constant':q['constant']}
return result
if __name__=='__main__':
rng=random.Random(20261022);symbolic();print('symbolic passed',flush=True);hypothesis_checks();print('hypothesis passed',dict(COUNTS),flush=True)
tiny_exhaustive(rng);print('tiny exhaustive passed',dict(COUNTS),flush=True);worked=examples(rng)
for kind in DATA_FIELDS:
for n in range(1,6):
for _ in range(300):check(kind,generated(kind,n,rng),rng)
print(kind,n,dict(BY_KIND[kind]),flush=True)
guaranteed_feasible(rng)
report={'result':'PASS','counts':dict(COUNTS),'by_kind':{k:dict(v) for k,v in BY_KIND.items()},'worked_examples':worked,'rejected_targets':rejected_examples(),'guaranteed_feasible_extra_per_n':{'intervals':300,'timetable':300},'edge_case_instances':9,'sampled_instances_per_kind_per_n':300,'dimensions':list(range(1,6)),'limitations':['Mathematical integers only; does not validate i64 checked arithmetic implementation.','All valid assignments enumerated per generated instance; target strings exhaustive through 9 bits, 22 sampled above 9 bits.','Finite input alphabets exhausted only in bounded-small cases; larger dimensions sampled.','Ranking, QAP, Squares, Arrangement source NO cases impossible under proof domains.'],'data_fields':DATA_FIELDS}
Path(__file__).with_name('adversary-report.json').write_text(json.dumps(report,indent=2)+'\n');print(json.dumps(report,indent=2))crosscheck.pyimport json,itertools as it
from pathlib import Path
import constructor as c
import adversary as a
base=Path(__file__).parent
cases=json.loads((base/'constructor-cases.json').read_text());cross=forward=0
for kind,d,q in cases:
aq=a.reduce(kind,d)
assert q==aq,(kind,d,q,aq)
cross+=1
if kind not in ['weighted','ranking','tardy','qap','squares','arrangement']:continue
n=len(d['p']) if kind=='weighted' else len(d['M']) if kind=='ranking' else len(d['d']) if kind=='tardy' else len(d['C']) if kind=='qap' else len(d['s']) if kind=='squares' else d['n']
k=len(d['D']) if kind=='qap' else d['k'] if kind=='squares' else n
assignments=it.product(range(k),repeat=n) if kind=='squares' else it.permutations(range(k),n)
for z in assignments:
val=c.source(kind,d,z)
if val is None:continue
if kind in ['weighted','ranking']:
ranks=z if kind=='ranking' else [z.index(i) for i in range(n)]
x=[int(ranks[i]<ranks[j]) for i,j in it.combinations(range(n),2)]
else:
cols=[z.index(i) for i in range(n)] if kind=='tardy' else z
x=[int(cols[i]==p) for i in range(n) for p in range(k)]
F=q['constant']+sum(v*x[i]*x[j] for i,j,v in q['q'])
assert F==val and q['lower']<=F<=q['upper'];forward+=1
print(json.dumps(dict(cross=cross,forward=forward,disagreements=0)))
(base/'crosscheck-report.json').write_text(json.dumps(dict(cross=cross,forward=forward,disagreements=0)))examples_check.pyfrom constructor import reduce,source,decode
from itertools import product
cases=[('weighted',dict(p=[1]*3,w=[1,2,3],prec=[]),[0]*3,10,10,14),('ranking',dict(M=[[0,1,2],[3,0,1],[2,3,0]]),[0]*3,4,4,8),('tardy',dict(d=[1,2,3],prec=[(0,1)]),[1,0,0,0,1,0,0,0,1],0,24,3),('qap',dict(C=[[0,1,1],[1,0,1],[1,1,0]],D=[[0,1,1],[1,0,1],[1,1,0]]),[1,0,0,0,1,0,0,0,1],6,111,36),('squares',dict(s=[1]*3,k=1),[1]*3,9,30,9),('arrangement',dict(n=3,edges=[(0,1),(1,2)]),[1,0,0,0,1,0,0,0,1],2,102,16),('intervals',dict(r=[0,1,2],d=[1,2,3],l=[1]*3),[1]*3,0,3,0),('timetable',dict(R=[[1]]*3,a=[[1,0,0],[0,1,0],[0,0,1]],b=[[1]*3]),[1]*3,0,3,0)]
for kind,d,x,v,C,U in cases:
q=reduce(kind,d);assert q['constant']==C and q['upper']==U
assert C+sum(w*x[a]*x[b] for a,b,w in q['q'])==v
assert source(kind,d,decode(kind,d,x))==v
no=[('weighted',dict(p=[1]*3,w=[1,2,3],prec=[(0,1),(1,2),(2,0)])),('tardy',dict(d=[1,2,3],prec=[(0,1),(1,0)])),('intervals',dict(r=[0]*3,d=[1]*3,l=[1]*3)),('timetable',dict(R=[[1]]*3,a=[[1,0,0]]*3,b=[[1]*3]))]
for kind,d in no:
q=reduce(kind,d)
assert min(q['constant']+sum(w*x[a]*x[b] for a,b,w in q['q']) for x in product([0,1],repeat=q['n']))>q['upper']
print('8 worked YES and 4 source NO examples reproduced; always-feasible types have no source NO instances') |
Agentic Review ReportInitial review: Structural and semanticAll eight exact variant edges, witness/value registrations, canonical examples, and paper proofs are present. Existing ILP edits only disambiguate trait methods. No generated exports or unrelated core changes appear in this diff. I traced the tournament, permutation/injection, group-square, start-slot, and timetable constructions against their source evaluators. The mathematical penalty separation and declared variable/coupling bounds are sound. Generic parameter-formula validation discovers the new rules through their canonical sources. QualityThe committed tests exhaust target bitstrings on small instances and now independently brute-force source optima/feasibility. They cover signed data, empty inputs, impossible windows/demands, precedence cycles, malformed witness lengths, and coefficient overflows. Follow-up tests add a five-task case with overlapping tournament triangles and regressions for each numerical failure mechanism found below. I reviewed the source-arithmetic bounds and the regressions; the implementation preserves the source evaluator's checked integer contract. The implementer reports Feature testIndependently exercised FindingsResolved Important finding — Source arithmetic could overflow after the new target certified a finite optimum. Locations: At the initial reviewed commit, the builder checked the expanded/combined QUBO arithmetic, but that did not establish that the original source evaluator can compute the recovered objective. Eliminated elapsed times or cancellation of directed costs can hide an overflow in the source's checked
For either instance, reproduce by creating it, selecting the one-step route from Additional boundary checks isolated two weighted-completion failures: (a) lengths Resolution verified: weighted completion now checks the signed elapsed-time bounds, each weighted-completion range, and partial objective sums before constructing the target. QAP checks each directed product and bounds accumulation before coefficient cancellation. All four reproductions now fail at Final verdict: no unresolved Critical, Important, or Minor findings. The initial numerical finding is resolved in |
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
left a comment
GiggleLiu
left a comment
There was a problem hiding this comment.
Agentic Review Report
PR #1214: Add Phase 1 direct QUBO encodings for scheduling and assignment
Review date: 2026-10-29. Fresh-context read-only review of 55823fbc894647fa83cfc70b7c60bca6bcba673e...37aa87857bb278364800e0902938065f4916a9aa. Used the PR's own stack base, not origin/main. Local implementation evidence is diff-1214.patch; GitHub context is context-1214.txt in this directory.
Verdict: HOLD — a valid interval-scheduling source can panic during reduction.
Structural and semantic review
Reviewed the eight new direct encodings, shared QUBO helpers, registrations, model parameter additions, existing ILP call-site adjustments, tests, and manual proofs against this PR's own base. No unrelated trait or macro changes or generated exports were found. The helper validates target witnesses before decoding; it accumulates coefficients in widened arithmetic, checks coefficient prefixes, and retains the source objective shift for optimization reductions.
The scheduling/ranking tournament has n(n−1)/2 variables. Its triangle penalty is x_ik + x_ijx_jk − x_ijx_ik − x_jk*x_ik, zero exactly for transitive triples. Weighted completion includes the diagonal processing cost and one of the two pair costs for each unordered pair; ranking uses the analogous pairwise matrix cost. Penalties exceed the complete objective range, including signed weights. Unit tardiness and original linear arrangement use permutation matrices. Quadratic assignment uses facility one-hot rows and location at-most-one products and retains both directed matrix entries. Sum-of-squares partition expands group sums with one-hot item rows. Interval scheduling has one variable per admissible start and penalizes pairs whose half-open intervals overlap. Timetable design encodes required counts and resource conflicts and creates an explicit NO target for invalid demand.
Derived variable and coupling counts from the constructed supports, rather than treating examples as proof. Signed/asymmetric costs, empty inputs, impossible windows, duplicate precedence constraints, self precedence, zero-duration tasks, and source arithmetic prefixes were traced. The mathematical encodings appear sound within their numeric range; the unchecked allocation below violates the error contract.
Quality review
The new tests cover source-versus-target exhaustive optima, invalid witnesses, signed values, zero/empty/infeasible cases, and coefficient overflow. A missing allocation boundary case is material: an accepted source can represent more start tuples than a Vec can hold, even though its start count fits usize. This case must return a typed error before allocation.
Feature tests and verification limits
Executed the retained rule tests using the compiled #1218 descendant test binary: direct_qubo --test-threads=2 passed 44 tests; staffscheduling_qubo --test-threads=2 passed 4 tests. The seven retained #1214 encodings and the helper methods they call are unchanged in that descendant; the helper file later adds an unrelated affine-square method. The original #1214 permutation-matrix OLA was reviewed statically; its descendant test/CLI result exercises the replacement in #1217.
Using the copied #1218 CLI, completed list --rules, show, create --example --to, inspect, direct path, reduce, and brute-force source and bundle solves for all eight source types. Extracted source evaluations matched direct brute force. The OLA result is explicitly the later replacement. Canonical results are smoke tests, not completeness proofs.
The interval allocation failure was independently reproduced with the #1218 CLI and a native path-dependency probe against exact #1224, where the relevant reducer is unchanged from #1214. Source evaluation returns Or(true); reduction exits 101 with capacity overflow.
Findings (severity order)
Critical — checked allocation contract is violated
src/rules/sequencingwithinintervals_qubo.rs:43 allocates Vec<(usize, i64, i64)> using the accepted number of starts without checking the byte capacity.
Concrete source:
{"type":"SequencingWithinIntervals","variant":{},"data":{"release_times":[0],"deadlines":[9223372036854775806],"lengths":[0]}}The source accepts this one-task instance and evaluates witness [0] as Or(true). There are 9,223,372,036,854,775,807 admissible starts, a valid usize on the supported 64-bit host. The tuple allocation exceeds isize::MAX bytes and panics immediately:
thread 'main' panicked at .../alloc/src/raw_vec/mod.rs:28:5:
capacity overflow
This is an arithmetic capacity failure, not a test that exhausts machine memory. Check derived allocation byte sizes with checked arithmetic and return ReductionError before allocation, including the later per-row index collection. The later Phase 3 StartChoices helper provides an existing pattern. Add this accepted-source regression.
Artifacts: interval-overflow-source.json, interval-overflow-route.json, interval-overflow-evaluate.txt, interval-overflow-reduce.txt, and numeric-probe.log in this report directory.
GitHub PR Audit — #1214
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.
There was a problem hiding this comment.
The allocation blocker is fixed at 2226ebec41c2dab0071179bde304e516234ace9f. The reduction validates the derived tuple layout before allocating; that also bounds each smaller per-task index array. Independent review, all 17 direct-QUBO tests, make check (7,102 tests plus formatting and Clippy), and CLI overflow/boundary regressions pass. The huge valid source now returns typed IntegerOverflow instead of panicking; schedules ending at i64::MAX still round-trip. This PR targets a feature branch, which does not trigger CI. The combined stack will receive fresh required CI against main before landing.
[Critical] Remove KSatisfiability KN variant and short-clause constructors
Declare exact parameter counts that constructions always produce
Tighten ILP num_nonzeros bounds to per-constraint counts
Tighten StaffScheduling and SWRTD QUBO size bounds
Add binary decision ILP to SAT and fix solution validators
Add staff-scheduling QUBO and tighten direct-reduction bounds
Add Phase 3 conditional direct QUBO reductions
Add Phase 2 direct QUBO reductions
GiggleLiu
left a comment
GiggleLiu
left a comment
There was a problem hiding this comment.
Agentic Review Report: stack consolidation
Approved current head 004ad174c12d9edf8d66de8c74db7fe72a9e533c for merging into fix/simultaneous-incongruences-complexity 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.
Adds the eight Phase 1 direct QUBO rules from #1213, removing the need to route these models through generic ILP penalty encoding. This draft is stacked on #1212 (
fix/simultaneous-incongruences-complexity); the diff is relative to that branch.The rules build sparse integer polynomials, check source-evaluation, coefficient, and energy-bound arithmetic, and register both witness extraction and completed-value recovery. Invalid penalized assignments are rejected; infeasible precedence systems recover
Min(None). Each rule includes parameter bounds, a canonical example, and a proof in the manual. Existing ILP helper calls are explicitly target-qualified where the new trait implementations make inference ambiguous.For example, the existing 3-facility/3-location QAP ILP constructor allocates 9 assignment variables plus 54 product variables before conversion to QUBO (source-based comparison). The new rule uses 9 QUBO bits; the canonical instance recovers objective 6. This demonstrates logical-variable savings, not measured annealer performance.
The simplification pass removes duplicate square-matrix dimensions and temporary decoding vectors, and skips insertion of zero coefficients into the sparse accumulator. These cleanups preserve encoding and recovery semantics. Fresh review also found that algebraic cancellation could hide overflow in source evaluation. Conservative bounds now reject those weighted-completion and QAP inputs before producing a target; regression tests first reproduced elapsed-time, weighted-product, partial-objective-sum, and directed-cost-sum overflow.
Validation:
make check: 7,100 tests passed, plus formatting and workspace/all-feature Clippy. Repeated after simplification and the review fix.make paper: compiled without warnings. Repeated after simplification and the review fix.The interval encoding is pseudopolynomial in the time horizon. Unrepresentable derived integer coefficients or bounds produce typed errors. No annealer hardware or embedding benchmark was run.
Repository CI currently triggers only for PRs targeting
mainordevelop, so this stacked base does not automatically trigger those workflows. Keep this PR in draft; #1213 remains open for later phases.