Classification of intractable/tractable satisfiability problem variants

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 NxN extension of the 15-Puzzle is intractable by D. Ratner and M. Warmuth (1986)


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.

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

Leave a Comment