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$

closed as off topic by Robin Kothari, Jeffε, Ryan Williams Sep 13 '10 at 4:40

Questions on Theoretical Computer Science Stack Exchange are expected to relate to research-level theoretical computer science within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here. If this question can be reworded to fit the rules in the help center, please edit the question.

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