Classification of intractable/tractable satisfiability problem variants

Question

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}$) ?

---

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

Answer 1

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.