feat: add NAESatisfiability → SetSplitting reduction (#841)

[zazabap]

Summary

Implements the NAESatisfiability → SetSplitting reduction rule using the new /verify-reduction → /add-reduction pipeline.

This is the first reduction implemented through the verified artifacts pipeline:

1. /verify-reduction produced Typst proof + dual Python scripts (PR docs: verify reduction #841 — NAESatisfiability → SetSplitting #980, 79K+ checks)
2. /add-reduction translated the verified Python reduce() to Rust

Implementation

Construction (from verified Python spec):

• Universe: 2n elements (positive + negative literal per variable)
• Complementarity subsets: {2i, 2i+1} for each variable i
• Clause subsets: map each literal to its universe element
• Overhead: universe_size = 2 * num_vars, num_subsets = num_clauses + num_vars

Solution extraction: Variable i is true iff element 2i is in partition part 0.

Files

• src/rules/naesatisfiability_setsplitting.rs — reduction implementation
• src/unit_tests/rules/naesatisfiability_setsplitting.rs — 5 tests (closed-loop, infeasible, structure, all-witnesses, known-assignment)
• docs/paper/verify-reductions/ — Typst proof + Python verification scripts from PR docs: verify reduction #841 — NAESatisfiability → SetSplitting #980

Pipeline Demo

Issue #841 → /verify-reduction (PR #980: 79K checks, 0 failures)
           → /add-reduction (this PR: Rust impl from verified Python spec)
           → /review-pipeline (next: agentic test with pred reduce/solve)

Test plan

• cargo test naesatisfiability_to_setsplitting — 5/5 pass
• cargo clippy — clean
• Reduction graph updated (SetSplitting now has 1 incoming reduction)

Closes #841

🤖 Generated with Claude Code

[zazabap]

Agentic Review Report

Structural Check

#	Check	Result
1	Rule file exists at src/rules/naesatisfiability_setsplitting.rs	PASS
2	Test file exists with at least 3 tests	PASS (5 tests)
3	Registered in src/rules/mod.rs	PASS
4	#[reduction(overhead)] macro present	PASS
5	Mathematical correctness (traced YES vector: n=4, 4 clauses → 8 subsets match expected)	PASS
6	extract_solution correctness (var i true iff config[2i]==0)	PASS
7	Overhead formula accuracy (universe_size=2n, num_subsets=n+m)	PASS
8	Build passes	PASS
9	Tests pass (5/5)	PASS
10	Clippy clean	PASS

10/10 structural checks pass.

---

Quality Check

Category	Rating
DRY	GOOD
KISS	GOOD
Cohesion	GOOD
Test quality	GOOD (5 tests: closed-loop, infeasible, structure, all-witnesses, known-assignment)
Naming	GOOD (follows test_<source>_to_<target>_* convention)
Error handling	MINOR — literal_to_element(0) would silently produce bogus index; add debug_assert!(lit != 0)
Documentation	GOOD (module doc explains encoding, overhead annotated)

One minor suggestion: add debug_assert!(lit != 0) to literal_to_element for defensive safety. Low risk since NAE-SAT never produces zero literals.

---

Agentic Feature Tests

#	Test	Result
1	pred list shows both NAESatisfiability and SetSplitting	PASS
2	pred show NAESatisfiability includes SetSplitting in outgoing	PASS
3	pred show SetSplitting includes NAESatisfiability in incoming	PASS
4	pred path NAESatisfiability SetSplitting finds direct path	PASS
5	pred create --example NAESatisfiability creates instance	PASS
6	pred reduce to SetSplitting succeeds	PASS
7	pred solve via direct ILP returns Or(true)	PASS
8	pred solve via NAE→SS→ILP chain returns Or(true) with correct back-mapping	PASS

8/8 agentic tests pass. End-to-end pipeline works: create → reduce → solve → extract.

---

Pipeline provenance: This reduction was implemented via the /verify-reduction → /add-reduction pipeline. Python verification (79K+ checks, dual independent implementations) preceded the Rust translation.

Generated by review-pipeline