<p>This list will be very long;)
Here are some of my favourite (NP-complete) variants of SAT:</p>

<ul>
<li><p>PLANAR($\le 3, 3$)-SAT (each clause contains at least two and at most three literals, each variable appears in exactly three clauses; 
twice in its non-negated form, and once in its negated form, and the bipartite incidence graph is planar.) </p>

<p>See: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, The complexity of multiterminal cuts, 
SIAM Journal of Computing 23 (1994) 864-894 </p></li>
<li><p>4-BOUNDED PLANAR 3-CONNECTED 3SAT (every clause contains exactly 3 distinct variables, every variable appears in at most 
4 clauses, the bipatite incident graph is planar and 3-connected )</p>

<p>See: Kratochvíl, A special planar satisfiability problem and a consequence of its NP-completeness, 
Discrete Applied Math. 52 (1994) 233-252  </p></li>
<li><p>MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT in which every variable appears exactly 3 times) </p>

<p>See: Moore and Robsen, Hard tilings problem with simple tiles, Discrete Compute. Geom. 26 (2001) 573-590   </p></li>
<li><p>I find very interesting that PLANAR-NAE-$k$SAT is in P for every $k$.</p>

<p>See <a href="https://cstheory.stackexchange.com/questions/5994/for-which-k-is-planar-nae-k-sat-in-p">this post</a>.</p></li>
</ul>

CC BY-SA 3.0
2013-10-03T14:32:12.883Z
If you find the last point interesting, you might also be interested to know that #PLANAR-NAE-3SAT (counting solutions) is tractable as well, whereas other seemingly simple SAT variants like PLANAR-MONOTONE-2SAT are tractable (or even trivial) as a decision problem, but #P-hard for counting. Note that the reduction from the last link above (reducing PLANAR-NAE-kSAT to PLANAR-NAE-3SAT) is not parsimonious, and that #PLANAR-NAE-4SAT is #P-hard.
William Whistler
CC BY-SA 3.0
2013-09-09T16:04:44.873Z
2013-09-09T16:04:44.873Z
2017-04-13T12:32:28.080Z
user13136
<p>(Making comment an answer as requested and expanding a bit.)</p>

<p>"A curious mind" should read <a href="http://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem">Schaefer's dichotomy theorem</a> and the <a href="http://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem#Generalizations">generalization</a> by <a href="http://www.sciencedirect.com/science/article/pii/S0022000008001141">Allender et al.</a> that shows that every possible SAT variant is either trivial or in one of six well-known complexity classes:</p>

<ol>
<li>NP-complete</li>
<li>P-complete</li>
<li>NL-complete</li>
<li>L-complete</li>
<li>⊕L-complete</li>
<li>co-NLOGTIME</li>
</ol>

CC BY-SA 3.0
2013-09-07T22:10:38.613Z
2013-09-08T04:10:25.287Z
2013-09-08T04:10:25.287Z
Tyson Williams
<p>On the "NP-complete side" I came across these variants (I asked a similar question on cs.stackexchange, too):</p>

<ul>
<li>Planar 3-SAT;</li>
<li>Planar 1-in-3 SAT and Positive Planar 1-in-3 SAT (see <a href="http://arxiv.org/pdf/cs/0601002v3.pdf">Mulzer and Rote</a>);</li>
<li>NAE 3-SAT;</li>
<li>2/2/4-SAT (see <a href="https://www.aaai.org/Papers/AAAI/1986/AAAI86-027.pdf">Finding a shortest solution for the NxN extension of the 15-Puzzle is intractable by D. Ratner and M. Warmuth (1986)</a>);</li>
<li>XSAT, NAE-SAT for Linear Monotone Formulas, XSAT for exact linear formulas (see the nice work of Ewald Speckenmeyer on linear XSAT problems: <a href="http://kups.ub.uni-koeln.de/3129/2/Dissertation_Endversion.pdf">Computational Complexity of SAT, XSAT and NAE-SAT for linear and mixed Horn CNF formulas</a>);</li>
<li>k-colourable Monotone NAE-3SAT (see <a href="http://arxiv.org/pdf/1003.3704">P Jain, On a variant of Monotone NAE-3SAT and the Triangle-Free Cut problem, 2010</a>).</li>
</ul>

CC BY-SA 3.0
2013-09-07T14:54:56.180Z
2013-09-07T15:09:30.030Z
2013-09-07T15:09:30.030Z
Marzio De Biasi
<p>Let $\mathrm{SAT}(k)$ be $\mathrm{SAT}$ for CNF formulas with at most $k$ occurrences of every variable. 
Then $\mathrm{SAT}(2)$ ist complete for $\mathsf{L}$ (i.e., deterministic log space, see my <a href="http://dx.doi.org/10.1007/978-3-540-24749-4_28">paper</a> in STACS 2004), whereas $\mathrm{SAT}(k)$ for $k\geq 3$ is NP-complete. </p>

CC BY-SA 3.0
2013-09-09T08:00:52.313Z
2013-09-09T08:00:52.313Z
Jan Johannsen
<p>Apart from the list above, there are also:  </p>

<ul>
<li>#SAT: model counting</li>
<li>All-SAT: model enumerating </li>
</ul>

CC BY-SA 3.0
2013-09-07T22:01:07.247Z
2013-09-07T22:01:07.247Z
sean
<p>There is a very classic connection between logic and algebra, which goes back to the origin of modern logic and the work of George Boole. A formula in propositional logic can be interpreted as an element of a Boolean algebra. The logical constants <em>true</em> and <em>false</em> become the algebraic notions of the top and bottom element of a lattice. The logical operations of conjunction, disjunction and negation will become the algebraic operations of meet, join and complementation in the Boolean algebra. This connection is less emphasised in modern treatments of logic, but it is particularly interesting in the context of your question. Algebra allows us to move away from many problem specific details and find generalisations of a problem that will apply to many different situations.</p>

<p>In the specific case of SAT, the algebraic question one may ask is what happens when we interpret formulae in more general lattices than Boolean algebras. On the logical side, you can generalise the satisfiability problem from propositional logic to intuitionistic logic. More generally, you can generalise the propositional satisfiability problem to that of determining if a formula, when interpreted over a bounded lattice (one with top and botto), defines the bottom element of the lattice. This generalisation allows you to treat problems in program analysis as satisfiability problems.</p>

<p>Another generalisation is to quantifier-free first-order logic where you get the question of Satisfiability Modulo a Theory. Meaning, in addition to having Boolean variables, you also have first-order variables and function symbols and you want to know if a formula is satisfiable. At this point you can ask questions about formulae in arithmetic, theories of strings, or arrays, etc. So we get a strict and very useful generalisation of SAT which has lots of applications in systems, computer security, programming languages, program verification, planning, artificial intelligence, etc.</p>

CC BY-SA 3.0
2013-09-16T16:43:27.610Z
2013-09-16T16:43:27.610Z
Vijay D
<p>I looked up on the internet, but I could not find any 'big-list' of variants of SAT problem.</p>

<p>Apart from the (common) </p>

<ul>
<li>SAT, </li>
<li>k-SAT, </li>
<li>MAX-kSAT, </li>
<li>Half-SAT, </li>
<li>XOR-SAT, </li>
<li>NAE-SAT </li>
</ul>

<p>what else variants are there? </p>

<p>(also it will be really useful if there complexity classes are given (where possible))</p>

CC BY-SA 3.0
2013-09-07T12:50:31.173Z
What would be the purpose of this list?
Tyson Williams
CC BY-SA 3.0
2013-09-07T13:23:35.487Z
Firstly because I wanted to present a talk to some undergraduate students. I was planning to talk about the variations of SAT and show some (non-trivial) reductions... they have already had a introductory course in TOC, so i thought this might be a good idea .. AND THE SECOND REASON being the fact there is no such list on the internet, this list will also serve any curious mind who wants to know about the variants.
Subhayan
CC BY-SA 3.0
2013-09-07T13:57:15.550Z
I am not sure how this list will help with your talk. Instead of reading an arbitrarily long list of SAT variants, a curious mind should read [Schaefer's dichotomy theorem](http://en.wikipedia.org/wiki/Schaefer's_dichotomy_theorem) and the generalization by Allender et al. that shows that every possible SAT variant is complete for one of six well-known complexity classes.
Tyson Williams
CC BY-SA 3.0
2013-09-07T14:21:37.747Z
that's a nice suggestion... thanks @TysonWilliams .. you can make that into an answer too, although that's not exactly what I was looking for, but surely this is helpful.
Subhayan
<cc.complexity-theory><sat><big-list>
variations of SAT
Subhayan
# variations of SAT

(Asked by: username_0 on 2013-09-07)

I looked up on the internet, but I could not find any 'big-list' of variants of SAT problem.

Apart from the (common)

* SAT,
* k-SAT,
* MAX-kSAT,
* Half-SAT,
* XOR-SAT,
* NAE-SAT

what else variants are there?

(also it will be really useful if there complexity classes are given (where possible))

**Tags:** cc.complexity-theory, sat, big-list

> **Comments:**
> **username_1**: What would be the purpose of this list?  
> **username_0**: Firstly because I wanted to present a talk to some undergraduate students. I was planning to talk about the variations of SAT and show some (non-trivial) reductions... they have already had a introductory course in TOC, so i thought this might be a good idea .. AND THE SECOND REASON being the fact there is no such list on the internet, this list will also serve any curious mind who wants to know about the variants.  
> **username_1**: I am not sure how this list will help with your talk. Instead of reading an arbitrarily long list of SAT variants, a curious mind should read [Schaefer's dichotomy theorem](http://en.wikipedia.org/wiki/Schaefer's_dichotomy_theorem) and the generalization by Allender et al. that shows that every possible SAT variant is complete for one of six well-known complexity classes.  
> **username_0**: that's a nice suggestion... thanks @TysonWilliams .. you can make that into an answer too, although that's not exactly what I was looking for, but surely this is helpful.  

---

## 6 answers

### Answer by username_2 on 2013-09-09. Score: 18

This list will be very long;)
Here are some of my favourite (NP-complete) variants of SAT:

* PLANAR($\le 3, 3$)-SAT (each clause contains at least two and at most three literals, each variable appears in exactly three clauses;
  twice in its non-negated form, and once in its negated form, and the bipartite incidence graph is planar.)

  See: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, The complexity of multiterminal cuts,
  SIAM Journal of Computing 23 (1994) 864-894
* 4-BOUNDED PLANAR 3-CONNECTED 3SAT (every clause contains exactly 3 distinct variables, every variable appears in at most
  4 clauses, the bipatite incident graph is planar and 3-connected )

  See: Kratochvíl, A special planar satisfiability problem and a consequence of its NP-completeness,
  Discrete Applied Math. 52 (1994) 233-252
* MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT in which every variable appears exactly 3 times)

  See: Moore and Robsen, Hard tilings problem with simple tiles, Discrete Compute. Geom. 26 (2001) 573-590
* I find very interesting that PLANAR-NAE-$k$SAT is in P for every $k$.

  See [this post](https://cstheory.stackexchange.com/questions/5994/for-which-k-is-planar-nae-k-sat-in-p).

> **Comments:**
> **username_3**: If you find the last point interesting, you might also be interested to know that #PLANAR-NAE-3SAT (counting solutions) is tractable as well, whereas other seemingly simple SAT variants like PLANAR-MONOTONE-2SAT are tractable (or even trivial) as a decision problem, but #P-hard for counting. Note that the reduction from the last link above (reducing PLANAR-NAE-kSAT to PLANAR-NAE-3SAT) is not parsimonious, and that #PLANAR-NAE-4SAT is #P-hard.  

---

### Answer by username_1 on 2013-09-07. Score: 17

(Making comment an answer as requested and expanding a bit.)

"A curious mind" should read [Schaefer's dichotomy theorem](http://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem) and the [generalization](http://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem#Generalizations) by [Allender et al.](http://www.sciencedirect.com/science/article/pii/S0022000008001141) that shows that every possible SAT variant is either trivial or in one of six well-known complexity classes:

1. NP-complete
2. P-complete
3. NL-complete
4. L-complete
5. ⊕L-complete
6. co-NLOGTIME


---

### Answer by username_4 on 2013-09-07. Score: 11

On the "NP-complete side" I came across these variants (I asked a similar question on cs.stackexchange, too):

* Planar 3-SAT;
* Planar 1-in-3 SAT and Positive Planar 1-in-3 SAT (see [Mulzer and Rote](http://arxiv.org/pdf/cs/0601002v3.pdf));
* NAE 3-SAT;
* 2/2/4-SAT (see [Finding a shortest solution for the NxN extension of the 15-Puzzle is intractable by D. Ratner and M. Warmuth (1986)](https://www.aaai.org/Papers/AAAI/1986/AAAI86-027.pdf));
* XSAT, NAE-SAT for Linear Monotone Formulas, XSAT for exact linear formulas (see the nice work of Ewald Speckenmeyer on linear XSAT problems: [Computational Complexity of SAT, XSAT and NAE-SAT for linear and mixed Horn CNF formulas](http://kups.ub.uni-koeln.de/3129/2/Dissertation_Endversion.pdf));
* k-colourable Monotone NAE-3SAT (see [P Jain, On a variant of Monotone NAE-3SAT and the Triangle-Free Cut problem, 2010](http://arxiv.org/pdf/1003.3704)).


---

### Answer by username_5 on 2013-09-09. Score: 7

Let $\mathrm{SAT}(k)$ be $\mathrm{SAT}$ for CNF formulas with at most $k$ occurrences of every variable.
Then $\mathrm{SAT}(2)$ ist complete for $\mathsf{L}$ (i.e., deterministic log space, see my [paper](http://dx.doi.org/10.1007/978-3-540-24749-4_28) in STACS 2004), whereas $\mathrm{SAT}(k)$ for $k\geq 3$ is NP-complete.


---

### Answer by username_6 on 2013-09-07. Score: 2

Apart from the list above, there are also:

* #SAT: model counting
* All-SAT: model enumerating


---

### Answer by username_7 on 2013-09-16. Score: 1

There is a very classic connection between logic and algebra, which goes back to the origin of modern logic and the work of George Boole. A formula in propositional logic can be interpreted as an element of a Boolean algebra. The logical constants *true* and *false* become the algebraic notions of the top and bottom element of a lattice. The logical operations of conjunction, disjunction and negation will become the algebraic operations of meet, join and complementation in the Boolean algebra. This connection is less emphasised in modern treatments of logic, but it is particularly interesting in the context of your question. Algebra allows us to move away from many problem specific details and find generalisations of a problem that will apply to many different situations.

In the specific case of SAT, the algebraic question one may ask is what happens when we interpret formulae in more general lattices than Boolean algebras. On the logical side, you can generalise the satisfiability problem from propositional logic to intuitionistic logic. More generally, you can generalise the propositional satisfiability problem to that of determining if a formula, when interpreted over a bounded lattice (one with top and botto), defines the bottom element of the lattice. This generalisation allows you to treat problems in program analysis as satisfiability problems.

Another generalisation is to quantifier-free first-order logic where you get the question of Satisfiability Modulo a Theory. Meaning, in addition to having Boolean variables, you also have first-order variables and function symbols and you want to know if a formula is satisfiable. At this point you can ask questions about formulae in arithmetic, theories of strings, or arrays, etc. So we get a strict and very useful generalisation of SAT which has lots of applications in systems, computer security, programming languages, program verification, planning, artificial intelligence, etc.


---

