[Rule] Satisfiability to NAESatisfiability

[wwang2]

Source

Satisfiability

Target

NAESatisfiability

Motivation

• NAESatisfiability is currently an isolated node in the reduction graph with zero inbound or outbound edges
• Satisfiability is the root of the entire reduction graph (connects to KSatisfiability, CircuitSAT, MaximumIndependentSet, MinimumDominatingSet, KColoring, etc.)
• This reduction immediately brings NAE-SAT into the connected component, enabling downstream rules like NAE-3SAT → Set Splitting ([Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING #382)
• Classic textbook reduction with clean gadget construction

Reference

• Garey, M. R. & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. Problem [LO1].
• Schaefer, T. J. (1978). "The complexity of satisfiability problems." Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 216–226.

Reduction Algorithm

Given a SAT instance with $n$ variables $x_1, \ldots, x_n$ and $m$ clauses $C_1, \ldots, C_m$:

1. Introduce a fresh sentinel variable $s$ (variable index $n+1$).
2. For each SAT clause $C_j = (l_1 \vee l_2 \vee \cdots \vee l_k)$, construct an NAE clause $C'_j = (l_1, l_2, \ldots, l_k, s)$.

Correctness (forward): If assignment $\alpha$ satisfies the SAT instance, set $s = \text{false}$. In each NAE clause $(l_1, \ldots, l_k, s)$: at least one $l_i$ evaluates to true (by SAT satisfaction) and $s$ is false, so the clause is not-all-equal.

Correctness (backward): Given an NAE-satisfying assignment:

• If $s = \text{false}$: each clause has at least one true literal (since not all can be false when $s$ is already false), so the original SAT formula is satisfied.
• If $s = \text{true}$: flip all variables (including $s$). By the symmetry property of NAE-SAT (complementing all variables preserves NAE satisfaction), we obtain a valid NAE assignment with $s = \text{false}$, reducing to the previous case.

Solution extraction: Given NAE-SAT solution, check sentinel variable. If $s = 0$ (false), return the first $n$ variables directly. If $s = 1$ (true), return the complement of the first $n$ variables.

Edge case: Single-literal SAT clauses $(l_1)$ become $(l_1, s)$ with 2 literals, meeting the NAE-SAT minimum clause length of 2.

Size Overhead

Target metric	Formula
num_vars	num_vars + 1
num_clauses	num_clauses
num_literals	num_literals + num_clauses

Validation Method

Closed-loop test: construct a Satisfiability instance, reduce to NAESatisfiability, solve NAE-SAT with brute force, extract solution back to SAT, and verify it satisfies all clauses. Also test the complement-extraction path by constructing cases where the sentinel ends up true.

Example

Source (SAT): 3 variables, formula: $(x_1 \vee x_2) \wedge (\neg x_1 \vee x_3) \wedge (\neg x_2 \vee \neg x_3)$

Target (NAE-SAT): 4 variables ($x_1, x_2, x_3, s$), clauses:

• $(x_1, x_2, s)$
• $(\neg x_1, x_3, s)$
• $(\neg x_2, \neg x_3, s)$

SAT solution: $(x_1 = \text{false}, x_2 = \text{true}, x_3 = \text{false})$ — config [0, 1, 0].

NAE-SAT solution with $s = \text{false}$: $(0, 1, 0, 0)$

• Clause 1 $(x_1, x_2, s) = (F, T, F)$: has true and false ✓
• Clause 2 $(\neg x_1, x_3, s) = (T, F, F)$: has true and false ✓
• Clause 3 $(\neg x_2, \neg x_3, s) = (F, T, F)$: has true and false ✓

Extracted SAT solution: $s = 0$, so return first 3 variables directly: [0, 1, 0] ✓

This example is non-trivial because the NAE condition is strictly stronger than SAT — not every SAT solution is an NAE-SAT solution. For instance, the assignment $(0,1,0)$ satisfies the original SAT formula, but its NAE-SAT extension $(0,1,0,0)$ fails NAE on any clause where all selected literals evaluate to the same truth value.

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing path Satisfiability → NAESatisfiability; connects isolated node
Non-trivial	✅ Pass	Sentinel variable construction with complement-based solution extraction
Correctness	⚠️ Warn	G&J problem number ambiguous (LO1 is SAT, not NAE-SAT); Schaefer (1978) verified
Well-written	⚠️ Warn	Minor: confusing self-contradictory commentary in example section

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

Pass. No reduction path exists from Satisfiability to NAESatisfiability. NAESatisfiability is currently an isolated node in the reduction graph with zero inbound or outbound edges. This reduction immediately connects it to the main component via the reduction graph root (Satisfiability). Strong motivation provided — enables downstream rules like NAE-3SAT → Set Splitting (#382).

Non-trivial

Pass. The reduction involves a genuine structural transformation:

• Introduces a fresh sentinel variable $s$
• Modifies every clause by appending $s$
• Solution extraction requires detecting the sentinel's value and potentially complementing all variables (exploiting NAE-SAT's complement symmetry)

This is not a simple relabeling, subtype coercion, or identity reduction.

Correctness

⚠️ Warn — G&J problem number ambiguity.

1. Schaefer (1978): Verified correct. Paper exists in ACM DL (DOI: 10.1145/800133.804350), discusses NAE-SAT, and establishes its NP-completeness via the dichotomy theorem. Already in project bibliography (references.bib). ✅

2. Garey & Johnson (1979): The issue cites "Problem [LO1]" but LO1 is Satisfiability (SAT) in G&J's appendix. NAE-SAT is problem LO3 in G&J. The citation may be intentionally referencing the source problem (SAT = LO1), but this is ambiguous and could be read as claiming NAE-SAT is LO1. Recommendation: Clarify the reference — cite LO1 for SAT and LO3 for NAE-SAT, or note "see discussion under LO1."

3. Sentinel variable construction: This is a well-known textbook reduction widely taught in complexity courses. Schaefer's original paper establishes NP-completeness of NAE-SAT through the dichotomy theorem framework rather than via an explicit sentinel construction. The sentinel reduction is a standard pedagogical presentation of the result, not directly from Schaefer's paper. This is fine for the issue — just noting for precision.

4. Reduction correctness: The forward and backward proofs are correct. The complement symmetry argument (if $s = \text{true}$, flip all variables) is valid since NAE-SAT is closed under complementation.

5. Overhead formulas verified against NAESatisfiability model getters (num_vars, num_clauses, num_literals):

   • num_vars = num_vars + 1 — adds sentinel ✅
   • num_clauses = num_clauses — same clause count ✅
   • num_literals = num_literals + num_clauses — one sentinel literal per clause ✅

Well-written

⚠️ Warn — minor issue in example commentary.

Template completeness: All required sections present and substantive. ✅

Section	Status
Source	✅ Satisfiability (valid, resolves via pred show)
Target	✅ NAESatisfiability (valid, resolves via pred show)
Motivation	✅ Concrete: connects isolated node, enables downstream rules
Reference	✅ Two citations (one with ambiguous problem number — see Correctness)
Reduction Algorithm	✅ Complete: step-by-step, forward/backward proofs, solution extraction, edge case
Size Overhead	✅ Correct metric names matching target getters
Validation Method	✅ Closed-loop test with complement-extraction path
Example	✅ Fully worked (see note below)

Algorithm completeness: Excellent — includes numbered construction, correctness proofs in both directions, explicit solution extraction procedure, and edge case handling for single-literal clauses. ✅

Symbol consistency: $n$ and $m$ defined inline ("$n$ variables... $m$ clauses"), overhead table uses code metric names (num_vars, num_clauses, num_literals) matching target getters. ✅

Example quality:

• 3 variables, 3 clauses — non-trivial ✅
• 2 satisfying assignments for the SAT formula ((0,1,0) and (1,0,1)) and 6 non-satisfying — good mix ✅
• Fully worked: source → construction → target → verification → extraction ✅

Minor issue: The final paragraph of the example section is confusing and self-contradictory: "the all-true assignment $(1,1,1,0)$ satisfies SAT but fails NAE on clause 1 since $(T, T, F)$ has both, while $(T, T, F)$ actually does satisfy NAE" — this contradicts itself in the same sentence. The intended point (NAE is strictly stronger than SAT) is valid but the worked example undercuts it. Consider removing or rewriting this paragraph.

Recommendations

• Fix G&J reference: cite both LO1 (SAT) and LO3 (NAE-SAT) for clarity
• Remove or rewrite the self-contradictory final paragraph in the example section

[zazabap]

Issue Quality Check — Rule (Re-check)

Check	Result	Details
Usefulness	✅ Pass	No existing path Satisfiability → NAESatisfiability; connects isolated node
Non-trivial	✅ Pass	Sentinel variable construction with complement-based solution extraction
Correctness	✅ Pass	Schaefer (1978) verified in bibliography; G&J cited for SAT (LO1); reduction is standard textbook result
Well-written	⚠️ Warn	Self-contradictory commentary in final example paragraph

Overall: 3 passed, 0 failed, 1 warning

Re-check with --force. Previous check (2026-03-23): 2 pass, 0 fail, 2 warnings → Now: 3 pass, 0 fail, 1 warning. Correctness upgraded from Warn to Pass (G&J LO1 reference is reasonable as a SAT source citation).

---

Usefulness

Pass. No reduction path exists from Satisfiability to NAESatisfiability. NAESatisfiability is currently an isolated node in the reduction graph (zero inbound edges; only outbound to ILP). This reduction immediately connects it to the main component via the reduction graph root (Satisfiability). Strong motivation provided — enables downstream rules like NAE-3SAT → Set Splitting (#382).

Non-trivial

Pass. The reduction involves a genuine structural transformation:

• Introduces a fresh sentinel variable $s$
• Modifies every clause by appending $s$
• Solution extraction requires detecting the sentinel's value and potentially complementing all variables (exploiting NAE-SAT's complement symmetry)

This is not a simple relabeling, subtype coercion, or identity reduction.

Correctness

Pass.

1. Schaefer (1978): Verified in project bibliography (schaefer1978 in references.bib). Paper exists in ACM DL (DOI: 10.1145/800133.804350), discusses NAE-SAT, and establishes its NP-completeness via the dichotomy theorem. ✅

2. Garey & Johnson (1979), Problem [LO1]: LO1 is Satisfiability (SAT), confirmed in the project knowledge base. The issue cites this as the source problem reference — this is reasonable context for the reduction's starting point. NAE-SAT is problem LO3 in G&J, which the issue does not misattribute. ✅

3. Reduction correctness: The sentinel variable construction is a well-known textbook reduction. The forward proof (set $s = \text{false}$, SAT satisfaction guarantees at least one true literal per clause) and backward proof (complement symmetry when $s = \text{true}$) are both correct. ✅

4. Overhead formulas verified against NAESatisfiability getters (num_vars, num_clauses, num_literals):

   • num_vars = num_vars + 1 — adds sentinel ✅
   • num_clauses = num_clauses — same clause count ✅
   • num_literals = num_literals + num_clauses — one sentinel literal per clause ✅

Recommendation

• Consider also citing G&J LO3 (NAE-SAT) for completeness alongside LO1 (SAT).

Well-written

⚠️ Warn — minor issue in example commentary.

Template completeness: All required sections present and substantive. ✅

Section	Status
Source	✅ Satisfiability (valid, resolves via pred show)
Target	✅ NAESatisfiability (valid, resolves via pred show)
Motivation	✅ Concrete: connects isolated node, enables downstream rules
Reference	✅ Two citations (Schaefer 1978, G&J 1979)
Reduction Algorithm	✅ Complete: numbered steps, forward/backward proofs, solution extraction, edge case
Size Overhead	✅ Correct metric names matching target getters (num_vars, num_clauses, num_literals)
Validation Method	✅ Closed-loop test with complement-extraction path
Example	✅ Fully worked

Algorithm completeness: Includes numbered construction, correctness proofs in both directions, explicit solution extraction procedure, and edge case handling for single-literal clauses. ✅

Symbol consistency: Variables $n$, $m$ defined inline ("$n$ variables... $m$ clauses"), overhead table uses code metric names matching target getters. ✅

Example quality:

• 3 variables, 3 clauses — non-trivial ✅
• 2 satisfying assignments for the SAT formula ([0,1,0] and [1,0,1]) and 6 non-satisfying — good mix ✅
• Fully worked: source → construction → target → verification → extraction ✅

Minor issue: The final paragraph of the example section is self-contradictory: it claims the all-true assignment $(1,1,1)$ "satisfies SAT" but $(1,1,1)$ actually fails clause 3 ($\neg x_2 \vee \neg x_3$). The intended point (NAE is strictly stronger than SAT) is valid, but the worked example is incorrect. Consider removing or rewriting this paragraph.

Recommendations

• Remove or fix the self-contradictory final paragraph in the example section — $(1,1,1)$ does not satisfy the original SAT formula
• Consider citing G&J LO3 (NAE-SAT) alongside LO1 (SAT)

[zazabap]

Fix-issue changelog

• Example: Rewrote self-contradictory final paragraph. The old text incorrectly claimed (1,1,1,0) satisfies SAT when it fails clause 3. Replaced with a correct illustration of the SAT-vs-NAE distinction.

Applied by /fix-issue.