[isPANN]

Stacked on #1217. Base: issue-1213-direct-qubo-phase4.

Adds a registered Decision<ILP<bool, i64>> → Satisfiability reduction using binary adders, comparisons, and Tseitin clauses. It encodes signed constraints and the objective threshold, recovers the original binary assignment from a satisfying witness, and supplies parameter bounds and a manual proof. DecisionILP also gains construction metadata and a fixed ILP solver pipeline.

For example, with x₀ + x₁ + x₂ = 1 and objective 3x₀ + 2x₁ + x₂, minimizing with bound 1 yields [0, 0, 1]; bound 0 produces an unsatisfiable SAT instance. Maximizing with bound 3 yields [1, 0, 0]; bound 4 is unsatisfiable. This is a decision reduction; it adds no Turing edge and does not claim to merge the optimization problems into one mutually reducible class.

Also fixes MaximalIS and MinimumVertexCover public validators accepting truncated or oversized assignments. For a two-vertex edge, [true] previously passed the public validators while evaluate() rejected its length; both APIs now reject it. Removes redundant timetable reconstruction, internal index clamping, panic wrappers, and implementation-name tests. Existing reduction tests now check recovered witnesses and known optimal values instead of copied fields.

Validation:

• make check passes: formatting, Clippy across all targets/features, and workspace tests including ignored tests and doctests.
• The two existing validator tests failed on truncated assignments before the fix and pass afterward.
• SAT encoding checks exercise both objective senses, feasible/infeasible thresholds, 432 pinned binary assignments with signed rows, and empty/full-width integer cases.
• Paper build and persisted CLI reduce/solve workflow passed before the final cleanup; coverage and paper build were not rerun after that cleanup.

[GiggleLiu]

Agentic Review Report

Reviewed head 0daa9a8265aefe40983beeba0464f8feea8c3316 against its stacked base 3d3b020c0d93f5e27ecce98eaf148321a7eced9d.

Structural and semantic

No blocking findings in this PR's changes. Both reduction endpoints have value Or; the objective sense is handled by Extremum::meets_bound. Signed normalization, constant rows, ripple adders, gate clauses and the complemented greater-than comparator preserve each binary assignment. Row normalization merges duplicate variables before encoding. Checked positive/negative totals bound the adder width by 64 and justify the declared variable, clause and literal bounds. Extraction validates the complete SAT witness before projecting its first source coordinates.

The public MaximalIS and MinimumVertexCover validators now check assignment length before indexing. The removed Lehmer clamp is internal to enumeration with valid dimensions. Decision construction and the ILP pipeline use existing registry mechanisms.

The new reference is traceable to the authors' paper, Translating Pseudo-Boolean Constraints into SAT. The proof in this PR supplies its own normalization, equivalence and size derivations.

Quality and verification

Built the exact PR head locally. All four new binary-ILP-to-SAT tests passed, including 432 signed assignment comparisons, both objective senses, infeasible bounds, empty rows, full-width coefficients, malformed witnesses and rejected arithmetic overflow. The complete library test executable then passed all 6,319 tests. This includes inherited stack changes and is not independent approval of those changes.

Feature test

Built the development CLI in the isolated checkout. Created and inspected the canonical DecisionILP instance, solved it with brute force, persisted its direct SAT route and reduction bundle, and solved the bundle through the SAT ILP pipeline. Both returned [0, 0, 1] and Or(true). No global CLI installation was changed.

Findings and disposition

No new blocking finding. Hold the PR until its prerequisite PRs are corrected and merged; this review does not authorize merging an unreviewed or defective base branch into main. No GitHub CI was recorded on this stacked PR at review time.

GitHub PR audit

GATE: PASS

• harm.secrets: OK. No credentials or private data introduced.
• harm.dangerous-files: OK. Source, tests and manual changes only.
• harm.generated-artifacts: OK. No generated exports or build outputs.
• harm.cache: OK. No caches committed.
• harm.debug-leftovers: OK. No temporary probes in production code.
• pr.description-quality: OK. Encoding, validator repairs and verification limits are described.
• pr.traceable: OK. Purpose and dependency on #1217 are explicit.

[GiggleLiu]

Agentic Review Report: stack consolidation

Approved current head b84842c747657d8238bc6cbb89e341f873a66eab for merging into issue-1213-direct-qubo-phase4 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.