<p>k-SAT limits the size of the clauses. E.g. 3-SAT is the satisfiability-problem, where each clause in the CNF has (at most) 3 literals. 1-SAT is in L, 2-SAT is in NL. For any k > 2, k-SAT is NP-complete.</p>

CC BY-SA 2.5
2010-09-12T17:09:11.777Z
2010-09-12T17:09:11.777Z
Mike B.
<p>No, that's not what you thought!</p>

<p>The "K" in K-SAT is not related to the number of variables in the formula; rather, it limits the number of "literals" in each "clause".</p>

<p>Let's define the terms:</p>

<p>atom = the same thing you called variable; e.g. "x", "y", "z", etc.</p>

<p>literal = an atom or its negation; e.g "x" or "$\neg$x".</p>

<p>clause = a disjunction of literals; e.g. $(x \vee y \vee \neg z \vee w)$.</p>

<p>CNF: A formula is said to be in Conjunctive Normal Form (CNF) if it consists of AND's of several clause. For instance, $(x \vee y) \wedge (y \vee \neg z \vee w)$ is a CNF formula.</p>

<p><strong>The followin problem is K-SAT:</strong>
Given a CNF formula $f$, in which each clause has <em>exactly</em> K literals, decide whether or not $f$ is satisfiable. That is, whether there is a an assignment to the atoms such that $f$ evaluates to TRUE.</p>

<p>See also <em>Mike Jason B Punkt</em>'s answer in this post.</p>

CC BY-SA 2.5
2010-09-12T17:53:23.490Z
Thanks - consise and informative. So a boolean formula is a k-SAT formula iff it is a CNF with at most k literals per clause?
Cam
CC BY-SA 2.5
2010-09-12T18:06:08.347Z
Not "**at most** k literals per clause", but "**exactly** k literals per clause". Other than that, you're right.
Sadeq Dousti
CC BY-SA 2.5
2010-09-12T18:13:23.450Z
Cool, thanks. Yeah I was wondering about that but Mike's answer says "3-SAT is the satisfiability-problem, where each clause in the CNF has (at most) 3 literals."
Cam
CC BY-SA 2.5
2010-09-12T18:19:30.420Z
Both the “at most k literals” definition and the “exactly k distinct literals” definition are used in literature.  The distinction is not important in most cases, with a notable exception of approximation algorithms.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-12T17:20:57.027Z
2010-09-12T17:20:57.027Z
Sadeq Dousti
<p>First of all I am of course aware of the wikipedia article: <a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem" rel="nofollow">http://en.wikipedia.org/wiki/Boolean_satisfiability_problem</a></p>

<p>However I still do not understand exactly what the problem is. To demonstrate that I've tried, I think it is as follows but I am not sure:</p>

<blockquote>
  <p>The problem of checking whether a given boolean equation with k distinct
  variables is satisfiable.</p>
</blockquote>

<p>For example, is this an instance of the 3-sat problem?</p>

<pre><code>x OR y OR z
</code></pre>

CC BY-SA 2.5
2010-09-12T17:18:31.307Z
I'm not surprised you can't follow that article; what a mess!  3SAT asks whether a formula $\wedge_{i} (x_{i1} \lor x_{i2} \lor x_{i3})$ is satisfiable, where each $x_{ij}$ is either a variable or its negation.
András Salamon
CC BY-SA 2.5
2010-09-12T17:29:45.357Z
The Wikipedia article does give an example of a 3SAT formula, if you scroll down.
Robin Kothari
CC BY-SA 2.5
2010-09-12T17:49:19.990Z
@Andas: Thanks. @Robin: I'm aware of that, but an example of a 3SAT formula doesn't define what a 3SAT formula is - hence the example problem I provided (which is obviously not NP-complete - that's partially why I was confused by that section of the article).
Cam
CC BY-SA 2.5
2010-09-12T17:50:57.490Z
Can someone explain why this question was downvoted so I can improve it?
Cam
CC BY-SA 2.5
2010-09-12T17:55:05.480Z
I voted the question down because it can be answered by consulting any textbook of computational complexity theory or even the Wikipedia article you linked to.  (I recommend a textbook because I do not think that that Wikipedia article is written very clearly.)
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-12T19:47:38.937Z
Vote for close. Same reason as Tsuyoshi.
Robin Kothari
CC BY-SA 2.5
2010-09-12T23:11:28.743Z
Voted to close.  Same reason.
Jeffε
<sat>
What is the k-SAT problem?
Cam
# What is the k-SAT problem?

(Asked by: username_0 on 2010-09-12)

First of all I am of course aware of the wikipedia article: http://en.wikipedia.org/wiki/Boolean_satisfiability_problem
However I still do not understand exactly what the problem is. To demonstrate that I've tried, I think it is as follows but I am not sure:

The problem of checking whether a given boolean equation with k distinct
  variables is satisfiable.

For example, is this an instance of the 3-sat problem?
x OR y OR z

**Tags:** sat
> **Comments:**
> **username_1**: I'm not surprised you can't follow that article; what a mess!  3SAT asks whether a formula $\wedge_{i} (x_{i1} \lor x_{i2} \lor x_{i3})$ is satisfiable, where each $x_{ij}$ is either a variable or its negation.  
> **username_2**: The Wikipedia article does give an example of a 3SAT formula, if you scroll down.  
> **username_0**: @Andas: Thanks. @Robin: I'm aware of that, but an example of a 3SAT formula doesn't define what a 3SAT formula is - hence the example problem I provided (which is obviously not NP-complete - that's partially why I was confused by that section of the article).  
> **username_0**: Can someone explain why this question was downvoted so I can improve it?  
> **username_3**: I voted the question down because it can be answered by consulting any textbook of computational complexity theory or even the Wikipedia article you linked to.  (I recommend a textbook because I do not think that that Wikipedia article is written very clearly.)  
> **username_2**: Vote for close. Same reason as Tsuyoshi.  
> **username_4**: Voted to close.  Same reason.  

---

## 2 answers

### Answer by username_6 on 2010-09-12. Score: 10 | Accepted answer

No, that's not what you thought!

The "K" in K-SAT is not related to the number of variables in the formula; rather, it limits the number of "literals" in each "clause".

Let's define the terms:

atom = the same thing you called variable; e.g. "x", "y", "z", etc.

literal = an atom or its negation; e.g "x" or "$\neg$x".

clause = a disjunction of literals; e.g. $(x \vee y \vee \neg z \vee w)$.

CNF: A formula is said to be in Conjunctive Normal Form (CNF) if it consists of AND's of several clause. For instance, $(x \vee y) \wedge (y \vee \neg z \vee w)$ is a CNF formula.

**The followin problem is K-SAT:**
Given a CNF formula $f$, in which each clause has *exactly* K literals, decide whether or not $f$ is satisfiable. That is, whether there is a an assignment to the atoms such that $f$ evaluates to TRUE.

See also *Mike Jason B Punkt*'s answer in this post.

> **Comments:**
> **username_0**: Thanks - consise and informative. So a boolean formula is a k-SAT formula iff it is a CNF with at most k literals per clause?  
> **username_6**: Not "**at most** k literals per clause", but "**exactly** k literals per clause". Other than that, you're right.  
> **username_0**: Cool, thanks. Yeah I was wondering about that but Mike's answer says "3-SAT is the satisfiability-problem, where each clause in the CNF has (at most) 3 literals."  
> **username_3**: Both the “at most k literals” definition and the “exactly k distinct literals” definition are used in literature.  The distinction is not important in most cases, with a notable exception of approximation algorithms.  

---

### Answer by username_5 on 2010-09-12. Score: 3

k-SAT limits the size of the clauses. E.g. 3-SAT is the satisfiability-problem, where each clause in the CNF has (at most) 3 literals. 1-SAT is in L, 2-SAT is in NL. For any k > 2, k-SAT is NP-complete.


---

