# Classification of intractable/tractable satisfiability problem variants

Recently I found in a paper  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}$) ?

# 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}\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}\mathcal{NP}$$-complete problem.

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

# $$kk$$-colourable Monotone NAE-3SAT

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

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

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

For $$k=4k=4$$ the problem is in $$\mathcal{P}\mathcal{P}$$. For $$k=5k=5$$ however, it is $$\mathcal{NP}\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}\mathcal{NP}$$-complete when restricted to linear formulas. Moreover, NAE-SAT and XSAT are still $$\mathcal{NP}\mathcal{NP}$$-complete on formulas only containing clauses of length at least $$kk$$, for each positive fixed integer $$k \geq 3k \geq 3$$. They are $$\mathcal{NP}\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.