Recently I found in a paper [1] a special symmetric version of SAT called the

2/2/4-SAT. But there are many \text{NP}-complete variants out there, for example:MONOTONE NAE-3SAT,MONOTONE 1-IN-3-SAT, …Some other variants are tractable: 2–\text{SAT}, Planar-NAE-\text{SAT}, …

Are there survey papers (or web pages) that classify all the (weird) \text{SAT} variants that have been proved to be \text{NP}-complete (or in \text{P}) ?

- Finding a shortest solution for the NxN extension of the 15-Puzzle is intractable by D. Ratner and M. Warmuth (1986)

**Answer**

# Classic, well-known results

As mentioned by Standa Zivny on the related question of CSTheory, Which SAT problems are easy?, there’s a well-known result by Schaefer from 1978 (quoting the answer of Zivny):

If SAT is parametrised by a set of relations allowed in any instance, then there are only 6 tractable cases: 2-SAT (i.e. every clause is binary), Horn-SAT, dual-Horn-SAT, affine-SAT (solutions to linear equations in

GF(2)), 0-valid (relations satisfied by the all-0 assignment) and 1-valid (relations satisfied by the all-1 assignment).

**Planar-3SAT** meaning the planar version of **3SAT** is known to be \mathcal{NP}-complete. See D Lichtenstein, Planar formulae and their uses, 1981. The non-planar version of 3SAT is of course the very well-known classic \mathcal{NP}-complete problem.

Not-All-Equal 3SAT (**NAE-3SAT**) is \mathcal{NP}-complete. However, the planar version of it is in \mathcal{P} as shown by Moret, Planar NAE3SAT is in P, 1988.

# More recent and/or “weird” variants

# k-colourable Monotone NAE-3SAT

Here’s a more exotic or weird variant, a decision problem called the **k-colourable Monotone NAE-3SAT**:

Given a monotone CNF expression \phi with exactly three distinct variables in each clause, such that the corresponding constraint graph G(\phi) is k-colourable, is the expression \phi not-all-equal satisfiable?

Here the corresponding constraint graph G(\phi) is a simple undirected graph associated with \phi as follows: Each variable of \phi is a vertex in G, and two vertices have an edge between them iff they appear in some clause together.

For k=4 the problem is in \mathcal{P}. For k=5 however, it is \mathcal{NP}-complete. See P Jain, On a variant of Monotone NAE-3SAT and the Triangle-Free Cut problem, 2010.

# Linear CNF variants

While not perhaps being exotic or weird, some well-known variants, namely **NAE-SAT** (not-all-equal SAT) and **XSAT** (Exact SAT; *exactly one* literal in each clause to 1 and all other literals to 0), of the satisfiability problem have been investigated in the *linear* setting. Clauses of a linear formula pairwise have at most one variable in common. Interestingly, the complexity status does not follow from Schaefer’s Theorem.

**NAE-SAT** and **XSAT** remain \mathcal{NP}-complete when restricted to linear formulas. Moreover, **NAE-SAT** and **XSAT** are still \mathcal{NP}-complete on formulas only containing clauses of length at least k, for each positive fixed integer k \geq 3. They are \mathcal{NP}-complete for monotone (no positive literals) linear formulas. However, **NAE-SAT** is polynomial-time decidable on exact linear formulas, where each pair of distinct clauses has exactly one variable in common.

Some further aspects regarding the complexity of **NAE-SAT** and **XSAT** under certain assumptions are probably still open. For more specifics, see for example Porschen and Schmidt, On Some SAT-Variants over Linear Formulas, 2009 and Porschen et al., Complexity Results for Linear XSAT-Problems, 2010.

**Attribution***Source : Link , Question Author : Vor , Answer Author : Community*