Resolve inconclusive reduction-correctness checks for 29 rules with target-solve timeouts

[isPANN]

Problem

The full corpus run completed all planned checks, but 29 direct reduction rules still have inconclusive target-solve results. Track resolving those validation gaps here. There were no detected wrong answers, invalid witnesses or non-timeout errors in the primary run; a timeout is not evidence that a reduction is mathematically incorrect.

Pinned baseline and method

Package de787aa7, from #1174; corpus b9ae9e39. Each of 256 source variants and 309 executable non-Turing rules received 100 cases (90 random + 10 special).

Check	Attempts	Agrees with independent stored truth	Timeouts	Mismatches
pred solve on original instances	25,600	25,598	2	0
Forced direct reduction, then pred solve on the bundle	30,900	28,853	2,047	0

280 / 309 rules agree on all 100 inputs. Nine of the remaining 29 have zero completed target solves. All 2,047 affected reduction cases have a successful original-source solve agreeing with truth; the uncertainty lies in completing and validating the forced target pipeline.

The bundle solver actually solves the target and recovers the source result; it does not substitute a direct source solve. Compare source feasibility and optimum with stored independent ground truth, then re-evaluate returned source witnesses using pred evaluate. This general witness re-evaluation uses the same package, so it is not an independent oracle; BicliqueCover and MinimumCostMaximumFlow also received independent witness checks. Integer comparisons are exact; floating comparisons use relative and absolute tolerance 1e-8.

Execution used a pinned debug CLI, 8 workers, 30-second solve budgets plus a process guard, and single-threaded HiGHS with fixed seed and zero requested optimality gaps. Timing is not a release-build benchmark. The 200 bounded-ILP reuse cases select the bounded variant in external copies without changing payloads or truth. Original direct solves use untouched corpus files.

Complete affected-rule inventory

Counts below are first-pass results out of 100. Exact variant keys are retained to avoid conflating registrations.

Exact direct rule	Agree	Timeout	Selected target backend
ExactCoverBy3Sets{} -> BoundedDiameterSpanningTree{"graph":"SimpleGraph","weight":"i64"}	0	100	brute-force
KSatisfiability{"k":"K3"} -> BicliqueCover{}	0	100	ilp
KSatisfiability{"k":"K3"} -> CyclicOrdering{}	0	100	brute-force
KSatisfiability{"k":"K3"} -> PreemptiveScheduling{}	0	100	ilp
KSatisfiability{"k":"K3"} -> QuadraticCongruences{}	0	100	brute-force
KSatisfiability{"k":"K3"} -> QuadraticDiophantineEquations{}	0	100	brute-force
KSatisfiability{"k":"K3"} -> RegisterSufficiency{}	0	100	ilp
NAESatisfiability{} -> PartitionIntoPerfectMatchings{"graph":"SimpleGraph"}	0	100	brute-force
ThreeDimensionalMatching{} -> ThreePartition{}	0	100	ilp
PartitionIntoCliques{"graph":"SimpleGraph"} -> DecisionMinimumCoveringByCliques{"graph":"SimpleGraph"}	2	98	ilp
SetSplitting{} -> Betweenness{}	5	95	brute-force
KSatisfiability{"k":"K3"} -> FeasibleRegisterAssignment{}	8	92	ilp
KSatisfiability{"k":"K3"} -> AcyclicPartition{"weight":"i64"}	9	91	ilp
KSatisfiability{"k":"K3"} -> OneInThreeSatisfiability{}	14	86	brute-force
MinimumFeedbackVertexSet{"weight":"One"} -> MinimumCodeGenerationUnlimitedRegisters{}	14	86	brute-force
KSatisfiability{"k":"K3"} -> Kernel{}	25	75	brute-force
KColoring{"graph":"SimpleGraph","k":"K3"} -> TwoDimensionalConsecutiveSets{}	30	70	brute-force
Partition{} -> ProductionPlanning{}	32	68	brute-force
KSatisfiability{"k":"K3"} -> SubsetSum{}	41	59	brute-force
MinimumVertexCover{"graph":"SimpleGraph","weight":"One"} -> EnsembleComputation{}	41	59	ilp
DecisionMinimumVertexCover{"graph":"SimpleGraph","weight":"One"} -> HamiltonianCircuit{"graph":"SimpleGraph"}	42	58	ilp
MinimumVertexCover{"graph":"SimpleGraph","weight":"i64"} -> MinimumWeightAndOrGraph{}	48	52	brute-force
KColoring{"graph":"SimpleGraph","k":"KN"} -> BicliqueCover{}	54	46	ilp
ClosestVectorProblem{"coefficient":"i64"} -> QUBO{"weight":"i64"}	55	45	ilp
Partition{} -> DecisionOpenShopScheduling{}	67	33	ilp
KSatisfiability{"k":"K3"} -> TimetableDesign{}	82	18	customized
ThreePartition{} -> SequencingWithReleaseTimesAndDeadlines{}	92	8	ilp
OptimalLinearArrangement{"graph":"SimpleGraph"} -> SequencingToMinimizeWeightedCompletionTime{}	93	7	ilp
DecisionOptimalLinearArrangement{"graph":"SimpleGraph"} -> ConsecutiveOnesMatrixAugmentation{}	99	1	ilp

The two direct-source timeouts are PrizeCollectingSteinerForest<SimpleGraph,f64> and <SimpleGraph,i64> on the same 8-vertex, 16-edge graph. Both agree with truth in representative 120-second retries. Preserve those first-pass timeouts rather than rewriting the initial totals.

What the diagnosis establishes

• 13 affected rules use brute force: the constructed target can have an enormous coordinate search space even when its source is easy to solve. Example: X3C → BoundedDiameterSpanningTree constructs a representative with 19 vertices and 51 edges; its registered backend enumerates a 2^num_edges space. This describes the possible search space, not the number of candidates evaluated before timeout.
• 15 affected rules use ILP pipelines: the command timeout does not isolate target-to-ILP construction, ingestion, presolve or optimization. Separate construction/serialization probes finished for the materialized representatives, but do not prove solver search is the dominant phase.
• One affected rule uses a customized backend: K3SAT → TimetableDesign uses required-pair/period backtracking. Do not describe it using the generic Cartesian brute-force dimension count.
• A concrete formulation-size problem: K3SAT → PreemptiveScheduling produces a representative with 370 tasks, horizon 370 and 4,071 precedence pairs. Its subsequent ILP construction implies 136,901 variables, 1,780,810 rows and 280,097,585 nonzero terms. These counts were derived from the constructor, not obtained by materializing an additional huge model. For unit task lengths the term count is 5*n*D + p*D*(D+1)/2; the same construction count also matches all 100 existing direct PreemptiveScheduling construction measurements.

Across the 31 affected groups (29 rules + 2 original variants), one representative per group was retried at 120 seconds: 10 agree, 21 still time out. These selective successes apply only to their named inputs and do not resolve the other timeouts for that rule.

Pinned formulation source: preemptivescheduling_ilp.rs.

Reproduce one fully unresolved rule

Use the package and corpus commits above. The source input is this existing X3C instance; stored truth is satisfiable. From a checkout whose pred is built from the pinned package commit:

cat > x3c-spanning-tree-route.json <<'JSON'
{"path":[{"from":{"name":"ExactCoverBy3Sets","variant":{}},"to":{"name":"BoundedDiameterSpanningTree","variant":{"graph":"SimpleGraph","weight":"i64"}}}]}
JSON

pred solve /path/to/pred-validation-corpus/instances/ExactCoverBy3Sets/random-001-bernoulli-3468098837.json --quiet --json --timeout 30
pred reduce /path/to/pred-validation-corpus/instances/ExactCoverBy3Sets/random-001-bernoulli-3468098837.json --via x3c-spanning-tree-route.json --quiet --json > reduced.json
pred solve reduced.json --quiet --json --timeout 30

The direct source solve agrees with truth; the forced target solve timed out at both 30 and 120 seconds in the audited run. Machines/build profiles can change timing.

Work plan and acceptance criteria

• Reproduce and profile the affected exact variants in an optimized build; separate construction, target encoding, solver execution and extraction. Record build, backend, thread settings and budgets.
• For brute-force targets, assess a total exact solver or registered total ILP pipeline. Coordinate overlapping solver-domain work with [Solver] Repair nine partial ILP routes currently falling back to brute force #1092; do not silently fall back to solving the original source, since that bypasses the reduction under test.
• For ILP targets, address concrete construction/formulation bottlenecks before merely raising timeouts. Investigate the cumulative precedence formulation in PreemptiveScheduling first; preserve mathematical semantics.
• Diagnose TimetableDesign's actual customized search separately.
• Rerun all affected existing inputs through the forced target pipeline, compare feasibility/optimum and recovered witnesses with ground truth, and preserve first-pass versus retry results separately.
• For any discovered semantic defect, add an independently justified failing regression test before fixing it. Reuse the current corpus; do not increase package/corpus size to manufacture more passes.
• Give every unresolved case a final evidence-backed disposition. Do not close a group solely because one representative succeeds or a larger timeout finishes. If exact solving remains infeasible, retain it as unverified and explicitly track the remaining mathematical verification rather than asserting correctness.
• Refresh the combined overhead/correctness dashboard and repeat the independent full-case/provenance audit.

Limits and scope

Corpus agreement is not a universal proof. Thirty-two rules have only YES inputs in the pinned corpus; an unchanged existing KN formula reused under K3 supplied supplemental NO checks for 19 K3 rules (8 agree, 11 remain timeouts even after 120-second retries). Keep that limitation visible, but broad corpus-label repair is a separate issue from this target-solve work. Do not interpret labels such as obvious_no as oracle answers.

The completed audit reconciled all 56,500 primary records and 218 supplemental attempts, checked exact case identities/routes, and verified pinned input/oracle/binary hashes. The local 2026-09-29-bf09cce8/correctness-run evidence contains results.jsonl, issue-report.json (every affected input, diagnosis and reproduction), diagnostics.json, ilp-construction-probes.jsonl, retry datasets and audit.json. These generated artifacts are not committed to the package; this issue includes the full affected-rule inventory and a portable reproduction.

Related: #1174 (audited branch), #1152 (general timeout concern), #1092 (total solver pipelines). Overhead-declaration precision is tracked in #1188; changing a formula cannot make these target solves complete.

[isPANN]

Fixed in #1188.