Source: Satisfiability
Target: NAESatisfiability
Motivation: Classic reduction proving NAE-SAT NP-complete. Bridges standard SAT to the symmetric NAE variant, enabling connections to MaxCut and graph coloring.
Reference: Garey & Johnson (1979), Computers and Intractability, Problem LO3. Also Schaefer (1978).
Reduction Algorithm
Given a CNF formula φ with n variables x_1, ..., x_n and m clauses C_1, ..., C_m (each clause a disjunction of literals):
Two-step reduction (3-SAT → NAE-4-SAT → NAE-3-SAT):
Step 1 (3-SAT → NAE-4-SAT): Add a fresh global dummy variable z to every clause.
- Clause C_j = (l_1 ∨ l_2 ∨ l_3) becomes NAE-4-clause (l_1, l_2, l_3, z).
- A 3-SAT satisfying assignment α yields NAE-4-SAT solution with z = false: each clause has at least one true literal (from α) and z = false.
Step 2 (NAE-4-SAT → NAE-3-SAT): For each NAE-4-clause (a, b, c, d), introduce fresh variable w_j and replace with two NAE-3-clauses: (a, b, w_j) and (¬w_j, c, d).
Solution extraction: From a NAE assignment, extract the original n variable values (ignore z and w_j variables). Due to NAE symmetry, may need to check both the assignment and its complement to find a satisfying assignment for the original formula.
Size Overhead
| Target metric (code name) |
Polynomial (using symbols above) |
num_vars |
n + 1 + m (original vars + dummy z + one w_j per clause) |
num_clauses |
2 * m (each original clause becomes two NAE-3-clauses) |
Validation Method
- Generate random 3-SAT instances, reduce to NAE-SAT, solve both with brute force, verify agreement.
- Test with both satisfiable and unsatisfiable instances.
Example
3-SAT formula: n=2, m=2
- C_1 = (x_1 ∨ x_2)
- C_2 = (¬x_1 ∨ x_2)
Step 1 (add dummy z):
- NAE-4: (x_1, x_2, z), (¬x_1, x_2, z) — wait, these are 3-literal clauses with z added, making them 3 literals. Actually for 2-literal clauses, adding z gives 3-literal NAE clauses directly.
For 3-literal clauses, Step 2 applies:
- C_1 = (a, b, c) with dummy z → (a, b, c, z) → split into (a, b, w_1) and (¬w_1, c, z)
SAT assignment x_1=T, x_2=T satisfies both clauses. NAE assignment with z=F: (T, T, F) for each resulting clause — NAE satisfied.
Source: Satisfiability
Target: NAESatisfiability
Motivation: Classic reduction proving NAE-SAT NP-complete. Bridges standard SAT to the symmetric NAE variant, enabling connections to MaxCut and graph coloring.
Reference: Garey & Johnson (1979), Computers and Intractability, Problem LO3. Also Schaefer (1978).
Reduction Algorithm
Given a CNF formula φ with n variables x_1, ..., x_n and m clauses C_1, ..., C_m (each clause a disjunction of literals):
Two-step reduction (3-SAT → NAE-4-SAT → NAE-3-SAT):
Step 1 (3-SAT → NAE-4-SAT): Add a fresh global dummy variable z to every clause.
Step 2 (NAE-4-SAT → NAE-3-SAT): For each NAE-4-clause (a, b, c, d), introduce fresh variable w_j and replace with two NAE-3-clauses: (a, b, w_j) and (¬w_j, c, d).
Solution extraction: From a NAE assignment, extract the original n variable values (ignore z and w_j variables). Due to NAE symmetry, may need to check both the assignment and its complement to find a satisfying assignment for the original formula.
Size Overhead
num_varsnum_clausesValidation Method
Example
3-SAT formula: n=2, m=2
Step 1 (add dummy z):
For 3-literal clauses, Step 2 applies:
SAT assignment x_1=T, x_2=T satisfies both clauses. NAE assignment with z=F: (T, T, F) for each resulting clause — NAE satisfied.