# What is the k-SAT problem? [closed]

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

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

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.