0
$\begingroup$

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
| cite | improve this question | |
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – András Salamon Sep 12 '10 at 17:18
  • $\begingroup$ The Wikipedia article does give an example of a 3SAT formula, if you scroll down. $\endgroup$ – Robin Kothari Sep 12 '10 at 17:29
  • $\begingroup$ @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). $\endgroup$ – Cam Sep 12 '10 at 17:49
  • $\begingroup$ Can someone explain why this question was downvoted so I can improve it? $\endgroup$ – Cam Sep 12 '10 at 17:50
  • 6
    $\begingroup$ 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.) $\endgroup$ – Tsuyoshi Ito Sep 12 '10 at 17:55
10
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Cam Sep 12 '10 at 17:53
  • $\begingroup$ Not "at most k literals per clause", but "exactly k literals per clause". Other than that, you're right. $\endgroup$ – M.S. Dousti Sep 12 '10 at 18:06
  • $\begingroup$ 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." $\endgroup$ – Cam Sep 12 '10 at 18:13
  • 2
    $\begingroup$ 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. $\endgroup$ – Tsuyoshi Ito Sep 12 '10 at 18:19
3
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

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