[Model] NAESatisfiability

[isPANN]

Motivation

Not-All-Equal SAT (G&J LO3) is a fundamental SAT variant with a beautiful symmetry property (if α is a solution, so is ¬α) and deep connections to graph coloring and MaxCut. It bridges the formula and graph problem categories. NAE-3SAT is the standard intermediate problem in the classic 3SAT → MaxCut reduction chain (relevant to #166).

Associated rule issues:

• [Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING #382 (NAE-3SAT → Set Splitting, open)
• Planned: SAT → NAESatisfiability, NAESatisfiability → MaxCut

Definition

Name: NAESatisfiability
Reference: Schaefer, T. J. (1978). "The complexity of satisfiability problems." Proc. 10th STOC, 216–226. Also Garey & Johnson (1979), Problem LO3.

Given a Boolean formula in CNF with n variables x_1, ..., x_n and m clauses C_1, ..., C_m, find a truth assignment such that in every clause, not all literals have the same truth value — i.e., each clause contains at least one true literal and at least one false literal.

Key symmetry: if α is a NAE-satisfying assignment, so is ¬α (the complement).

Variables

• Count: n (one per Boolean variable)
• Per-variable domain: binary {0, 1}
• Dims: [2; n] — n binary variables
• Meaning: x_i = 1 iff variable i is assigned true. A configuration is satisfying if every clause contains at least one true literal and at least one false literal.

Schema (data type)

Type name: NAESatisfiability
Variants: none (reuses CNFClause from existing SAT infrastructure)

Field	Type	Description
num_vars	usize	Number of Boolean variables n
clauses	Vec<CNFClause>	Clauses; each clause has ≥ 2 literals

Size fields: num_vars = n, num_clauses = m, num_literals = total literal count.

Complexity

• Best known exact algorithm: 2^num_vars — brute-force over all assignments (halved to 2^(n-1) by NAE symmetry — fix x_1 = true). No dedicated sub-2^n algorithm substantially better than 3-SAT.
• References: Schaefer (1978), dichotomy theorem.

Extra Remark

NAE-SAT has complement symmetry: any NAE-satisfying assignment and its bitwise complement are both solutions. This makes NAE-SAT naturally connected to MaxCut (partition problems). NAE-3-SAT remains NP-complete even for monotone instances (no negated literals), proven by Schaefer (1978). It is a key problem in Schaefer's dichotomy theorem classifying tractable vs NP-complete Boolean CSPs.

Reduction Rule Crossref

• [Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING #382 (NAE-3SAT → Set Splitting)
• SAT → NAESatisfiability (to be filed)
• NAESatisfiability → MaxCut (to be filed)

How to solve

• It can be solved by (existing) brute force. (Enumerate all 2^n assignments, check NAE constraint on each clause.)
• It can be solved by reducing to ILP.
• Other, refer to ...

Example Instance

Variables: x_1, x_2, x_3, x_4, x_5 (n = 5)
Clauses (NAE-3-SAT):

• C_1: (x_1, x_2, ¬x_3)
• C_2: (¬x_1, x_3, x_4)
• C_3: (x_2, ¬x_4, x_5)
• C_4: (¬x_2, x_3, ¬x_5)
• C_5: (x_1, ¬x_3, x_5)

m = 5 clauses, search space = 2^5 = 32 configurations.

Expected Outcome

Satisfying solution: config = [0, 0, 0, 1, 1] (x_1=F, x_2=F, x_3=F, x_4=T, x_5=T)

• C_1: (F, F, T) — not all equal ✓
• C_2: (T, F, T) — not all equal ✓
• C_3: (F, F, T) — not all equal ✓
• C_4: (T, F, F) — not all equal ✓
• C_5: (F, T, T) — not all equal ✓

Complement config = [1, 1, 1, 0, 0] is also a solution (NAE symmetry).

Total NAE-satisfying assignments: 10 (5 complement pairs).

BibTeX

@article{Schaefer1978,
  author  = {Thomas J. Schaefer},
  title   = {The Complexity of Satisfiability Problems},
  journal = {Conference Record of the 10th Annual ACM Symposium on Theory of Computing (STOC)},
  pages   = {216--226},
  year    = {1978},
  doi     = {10.1145/800133.804350}
}

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	Pass	New problem; concrete reductions to/from existing SAT and MaxCut
Non-trivial	Pass	Genuinely different feasibility constraint from Satisfiability (NAE vs at-least-one-true)
Correctness	Pass	Schaefer (1978) verified in ACM DL and already in references.bib; G&J LO3 confirmed; example brute-force verified
Well-written	Pass	All 12 required sections present and substantive

Overall: 4 passed, 0 failed, 2 warnings

---

Usefulness

NAESatisfiability does not exist in the codebase yet. The issue mentions three concrete reductions:

• SAT → NAESatisfiability (Satisfiability exists ✓)
• NAESatisfiability → MaxCut (MaxCut exists ✓, relevant to [Rule] KSatisfiability to MaxCut #166)
• [Rule] NOT-ALL-EQUAL 3SAT to SET SPLITTING #382 NAE-3SAT → SetSplitting (SetSplitting not yet implemented — does not block this model)

Motivation is substantive: correctly identifies NAE-SAT as the standard intermediate in the 3SAT → MaxCut reduction chain, with complement symmetry bridging formula and graph categories.

Non-trivial

NAESatisfiability is not a re-skin or variant of Satisfiability:

• SAT: each clause needs ≥1 true literal
• NAE-SAT: each clause needs ≥1 true literal and ≥1 false literal (strictly stronger)
• The complement symmetry property (α satisfying ⟹ ¬α satisfying) has no analog in standard SAT
• Cannot be expressed as a type parameter variant — the difference is in the evaluation function, not the data structure
• Not isomorphic to any existing problem in the codebase (checked against all 82 problem types)

Correctness

Reference verification:

• Schaefer (1978) — "The Complexity of Satisfiability Problems," Proc. 10th STOC, pp. 216–226. DOI: 10.1145/800133.804350. ✅ Already in docs/paper/references.bib. NAE-SAT NP-completeness and dichotomy theorem confirmed.
• Garey & Johnson (1979), Problem LO3 — ✅ Confirmed as the standard G&J classification for Not-All-Equal SAT.
• Monotone NAE-3-SAT NP-complete — ✅ Follows from Schaefer's dichotomy theorem, confirmed by multiple sources.
• Complement symmetry — ✅ Mathematically trivial to verify and computationally confirmed on the example.
• Complexity O(2^n) — ✅ Correct for general brute-force. The 2^(n−1) optimization via fixing x₁=true exploiting symmetry is standard.

Example verification (brute-force enumeration of all 16 configs):

• Claimed solution [1,1,0,0]: ✅ NAE-satisfying
• Complement [0,0,1,1]: ✅ NAE-satisfying (confirms symmetry)
• Total NAE-satisfying assignments: 4 — {[0,0,1,1], [0,1,1,1], [1,0,0,0], [1,1,0,0]}
• Two complement pairs: {[1,1,0,0], [0,0,1,1]} and {[1,0,0,0], [0,1,1,1]}

Well-written

All 12 required sections are present and substantive. Symbols defined before use, consistent across sections. Schema reuses existing CNFClause infrastructure — good integration.

⚠️ Warning 1: Example size. Search space is 2⁴ = 16 configurations, below the recommended 128–10,000 range. A 5-variable instance (32 configs) would provide richer verification, though this is not blocking.

⚠️ Warning 2: Complexity expression format. The issue states "O(2^n)" in prose. For declare_variants!, this should be the concrete expression "2^num_vars". The mapping is clear from the size fields section, but an explicit expression string would be better.

Recommendations

• Consider expanding to a 5-variable example for a larger search space
• State the complexity expression explicitly as 2^num_vars (matching the size field name) for direct use in declare_variants!

[isPANN]

Fix-issue changelog

• Complexity: changed prose O(2^n) to explicit expression 2^num_vars for direct use in declare_variants!
• Example Instance: expanded from n=4 (16 configs) to n=5 (32 configs, 10 NAE-satisfying solutions)
• Expected Outcome: updated to new example — solution [0,0,0,1,1], complement [1,1,1,0,0], verified by brute-force enumeration

Applied by /fix-issue.