What is the k-SAT problem? 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
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.