Repository navigation
Add staff-scheduling QUBO and tighten direct-reduction bounds - #1217
Merged
GiggleLiu merged 25 commits intoOct 29, 2026
Merged
Conversation
Collaborator
Author
Verification certificateVERIFIED — StaffScheduling → DecisionQUBO. Mathematical construction was independently checked before production registration; production output is subsequently compared exactly with that prototype. Constructor and proof-only fresh-context adversary passed, with 124 shared target polynomials and 0 disagreements. Type resolution
::Solution=P::Solution, Value=Or. Thus source Or→target Or, with identity completed decision recovery. The source is not Boolean schedule selection and is not an optimization problem. Independent evidence
Constructor audit: {
"seed": 4412026,
"counts": {
"symbolic": 133,
"size": 23748,
"structure": 167202,
"forward_backward": 45085,
"extraction": 54675,
"yes_example": 2,
"no_example": 2
},
"total": 290847
}Adversary audit: {
"verdict": "PASS",
"counts": {
"exhaustive_bounded_block_ranges": 257,
"multiplicity_and_nonunique_encoding": 2,
"worked_example_assignments": 2304,
"source_target_decisions": 7086,
"forward_backward_witnesses": 2088,
"size_and_coefficient_bounds": 3605,
"assignment_identity_and_extraction": 51400,
"malformed_target_rejections": 16,
"unsatisfying_extraction_rejections": 2303,
"dedicated_degenerate_cases": 8,
"early_no": 3481,
"malformed_source_rejections": 6,
"sympy_polynomial_identities": 3,
"independent_diagonal_bounds": 10416,
"i128_product_bound_checks": 2,
"large_block_weight_bounds": 9,
"random_evaluation_prefix_orders": 1000,
"typed_arithmetic_rejections": 5,
"negative_requirement_boundaries": 4,
"composition_feasible_count_witnesses": 166,
"exact_cover_staff_qubo_composition": 120,
"hypothesis_general": 200,
"hypothesis_planted": 200
},
"arithmetic_boundaries": {
"safe_budget_for_separate_sum_guard": 2322860046,
"next_rejected_budget": 2322860047,
"safe_negative_sum": 9223372032470907730,
"unsafe_negative_sum": 9223372041411595117,
"sqrt_i64_max": 3037000499
},
"shared_instances": 124,
"seed": 20261022,
"limits": [
"Finite base family has W in {0,1,2}, requirements in {-1,0,1,2}, ordered duplicate-permitting uniform-k patterns.",
"All (s,p) in 0..5 covered; families of at most 300 instances exhausted, others have 300 distinct seeded samples.",
"Hypothesis adds W through 6; arbitrary i64 coefficient bounds are algebraic, boundary checks finite.",
"No repository code, prototype, or shared corpus was read; this validates the proof and independent reference only.",
"Exact-cover composition is independently modeled mathematically; no repository graph dispatch was exercised.",
"No real allocation exhaustion, usize overflow, Rust serialization, or implementation error types were exercised."
]
}Claims and evidence categories
Raw solves: 219/219 proven decisions under 15 s/one-worker/linearization2, no timeout. Oracle/constructor checks: the checks above construct some target witnesses from independent source witnesses and inspect residual identities; they are not counted as raw solves. Coefficient checks: 124 constructor–adversary structural agreements, then219 production–prototype agreements; these are also not raw solves. Per-case raw table and baseline audit are posted separately. Corpus integrity:32,372 files before/after,0 changed/added/removed. Typst proof#set page(margin: 20mm)
#set text(size: 10pt)
= Bounded staffing counts to Decision QUBO
*Theorem.* For the exact StaffScheduling constructor described below, the following finite quadratic Boolean construction preserves feasibility, recovers every satisfying target witness, and maps completed decision values identically. Integer arithmetic that cannot be represented by the implementation must return a typed reduction overflow, before returning a target. This is not a positive-requirement-only or Boolean-worker variant.
== Source and endpoint contract
There are $s$ schedule patterns $A_j in {0,1}^p$, each with exactly $k$ active periods. Duplicate patterns are permitted. Each requirement $r_u$ is any signed i64 integer. The budget $W$ is a nonnegative i64 integer, with $W+1$ representable as usize. Empty patterns, empty periods, zero budget, empty schedule collection, and arbitrary $k$ when there are no patterns are accepted. The witness is the length-$s$ vector of integer multiplicities $c_j in [0,W]$. The evaluator first checks the witness length, then each coordinate bound, then checked i64 total worker count, and only if the budget is satisfied, checked period coverage. It accepts exactly when $sum_j c_j <= W$ and $sum_j A_(j,u)c_j >= r_u$ for every period. Negative requirements impose no condition because coverage is nonnegative. Type resolution is StaffScheduling.Value = Or, Decision(QUBO(i64)).Value = Or, and QUBO(i64).Value = Min(i64).
== Construction
1. For each integer $B >= 0$, define $b(B)=ceil(log_2(B+1))$ with $b(0)=0$. If $b>0$, take weights $1,2,...,2^(b-2),B-(2^(b-1)-1)$. Their sum is exactly $B$, each is positive, and their subset sums cover every integer from zero through $B$. The last weight is at most $2^(b-1)$; the preceding weights cover $[0,2^(b-1)-1]$, so the intervals with and without the last weight overlap or touch. Encoding is generally nonunique; extraction returns the weighted sum, never an index.
2. If any $r_u>W$, return a zero-variable target polynomial $Q=0$ with bound $-1$. Every period has coverage at most total workers, so the source is NO. Extraction cannot succeed.
3. Otherwise allocate a bounded binary block for each $c_j in [0,W]$, followed by a budget slack block $z in [0,W]$. For each positive requirement allocate surplus $h_u in [0,W-r_u]$. Nonpositive requirement rows are omitted.
4. Define the nonnegative integer polynomial
$ F = (sum_j c_j + z - W)^2 + sum_(u:r_u>0) (sum_j A_(j,u)c_j - h_u-r_u)^2. $
Every encoded variable here is a linear weighted sum of its own Boolean block. Expand using $x_i^2=x_i$ and combine coefficients for unordered pairs. The omitted constant is $C=W^2+sum_(u:r_u>0)r_u^2$. The actual QUBO has energy $Q=F-C$ and the Decision bound is $-C$. Penalty weight is exactly one; integer residual squares separate YES energy zero from every violation by at least one. There is no optimization surrogate or supplied optimum bound.
== Correctness
*Forward.* A source witness obeys total workers at most $W$. Choose $z=W-sum_j c_j$, within $[0,W]$. Each positive requirement has coverage between $r_u$ and $W$, so choose $h_u="coverage"_u-r_u$ within its block's range. Every block has a representing bitstring by the interval argument. Every residual vanishes, hence $F=0$ and $Q=-C$ satisfies the target threshold.
*Backward.* Every Boolean block decodes within its prescribed finite range. If the target accepts, $Q<=-C$, so $F<=0$. All residuals are nonnegative integer squares; each must vanish. The budget equality implies $sum c_j=W-z<=W$. The positive coverage equalities imply $"coverage"_u=r_u+h_u>=r_u$. All omitted nonpositive requirements hold because coverage is nonnegative. Thus the decoded count vector satisfies the original source. The case $r_u>W$ cannot yield a target witness.
*Witness extraction.* Validate the target configuration length and Boolean domain, evaluate its actual emitted polynomial once, and reject unless its Decision value is true. Decode just the $s$ count blocks by checked integer weighted sums. Budget and coverage then bound every source addition by $W$, so evaluation of the recovered witness cannot overflow. Reject malformed target lengths or unsatisfying target assignments; never repair a bitstring or reduce a count modulo a bound.
*Completed result.* Both endpoints are decision problems; completed Or(false) and Or(true) map identically. No source witness is extracted from a completed NO result. Along ExactCoverBy3Sets to StaffScheduling, the existing count-to-selected-set map and identity aggregate map compose. Its budget $q$ and $3q$ unit requirements force exactly $q$ workers with no overlaps, hence all selected multiplicities are one. This chain must be solved through its actual QUBO, separately from the already present direct exact-cover QUBO.
== Arithmetic and size
All inputs remain in their constructor domains. Before returning a target, conservatively check $s W<=2^63-1$ so the source's total count fold is safe even on budget-violating coordinate-valid witnesses. Successful witnesses have the stronger bound $W$ for both total and coverage. Do not take absolute values of negative requirements: they are skipped, including i64::MIN. Every positive $r_u<=W$ and every $W-r_u$ is safe. Zero-variable NO branches may return without arithmetic for unavailable source configurations because they do not certify any witness; the implementation should document the order of guards.
With $p_+$ positive requirements, the precise non-early-return variable count is
$ N=(s+1)b(W)+sum_(u:r_u>0)b(W-r_u). $
Thus $N<=(s+p+1)b(W)<=63(s+p+1)$ for i64 budgets, and $N<=(s+p+1)(W+1)$ is a valid registry upper bound using existing parameters only. Couplings after coefficient cancellation are at most $N(N-1)/2$, or the simpler $N^2$. These are upper bounds, not measured support. Construction uses the sum of squared row widths, at most $(p+1)N^2$ coefficient operations plus $O(s+p)$ row bookkeeping, and $O(p+N+E)$ construction storage. Its bit count is logarithmic in the worker budget; the loose polynomial registry bound must not be mistaken for unary encoding.
For $W>0$, each variable weight is at most $W$. A single residual contributes at most $3W^2$ in absolute diagonal coefficient and $2W^2$ per off-diagonal. A variable appears in at most $p+1$ residuals, so maximum coefficient magnitude is at most $3(p+1)W^2$; the constant is at most $(p+1)W^2$. Ordered-map coefficient updates add a logarithmic lookup factor. The magnitude bit length is at most $ceil(log_2(3(p+1)W^2+1))$. For $W=0$, every block is empty and every permitted residual is zero. Check intermediate coefficient accumulation, the omitted constant, its negative, and separate positive/negative sums of the final polynomial against i64. This last check certifies all target evaluation prefixes, even when combined coefficients have cancellation. i128 products of two i64 weights and twice their product are representable; constants and accumulations narrow only with checked conversions. Checked usize counts and a byte-size guard precede allocation of the budget and coverage rows; source-sized bookkeeping uses the already validated period list. Arithmetic rejection is typed, never wrapping, saturation or constructor-domain modification.
#table(columns: 2,
[Target parameter], [Certified relation],
[num_vars], [$N=(s+1)b(W)+sum_(u:r_u>0)b(W-r_u)<=63(s+p+1)$; early NO gives zero],
[num_quadratic_terms], [$E<=N(N-1)/2<=(63(s+p+1))^2$],
)
== Worked YES
Take three schedules on three periods: $A_0=(1,1,0)$, $A_1=(0,1,1)$, $A_2=(1,0,1)$, $k=2$, $W=3$, requirements $(2,2,2)$. Every count and budget block has weights $(1,2)$; each surplus has weight $(1)$. Thus $N=11$ and $C=9+4+4+4=21$. Counts $(1,1,1)$, slack zero, and all surpluses zero give residuals $(0,0,0,0)$, hence $F=0$ and $Q=-21$. The actual target threshold is $-21$ and extraction returns the three integer counts.
== Worked NO
Use the same three patterns and requirements, but $W=2$. Each count/budget block has weights $(1,1)$, and all surplus bounds are zero, hence $N=8$, $C=4+4+4+4=16$. If every coverage residual vanished, total coverage would be six. Each worker contributes two units, so at least three workers would be required, contradicting the budget two. No target reaches $Q<=-16$. Counts $(1,1,1)$ with budget slack zero yield $F=1$ and $Q=-15$. Nonnegative integer residuals prove this is the minimum and still NO. Multiplicity is essential: with a single all-active pattern, demand two and budget two, count two is required; a Boolean selection cannot represent that YES instance.
Constructor scriptimport json,random,itertools,collections
from pathlib import Path
import sympy as S
from prototypes import staff
OUT=Path(__file__).parent
counts=collections.Counter()
def check(section,condition):
assert condition,section
counts[section]+=1
def valid(d,c):
return len(c)==len(d['schedules']) and all(0<=v<=d['num_workers'] for v in c) and sum(c)<=d['num_workers'] and all(sum(v for v,row in zip(c,d['schedules']) if row[u])>=r for u,r in enumerate(d['requirements']))
def represent(q,d,c):
values=list(c)+[d['num_workers']-sum(c)]+[sum(v for v,row in zip(c,d['schedules']) if row[u])-r for u,r in enumerate(d['requirements']) if r>0]
bounds=[d['num_workers']]*(len(c)+1)+[d['num_workers']-r for r in d['requirements'] if r>0]
bits=[]
for v,B in zip(values,bounds):
weights=[];power=1
while B:w=min(power,B);weights.append(w);B-=w;power*=2
encoded=[0]*len(weights)
for i in reversed(range(len(weights))):
if v>=weights[i]:encoded[i]=1;v-=weights[i]
assert v==0
bits+=encoded
return bits
def inspect(d,exhaust=False):
q=staff(d);s=len(d['schedules']);p=len(d['requirements']);W=d['num_workers']
impossible=any(r>W for r in d['requirements'])
N=0 if impossible else (s+1)*W.bit_length()+sum((W-r).bit_length() for r in d['requirements'] if r>0)
check('size',q.n==N and q.n<=63*(s+p+1) and q.n<=(s+p+1)*(W+1))
check('size',sum(i!=j for i,j in q.q)<=q.n*(q.n-1)//2)
check('structure',all(0<=i<=j<q.n and v!=0 for (i,j),v in q.q.items()))
check('structure',max(map(abs,q.q.values()),default=0)<=3*(p+1)*W*W)
possible=False
for c in itertools.product(range(W+1),repeat=s):
if valid(d,c):
possible=True;b=represent(q,d,c);check('forward_backward',len(b)==q.n and q.energy(b)==0)
check('extraction',[sum(v*b[i] for i,v in row) for row in q.rows]==list(c))
if impossible:check('forward_backward',not possible and q.c==1)
if exhaust:
target_yes=False
for b in itertools.product(range(2),repeat=q.n):
energy=q.energy(b)
check('structure',energy>=0)
if energy==0:
c=[sum(v*b[i] for i,v in row) for row in q.rows]
check('extraction',valid(d,c));target_yes=True
check('forward_backward',possible==target_yes)
else:
for _ in range(12):
b=[R.randrange(2) for _ in range(q.n)]
if impossible:check('structure',q.energy(b)==1);continue
# Check residual identity using independently sliced bounded-weight blocks.
c=[sum(v*b[i] for i,v in row) for row in q.rows]
at=s*W.bit_length();res=[]
for B in [W]+[W-r for r in d['requirements'] if r>0]:
k=B.bit_length();weights=[1<<i for i in range(max(0,k-1))]+([B-((1<<(k-1))-1)] if k else [])
res.append(sum(v*x for v,x in zip(weights,b[at:at+k])));at+=k
expected=(sum(c)+res[0]-W)**2
v=1
for u,r in enumerate(d['requirements']):
if r>0:expected+=(sum(c[j] for j in range(s) if d['schedules'][j][u])-r-res[v])**2;v+=1
check('structure',q.energy(b)==expected)
if expected==0:check('extraction',valid(d,c))
return q
R=random.Random(4412026)
x,y,z,r=S.symbols('x y z r',integer=True)
expanded=S.Poly(S.expand((x*y+z-r)**2),x,z)
check('symbolic',S.expand((x*y+z-r)**2)==x*x*y*y+z*z+r*r+2*x*y*z-2*r*x*y-2*r*z)
# Symbolic certificates for both registered upper bounds, with nonnegative gaps.
s,p,b,delta,N=S.symbols('s p b delta N',nonnegative=True,integer=True)
exact_N=(s+1)*b+p*b-delta
check('symbolic',S.expand((s+p+1)*b-exact_N)==delta)
check('symbolic',S.expand(63*(s+p+1)-exact_N)==S.expand((63-b)*(s+p+1)+delta))
check('symbolic',S.simplify(N*N-N*(N-1)/2)==N*(N+1)/2)
check('symbolic',S.expand((63*(s+p+1))**2-N**2)==S.expand((63*(s+p+1)-N)*(63*(s+p+1)+N)))
for B in range(128):
k=B.bit_length();w=[1<<i for i in range(max(0,k-1))]+([B-((1<<(k-1))-1)] if k else [])
check('symbolic',sum(w)==B and {sum(a*b for a,b in zip(w,t)) for t in itertools.product(range(2),repeat=k)}==set(range(B+1)))
# Exhaust every constant-weight schedule matrix, requirement vector and budget in this finite domain.
for p in range(3):
for s in range(3):
for k in range(p+1):
patterns=[list(t) for t in itertools.product([False,True],repeat=p) if sum(t)==k]
for A in itertools.product(patterns,repeat=s):
for req in itertools.product([-1,0,1,2,3],repeat=p):
for W in range(3):inspect(dict(schedules=list(A),requirements=req,num_workers=W),True)
# 300 source-domain samples per (s,p) through 5, independently enumerate source counts.
for s in range(6):
for p in range(6):
for _ in range(300):
k=R.randrange(p+1);patterns=[list(t) for t in itertools.product([False,True],repeat=p) if sum(t)==k]
inspect(dict(schedules=[R.choice(patterns) for _ in range(s)],requirements=[R.randrange(-2,5) for _ in range(p)],num_workers=R.randrange(4)))
A=[[1,1,0],[0,1,1],[1,0,1]]
for W,E,section in [(3,0,'yes_example'),(2,1,'no_example')]:
d=dict(schedules=A,requirements=[2,2,2],num_workers=W);q=staff(d)
check(section,q.n==(11 if W==3 else 8) and q.c==(21 if W==3 else 16))
check(section,min(q.energy(b) for b in itertools.product(range(2),repeat=q.n))==E)
# Explicit signed-boundary requirements are skipped without absolute-value arithmetic.
q=staff(dict(schedules=[[True]],requirements=[-(1<<63)],num_workers=2))
check('structure',q.n==4 and q.c==4)
(OUT/'constructor-counts.json').write_text(json.dumps(dict(seed=4412026,counts=dict(counts),total=sum(counts.values())),indent=2))
print(dict(counts),sum(counts.values()),flush=True)Independent adversary script"""Independent proof-only checker. No repository or shared-corpus imports."""
import itertools as it
import json
import math
import random
from collections import Counter
from dataclasses import dataclass
from pathlib import Path
import sympy as sp
from hypothesis import given, settings, strategies as st
from ortools.sat.python import cp_model
OUT = Path(__file__).resolve().parent
MAX = 2**63 - 1
MIN = -2**63
COUNTS = Counter()
class Overflow(Exception):
pass
def checked(value):
if not MIN <= value <= MAX:
raise Overflow(value)
return value
@dataclass(frozen=True)
class Instance:
schedules: tuple
requirements: tuple
budget: int
k: int
@property
def s(self):
return len(self.schedules)
@property
def p(self):
return len(self.requirements)
def source(inst, counts):
if len(counts) != inst.s or any(type(c) is not int or c < 0 or c > inst.budget for c in counts):
return False
total = 0
for c in counts:
total = checked(total + c)
if total > inst.budget:
return False
for u, r in enumerate(inst.requirements):
coverage = 0
for row, c in zip(inst.schedules, counts):
if row[u]:
coverage = checked(coverage + c)
if coverage < r:
return False
return True
def source_solve(inst):
# This oracle knows no QUBO variables, row penalties, or slack construction.
for counts in it.product(range(inst.budget + 1), repeat=inst.s):
if source(inst, counts):
return counts
return None
def weights(bound):
n = bound.bit_length()
return tuple(1 << i for i in range(n - 1)) + ((bound - ((1 << (n - 1)) - 1),) if n else ())
@dataclass
class Target:
n: int
coefficients: dict
threshold: int
count_blocks: list
all_blocks: list
rows: list
constant: int
early: bool = False
def build(inst, arithmetic=False):
if any(r > inst.budget for r in inst.requirements):
return Target(0, {}, -1, [], [], [], 0, True)
if arithmetic:
checked(inst.s * inst.budget)
n = 0
blocks = []
def block(bound):
nonlocal n
entries = tuple((n + j, w) for j, w in enumerate(weights(bound)))
n += len(entries)
blocks.append(entries)
return entries
counts = [block(inst.budget) for _ in range(inst.s)]
budget_slack = block(inst.budget)
rows = [(dict(it.chain.from_iterable(counts + [budget_slack])), -inst.budget)]
for u, req in enumerate(inst.requirements):
if req > 0:
terms = dict(it.chain.from_iterable(counts[j] for j in range(inst.s) if inst.schedules[j][u]))
terms.update((i, -w) for i, w in block(inst.budget - req))
rows.append((terms, -req))
polynomial = Counter()
constant = 0
for row, offset in rows:
constant += offset * offset
if arithmetic:
checked(constant)
for i, a in row.items():
polynomial[i, i] += a * a + 2 * a * offset
if arithmetic:
checked(polynomial[i, i])
for (i, a), (j, b) in it.combinations(row.items(), 2):
key = min(i, j), max(i, j)
polynomial[key] += 2 * a * b
if arithmetic:
checked(polynomial[key])
polynomial = {key: v for key, v in sorted(polynomial.items()) if v}
if arithmetic:
checked(-constant)
checked(sum(v for v in polynomial.values() if v > 0))
checked(sum(v for v in polynomial.values() if v < 0))
return Target(n, polynomial, -constant, counts, blocks, rows, constant)
def energy(target, bits, arithmetic=False):
value = 0
for (i, j), coeff in target.coefficients.items():
value += coeff * bits[i] * bits[j]
if arithmetic:
checked(value)
return value
def extract(inst, target, bits):
if len(bits) != target.n or any(type(x) is not int or x not in (0, 1) for x in bits):
return None
if energy(target, bits) > target.threshold:
return None
result = tuple(sum(w * bits[i] for i, w in block) for block in target.count_blocks)
return result
def target_solve(target, minimize=False):
if not target.n:
return (0, ()) if 0 <= target.threshold or minimize else None
model = cp_model.CpModel()
variables = [model.new_bool_var(f'x{i}') for i in range(target.n)]
terms = []
for (i, j), coeff in target.coefficients.items():
if i == j:
variable = variables[i]
else:
variable = model.new_bool_var(f'e{i}_{j}')
model.add_multiplication_equality(variable, [variables[i], variables[j]])
terms.append(coeff * variable)
if minimize:
model.minimize(sum(terms))
else:
model.add(sum(terms) <= target.threshold)
solver = cp_model.CpSolver()
solver.parameters.num_search_workers = 1
solver.parameters.random_seed = 1729
status = solver.solve(model)
assert status in (cp_model.OPTIMAL, cp_model.INFEASIBLE), status
if status == cp_model.INFEASIBLE:
return None
bits = tuple(solver.value(x) for x in variables)
return energy(target, bits), bits
def encode(block, value):
# Explicit subset search, independent of the proof's interval argument.
for bits in it.product((0, 1), repeat=len(block)):
if sum(w * bit for (_, w), bit in zip(block, bits)) == value:
return bits
raise AssertionError((block, value))
def forward(inst, target, counts):
values = list(counts) + [inst.budget - sum(counts)]
values += [sum(row[u] * c for row, c in zip(inst.schedules, counts)) - req
for u, req in enumerate(inst.requirements) if req > 0]
return tuple(it.chain.from_iterable(encode(block, value) for block, value in zip(target.all_blocks, values)))
def check_instance(inst, rng, export=False):
target = build(inst, arithmetic=True)
witness = source_solve(inst)
solution = target_solve(target)
assert (witness is not None) == (solution is not None), (inst, witness, solution)
COUNTS['source_target_decisions'] += 1
if solution is not None:
recovered = extract(inst, target, solution[1])
assert recovered is not None and source(inst, recovered)
bits = forward(inst, target, witness)
assert energy(target, bits, True) == target.threshold
assert extract(inst, target, bits) == witness
COUNTS['forward_backward_witnesses'] += 1
if not target.early:
expected_n = (inst.s + 1) * inst.budget.bit_length() + sum((inst.budget - r).bit_length() for r in inst.requirements if r > 0)
assert target.n == expected_n
assert target.n <= (inst.s + inst.p + 1) * inst.budget.bit_length()
assert target.n <= (inst.s + inst.p + 1) * (inst.budget + 1)
assert sum(i != j for i, j in target.coefficients) <= target.n * (target.n - 1) // 2
bound = 3 * (inst.p + 1) * inst.budget**2
assert max(map(abs, target.coefficients.values()), default=0) <= bound
assert target.constant <= (inst.p + 1) * inst.budget**2
COUNTS['size_and_coefficient_bounds'] += 1
assignments = it.product((0, 1), repeat=target.n) if target.n <= 6 else [tuple(rng.randrange(2) for _ in range(target.n)) for _ in range(4)]
for bits in assignments:
residual_squares = (sum(bits[i] * a for i, a in row.items()) + offset for row, offset in target.rows)
f = sum(x * x for x in residual_squares)
assert energy(target, bits, True) + target.constant == f
recovered = extract(inst, target, bits)
assert (recovered is not None) == (f == 0)
if recovered is not None:
assert source(inst, recovered)
COUNTS['assignment_identity_and_extraction'] += 1
else:
assert target.n == 0 and extract(inst, target, ()) is None
COUNTS['early_no'] += 1
if export:
return {'schedules': inst.schedules, 'requirements': inst.requirements,
'budget': inst.budget, 'k': inst.k, 'n': target.n,
'threshold': target.threshold, 'constant': target.constant,
'coefficients': [[i, j, v] for (i, j), v in target.coefficients.items()],
'source_yes': witness is not None, 'source_witness': witness,
'target_witness': solution[1] if solution else None,
'early_no': target.early}
def uniform_patterns(p, k):
return [tuple(int(i in active) for i in range(p)) for active in it.combinations(range(p), k)]
def family_size(s, p):
choices = sum(math.comb(p, k)**s for k in range(p + 1)) if s else 1
return 3 * 4**p * choices
def finite_family(s, p):
for w in range(3):
for requirements in it.product((-1, 0, 1, 2), repeat=p):
if not s:
yield Instance((), requirements, w, p + 2)
else:
for k in range(p + 1):
for patterns in it.product(uniform_patterns(p, k), repeat=s):
yield Instance(patterns, requirements, w, k)
def sampled_family(s, p, rng):
selected = set()
while len(selected) < 300:
k = rng.randrange(p + 1) if s else p + 2
patterns = tuple(rng.choice(uniform_patterns(p, k)) for _ in range(s)) if s else ()
inst = Instance(patterns, tuple(rng.choice((-1, 0, 1, 2)) for _ in range(p)), rng.randrange(3), k)
if inst not in selected:
selected.add(inst)
yield inst
def finite_checks():
rng = random.Random(20261022)
coverage = []
shared = []
for s in range(6):
for p in range(6):
size = family_size(s, p)
exhaustive = size <= 300
instances = finite_family(s, p) if exhaustive else sampled_family(s, p, rng)
n = 0
for inst in instances:
item = check_instance(inst, rng, export=n < 3)
if item:
shared.append(item)
n += 1
assert n == (size if exhaustive else 300)
coverage.append({'s': s, 'p': p, 'family_size': size, 'mode': 'exhaustive' if exhaustive else 'unique_seeded_samples', 'instances': n})
print(json.dumps(coverage[-1]), flush=True)
(OUT / 'finite-coverage.json').write_text(json.dumps(coverage, indent=2) + '\n')
return shared
@st.composite
def general_instances(draw):
s = draw(st.integers(0, 5))
p = draw(st.integers(0, 5))
w = draw(st.integers(0, 5))
k = draw(st.integers(0, p))
patterns = uniform_patterns(p, k)
rows = tuple(draw(st.lists(st.sampled_from(patterns), min_size=s, max_size=s)))
req = tuple(draw(st.lists(st.integers(-3, w + 1), min_size=p, max_size=p)))
return Instance(rows, req, w, k)
@st.composite
def known_feasible_instances(draw):
s = draw(st.integers(1, 5))
p = draw(st.integers(1, 5))
w = draw(st.integers(1, 6))
k = draw(st.integers(0, p))
rows = tuple(draw(st.lists(st.sampled_from(uniform_patterns(p, k)), min_size=s, max_size=s)))
counts = [0] * s
for _ in range(draw(st.integers(0, w))):
counts[draw(st.integers(0, s - 1))] += 1
req = tuple(draw(st.integers(-2, sum(a[u] * c for a, c in zip(rows, counts)))) for u in range(p))
return Instance(rows, req, w, k), tuple(counts)
@settings(max_examples=200, deadline=None, derandomize=True, database=None)
@given(general_instances())
def test_general_hypothesis(inst):
check_instance(inst, random.Random(11))
COUNTS['hypothesis_general'] += 1
@settings(max_examples=200, deadline=None, derandomize=True, database=None)
@given(known_feasible_instances())
def test_planted_hypothesis(pair):
inst, counts = pair
assert source(inst, counts)
target = build(inst, arithmetic=True)
bits = forward(inst, target, counts)
assert energy(target, bits) == target.threshold
assert extract(inst, target, bits) == counts
assert target_solve(target) is not None
COUNTS['hypothesis_planted'] += 1
def block_checks():
for bound in range(257):
w = weights(bound)
represented = {sum(a * b for a, b in zip(w, bits)) for bits in it.product((0, 1), repeat=len(w))}
assert represented == set(range(bound + 1))
assert sum(w) == bound and len(w) == bound.bit_length()
assert all(0 < x <= bound for x in w)
COUNTS['exhaustive_bounded_block_ranges'] += 1
# The extraction must retain multiplicities and nonunique subset encodings.
inst = Instance(((1,),), (2,), 2, 1)
target = build(inst)
accepted = []
for bits in it.product((0, 1), repeat=target.n):
result = extract(inst, target, bits)
if result is not None:
accepted.append(result)
assert accepted == [(2,)]
inst = Instance(((1,), (1,)), (1,), 2, 1)
target = build(inst)
accepted_counts = Counter()
for bits in it.product((0, 1), repeat=target.n):
result = extract(inst, target, bits)
if result is not None:
assert source(inst, result)
accepted_counts[result] += 1
assert accepted_counts[(1, 0)] > 1 and accepted_counts[(2, 0)] > 0
COUNTS['multiplicity_and_nonunique_encoding'] += 2
def examples_and_malformed():
exported = []
patterns = ((1, 1, 0), (0, 1, 1), (1, 0, 1))
for w, expected_n, expected_c, expected_min in [(3, 11, 21, -21), (2, 8, 16, -15)]:
inst = Instance(patterns, (2, 2, 2), w, 2)
target = build(inst)
assert (target.n, target.constant) == (expected_n, expected_c)
solution = target_solve(target, minimize=True)
all_energies = [energy(target, bits) for bits in it.product((0, 1), repeat=target.n)]
assert solution[0] == min(all_energies) == expected_min
COUNTS['worked_example_assignments'] += len(all_energies)
exported.append(check_instance(inst, random.Random(7), True))
bad = [(), (0,) * (target.n - 1), (0,) * (target.n + 1)]
for value in (-1, 2, 0.5, '1', None):
bad.append((value,) + (0,) * (target.n - 1))
for bits in bad:
assert extract(inst, target, bits) is None
COUNTS['malformed_target_rejections'] += 1
for bits in it.product((0, 1), repeat=target.n):
if energy(target, bits) > target.threshold:
assert extract(inst, target, bits) is None
COUNTS['unsatisfying_extraction_rejections'] += 1
for inst in [Instance((), (), 0, 99), Instance((), (MIN, 0), 0, 99),
Instance((), (1,), 0, 99), Instance(((), ()), (), 2, 0),
Instance(((0, 0),), (0, -5), 0, 0), Instance(((1,),), (2,), 2, 1),
Instance(((1,), (1,)), (2,), 2, 1), Instance(((0,),), (1,), 2, 0)]:
exported.append(check_instance(inst, random.Random(8), True))
COUNTS['dedicated_degenerate_cases'] += 1
inst = Instance(((1,), (1,)), (0,), 2, 1)
for counts in [(), (1,), (0, 0, 0), (-1, 0), (3, 0), (2, 1)]:
assert source(inst, counts) is False
COUNTS['malformed_source_rejections'] += 1
return exported
def symbolic_checks():
for inst in [Instance(((1, 0), (0, 1), (1, 0)), (1, -2), 3, 1),
Instance(((1, 1), (1, 1)), (2, 1), 2, 2), Instance((), (0,), 0, 5)]:
target = build(inst)
x = sp.symbols(f'x0:{target.n}')
independent = sum((sum(a * x[i] for i, a in row.items()) + c)**2 for row, c in target.rows)
independent = sp.expand(independent).subs({a**2: a for a in x})
emitted = sum(v * x[i] * x[j] if i != j else v * x[i] for (i, j), v in target.coefficients.items())
assert sp.expand(independent - emitted - target.constant) == 0
COUNTS['sympy_polynomial_identities'] += 1
# Per residual: ordinary bit coefficient a^2-2ra and surplus a^2+2ra.
# Enumerating the full small triangle checks the sharper derived W^2 bound.
for w in range(31):
for r in range(w + 1):
for a in range(w + 1):
assert abs(a*a - 2*r*a) <= w*w
if a <= w-r:
assert a*a + 2*r*a <= w*w
COUNTS['independent_diagonal_bounds'] += 1
a, r, w = sp.symbols('a r w')
assert sp.expand(a*a - 2*r*a - ((a-r)**2-r*r)) == 0
assert sp.expand((w-r)**2 + 2*r*(w-r) - (w*w-r*r)) == 0
def composition_checks():
rng = random.Random(20261023)
exported = []
for trial in range(120):
q = trial % 3
p = 3 * q
options = uniform_patterns(p, 3) if p else []
s = rng.randrange(7) if options else 0
rows = tuple(rng.choice(options) for _ in range(s))
inst = Instance(rows, (1,) * p, q, 3)
exact_cover = any(all(sum(row[u] * flag for row, flag in zip(rows, flags)) == 1 for u in range(p))
for flags in it.product((0, 1), repeat=s))
target = build(inst, arithmetic=True)
result = target_solve(target)
assert exact_cover == (result is not None)
for counts in it.product(range(q + 1), repeat=s):
if source(inst, counts):
assert sum(counts) == q and all(c in (0, 1) for c in counts)
assert all(sum(row[u] * c for row, c in zip(rows, counts)) == 1 for u in range(p))
COUNTS['composition_feasible_count_witnesses'] += 1
if result:
counts = extract(inst, target, result[1])
assert counts is not None and source(inst, counts)
assert all(c in (0, 1) for c in counts)
COUNTS['exact_cover_staff_qubo_composition'] += 1
if trial < 6:
exported.append(check_instance(inst, rng, True))
return exported
def expect_overflow(call):
try:
call()
except Overflow:
COUNTS['typed_arithmetic_rejections'] += 1
else:
raise AssertionError('Expected arithmetic overflow')
def arithmetic_checks():
assert 2 * MAX * MAX <= 2**127 - 1
# All three pairwise i128 products fit, but their arbitrary sum need not.
assert MAX * MAX + 2 * MAX * MAX > 2**127 - 1
COUNTS['i128_product_bound_checks'] += 2
for bound in [0, 1, 2, 3, 2**31-1, 2**31, 2**62-1, 2**62, MAX]:
w = weights(bound)
assert sum(w) == bound and len(w) <= 63
assert len(w) == bound.bit_length()
COUNTS['large_block_weight_bounds'] += 1
# Budget row with one block: energy lies in [-W^2, 0].
# Its exact negative coefficient sum is W^2+sum_{i<j}2a_i*a_j.
def negative_sum(w):
a = weights(w)
return sum(2*w*x-x*x for x in a)
lo, hi = 0, math.isqrt(MAX) + 1
while lo + 1 < hi:
mid = (lo + hi)//2
if negative_sum(mid) <= MAX:
lo = mid
else:
hi = mid
assert negative_sum(lo) <= MAX < negative_sum(hi)
inst = Instance((), (), lo, 77)
target = build(inst, arithmetic=True)
rng = random.Random(23)
for _ in range(1000):
bits = tuple(rng.randrange(2) for _ in range(target.n))
values = [v * bits[i] * bits[j] for (i, j), v in target.coefficients.items()]
rng.shuffle(values)
total = 0
for value in values:
total = checked(total + value)
assert total == energy(target, bits)
COUNTS['random_evaluation_prefix_orders'] += 1
expect_overflow(lambda: build(Instance((), (), hi, 77), arithmetic=True))
expect_overflow(lambda: build(Instance((), (), math.isqrt(MAX) + 1, 77), arithmetic=True))
expect_overflow(lambda: build(Instance(((1,), (1,)), (0,), MAX, 1), arithmetic=True))
expect_overflow(lambda: build(Instance(((1,),), (MAX,), MAX, 1), arithmetic=True))
expect_overflow(lambda: source(Instance(((1,), (1,)), (0,), MAX, 1), (MAX, 1)))
# Length and coordinate validation precede the overflowing total fold.
assert source(Instance(((1,), (1,)), (0,), MAX, 1), (MAX,)) is False
assert source(Instance(((1,), (1,)), (0,), MAX, 1), (MAX, -1)) is False
assert source(Instance(((1,), (1,)), (0,), MAX, 1), (MAX, MAX + 1)) is False
# Budget failure precedes coverage, and a successful witness bounds coverage.
assert source(Instance(((1,), (1,)), (MAX,), MAX, 1), (MAX, 0))
early = build(Instance(((1,), (1,), (1,)), (MAX,), MAX - 1, 1), arithmetic=True)
assert early.early and extract(Instance((), (), 0, 0), early, ()) is None
for negative in [MIN, MIN+1, -1, 0]:
target = build(Instance(((1,),), (negative,), 0, 1), arithmetic=True)
assert target.n == 0 and target.threshold == 0
assert extract(Instance(((1,),), (negative,), 0, 1), target, ()) == (0,)
COUNTS['negative_requirement_boundaries'] += 1
return {'safe_budget_for_separate_sum_guard': lo, 'next_rejected_budget': hi,
'safe_negative_sum': negative_sum(lo), 'unsafe_negative_sum': negative_sum(hi),
'sqrt_i64_max': math.isqrt(MAX)}
def main():
block_checks()
shared = examples_and_malformed()
symbolic_checks()
boundary = arithmetic_checks()
shared += composition_checks()
shared += finite_checks()
test_general_hypothesis()
test_planted_hypothesis()
(OUT / 'shared-instances.json').write_text(json.dumps(shared, indent=2) + '\n')
report = {'verdict': 'PASS', 'counts': dict(COUNTS), 'arithmetic_boundaries': boundary,
'shared_instances': len(shared), 'seed': 20261022,
'limits': ['Finite base family has W in {0,1,2}, requirements in {-1,0,1,2}, ordered duplicate-permitting uniform-k patterns.',
'All (s,p) in 0..5 covered; families of at most 300 instances exhausted, others have 300 distinct seeded samples.',
'Hypothesis adds W through 6; arbitrary i64 coefficient bounds are algebraic, boundary checks finite.',
'No repository code, prototype, or shared corpus was read; this validates the proof and independent reference only.',
'Exact-cover composition is independently modeled mathematically; no repository graph dispatch was exercised.',
'No real allocation exhaustion, usize overflow, Rust serialization, or implementation error types were exercised.']}
(OUT / 'report.json').write_text(json.dumps(report, indent=2) + '\n')
print(json.dumps(report, indent=2), flush=True)
if __name__ == '__main__':
main()Constructor implementation imported as prototypes.py (staffing portion)"""Research polynomials, not certified production reductions."""
from collections import defaultdict
from itertools import combinations
class Q:
def __init__(self): self.n=0; self.q=defaultdict(int); self.c=0; self.decision=False
def var(self): i=self.n; self.n+=1; return i
def add(self,i,j,v): self.q[min(i,j),max(i,j)]+=v
def square(self,terms,c=0,p=1):
terms=dict(terms); self.c+=p*c*c
for i,v in terms.items(): self.add(i,i,p*(v*v+2*c*v))
for (i,v),(j,w) in combinations(terms.items(),2): self.add(i,j,2*p*v*w)
def one(self,row,p=1): self.square([(i,1) for i in row],-1,p)
def integer(self,bound):
assert bound>=0
terms=[]; weight=1
while bound:
v=min(weight,bound); terms.append((self.var(),v)); bound-=v; weight*=2
return terms
def finish(self): self.q={ij:v for ij,v in self.q.items() if v}; return self
def energy(self,bits): return self.c+sum(v*bits[i]*bits[j] for (i,j),v in self.q.items())
def staff(d):
q=Q(); q.decision=True; W=d['num_workers']; r=d['requirements']; A=d['schedules']
if any(v>W for v in r): q.c=1; q.rows=[]; return q.finish()
q.rows=[q.integer(W) for _ in A]
q.square([t for row in q.rows for t in row]+q.integer(W),-W)
for u,required in enumerate(r):
if required<=0: continue
q.square([t for row,a in zip(q.rows,A) if a[u] for t in row]+[(i,-v) for i,v in q.integer(W-required)],-required)
return q.finish() |
Collaborator
Author
Phase 4 domain and practicality auditThe final shipping scope is StaffScheduling → DecisionQUBO only. This is stacked on Phase 3 commit All rejected encodings below are preliminary research prototypes, not certified reductions. A timeout establishes failure of this proposed encoding under this validation gate, not impossibility of a better future formulation. Screening stopped at the first failure. The remaining 100-case candidate corpora were inventoried but not raw-solved after rejection. No rejected reducer, registration, example, test runner or research artifact is included in the package. Domains, semantics, routes, and endpoints
Primary sources and interpretationThe source code determines the variant; roadmap prose is a hypothesis. Venturelli et al. use fixed-makespan decisions with search, which cannot silently replace the repository's optimization contract. Zhang, Lo Bianco and Beck analyze direct job-shop QUBOs and their scale; exact makespan and sum-of-completion surrogates are distinct. Lucas and Glover et al. supply squared-constraint tools, not a proof of this exact staffing variant. The staffing certificate supplies the finite multiplicity bounds and both directions independently. Sethi's register-allocation paper supports examining sequencing-dependent liveness; it does not justify a static interference replacement. The cumulative-cost primary paper includes signed costs and special precedence structures; its special-case algorithm is not a general direct reduction. The Wagner–Whitin lot-sizing source was identified, but its uncapacitated setting cannot establish the repository's exact capacitated decision variant. Flow-shop DOI 10.1145/3638530.3664150 and the Garey–Johnson SR5 scan were located but full text was unavailable; they are not treated as verification evidence. Validation protocol and limitationsThe inventory and suite were fixed before screening: all 100 independent cases per candidate, canonical cases, explicit boundaries, and relevant incoming corpus families for surviving rules. Fixed small-case raw budget: 15 seconds, one worker, CP-SAT 9.15.6755, linearization_level=2, random_seed=1. The raw model contains only emitted Boolean quadratic terms, exact Boolean product equalities (one auxiliary per nonzero off-diagonal), and the emitted Decision threshold or optimization objective. No source constraints, source witness hints, expected-optimum bounds, or truth-dependent solver configuration. CP-SAT's linearization setting is documented in its parameter source. Decision YES requires a certified threshold witness; NO requires INFEASIBLE. Optimization requires OPTIMAL, never a FEASIBLE incumbent. Independent truth is checked only after solving. Feasibility raw results, separate oracle/constructor checks and exact coefficient comparisons are reported separately. Source timing includes debug-CLI startup. Construction and recovery are measured through actual CLI bundles. Dense target memory was not material for the shipped sparse targets; peak RSS was not separately measured. Finite tests do not establish performance for larger p,s,W or different target solvers. Numeric magnitude remains visible: staffing uses O(log W) bits per count, squared coefficients can overflow even when the source does not. Typed errors reject unrepresentable constructions, including conservative guards; no silent source-domain restriction or saturation. All corpus-specific scripts, environments, logs, rejected prototypes, proofs and reports remain outside both this repository and the read-only corpus. The whole corpus tree, including hidden files, is SHA-256 checked before/after. Existing-route timeouts/semantic gaps are recorded as unavailable evidence, never evidence that a new rule is superior. Timeout diagnosisRepeated the unchanged canonical PreemptiveScheduling and FlowShopScheduling emitted prototype polynomials under the same 15-second configuration, collecting solver response statistics. Both remained unresolved, with no MODEL_INVALID result. Preemptive: FEASIBLE, objective −545 versus best bound −798, 17,484 conflicts, 337,701 branches and 637,439 LP iterations. Flow: UNKNOWN, 29,942 conflicts, 133,161 branches and 346,316 LP iterations. Thus Boolean-product LP strengthening was active but insufficient for these encodings. No source constraints or optimum bounds were introduced, and no budget was increased. This diagnostic supports deferral; it is not proof that another formulation cannot work. No formulation or solver fix was made, so no partial rerun is claimed to clear a failure. |
Collaborator
Author
Phase 4 measurementsMeasured on a 32-GiB macOS host, debug CLI; seconds are wall-clock and include startup where stated. Solver: OR-Tools 9.15.6755 CP-SAT, 15 s,1worker,linearization2,seed 1. Product auxiliaries equal the coupling count. Source cases are small; expanded target size is shown separately. Complete independent corpus inventoryEach row has 100 verified source instances; ranges are actual source dimensions.
Shipped production results219/219 proven decisions,0 timeouts:115 staffing (100 corpus,13 boundaries,2 canonical) and104 incoming X3C (100 corpus,1 canonical,3 independently enumerated boundary instances). X3C corpus has no NO instance; the separate exhaustive six-element intersecting-triples instance supplies an actual NO chain. Every YES witness evaluates true at the original source, every completed Or value maps identically, every emitted polynomial equals the independently verified prototype.
Direct staffing had no old QUBO route. This adds connectivity but does not beat source brute force. Existing direct X3C is much better than routing through staffing:7 variables,13 couplings/auxiliaries,max coefficient 4(3bits),raw 0.0007..0.0015 s on the same101 canonical/corpus sources. The new upstream route is validated for compatibility, not recommended over that direct edge. Rejected prototype screening and existing-route baselines
RootedTreeStorageAssignment: no certified direct prototype; full branching proof/practicality unresolved, direct corpus0/100. DecisionOpenShop is separately inventoried and its old route measured; no new decision prototype ships. The other rejected candidates stop at first timeout; unattempted cases and upstream chains remain unverified. Time-indexed shop/preemptive grids depend pseudopolynomially on duration sums; quantity one-hot production depends pseudopolynomially on capacities. Binary-slack constructions still depend on coefficient magnitude and conditioning.
All shortest available routes were constructed on identical canonical and first-corpus inputs; all existing paths were enumerated. Almost all baseline QUBOs lack proven optimum under the same15 s limit, so completed recovery is unavailable. The tiny DecisionOpenShop canonical target is OPTIMAL with a valid extracted witness, but its existing route has no aggregate-capable path; this inherited gap is not fixed here. Signed setup ILP semantics are not established, so those source results are observational only. No baseline failure is claimed as a speedup. Composed parameter bounds
Existing baseline shortest-route composed bounds
|
Collaborator
Author
Production raw-target per-case resultsAll219cases. N=target bits; E=nonzero off-diagonals and exact product auxiliaries; M=max coefficient magnitude, B=bit length; C=CLI construction; R=raw solve; F=construction+solver-model+solve+aggregate/witness recovery+source evaluate; S=source solve (debug CLI). Each row passed independent truth, exact coefficient equivalence, completed aggregate recovery, and YES source evaluation.
raw.pyimport json,time
from ortools.sat.python import cp_model
def solve(q):
start=time.monotonic(); model=cp_model.CpModel(); x=[model.new_bool_var(f'x{i}') for i in range(q.n)]; terms=[]; aux=0
for (i,j),v in q.q.items():
if i==j:terms.append(v*x[i])
else:
y=model.new_bool_var(f'p{i}_{j}');model.add_multiplication_equality(y,[x[i],x[j]]);terms.append(v*y);aux+=1
if q.decision:model.add(sum(terms)<=-q.c)
else:model.minimize(sum(terms))
solver=cp_model.CpSolver();solver.parameters.max_time_in_seconds=15;solver.parameters.num_search_workers=1;solver.parameters.linearization_level=2;solver.parameters.random_seed=1
constructed=time.monotonic();status=solver.solve(model);end=time.monotonic()
result=dict(status=solver.status_name(status),solver_model_seconds=constructed-start,solve_seconds=end-constructed,variables=q.n,couplings=aux,solver_auxiliaries=aux,coefficient_max=max(map(abs,q.q.values()),default=0),coefficient_bits=max(map(abs,q.q.values()),default=0).bit_length(),constant=q.c)
result['search_statistics']=solver.response_stats()
if status in (cp_model.OPTIMAL,cp_model.FEASIBLE):
bits=[int(solver.value(v)) for v in x];result.update(bits=bits,energy=q.energy(bits))
return result
if __name__=='__main__':
from prototypes import Q
q=Q();x=q.var();q.add(x,x,-3);q.finish();r=solve(q)
assert r['status']=='OPTIMAL' and r['energy']==-3
q.decision=True;q.c=4;r=solve(q);assert r['status']=='INFEASIBLE'
print('raw validator self-checks passed')production.pyimport json,time,itertools,sys
from inventory import ROOT,OUT,dimensions
from screen import cli
from prototypes import Q,staff
from raw import solve
folder=OUT/'production';folder.mkdir(exist_ok=True)
def paths(name):
p=cli(['path',name,'DecisionQUBO/i64','--limit','all']);(folder/(name+'-paths.json')).write_text(json.dumps(p,indent=2));return p['paths']
def route(name,through):
p=next(p for p in paths(name) if [s['to']['name'] for s in p['path']]==through)
f=folder/(name+'-'+str(len(through))+'-route.json');f.write_text(json.dumps(p));return f
sr=route('StaffScheduling',['DecisionQUBO'])
xr=route('ExactCoverBy3Sets',['StaffScheduling','DecisionQUBO'])
xd=route('ExactCoverBy3Sets',['DecisionQUBO'])
mid=folder/'x3c-staff-route.json';mid.write_text(json.dumps(cli(['path','ExactCoverBy3Sets','StaffScheduling','--limit','all'])['paths'][0]))
inv=json.loads((OUT/'inventory.json').read_text())
cases=[('model-canonical',cli(['create','--example','StaffScheduling']),True,sr)]
cases += [('rule-canonical',cli(['create','--example','StaffScheduling','--to','DecisionQUBO/i64']),True,sr)]
cases += [(r['truth']['instance'],json.loads((ROOT/r['truth']['instance']).read_text()),r['truth']['value'],sr) for r in inv if r['truth']['problem']=='StaffScheduling']
cases += [('edge-'+str(i),r['source'],r['truth'],sr) for i,r in enumerate(json.loads((OUT/'staff-edge-results.json').read_text()))]
xt=[json.loads(l) for l in (ROOT/'ground-truth/set/ExactCoverBy3Sets.jsonl').read_text().splitlines()]
xcs=[('x3c-canonical',cli(['create','--example','ExactCoverBy3Sets']),True)]+[(t['instance'],json.loads((ROOT/t['instance']).read_text()),t['value']) for t in xt]
cases += [(label,source,truth,xr) for label,source,truth in xcs]
for idx,(label,source,truth,routefile) in enumerate(cases):
base_start=time.monotonic();base=cli(['solve','-','--timeout','15'],source);base_secs=time.monotonic()-base_start
start=time.monotonic();b=cli(['reduce','-','--via',str(routefile)],source);constructed=time.monotonic()
d=b['target']['data'];q=Q();q.decision=True;q.n=d['inner']['num_vars'];q.q={(i,j):v for i,j,v in d['inner']['entries']};q.c=-d['bound'];q.finish()
model=source if source['type']=='StaffScheduling' else cli(['reduce','-','--via',str(mid)],source)['target']
p=staff(model['data']);assert (q.n,q.q,q.c)==(p.n,p.q,p.c)
# The measured workflow excludes the independent coefficient check and baseline.
raw_start=time.monotonic();r=solve(q)
assert r['status'] in ('OPTIMAL','INFEASIBLE'),(label,r['status'])
assert (r['status']=='OPTIMAL')==truth,(label,truth,r['status'])
agg=cli(['extract','-','--value='+json.dumps(truth)],b);assert agg['value']==truth
if truth:
ext=cli(['extract','-','--config',json.dumps([bool(v) for v in r['bits']])],b);assert ext['evaluation']=='Or(true)'
ev=cli(['evaluate','-','--config',json.dumps(ext['solution'])],source);assert ev['result']=='Or(true)'
r['source_witness']=ext['solution']
else:r['source_witness']=None
r.update(case=label,source_type=source['type'],truth=truth,source_dimensions=dimensions(source['type'],source['data']) if source['type']=='StaffScheduling' else dict(universe=source['data']['universe_size'],subsets=len(source['data']['subsets'])),source_seconds=base_secs,source_solve=base,construction_seconds=constructed-start,full_seconds=constructed-start+time.monotonic()-raw_start,aggregate=agg,coefficient_equivalence=True)
(folder/f'case-{idx}-bundle.json').write_text(json.dumps(b))
with (folder/'results.jsonl').open('a') as f:f.write(json.dumps(r)+'\n')
print(idx,label,r['status'],round(r['solve_seconds'],3),flush=True)
# Existing X3C direct route is a same-input comparison, not a claimed improvement.
for label,source,truth in xcs:
start=time.monotonic();b=cli(['reduce','-','--via',str(xd)],source);constructed=time.monotonic();d=b['target']['data'];q=Q();q.decision=True;q.n=d['inner']['num_vars'];q.q={(i,j):v for i,j,v in d['inner']['entries']};q.c=-d['bound'];q.finish();r=solve(q)
assert r['status'] in ('OPTIMAL','INFEASIBLE') and (r['status']=='OPTIMAL')==truth
agg=cli(['extract','-','--value='+json.dumps(truth)],b);assert agg['value']==truth
if truth:assert cli(['extract','-','--config',json.dumps([bool(v) for v in r['bits']])],b)['evaluation']=='Or(true)'
r.update(case=label,construction_seconds=constructed-start,full_seconds=time.monotonic()-start)
with (folder/'x3c-direct-results.jsonl').open('a') as f:f.write(json.dumps(r)+'\n')
# Native CLI solver on the rule fixture and a NO fixture, with completed recovery.
for idx in [1,113]:
b=json.loads((folder/f'case-{idx}-bundle.json').read_text());sol=cli(['solve','-','--solver','brute-force'],b)
(folder/f'cli-solve-{idx}.json').write_text(json.dumps(sol,indent=2))
print('native CLI solve',idx,sol,flush=True)
print('ALL PRODUCTION CASES PASS',len(cases),flush=True)upstream_boundaries.pyimport json,itertools,time
from inventory import OUT
from screen import cli
from prototypes import Q,staff
from raw import solve
folder=OUT/'production';route=folder/'ExactCoverBy3Sets-2-route.json';mid=folder/'x3c-staff-route.json'
cases=[(6,[[0,1,2],[0,3,4],[1,4,5]]),(0,[]),(3,[[0,1,2],[0,1,2]])]
for idx,(n,sets) in enumerate(cases):
truth=any(all(sum(bit for bit,S in zip(bits,sets) if u in S)==1 for u in range(n)) and sum(bits)==n//3 for bits in itertools.product([0,1],repeat=len(sets)))
source=dict(type='ExactCoverBy3Sets',variant={},data=dict(universe_size=n,subsets=sets))
t=time.monotonic();base=cli(['solve','-','--timeout','15'],source);base_seconds=time.monotonic()-t
t=time.monotonic();b=cli(['reduce','-','--via',str(route)],source);construction=time.monotonic()-t
d=b['target']['data'];q=Q();q.n=d['inner']['num_vars'];q.q={(i,j):v for i,j,v in d['inner']['entries']};q.c=-d['bound'];q.decision=True;q.finish()
middle=cli(['reduce','-','--via',str(mid)],source)['target'];p=staff(middle['data']);assert (q.n,q.q,q.c)==(p.n,p.q,p.c)
t=time.monotonic();r=solve(q);assert r['status'] in ['OPTIMAL','INFEASIBLE'] and (r['status']=='OPTIMAL')==truth
agg=cli(['extract','-','--value='+json.dumps(truth)],b);assert agg['value']==truth
if truth:
recovered=cli(['extract','-','--config',json.dumps([bool(x) for x in r['bits']])],b);assert recovered['evaluation']=='Or(true)'
assert cli(['evaluate','-','--config',json.dumps(recovered['solution'])],source)['result']=='Or(true)'
r.update(case='upstream-edge-'+str(idx),source_type='ExactCoverBy3Sets',truth=truth,source_dimensions=dict(universe=n,subsets=len(sets)),source_seconds=base_seconds,source_solve=base,construction_seconds=construction,full_seconds=construction+time.monotonic()-t,aggregate=agg,coefficient_equivalence=True)
(folder/f'upstream-edge-{idx}-bundle.json').write_text(json.dumps(b))
with (folder/'results.jsonl').open('a') as f:f.write(json.dumps(r)+'\n')
print(idx,r['status'],r['solve_seconds']) |
Collaborator
Author
Agentic Review ReportVerdict: PASS for the reviewed code and feature workflow; no unresolved findings. Final paper and coverage gates remain the implementer's responsibility and were still pending when this report was written. Review scope: the uncommitted Phase 4 changes relative to Structural and semanticPASS. The new edge is I traced the budget/coverage squares, omitted constant, decision threshold, and extraction against the actual source evaluator. The construction preserves multiplicities, duplicate and empty patterns, empty schedule/period collections, arbitrary signed requirements including All ten Phase 4 candidates are accounted for in Quality and evidencePASS. The native tests first failed because the direct edge was absent, then passed. They compare independently brute-forced source feasibility with exhaustive target assignments, check every satisfying target's decoded source witness, reject malformed and unsatisfying targets, exercise multiplicity and signed/empty cases, and check typed overflow and both completed decision values. I inspected the mathematical certificate and verification scripts/results: 290,847 constructor checks, independent adversary coverage including 7,086 source/target decision comparisons and 51,400 assignment identity/extraction checks, and 124 shared polynomial comparisons with zero disagreements. These supplement the proof rather than establish universal correctness by count. The production evidence is complete: 219/219 raw target decisions, zero timeouts, consisting of 115 staffing cases (100 corpus, 13 boundaries, two canonical) and 104 incoming X3C cases (100 corpus, one canonical, three generated boundaries). The X3C corpus is all YES; a separate independently enumerated intersecting-triples instance verifies the actual NO chain. Every emitted polynomial matches the verified prototype; completed values and every YES witness recover to the original source. The fixed raw solver sees only polynomial products and the emitted threshold: 15 seconds, one worker, linearization level 2, seed 1. Slowest solve: 13.9043 seconds. The existing direct X3C baseline also completes all 101 canonical/corpus inputs and is materially smaller/faster. The corpus integrity record reports all 32,372 files unchanged. Feature testPASS. I ran Separate arithmetic oracle/recovery evidence, not additional raw solves: with no schedule patterns or periods, budget 2,322,860,046 constructs successfully and its 32-bit all-true budget-slack witness recovers the valid empty source witness; budget 2,322,860,047 returns a typed reduction overflow because the final negative coefficient sum exceeds FindingsNo unresolved Critical, Important, or Minor findings. Resolved Minor: Not checked here: final paper/coverage results, hardware embedding, or larger-instance performance. The 13.9-second worst case has limited margin under the fixed 15-second gate; conservative arithmetic guards can reject representable special cases. |
Open
57 tasks
isPANN
changed the title
isPANN
marked this pull request as ready for review
October 27, 2026 12:57
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>
This was referenced Oct 29, 2026
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 #1217: Add staff-scheduling QUBO and tighten direct-reduction bounds
Review date: 2026-10-29. Fresh-context read-only review of 109985f4103d4c4785f60b8a34007580cd7f2434...3d3b020c0d93f5e27ecce98eaf148321a7eced9d. Used the PR's own stack base, not origin/main. Local implementation evidence is diff-1217.patch; GitHub context is context-1217.txt in this directory.
Verdict: No new blocking finding in this diff. Hold stack integration until #1214 is fixed.
Structural and semantic review
Reviewed StaffScheduling, the replacement OLA and ThreePartition encodings, revised coupling bounds, intentional SCS removal, helper/test updates, and manual changes against the exact #1216 base.
StaffScheduling represents each schedule count in [0,W], plus a budget slack in [0,W] and period surplus in [0,W−r_t]. Bounded binary weights sum to the bound and represent every integer in that range. Its equations are total-count + budget-slack = W and coverage − surplus = r_t. Negative requirements impose no condition; r_t > W gives an explicit NO target. Checked decoded sums and source accumulation limits.
OLA uses n(n−1)/2 comparison variables. For an edge {u,v}, distance equals one plus the number of other vertices between its endpoints; each contribution is the XOR of the relevant comparison bits. The objective is nonnegative on every bit assignment. Triangle penalties with weight m(n−1)+1 therefore force a transitive total order.
ThreePartition enumerates eligible value triples and encodes bounded multiplicities, then enforces the exact count of each distinct value. Extraction consumes distinct indexed copies. Counting incidences ensures n/3 triples. For multiplicity bounds M_t, 3*sum(M_t) <= choose(n,2), giving N <= n(n−1)/6. For a value row v, complementary pairs are disjoint value classes, so its bit degree D_v <= n/2 and sum(D_v) <= 3N. Thus sum(choose(D_v,2)) <= n(n−1)(n−2)/8, validating the coupling bound.
Recomputed tightened bounds for cyclic ordering, shortest superstring, and StackerCrane from actual products. The SCS rule and its direct-QUBO tests are removed as explicitly documented after failure of the runtime acceptance gate; the existing ILP route remains.
Quality review
The replacement encodings have independent brute-force round trips and infeasible/empty/boundary coverage. Integer multiplicities and bounded remainder bits were checked for non-powers of two. The value-aggregation ThreePartition proof does not assume equal items are interchangeable without tracking their indexed copies during extraction. The author corpus claims were inspected but are not substituted for these derivations.
Feature tests and verification limits
The compiled #1218 descendant retains these exact production changes. direct_qubo --test-threads=2 passed all 44 tests, and staffscheduling_qubo --test-threads=2 passed all 4 tests. CLI discovery/example/inspect/direct-path/reduce workflows and independent source/target brute-force solves passed for StaffScheduling, OLA, and ThreePartition. Each extracted source evaluation equals the source optimum/feasibility. The other retained encodings were also exercised in a total of 24 CLI round trips.
Exact #1217 full make/test/doc/coverage commands were not rerun; shared resources were used for the descendant tests, CLI, and numeric boundary probe. GitHub checks were absent from the collected stack metadata; author local checks are recorded only as author claims.
Findings (severity order)
No new blocking finding. The #1214 interval allocation panic remains inherited and blocks stack integration until repaired. The intentional SCS removal is within this PR's stated performance scope, not an unrelated deletion.
GitHub PR Audit — #1217
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
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 2cd3218cec051e6966e0ea27524a65ba87aefe68 for merging into issue-1213-direct-qubo-phase3 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 an exact
StaffScheduling → DecisionQUBO<i64>reduction and reduces the theoretical overhead of the direct QUBO rules inherited from the stack. Linear arrangement and three-partition use smaller encodings; four other rules receive proved tighter coupling bounds. The direct shortest-common-supersequence rule is withdrawn because it failed the small-instance runtime criterion. Its existing ILP route remains.The resulting stack retains 24 direct rules, with all 2,400 independent corpus cases passing and zero timeouts or mismatches.
References #1213; keep the roadmap open. This remains a draft stacked on #1216 (
issue-1213-direct-qubo-phase3), which is stacked on #1215/#1214. The 24-rule validation includes inherited rules; this PR does not introduce 24 new edges.Constructions and theoretical bounds
n²to exactlyn(n−1)/2; couplings are bounded byn(n−1)(n−2)/2, cubic even for dense graphs.n²/3to at mostn(n−1)/6, and couplings are bounded byn(n−1)(n−2)/8. Coefficients depend on item counts rather than squared size magnitudes.The remaining bound improvements count the actual possible interactions without changing the constructions:
n(n−1)(n−2)/2n(n−1)(2n−1)2n²(n−1)binom(63(s+1), 2) + p(3969s+1953)Here
nis respectively the element, string, or required-arc count;sandpare the schedule and period counts. Staffing retains the variable bound63(s+p+1); its coupling bound is linear in periods for fixed schedule count. The manual includes the constructions, bidirectional correctness arguments, extraction contracts, and support-count proofs. Graph metadata and parameter regressions use the same formulas.Verification
pred-validation-corpusatb9ae9e39f6e51237760f26f8aec205d485490ab0. All 2,400 actual emitted targets completed correctly. The corpus tracked tree remains unchanged.linearization_level=2, seed 1; two concurrent cases. Exact Boolean-product linearization uses only emitted target coefficients and decision bounds, with no source hints or oracle objective cutoffs. Optimization requires OPTIMAL; decision NO requires INFEASIBLE. Every result passes actual CLI aggregate recovery, witness extraction where applicable, and source evaluation against independent corpus truth.make checkpasses 7,133 tests/doctests, formatting, and clippy. Line coverage is 98.15% for linear arrangement and 95.20% for three-partition. Paper and website builds pass. Browser verification confirms the updated bounds, 368 graph edges, absent SCS direct-QUBO edge, retained SCS-to-ILP route, and no browser errors./simplifyfound no further worthwhile cleanup.Verified source commit:
3d3b020c0d93f5e27ecce98eaf148321a7eced9d. Its diff has SHA-256672fc2886a48792c0879c11771dc35b591593be6605e156df3851a2991a0a446relative to0dd744809f524cd5669ea04f4f699cc428bbf53c, exactly matching the tested working snapshot; the final tested CLI has SHA-25631a19445bf633bd7c9ec60a6c7bb5bb0596f935d22c7b42a0032a4aa28d014b5.Limits and deferred work
ShortestCommonSupersequence's original encoding and two mathematically checked replacements failed the small-case runtime criterion, so the direct rule, registration, example, and theorem are removed. This is a practicality failure, not a demonstrated mathematical counterexample. Its removal is explicit in the 24-rule total; no timeout is accepted as a passing case.
The other Phase 4 candidates remain deferred: JobShopScheduling, OpenShopScheduling, FlowShopScheduling, PreemptiveScheduling, SequencingWithDeadlinesAndSetUpTimes, SequencingToMinimizeMaximumCumulativeCost, ProductionPlanning, RegisterSufficiency, and RootedTreeStorageAssignment. Earlier deferrals and unrelated verification gaps remain outside scope.
Larger-instance performance and hardware embedding remain unverified. Finite checks are not proof-assistant certification or a source-solver speedup claim. Remote CI/Codecov is not claimed: the workflows target PR bases
main/develop, while this PR targets the Phase 3 branch.The earlier staffing-specific certificate, measurements, and review report document the original staffing work. Their earlier whole-stack scope and bounds are superseded by this description.