[Rule] NAESatisfiability to Satisfiability

[isPANN]

Source

NAESatisfiability

Target

Satisfiability

Motivation

This direct clause-doubling construction connects NAE-SAT back to ordinary SAT, completing the reverse direction of the existing SAT to NAE-SAT rule without crossing into an optimization problem.

Reference

Gurumukhani, Paturi, Saks, and Talebanfard, “Local Enumeration: The Not-All-Equal Case,” STACS 2025, Section 2. They define the negation-closure of a k-CNF formula by adding the literalwise negation of every clause and state that its SAT solutions are exactly the NAE solutions of the original formula. Schaefer, “The Complexity of Satisfiability Problems,” STOC 1978, gives the same clause-and-complement identity for the classical ternary NAE relation.

Reduction Algorithm

Let the source have variables x_1,...,x_n and clauses C_1,...,C_m, each containing at least two literals.

1. Keep the same n Boolean variables.
2. For each source clause C=(l_1,...,l_r), add two CNF clauses:
   • (l_1 OR ... OR l_r), excluding the all-false assignment;
   • (not l_1 OR ... OR not l_r), excluding the all-true assignment.
3. Extract the source configuration unchanged.

For every r >= 2, let v_i be the truth value of l_i. The first target clause holds iff some v_i is true, and the second holds iff some v_i is false. Their conjunction therefore holds iff the tuple (v_1,...,v_r) contains both truth values, exactly the NAE condition. This argument is independent of clause arity and remains valid for tautological clauses, repeated literals, and repeated variables.

If m=0, the construction emits the empty conjunction. It is true under every assignment in both models (including the unique empty assignment when n=0), and identity extraction remains valid.

Size Overhead

Target metric	Formula
num_vars	num_vars
num_clauses	2 * num_clauses
num_literals	2 * num_literals

Validation Method

• Compare source NAE evaluation with target CNF evaluation for every assignment.
• Include the empty conjunction, positive and negated literals, repeated literals, tautological clauses, and arbitrary clause lengths r >= 2.
• Check both a satisfiable source instance and an unsatisfiable source instance.
• The canonical three-variable instance was checked over all eight assignments.

Example

1. Source instance: clauses (x_1,x_2,x_3), (not x_1,x_2), and (x_1,not x_2,not x_3).
2. Construction: produce six SAT clauses: each source clause and its literalwise complement.
3. Target witness: x=[0,0,1]. The source literal values are [0,0,1], [1,0], and [0,1,0], so every clause contains both truth values; the same assignment satisfies all six target clauses.
4. Round trip: extraction returns [0,0,1]. As a rejecting near-witness, [0,1,0] satisfies each original clause as an ordinary OR clause but makes (not x_1,x_2) all true, so both the source NAE instance and the doubled CNF reject it. The script checked all eight assignments.
5. NO instance: the one-variable source clause (x_1,x_1) is monochromatic for both assignments. Its target is (x_1 OR x_1) AND (not x_1 OR not x_1), which is likewise unsatisfiable.

BibTeX

@inproceedings{Gurumukhani2025,
  author = {Gurumukhani, Mohit and Paturi, Ramamohan and Saks, Michael and Talebanfard, Navid},
  title = {Local Enumeration: The Not-All-Equal Case},
  booktitle = {42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume = {327},
  pages = {42:1--42:19},
  year = {2025},
  doi = {10.4230/LIPIcs.STACS.2025.42}
}

@inproceedings{Schaefer1978,
  author = {Schaefer, Thomas J.},
  title = {The Complexity of Satisfiability Problems},
  booktitle = {Proceedings of the Tenth Annual ACM Symposium on Theory of Computing},
  pages = {216--226},
  year = {1978},
  doi = {10.1145/800133.804350}
}

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No implemented or proposed duplicate, and pred path NAESatisfiability Satisfiability --json reports no existing path.
Non-trivial	✅ Pass	The construction adds a second, literalwise-complemented CNF constraint for every source clause; this is a genuine constraint transformation, not a subtype cast or variable relabeling.
Correctness	✅ Pass	The cited paper exists with the stated metadata, its ternary NAE relation has exactly the stated two-clause CNF encoding, and exhaustive checks confirm the generalized clause identity.
Completeness	❌ Fail	The only cited source states NAE for sets of size at most 3 and explicitly writes the encoding only for the ternary relation, while the repository source model accepts clauses of every length at least 2. The algorithm works on tested longer clauses, but the mandatory full-domain literature support is absent.
Well-written	✅ Pass	All required sections are substantive, target size metrics are valid, the algorithm and identity extraction are implementable, and the example includes both a witness and a rejecting near-witness.

Overall: 4 passed, 1 failed

---

Usefulness

• Both endpoint models resolve through pred show.
• pred path NAESatisfiability Satisfiability --json reports no reduction path.
• Searching all repository issues for these endpoint names found only this proposal in this direction; the other matches are the already-implemented reverse direction, Satisfiability → NAESatisfiability.

Non-trivial

The source variables are retained, but every NAE constraint is replaced by two ordinary CNF constraints. This constructs new constraints and doubles the clause/literal-occurrence structure, so it satisfies the non-triviality criterion.

Correctness

• Thomas J. Schaefer, “The Complexity of Satisfiability Problems,” STOC 1978, pp. 216–226, DOI 10.1145/800133.804350, exists with the title, author, year, pages, and DOI given in the issue. It is also present in docs/paper/references.bib as schaefer1978.
• In the proof sketch of Theorem 7.1 (p. 225), Schaefer writes the ternary NAE relation as the conjunction of a clause and its literalwise complement, excluding precisely 000 and 111. This directly supports the issue's per-clause identity for arity 3.
• As an independent cross-check of the semantics, Liu, “The Curse and Blessing of Not-All-Equal in k-Satisfiability” (2018), defines NAE-k-SAT by requiring each clause's literal truth values to be not all equal.
• A direct exhaustive script checked 80,152 clause/assignment pairs for 1–3 variables, clause lengths 2–5, with repeated and complementary literals allowed. In every case, NAE(C) equaled SAT(C ∧ complement(C)). It also checked the issue's three-clause example over all eight assignments: [0,0,1] is accepted and [0,1,0] is rejected as claimed.

No lower-overhead construction is possible within this same-variable direct encoding: the stated output sizes are exact (n variables, 2m clauses, and twice the literal occurrences).

Completeness

Literature scope. Schaefer's NP2 problem statement on p. 217 restricts the sets to, in the paper's words, “each having at most 3 members.” The explicit CNF identity in the proof sketch of Theorem 7.1 is likewise for R(x,y,z). The repository's NAESatisfiability schema and constructor instead allow every clause length r ≥ 2, without an upper bound. Therefore, the cited theorem/proof does not establish the proposed rule on the full source domain. Under the mandatory completeness criterion, this is a failure even though the issue's elementary argument and exhaustive checks strongly indicate that the algorithm itself is correct.

Codebase domain and hand traces. src/models/formula/nae_satisfiability.rs enforces only a minimum clause length of 2; empty clause collections, arbitrary longer clauses, repeated literals/variables, tautological clauses, and unused variables are allowed. Two existing same-source rules were inspected: src/rules/naesatisfiability_ilp.rs and src/rules/naesatisfiability_setsplitting.rs; both iterate over arbitrary-length clauses without assuming arity 3.

1. Empty formula, n=0, no clauses. The construction keeps zero variables and emits zero clauses. Both source and target are true under the empty assignment, and identity extraction returns the empty configuration.
2. Repeated literal, C=(x_1,x_1). For x_1=0, the first target clause is false; for x_1=1, the complemented clause is false. Thus the target is unsatisfiable, matching the source NAE clause, which is monochromatic under both assignments.
3. Tautological/repeated-variable clause, C=(x_1,¬x_1,x_1). Under either assignment the source contains both truth values. Both target clauses are tautologies, so identity extraction remains correct.

These traces also show that the construction itself handles the tested edge inputs. The issue should nevertheless document the empty-formula case and, more importantly, supply literature that covers arbitrary clause arity (or explicitly identify the arbitrary-arity statement as a proved lemma and provide an acceptable source for that lemma).

Well-written

• Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example, and BibTeX are all present and substantive.
• num_vars, num_clauses, and num_literals are valid target size_fields, and the formulas are exact.
• All algorithm symbols are defined, and solution extraction is unambiguous.
• The example is non-degenerate for a feasibility problem: it exercises positive/negative literals and distinguishes a satisfying witness from an ordinary-SAT near-witness rejected by NAE.

Recommendations

• Add a reference or textbook statement for arbitrary-arity NAE constraints, not only NAE-3-SAT. If the intended support is the elementary Boolean identity itself, state it as a lemma quantified over every r ≥ 2 and cite a source that states the same full-domain encoding.
• Add the empty conjunction explicitly to the algorithm/validation discussion.

[isPANN]

Rule Fix

Diagnosis:

• Literature coverage: the original citation explicitly presented the clause-and-complement identity only for ternary NAE, while the repository model accepts arbitrary clause lengths r >= 2.
• Example coverage: the original example contained a rejecting assignment but no unsatisfiable source instance.
• Edge-case documentation: the construction handled the empty conjunction, but the issue body did not state that case.
• All remaining structured checks passed: direction, both correctness directions, gadget/constraint completeness, identity extraction, polynomial time, exact overhead, type compatibility (Or -> Or), objective/bound handling, and target-instance validity. The undirected-rerouting check is not applicable to a CNF target.

Literature:

• Gurumukhani, Paturi, Saks, and Talebanfard, “Local Enumeration: The Not-All-Equal Case,” STACS 2025, Section 2, defines the negation-closure of a k-CNF formula and states that its SAT solutions are exactly the NAE solutions of the original formula. This is the proposed construction on arbitrary clause width.
• Schaefer 1978 remains cited as the classical ternary instance of the same identity.

Changes:

• Added the full-width STACS 2025 reference and BibTeX entry.
• Added a quantified r >= 2 correctness proof covering arbitrary arity, repeated literals/variables, and tautological clauses.
• Documented the empty-conjunction case.
• Added the unsatisfiable source instance (x_1,x_1) and its doubled-CNF image.
• Left the construction and exact overhead formulas unchanged.

Smoke test:

• 93 checks passed across all mandatory buckets.
• Covered the issue's YES instance, a constructed NO instance, three boundary cases, 50 deterministic generated formulas, 33 identity-extraction witnesses, five overhead spot-checks, and target validity for every generated target.

[isPANN]

Issue Quality Re-check — Rule

Check	Result	Details
Usefulness	✅ Pass	Both endpoints exist and pred path NAESatisfiability Satisfiability --json reports no existing path.
Non-trivial	✅ Pass	Each NAE clause is transformed into two ordinary CNF constraints, changing the constraint structure.
Correctness	✅ Pass	Both cited papers and their claimed roles were verified; the generalized construction also passed 93 independent smoke checks.
Completeness	✅ Pass	The new STACS 2025 source explicitly gives the negation-closure construction for k-CNF, and the issue now proves and documents every repository-supported case.
Well-written	✅ Pass	All required sections, target metrics, extraction, boundary behavior, YES example, and NO example are complete and implementable.

Overall: 5 passed, 0 failed, 0 warnings

Change from the previous check: Completeness changed from Fail to Pass after adding full-width literature support, a quantified correctness lemma, explicit empty-formula behavior, and a genuine NO instance.

---

Usefulness

• pred show resolves both NAESatisfiability and Satisfiability.
• pred path NAESatisfiability Satisfiability --json reports no reduction path, so the proposed edge is novel in the current graph.

Non-trivial

The variables are retained, but every source constraint produces both its ordinary clause and its literalwise negation. This doubles the clause/literal-occurrence structure and is more than a relabeling or subtype coercion.

Correctness

• Gurumukhani, Paturi, Saks, and Talebanfard, “Local Enumeration: The Not-All-Equal Case”, STACS 2025, has the stated authors, venue, pages, and DOI. Section 2 defines the negation-closure by adding every clause's negation-clause and states that the NAE solutions are exactly its SAT solutions.
• Schaefer, “The Complexity of Satisfiability Problems”, STOC 1978, has the stated metadata and supplies the classical ternary instance of the identity.
• The issue's direct proof is correct: for any clause, its original disjunction requires at least one true literal and its complemented disjunction requires at least one false literal.
• The re-smoke passed 93 checks: the worked YES instance, an unsatisfiable source instance, three edge cases, 50 generated feasibility comparisons, 33 identity-extraction checks, five overhead checks, and target validity throughout.

Completeness

The STACS construction covers k-CNF rather than only ternary NAE. For a finite mixed-width formula, take k to be its maximum clause width; the construction remains clause-local. The issue additionally quantifies its proof over every r >= 2, matching the repository constructor.

The source implementation permits an empty clause collection, arbitrary widths at least two, repeated literals/variables, tautological clauses, and unused variables. Existing NAESatisfiability -> ILP and NAESatisfiability -> SetSplitting rules likewise iterate over arbitrary-width clauses. Traces of the repaired issue body give:

1. Empty formula (n=0, no clauses): zero target clauses; both empty conjunctions accept the empty assignment.
2. Repeated literal (x_1,x_1): the target contains mutually incompatible positive and negative unit-equivalent clauses, so both source and target are unsatisfiable.
3. Tautological repeated-variable clause (x_1,not x_1,x_1): both target clauses are tautologies and the NAE clause is always satisfied.

Well-written

• Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example, and BibTeX are present and substantive.
• num_vars, num_clauses, and num_literals match target size fields; all formulas are exact.
• Forward and backward correctness follow from the explicit per-clause equivalence, and solution extraction is the identity map.
• The main example exercises mixed signs and both accepted/rejected assignments; the added repeated-literal formula supplies an actual NO instance.

Recommendations

• None blocking implementation.