Fix #1102: MaxCut/One to Maximum2Satisfiability

[isPANN]

Summary

Add the unweighted MaxCut to Maximum 2-SAT reduction as a stacked change on the MaxCut/One model work.

Fixes #1102

[isPANN]

Implementation Summary

Changes

• Added the direct witness-preserving MaxCut<SimpleGraph, One> -> Maximum2Satisfiability rule with exact n-variable, 2m-clause overhead and identity witness extraction.
• Added closed-loop, pointwise affine-identity, exact-structure, empty/isolated/disconnected, self-loop, parallel-edge, exhaustive small-graph, and canonical-example tests.
• Registered a canonical four-cycle-plus-diagonal example with source optimum 4 and target optimum 9.
• Added a fixture-driven paper theorem, worked example, truth-table proof, loop/parallel-edge discussion, and the Gramm et al. reference.

Verification

• Mathematical constructor: 3,402,051 checks, 0 failures.
• Independent adversary: 1,481,769 checks, 0 failures.
• Cross-comparison: 5 shared targets and 229 value/extraction checks, 0 disagreements.
• make paper, make fmt-check, make clippy, make test, and make coverage passed.
• Example, graph, and schema exports completed successfully.

Deviations from Plan

• This stacked base has no make regenerate-fixtures target. The equivalent example export command was run directly; example, graph, schema, and PDF outputs are gitignored in this checkout, so no generated files were committed.
• The repository Rust test exhausts simple graphs through four vertices; the separate mathematical validators exhaust through five vertices and add focused loop/parallel multigraph coverage.

Open Questions

• None.

[isPANN]

Agentic Review Report

Scope note: This is a stacked PR targeting 1075-growth-domain. Review findings are scoped to the actual five-file PR delta, not the parent branch's main-relative changes.

Structural Check

Structural Review: rule MaxCut/One → Maximum2Satisfiability

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/maxcut_maximum2satisfiability.rs
2	#[reduction(...)] macro present	PASS — exact overhead declared at src/rules/maxcut_maximum2satisfiability.rs:29
3	ReductionResult implementation present	PASS — src/rules/maxcut_maximum2satisfiability.rs:16
4	ReduceTo implementation present	PASS — unit-weight MaxCut<SimpleGraph, One> to Maximum2Satisfiability at src/rules/maxcut_maximum2satisfiability.rs:35
5	Test module link present	PASS — src/rules/maxcut_maximum2satisfiability.rs:78
6	Test file exists	PASS — src/unit_tests/rules/maxcut_maximum2satisfiability.rs
7	Closed-loop test present	PASS — src/unit_tests/rules/maxcut_maximum2satisfiability.rs:31; four additional focused tests cover structure, boundaries, exhaustive graphs, and the canonical example
8	Registered in rules/mod.rs	PASS — module at src/rules/mod.rs:79
9	Canonical rule example registered	PASS — builder at src/rules/maxcut_maximum2satisfiability.rs:56, aggregated at src/rules/mod.rs:491, and validated at src/unit_tests/rules/maxcut_maximum2satisfiability.rs:125
10	Example-db lookup/build tests exist	PASS — shared lookup, uniqueness, consistency, and authored-direct-reduction coverage tests exist; full example-db test suite passed
11	Paper reduction-rule entry present	PASS — docs/paper/reductions.typ:11451, with construction, truth table, correctness proof, edge-case discussion, extraction, and executable example
12	Blacklisted generated files absent	PASS — no blacklisted generated path appears in the five-file delta

Build Status

• make test: PASS — 5,436 library tests, 75 integration tests, 161 CLI unit tests, 330 CLI integration tests, 17 symbolic CLI tests, 26 macro tests, and all doctests passed with zero failures.
• make clippy: PASS — cargo clippy --all-targets --features ilp-highs -- -D warnings completed successfully.
• Worktree remained clean after verification.

Semantic Review

• Reduction construction: OK — each edge occurrence (u,v) produces [u+1,v+1] and [-(u+1),-(v+1)].
• Mathematical correctness: OK — equal endpoint bits satisfy exactly one clause and unequal bits satisfy both, giving sat(x) = m + cut_G(x) and identical maximizers.
• Solution extraction: OK — the target uses the source's n Boolean variables in the same order, so identity extraction has the correct source length and meaning.
• Overhead accuracy: OK — exactly num_vertices variables and two clauses per edge occurrence match the declared formulas.
• Loop handling: OK — complementary repeated-literal clauses contribute one while a loop contributes zero to the cut; explicitly tested.
• Parallel-edge handling: OK — repeated clause pairs preserve edge multiplicity; explicitly tested.
• Test strength: OK — pointwise preservation and extraction are checked for every assignment, with all simple graphs through four vertices plus empty, isolated, disconnected, loop, and parallel cases.
• Canonical example: OK — four-cycle plus diagonal produces four variables, ten clauses, source optimum 4, and target optimum 9.
• Paper proof: OK — its truth table, affine identity, both optimality directions, loop/parallel analysis, and extraction argument are logically sound.

Issue Compliance

#	Check	Status
1	Source/target match issue	OK — MaxCut<SimpleGraph, One> → Maximum2Satisfiability
2	Reduction algorithm matches	OK — one variable per vertex and the requested clause pair per edge occurrence
3	Solution extraction matches	OK — direct identity mapping
4	Correctness preserved	OK — exact affine identity holds pointwise, including loops and parallel occurrences
5	Overhead expressions match	OK — exactly n variables and 2m clauses
6	Example matches	OK — requested graph, ten clauses, witness [0,1,0,1], and values 4/9

Summary

• 12/12 structural checks passed.
• 6/6 issue-compliance checks passed.
• No structural, mathematical, overhead, extraction, test, generated-file, or issue-compliance findings.

---

Quality Check

Quality Review

Design Principles

• DRY: OK — Clause-pair construction is expressed once in a direct iterator pipeline; no duplicated production logic was introduced.
• KISS: ISSUE — The implementation is otherwise minimal, but unchecked usize-to-i32 conversions silently corrupt vertex identifiers outside the signed-literal range (src/rules/maxcut_maximum2satisfiability.rs:44-45).
• HC/LC: OK — Reduction construction, extraction, example registration, and tests remain in established modules without new coupling or mixed responsibilities.

Test Quality

• Naive test detection: OK.
  • The closed-loop test independently solves both optima and verifies every optimal target witness extracts to an optimal source witness.
  • The structure test checks exact clauses and the affine identity for every assignment of a nontrivial four-vertex, five-edge graph.
  • Boundary coverage includes empty, isolated, disconnected, loop, and parallel-edge inputs.
  • Exhaustive coverage checks every simple graph through four vertices and every assignment.
  • Canonical example serialization and witness contents are checked semantically.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• src/rules/maxcut_maximum2satisfiability.rs:44-45 converts one-based vertex identifiers from usize to i32 using as. For an index at or above i32::MAX, this wraps into a negative or zero literal, changing polarity, aliasing variables, or creating literal zero while the target still advertises the original num_vertices. Use checked conversion and fail explicitly when the source cannot be represented by CNFClause's signed-literal encoding.

Minor (Nice to Have)

None.

Summary

• Important — replace the unchecked one-based vertex-index casts with explicit checked conversion so unrepresentable graphs fail instead of producing corrupted literals.

---

Agentic Feature Tests

Feature: MaxCut/SimpleGraph/One → Maximum2Satisfiability
Verdict: Pass with one confirmed medium-severity documentation issue
Critical issues: 0
Repository changes: None; worktree remained clean.

Check	Result
CLI build	Pass
Rule visible in pred list --rules	Pass
pred show for source and target	Pass
Canonical rule-example creation	Pass
Source brute-force solve	Pass: optimum Max(4)
Exact-target reduction	Pass
Target dimensions	Pass: 4 variables, 10 clauses
Target brute-force solve	Pass: optimum Max(9)
Default ILP target solve	Pass: optimum Max(9)
Bundle solve and witness extraction	Pass
Canonical configuration evaluation	Pass
Objective relation	Pass: `sat(x) =

Tested downstream workflow

The test exercised pred list --rules, pred show for both endpoints, rule-example creation, source solving, exact-target reduction, bundle inspection/solving, target-side example creation/solving, and evaluation of optimal and non-optimal configurations. The catalog showed the exact edge and overhead. The canonical rule source had four vertices and five edges; reduction produced ten clauses and preserved [0,1,0,1]. Bundle solving reported target Max(9) and extracted source Max(4). The all-zero assignment also confirmed Max(5) = |E| + Max(0).

Issues Found

1. [Medium, confirmed] Feature-specific paper commands select the model example instead of the displayed rule example.

   Location: docs/paper/reductions.typ:11456

   The displayed command is effectively:

   pred create --example MaxCut/SimpleGraph/One -o maxcut.json
   

   This creates the generic model fixture with five vertices and seven edges, while the surrounding paper example describes the rule fixture with four vertices and five edges. Reproducing the complete displayed sequence yielded 5 variables/14 clauses and optima 13/6 instead of 4 variables/10 clauses and optima 9/4; its four-bit evaluation then failed because the created source has five variables.

   The reproducible rule-example selector is:

   pred create --example MaxCut/SimpleGraph/One --to Maximum2Satisfiability -o maxcut.json
   

   Classification: confirmed in the current PR worktree. The reduction and CLI behavior are correct; this is a documentation defect.

Discoverability and Friction

General CLI documentation correctly explains that rule fixtures require both --example <SOURCE> and --to <TARGET>. Catalog and show output make the new rule easy to discover. The significant friction is the paper command block omitting --to, contradicting the general guidance and failing to reproduce its own example.

---

Generated by review-pipeline