feat: add NAESatisfiability → SetSplitting reduction (#841) [full pipeline v2]

[zazabap]

Summary

Implements NAESatisfiability → SetSplitting using the updated /verify-reduction → /add-reduction pipeline. Compare with PR #984 (old pipeline) to see the differences.

What's new vs PR #984

Aspect	PR #984 (old)	This PR (new)
Type gate	Not checked	Or → Or verified in Step 1
Test vectors JSON	Not exported	Exported, used for Rust test generation
Canonical example in example_db	Missing (#974 Check 9)	Included in rule_builders.rs
Example-db lookup test	Missing (#974 Check 10)	Included in example_db.rs
Verification artifact cleanup	Artifacts left in repo	Cleaned up — Python/Typst/PDF removed
Tests	5 tests	7 tests (added all-assignments round-trip, larger instance)

Commit structure

1. 168f6be — verification artifacts (Typst proof + Python scripts from PR docs: verify reduction #841 — NAESatisfiability → SetSplitting #980)
2. 17e9bca — Rust implementation + example_db + tests + artifact cleanup

The second commit shows the clean pattern: -6942 lines (artifacts removed) + 324 lines (Rust added).

Pipeline flow demonstrated

Issue #841 → /verify-reduction (type gate: Or→Or ✓)
           → Typst proof + constructor (32K checks) + adversary (46K checks)
           → test vectors JSON exported
           → /add-reduction (Rust from verified Python spec)
             → Step 1: reduce_to() + extract_solution()
             → Step 3: 7 tests from test vectors
             → Step 4: canonical example in rule_builders.rs
             → Step 4b: example-db lookup test
             → Step 7: verification artifacts cleaned up

Test plan

• cargo test naesatisfiability_to_setsplitting — 7 tests pass
• cargo clippy — clean
• Canonical example registered and passing coverage gate
• Verification artifacts removed from docs/paper/verify-reductions/

Closes #841

🤖 Generated with Claude Code

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 98.04%. Comparing base (423506c) to head (bd516ef).
⚠️ Report is 1 commits behind head on main.

Additional details and impacted files

@@           Coverage Diff            @@
##             main     #985    +/-   ##
========================================
  Coverage   98.03%   98.04%            
========================================
  Files         784      786     +2     
  Lines       82310    82461   +151     
========================================
+ Hits        80695    80846   +151     
  Misses       1615     1615            

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.