bug: 5 unsound reductions — reduce_to() constructions are mathematically incorrect

[zazabap]

Summary

Five reductions have unsound reduce_to() constructions — target feasibility does not imply source feasibility. Confirmed by brute-force exhaustive search on NO instances.

Affected Rules

Rule	PR	Root Cause	NO-instance evidence
HamiltonianPath → ConsecutiveOnesSubmatrix	#779	C1P on incidence matrix is necessary but not sufficient for HP	6-vertex graph: 30 C1P solutions, only 10 are valid paths
Partition → ShortestWeightConstrainedPath	#779	Weight bound S/2 + n is an inequality — non-partition paths satisfy it	[1,2,6] (odd sum): target has feasible path. [1,2,3,10]: same.
ThreePartition → FlowShopScheduling	#972	Separator [0,L,0] only blocks machine 1. ALL permutations meet deadline.	[4,4,4,6,6,6], B=15: 2520 feasible schedules (should be 0)
ThreePartition → SeqMinWeightTardiness	#972	Element deadlines = horizon, so elements are never tardy	[4,4,4,6,6,6], B=15: 2520 zero-tardiness schedules (should be 0)
ThreePartition → JobShopScheduling	#972	Separator only constrains machine 0. Threshold = machine-0 total.	Optimal makespan always achievable regardless of partition

Verified Sound (38 rules)

All other rules from PRs #777, #779, #804, #972 were tested with NO instances and/or code-reviewed against textbook constructions. Notable:

• ThreePartition → ResourceConstrainedScheduling: SOUND (structural constraint enforces exactly 3 per slot)
• ThreePartition → SequencingWithReleaseTimesAndDeadlines: SOUND (fillers rigidly pinned with release=deadline-1)
• All HC→X (6 rules): SOUND (budget/penalty arguments verified)
• All KSat→X, Partition→{BinPacking,SubsetSum,MultiprocessorScheduling,SequencingWithinIntervals}: SOUND

Why Unit Tests Pass

Closed-loop tests only verify the forward direction or check "at least some brute-force witnesses extract correctly." They never test NO instances (infeasible source → target should be infeasible).

Discovery Method

Systematic CLI round-trip testing found 4 rules where ILP witnesses extracted to invalid source configs. Deeper investigation revealed the reductions themselves are unsound. A 5th (Partition→SWCP) was found by extending NO-instance testing to all 39 surviving rules.

Fix Options

1. Fix the reductions — redesign reduce_to() with correct constructions from literature
2. Remove the 5 unsound reductions — delete rule files, tests, paper entries, registry entries
3. Replace with correct multi-hop chains — keep problem models, remove incorrect direct edges

Supersedes

#1000, #1001, #1002, #1003, #1004 (all closed)

[isPANN]

Systematic verification update: 10 additional buggy rules found

Full three-check verification (NO-instance soundness, YES-instance witness round-trip, overhead formula) was run on all ~70 non-ILP reduction rules using random instance sampling with SmallRng fixed seeds.

Correction to "Verified Sound" list

Partition → SequencingWithinIntervals was listed as SOUND in the original issue but is actually UNSOUND. The enforcer task with release=S/2, deadline=S/2+1 does not prevent scheduling when S is odd — floor(S/2) and ceil(S/2) create asymmetric time blocks that allow NO-instances of Partition to be schedulable. 28 of ~40 tested NO instances exhibited this behavior (seed 42).

New unsound reductions (NO-instance soundness failures)

Rule	Root Cause	Counterexample
Partition → SequencingWithinIntervals	Enforcer task fails for odd sums; asymmetric time blocks allow unbalanced assignments	Seed 42, 4-element instances with odd total sum
ExactCoverBy3Sets → MinWeightSolutionToLinearEquations	is_consistent() allows fractional column multipliers, not just binary 0/1. When elements appear in exactly 2 sets, x=[1/2,...] is valid rational solution	{universe=6, subsets=[[0,3,5],[1,2,3],[0,1,4],[2,4,5]]} — no binary exact cover but rational solution exists
SubsetSum → CapacityAssignment	Reduction sets delay budget = S−B, enforcing sum ≥ B (inequality), not sum = B (equality). Any subset with sum > B is feasible in the target	{sizes=[17,7,20,15,16,12], target=11} — 87/87 NO instances map to feasible target

Extraction bugs (YES-instance witness round-trip failures)

Rule	Root Cause
MVC → EnsembleComputation	extract_solution iterates all budget steps (including padding), collecting operand vertices. Over-selects vertices, producing valid but non-optimal covers
SpinGlass → MaxCut (with fields)	Ancilla-based construction flips all spins when ancilla=1, then removes ancilla. Does not preserve optimality — extracted source solutions are not always optimal. Overhead formula also wrong (num_vertices=num_spins should be num_spins+1)
MIS → Triangular	triangular::map_weighted does not preserve optimal MIS values through the reduction. Target-optimal solutions map back to sub-optimal source solutions

Overhead-only bugs (reduction logic sound, formula wrong)

Rule	Declared	Actual
SAT → Coloring	num_vertices = num_vars + num_literals, num_edges = num_vars + num_literals	3 + 2*num_vars + 5*(num_literals - num_clauses) vertices; edges also more complex
CircuitSAT → SpinGlass	num_spins = num_assignments, num_interactions = num_assignments	Each gate creates 2-4 gadget spins + multiple interactions (AND/OR = 3 spins, XOR = 4, NOT = 2)
MIS → GridGraph (KSG)	num_edges = num_vertices^2	Actual KSG mapping produces more edges (e.g., 27 edges for n=5 vs bound of 25)
MIS → Triangular	num_vertices = num_vertices^2	Actual produces far more vertices (57 vs 25 for n=5)

Panic bug

Rule	Issue
SAT → CircuitSAT	reduce_to() panics when a SAT instance declares variables that don't appear in any clause. Circuit::variables() only collects syntactically-present variables, causing unwrap() at line 109

Updated totals

• Original bug: 5 unsound reductions — reduce_to() constructions are mathematically incorrect #1006: 5 unsound rules
• New unsound (NO-instance): +3 rules (Partition→SWI, X3C→MinWeightSolnLinEq, SubsetSum→CapacityAssignment)
• New extraction bugs: +3 rules (MVC→EnsembleComputation, SpinGlass→MaxCut/fields, MIS→Triangular)
• Overhead-only bugs: +4 rules (SAT→Coloring, CircuitSAT→SpinGlass, MIS→GridGraph, MIS→Triangular)
• Panic: +1 rule (SAT→CircuitSAT)
• Total: 16 buggy rules (5 original + 11 new)

All ~55 remaining non-ILP rules pass all applicable checks.