Fix #1101: NAESatisfiability to Satisfiability

[isPANN]

Summary

Implement the direct clause-doubling reduction from NAESatisfiability to Satisfiability.

Fixes #1101

[isPANN]

Implementation Summary

Changes

• Added the direct NAESatisfiability -> Satisfiability reduction by emitting each source clause and its literalwise complement, with identity witness extraction and exact overhead metadata.
• Registered the primitive reduction and its canonical three-variable example.
• Added semantic tests for feasible and infeasible instances, exact target structure and overhead, empty formulas, arbitrary-width clauses, repeated literals, tautologies, graph registration, and fixture integrity.
• Added a fixture-backed paper theorem, proof, tutorial example, and the STACS 2025 reference.

Deviations from Plan

• Consolidated the canonical source instance into one constructor shared by the example export and closed-loop test to prevent fixture drift.
• No other deviations.

Open Questions

• None.

Verification

• Mathematical constructor: 208,290 checks.
• Independent adversary: 459,326 assignment instances and 918,652 direction checks.
• Cross-comparison: 5 targets and 29 assignments, zero disagreements.
• make test clippy: passed.
• make paper: passed.

[isPANN]

Agentic Review Report

Structural Check

Structural Review: rule NAESatisfiability → Satisfiability

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/naesatisfiability_satisfiability.rs
2	#[reduction(...)] macro present	PASS — exact overhead metadata at src/rules/naesatisfiability_satisfiability.rs:26
3	ReductionResult impl present	PASS — src/rules/naesatisfiability_satisfiability.rs:13
4	ReduceTo impl present	PASS — src/rules/naesatisfiability_satisfiability.rs:31
5	Test path link present	PASS — src/rules/naesatisfiability_satisfiability.rs:82
6	Test file exists	PASS — src/unit_tests/rules/naesatisfiability_satisfiability.rs
7	Closed-loop test present	PASS — src/unit_tests/rules/naesatisfiability_satisfiability.rs:10
8	Registered in rules/mod.rs	PASS — module at src/rules/mod.rs:112; canonical example aggregation at src/rules/mod.rs:521
9	Canonical rule example registered	PASS — rule-local specification at src/rules/naesatisfiability_satisfiability.rs:65, registered at src/rules/mod.rs:521
10	Example-db lookup tests exist	PASS — generic database coverage plus rule-local fixture validation at src/unit_tests/rules/naesatisfiability_satisfiability.rs:109
11	Paper reduction-rule entry present	PASS — docs/paper/reductions.typ:13071
12	Blacklisted generated-file check	PASS — no blacklisted generated paths in the corrected stacked-PR delta

Build Status

• make test: PASS — all workspace, integration, CLI, macro, and documentation tests passed; the six new rule tests passed.
• make clippy: PASS — cargo clippy --all-targets --features ilp-highs -- -D warnings completed successfully.

Semantic Review

• Reduction construction: OK — each source clause is emitted together with its literalwise complement.
• Mathematical trace: OK — the original clause excludes an all-false literal pattern and the complemented clause excludes an all-true pattern, so their conjunction accepts exactly the NAE assignments.
• Correctness preservation: OK — the paper independently proves both directions at docs/paper/reductions.typ:13115-13117.
• extract_solution: OK — identity extraction returns exactly the source variables because no variables are added or reordered.
• Exact overhead: OK — num_vars = n, num_clauses = 2m, and num_literals = 2L match the construction and runtime metadata assertions.
• Edge cases: OK — empty conjunction, arbitrary width, repeated literals, tautological clauses, infeasibility, and identity extraction are covered.
• Example quality: OK — the canonical example contains full source/target instances and an end-to-end witness.
• Paper quality: OK — precise construction, sound bidirectional proof, exact sizes, fixture-backed tutorial, and identity extraction including n=0.
• Reference integration: OK — STACS 2025 reference added at docs/paper/references.bib:1583.

Issue Compliance

#	Check	Status
1	Source/target match issue	OK
2	Reduction algorithm matches	OK
3	Solution extraction matches	OK
4	Correctness preserved	OK
5	Overhead expressions match	OK
6	Example matches	OK

Summary

• 12/12 structural checks passed.
• 6/6 issue-compliance checks passed.
• No structural, mathematical, overhead, extraction, paper-proof, generated-file, build, or lint issues found.

---

Quality Check

Quality Review

Design Principles

• DRY: OK — clause transformation is implemented once and shared test/example infrastructure is reused.
• KISS: OK — the construction is a direct single-pass flat_map with no unnecessary branching or abstraction.
• HC/LC: OK — construction, extraction, and canonical fixture are localized in the rule module; registration is limited to src/rules/mod.rs.

Test Quality

• Naive test detection: OK.
  • Closed-loop coverage checks source evaluation, target evaluation, and extraction.
  • An explicitly infeasible repeated-literal clause checks both sides.
  • Exact emitted clauses and all three overhead fields are asserted.
  • Exhaustive assignment comparison covers empty, arbitrary-width, repeated-literal, and tautological cases.
  • Graph registration and canonical fixture behavior are independently asserted.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

None.

Minor (Nice to Have)

None.

Summary

• No quality issues found in PR Fix #1101: NAESatisfiability to Satisfiability #1110’s five-file delta against origin/1075-growth-domain.

---

Agentic Feature Tests

Agentic Feature Test Report

Feature: NAESatisfiability → Satisfiability
Project type: Rust library + pred CLI
Profile: Ephemeral downstream CLI user
Verdict: Partial failure
Critical issues: 1 confirmed user-path failure
Repository changes: None

Test Results

Area	Result
Default CLI build	Pass
Rule discoverability (pred list --rules, pred show, pred path)	Pass
Canonical example creation	Pass
Source solving	Pass
Direct reduction	Pass
Satisfiable bundle solving/extraction	Pass
Repeated-literal infeasible semantics	Reduction correct
Infeasible bundle solving	Fail
Empty conjunction semantics	Pass via valid raw problem JSON
Empty conjunction creation through --clauses ''	Not exposed by documented CLI syntax

The canonical workflow produced the expected paired clauses, solved both source and target as Or(true), and extracted the identical witness. The repeated-literal source (x1, x1) reduced correctly to (x1 OR x1) AND (NOT x1 OR NOT x1); direct source and target solves both returned Or(false). A zero-variable empty conjunction reduced to an empty SAT formula and solved/extracted successfully.

Issues Found

High — Infeasible reduction bundles cannot be solved

Classification: Confirmed in the current PR worktree and independently reproduced by review-pipeline.
Scope: Generic bundle solver exposed by this rule; not introduced by PR #1110’s five-file delta.
Location: problemreductions-cli/src/commands/solve.rs:130

Reproduction:

pred create NAESatisfiability --num-vars 1 --clauses '1,1' -o repeated.json
pred reduce repeated.json --to Satisfiability -o repeated-bundle.json
pred solve repeated-bundle.json --solver brute-force

Actual result, exit status 1:

Error: Bundle solving requires a witness-capable target problem and
witness-capable reduction path; Satisfiability only supports
aggregate-value solving.

This diagnostic is incorrect: Satisfiability is witness-capable. The target is infeasible, so no witness exists; direct source and target solves correctly report Or(false). A downstream user therefore cannot use the documented reduce-then-solve workflow for negative instances.

Recommended fix: Distinguish “infeasible, therefore no witness exists” from “target lacks witness support.” For an exact witness-preserving bundle whose target evaluates to Or(false), return source infeasibility without attempting witness extraction or reporting a capability error.

Friction Notes

• The rule is discoverable through catalog/show/path output, but generic docs do not explain this clause-doubling construction.
• Empty clause lists and empty configurations are not expressible using --clauses '' / --config ''; raw problem JSON was required for that boundary test.
• These notes do not indicate a mathematical defect in the reduction.

---

Generated by review-pipeline