Note: this is a translation with some re-writing of a previously published post: Le problème SAT.

I’m going to explain what the SAT problem is, because I’m going to talk about it a bit more soon. It’s one of the fundamental blocks around the P vs NP question; I’m going to write a blog post about NP-hard problems, but writing a post about SAT specifically is worth it. Also: I did my master thesis on SAT-related questions, so it’s a bit of a favorite topic of mine 🙂

SAT is a common abbreviation for “boolean satisfiability problem”. Everything revolves around the concept of boolean formulas, and a boolean formula can look like this:

Let me unpack this thing. The first concept is variables: here, , or . They’re kind of like the “unknowns” of an equation: we want to find values for , and . Moreover, we’re in a somewhat weird universe, the boolean universe: the only values , and can take are 0 or 1.

Then, we have some weird symbols. means “or”, and means “and”. And the small bars above some of the letters indicate a negation. We combine these symbols with variables to get expressions, whose value can be computed as follow:

• If , then , otherwise ( is the opposite value of ). We read this “not “.
• If , then ; if , then ; if and , then . In other words, if or . Note that in this context, when we say “or”, we do not use exactly the same meaning than in everyday language: we mean “if or if or if both are equal to 1″. We read this: “ or “.
• If and , then , otherwise . We read this: “ and “.

I’m summarizing all this in this table, for every possible value of and :

We can combine these expressions any way that we want to get boolean formulas. So the following examples are boolean formulas:

And then, by assigning values (0 or 1) to the individual variables, we can evaluate a formula for the assignment, that is to say, say if the value that the formula “computes” is 0 or 1. If the formula evaluates to 1 with an assignment, we say that this assignment satisfies the formula. And we say that a formula is satisfiable if there exists an assignment that makes it evaluate to 1 – hence the name of the problem, “boolean satisfiability”.

Boolean satisfiability in general is kind of “annoying” because it doesn’t have much structure to it: it’s hard to think about and it’s hard to say much about it, really. One thing that is always feasible, however, is to look at all the possibilities for all the variables, and see if there exists a combination of values that satisfies the formula. Picking one of the example above, and calling the formula :

And let’s enumerate all possibilities:

This table answers the question “is there values of , and for which evaluates to 1 (the answer is yes) and it even goes further by giving said values (for instance, , and are values that satisfy the formula).

The issue is that it’s not really manageable to write such a table as soon as we get a lot of variables. The reason for that is that, for every variable, I need to check what happens for its 0 value and for its 1 value. So I have two choices for the first variable, two choices for the second variable, two choices for the third variable, and so on. The choices multiply with each other: similarly to the table above, I need a line for every possible combination of values of variables. For 3 variables, lines. For 5 variables, lines, that starts to be annoying to do by hand. For 20 variables, lines, the result is not necessarily instant anymore on a computer. And it continues growing: for variables, I need lines, which it grows faster and faster: the joys of power functions.

For the people who followed the previous explanations, this is NOT a polynomial time algorithm: it’s an exponential time algorithm. (Not even considering the fact that I’m only enumerating the possibilities and not evaluating the formula yet).

Since the general SAT problem seems fairly complicated to tackle, one can wonder if there are “subgroups” that are easy to solve, or that are easier to think about. And, indeed, there are such subgroups.

Suppose that, instead of getting an arbitrary combination of variables and symbols, I restrict myself of formulas such as this one: . That’s a form where I have “groups” of variables linked by ““, themselves grouped by . Then that’s an “easy” case: for the formula to be satisfiable, I only need one of the “groups” to evaluate to 1 (because they are linked by “or” operators, so the formula evaluates to 1 if at least one of the groups evaluates to 1). And a given group evaluates to 1, unless it contains both one variable and its negation, like . In that case, since within a group I need all the variables to be equal to 1 for the group to evaluate to 1, and since a variable and its negation cannot be equal both to 1, the group would evaluate to 0. So unless all the groups contain a variable and its negation, the formula is satisfiable – a fairly easy condition to verify.

If I consider the “opposite” of the previous setup, with formulas such as , we have “groups” of variables linked by , themselves grouped by . This type of formulas are called CNF formulas (where CNF means “conjunctive normal form”). A CNF formula is defined as a set of clauses (the “groups”), all linked by symbols (“and”). A clause is a set of one or several literals that are linked by symbols (“or”). A literal is either a variable (for example ) or its negation (for example ).

The question asked by an instance of the SAT problem is “can I find values for all variables such that the whole formula evaluates to 1?”. If we restrict ourselves to CNF formulas (and call the restricted problem CNF-SAT), this means that we want that all the clauses evaluate to 1, because since they are linked by “and” in the formula, I need that all of its clauses evaluate to 1. And for each clause to have value 1, I need at least one of the literals to have value 1 in the clause (I want the first literal or the second literal or the third literal or… to be equal to 1). As previously mentioned: it can happen that all the literals are equal to 1 – the clause will still be equal to 1.

It turns out that we can again look at subgroups within CNF formulas. Let us consider CNF formulas that have exactly 2 literals in all clauses – they are called 2-CNF formulas. The associated problem is called 2-CNF-SAT, or more often 2-SAT. Well, 2-SAT can be solved in linear time. This means that there exists an algorithm that, given any 2-CNF formula, can tell in linear time whether the formula is satisfiable or not.

Conversely, for CNF formulas that have clauses that have more than 2 literals… in general, we don’t know. We can even restrict ourselves to CNF formulas that have exactly 3 literals in each clause and still not know. The associated problem is called 3-CNF-SAT, or (much) more often 3-SAT.

From a “complexity class” point of view, 3-SAT is in NP. If I’m given a satisfiable 3-CNF formula and values for all variables of the formula, I can check in polynomial time that it works: I can check that a formula is satisfiable if I have a proof of it. (This statement is also true for general SAT formulas.)

What we do not know, however, is whether 3-SAT is in P: we do not know if there exists a polynomial time algorithm that allows us to decide if a 3-CNF formula can be satisfied or not in the general case. The difficulty of the problem still does not presume of the difficulty of individual instances. In general, we do not know how to solve the 3-SAT problem; in practice, 3-SAT instances are solved every day.

We also do not know whether 3-SAT is outside of P: we do not know if we need an algorithm that is “more powerful” than a polynomial time algorithm to solve the problem in the general case. To answer that question (and to prove it) would actually allow to solve the P vs NP problem – but to explain that, I need to explain NP-hard problems, and that’s something for the next post, in which I’ll also explain why it’s pretty reasonable to restrict oneself to 3-SAT (instead of the general SAT problem) when it comes to studying the theory of satisfiability 🙂