Actions

NP-completeness of SAT

From Learning Logic for Computer Science

The problem of determining the satisfiability of a given propositional formula can also be studied from a computation and complexity-theoretic perspective.

There are several variants of this problem, depending on which formulas are considered as inputs:

  • PL-SAT: given a propositional formula in BNF, determine whether it is satisfiable.
  • SAT: given a propositional formula in CNF, determine whether it is satisfiable.
  • $k$-SAT (for a given natural number $k$): given a propositional formula in CNF where every clause has at most $k$ literals, determine whether it is satisfiable.

Clearly, the input formula is encoded as a string.

Theorem The satisfiability of propositional formulas is an NP-complete problem. More precisely, PL-SAT, SAT, and $k$-SAT, for $k \geq 3$ are NP-complete.

Proof(s)

Given a propositional formula $\varphi$, whether a given assignment $\text{vars}(\varphi) \to \{0,1\}$ is a 1-assignment can be determined in time polynomial in $\text{size}(\varphi)$. Therefore, all the problems mentioned in the theorem are in NP. What remains to be shown is that they are NP-complete.

From an NP-problem to PL-SAT

To show that PL-SAT is NP-hard, we need to show that every problem in NP can be reduced to PL-SAT in polynomial time.

So we assume $L$ is some problem in NP. Then there is a non-deterministic Turing machine $T$ which recognizes $L$ in time polynomial time. This Turing machine $T$ can be turned into a Turing machine $T'$ which still recognizes $L$ and, in addition, has the following property: there is a constant $c \in \mathbf N$ such that for every $u \in L$, the TM $T'$ has an accepting run with exactly $n^c + c$ steps and which uses at most $n^c + c$ tape cells.

The computations of $T'$ on a particular input can be described by propositional formulas. In particular, there are formulas $\text{Computations}_{k,l}$ which describe all computations with $k$ steps and within space $l$.

In other words, for every word $u$ over the given input alphabet, say $A$, the following propositional formula is satisfiable if and only if $u$ is accepted by $T'$: $$\text{AcceptComputation}[u] = \text{Computation}_{|u|^c+c,|u|^c+c} \wedge \text{Init}[u] \wedge \text{Final}[u]\enspace,$$ where

  • $\text{Init}[u]$ expresses that the first configuration is the initial configuration for $u$ and
  • $\text{Final}[u]$ expresses that the last configuration is accepting.

The second formula is easy to come up with, because we only need to express that $q_\text{acc}$ is the state in the last configuration: $$\text{Accept}[u] = X_{|u|^c + c}^{q_\text{acc}}\enspace.$$

The first formula is somewhat more complex, because we need to describe that the first configuration is the initial configuration for the word $u$: $$\text{Init}[u] = X_0^{q_\text{init}} \wedge X_0^0 \wedge \bigwedge_{i<|u|} X_0^{i,u(i)} \wedge X_0^{|u|,\_} \wedge \bigwedge_{|u| < i < |u|^c + c} \bigwedge_{b \in B} \neg X_0^{i,b} \enspace.$$ The first conjunct states that $T'$ starts in the initial state; the second conjunct states that $T'$ starts with its head at the beginning of the tape; the remaining conjuncts state that the initial inscription of the tape is $u\_$.

This means that the function $f \colon A^* \to F_\text{PL}$ defined by $$ f(u) = \text{AcceptComputation[u]} $$ is such that, for every $u \in A^*$, the formula $f(u)$ is satisfiable iff $u \in L$, in other words, $$ f(u) \in \text{PL-SAT} \qquad \text{ iff } \qquad u \in L \enspace.$$

This means that $f$ is a polynomial-time reduction from $L$ to PL-SAT, provided $f$ can be computed in polynomial time. This can be shown easily.

From PL-SAT to 3-SAT

In general, there cannot be a polynomial-time translation from arbitrary propositional formulas in BNF into equivalent formulas in CNF, not because such formulas would not exist, but because constructing such a formula would take too much time as it would be too long.

The idea is to construct for a given formula $\varphi$ in BNF a formula $\psi$ such that $\varphi \sqsubseteq \psi$. Then we know that $\varphi$ is satisfiable if and only if $\psi$ is satisfiable (and that 1-assignments of $\psi$ are also 1-assignments of $\varphi$).—A straightforward way to do this results in formulas which have, in fact, at most three literals per clause.

In the definition of $f$ we use a function $g$ defined by induction. This function maps every propositional formula $\varphi$ to a formula $g(\varphi)$ in CNF where also variables $X_\psi$ with $\psi$ being an arbitrary propositional variable occur. The main property of $g$ is the following.

For every formula $\varphi$ and every partial assignment $\beta \colon \text{vars}(\varphi) \to \{0,1\}$ there is a exactly one partial assignment $\beta' \colon \text{vars}(g(\varphi)) \to \{0,1\}$ with $\beta \subseteq \beta'$ and such that $\beta' \mymodels g(\varphi)$ and $\beta'(X_\varphi) = \llbracket \varphi \rrbracket_\beta$. Then $f$ is easy to come up with: $f(\varphi) = g(\varphi) \wedge X_\varphi$.

For notational convenience, the values of $g$ are written in clausal notation.

Base elements

  • $g(\top) = \{\{X_\top\}\}$, $g(\bot) = \{\{\neg X_\bot\}\}$.
  • $g(X_i) = \{\{X_i\}\}$ for every $i \in \mathbf N$.

Inductive rules

  • $\varphi = \neg \psi$. Then $g(\varphi) = \{\{X_\varphi, X_\psi\}, \{\neg X_\varphi, \neg X_\psi\}\} \cup g(\psi)$.
  • $\varphi = \varphi_0 \vee \varphi_1$. Then $g(\varphi) = \{\{\neg X_{\varphi_0}, X_\varphi\}, \{\neg X_{\varphi_1}, X_\varphi\}, \{\neg X_\varphi, X_{\varphi_0}, X_{\varphi_1}\}\} \cup g(\varphi_0) \cup g(\varphi_1)$.
  • $\varphi = \varphi_0 \wedge \varphi_1$. Then $g(\varphi) = \{\{\neg X_\varphi, X_{\varphi_0}\}, \{\neg X_\varphi, X_{\varphi_1}\}, \{\neg X_{\varphi_0}, \neg X_{\varphi_1}, X_\varphi\}\} \cup g(\varphi_0) \cup g(\varphi_1)$.

Observe that $X_0 \wedge X_1 \leftrightarrow X_2 \SemEquiv (\neg X_2 \vee X_0) \wedge (\neg X_2 \vee X_1) \wedge (\neg X_0 \vee \neg X_1 \vee X_2)$ and $X_0 \vee X_1 \leftrightarrow X_2 \SemEquiv (\neg X_0 \vee X_2) \wedge (\neg X_1 \vee X_2) \wedge (\neg X_2 \vee X_0 \vee X_1)$.

That $g$ has the above property can be proved by induction.

Application

The theorem stating that SAT is NP-complete has a practical meaning in the following sense: Every problem in NP can be tackled using a SAT solver. The only thing one has to do is to apply a reduction from the problem to the problem SAT.

Exercises

Exercise Wir betrachten folgende nichtdeterministische Turing-Maschine $M$ Machine-01.svg mit der Laufzeitschranke $n^c+c$ für $c=1$.

  1. Welche Sprache erkennt $M$?
  2. Finden Sie eine 1-Belegung $\beta$ für $\text{Init}[0a1]$. Beschreiben Sie $\beta$ durch Angabe der Menge $\{X\in\operatorname{vars}(\text{Init}[0a1])\mid \beta(X)=1\}$.
  3. Betrachten Sie das Eingabewort $w=00aa11$ und beantworten Sie folgende Fragen:
    1. Gibt es eine 1-Belegung von $\text{AcceptComputation}[w]$, sodass $\beta(X^{4}_4)=1$?
    2. Gibt es eine 1-Belegung von $\text{AcceptComputation}[w]$, sodass $\beta(X^{q_2}_5)=1$?
    3. Gibt es zwei verschiedene 1-Belegungen $\beta_1$ und $\beta_2$ von $\text{AcceptComputation}[w]$, sodass $\beta_1(X_3^{q_0})\neq\beta_2(X_3^{q_1})$?

Exercise Im folgenden betrachten wir Berechnungen der nichtdeterministischen Turingmaschine $M$ über dem Bandalphabet $B=\{0,1,\_\}$ mit den Zuständen $Q=\{q_0,q_1\}$, dem Startzustand $q_0$, den Transitionen $\{(q_0,0)\to (q_0,0,R); (q_0,1)\to (q_1,1,R); (q_1,0)\to (q_1,1,R);(q_1,0)\to (q_0,0,R); (q_1,1)\to (q_1,1,R)\}$.

  1. Wie viele Variablen werden bei der Modellierung von Berechnungen für die oben genannte Turingmaschine benötigt, wenn man $k=5$ Schritte betrachtet und das Band maximal Länge $\ell=6$ hat?
  2. Geben Sie die ersten fünf Konfiguration von zwei verschiedenen Berechnungen der Turingmaschine mit dem initialen Bandinhalt $u=011000$ an.
  3. Gibt es eine 1-Belegung $\beta$ von $\text{Computation}^6_4$ mit $\beta(X_0^{0,0})=1$? Begründen Sie Ihre Antwort kurz.
  4. Gibt es eine 1-Belegung $\beta$ von $\text{Computation}^6_4$, sodass $\beta(X_i^{p,1})=\beta(X_{i+1}^{p,0})=1$ für irgendeinen Schritt $i\leq 4$ und eine Position $p\leq 5$ gilt? Begründen Sie Ihre Antwort kurz.
  5. Wie viele verschiedene knappe 1-Belegung $\beta$ von $\text{Init}[011000]\wedge \text{Computation}^{6}_{2}$ gibt es? Dabei sei $\text{Init}[u]$ wie hier definiert. Begründen Sie Ihre Antwort kurz.
  6. Wie viele verschiedene knappe 1-Belegung $\beta$ von $\text{Init}[011000]\wedge \text{Computation}^{6}_{5}$ gibt es? Begründen Sie Ihre Antwort kurz.



Lösung

Zunächst eine kurze Überlegung welche Berechnungen $M$ durchführen kann: $M$ liest den Bandinhalt von links nach rechts. Liest $M$ eine $1$, können alle direkt folgende $0$en durch $1$en ersetzt werden. Das geschieht aber nichtdeterministisch, sodass die $0$en erstetzt werden können aber nicht müssen. Wird eine $1$ nicht ersetzt, so darf auch eine weitere direkt folgende $0$ ersetzt werden.

  1. Allgemein gilt $|\{X_i^q \mid i\leq k, q\in Q \} \cup \{X_i^{j,b} \mid i\leq k, b\in B, j < l \} \cup \{X_i^j \mid j< l, i\leq k \}| = (k+1)|Q|+(k+1)l|B|+(k+1)l$. Somit gibt es bei $|Q|=2$, $|B|=3$, $k=5$ und $\ell=$6 insgesamt $156$ ($=12+108+36$) Variablen benötigt.
    • $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_0,011000,4)$
    • $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4)$
  3. Ja, die gibt es. Es gibt das Wort $000000$, der Länge 6, bei dem die Turingmaschine vier Schritte hintereinander den Bandinhalt unverändert lässt und nur Ihren Kopf bewegt. Da $\beta(X_0^{0,0})$ bedeutet bei korrekter Modellierung dann nur, dass initial das erste Zeichen $0$ ist, was für das gegebene Wort der Fall ist.
  4. Nein, die kann es nicht geben. Würde es diese geben, müsste die Turingmaschine im Schritt $i+1$ an der Position $p$ die $1$ zu einer $0$ ersetzen. Doch die Turingmaschine kann aufgrund ihrer Transitionsmenge nur eine $0$ schreiben, wenn an der Stelle bereits eine $0$ gelesen wurde. D.h. bei korrekter Modellierung wird die Teilformel $\text{Transitions}$ nicht erfüllt.
  5. Genau eine. In den ersten zwei Schritten gibt es für die gegebene nur eine mögliche Konfigurationsfolge. Nichtdeterminismus ist erst möglich, sobald eine $0$ nach einer $1$ gelesen wurde und sich die TM im Zustand $q_1$ befindet. Da eine erfüllende knappe Belegung genau einer gültigen Konfiguration entspricht (Der Bandinhalt, die Kopfposition sind in jedem Schritt ist eindeutig), kann es also auch nicht verschiedene Belegungen geben.
  6. Drei Möglichkeiten, da es auch genau drei mögliche gülte Konfigurationsfolgen für die ersten fünf Schritte der Turingmaschine gibt und jede einer knappen $1$-Belegung entspricht. Da der Kopf sich immer nur nach rechts bewegt, muss nur betrachtet werden, wie viele Möglichkeiten es gibt $0$en durch $1$en in den ersten fünf Schritten zu ersetzen. Es ergeben sich folgende drei Berechnungen:
    • $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_0,011000,4),(q_0,011000,5)$
    • $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4),(q_0,011100,5)$
    • $(q_0,011000,0),(q_0,011000,1),(q_1,011000,2),(q_1,011000,3),(q_1,011100,4),(q_1,011110,5)$
Retrieved from "https://logic4free.informatik.uni-kiel.de/index.php?title=NP-completeness_of_SAT&oldid=4439"