Lesson 3

The input of the satisfiability problem is a formula in conjunctive normal form (CNF): \[(x \lor y \lor z) \land (\overline{x}\lor y) \land (\overline{y}\lor z) \land (\overline{z}\lor x) \land (\overline{x}\lor \overline{y}\lor \overline{z}) \ .\] All variables here are Boolean (take values true and false; as usual, we will replace them everywhere with 1 and 0). Each bracket is a disjunction, also called a clause or a constraint. Thus, the formula asks us to assign values to three Boolean variables that satisfy five constraints: the first constraint says that \(x,y,z\) cannot simultaneously take the value 0, the second — that one cannot assign \(x=1\) and \(y=0\) simultaneously, and so on. A literal is called a variable (\(x\)) or its negation (\(\overline{x}\)) is called a literal.

We will call a formula satisfiable if it is possible to assign (Boolean) values to the variables of this formula such that the formula evaluates to true/one. Thus, the formula is unsatisfiable if the truth table of the Boolean function it defines consists of only zeros.

The following code shows that the formula above is unsatisfiable. If we remove the last constraint, it becomes satisfiable. As can be seen, the variables in the formula are represented by consecutive numbers.

from pycosat import solve

clauses = [[-1, -2, -3], [1, -2], [2, -3], [3, -1], [1, 2, 3]]

print(solve(clauses))
print(solve(clauses[:-1]))

UNSAT
[-1, -2, -3]