Modelling and solving: SAT and puzzles

Modelling

The approach

Modelling means translating a statement in plain language into a set of formulas $\Sigma$, then asking the questions of chapter 2:

• are the facts consistent? That is asking whether $\Sigma$ is satisfiable;
• does a statement $A$ follow from the facts? That is asking whether $\Sigma \vDash A$, that is, whether $\Sigma \cup \{\lnot A\}$ is unsatisfiable;
• what exactly do we know? These are the models of $\Sigma$.

The first step is to choose the variables: one per elementary fact, which can be true or false independently of the others. “Alice comes” is a variable $a$. “Alice and Bob come” is not one: it is $a \land b$.

Translating natural language

Natural language is richer, and more ambiguous, than logic. The common phrasings:

A complete example

We are organising a party. Three guests, Alice, Bob and Chloé, and three constraints:

1. if Alice comes, Bob comes too;
2. Bob and Chloé do not come together;
3. Chloé comes, unless Alice comes.

Variables $a$, $b$, $c$: “Alice (Bob, Chloé) comes”. The facts:

Consistency. We reason by cases on $a$.

• $a = 1$: constraint 1 forces $b = 1$, constraint 2 then forces $c = 0$, and constraint 3 is satisfied by $a$. Model: $a = 1, b = 1, c = 0$.
• $a = 0$: constraint 3 forces $c = 1$, constraint 2 then forces $b = 0$, and constraint 1 is satisfied (false antecedent). Model: $a = 0, b = 0, c = 1$.

$\Sigma$ is satisfiable, with two models: the facts are consistent, but they do not tell who comes.

Consequences. A statement is a consequence of $\Sigma$ if it is true in both models. “Bob and Chloé do not both come”: yes, it was a hypothesis. “Bob comes or Chloé comes”, $b \lor c$: true in both, so $\Sigma \vDash b \lor c$. “Bob comes”: false in the second model, so $\Sigma \not\vDash b$.

Letting a machine solve it

The SAT problem

Deciding whether a formula in CNF is satisfiable is called the SAT problem. It is the first problem shown to be NP-complete (Cook, 1971): no algorithm is known that always solves it in polynomial time, and finding one would solve thousands of other problems at a stroke.

In practice, however, SAT solvers handle formulas with millions of variables. They are used to verify circuits, plan, schedule, solve sudokus, and choose compatible versions of the packages of a software distribution. The approach is always the one of this chapter: model in CNF, then give the formula to the solver.

The DPLL algorithm

Modern solvers all descend from a 1962 algorithm, DPLL (Davis, Putnam, Logemann, Loveland). It works on a CNF and alternates two moves.

1. Unit propagation. A clause reduced to a single literal forces its value. If $\lnot s$ is a clause, $s$ must be 0. We then simplify all the clauses: those containing $\lnot s$ are satisfied and disappear; in the others, the literal $s$ is false and disappears. New unit clauses may appear: we start again.
2. Choice. When nothing more is forced, we choose a variable, try a value, and backtrack if we reach a contradiction.

If a clause becomes empty (all its literals are false), the branch fails. If all the clauses are satisfied, we have found a model.

The puzzles of Knights and Knaves

The logician Raymond Smullyan invented an island inhabited by two kinds of people: Knights always tell the truth, Knaves always lie. We meet some inhabitants, they speak, and we deduce who is who.

The modelling fits in one rule. Let $x$ be the variable “$X$ is a Knight”. If $X$ asserts $S$:

• if he is a Knight, $S$ is true;
• if he is a Knave, $S$ is false.

In both cases: $x \leftrightarrow S$.