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)

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.