Actions

Satisfiability (propositional logic)

From Learning Logic for Computer Science

A propositional formula is satisfiable if there is a 1-assignment for it; a set of propositional formulas is satisfiable if there is a simultaneous 1-assignment for its elements.

Individual formula

Definition A propositional formula $\varphi$ is satisfiable if there is a variable assignment $\beta$ such that $\beta \mymodels \varphi$, that is, if there is a 1-assignment for it. In symbols: $\text{Sat} \varphi$.

If a formula is not satisfiable, it is said to be unsatisfiable or a contradiction, in symbols: $\text{Unsat} \varphi$.

Example The formula $(X_0 \vee \neg X_1) \wedge \neg X_0$ is satisfiable, because $\{X_0 \mapsto 1, X_1 \mapsto 0\}$ is a 1-assignment for this formula. The formula $X_0 \wedge \neg X_0$ is not satisfiable.

Remark A propositional formula $\varphi$ is unsatisfiable if, and only if, $\varphi \SemEquiv \bot$.

An extreme case of satisfiability is when every assignment is a 1-assignment for a given formula $\varphi$. Then the formula is said to be a tautology or (universally) valid, in symbols: $\models \varphi$.

Example The formulas $X_0 \vee \neg X_0$ and $\top$ are tautologies, whereas $(X_0 \vee \neg X_1) \wedge \neg X_0$ is no tautology.

Remark A propositional formula $\varphi$ is a tautology if, and only if, $\varphi \SemEquiv \top$.

Note, that the notion $\models \varphi$ comes from the entailment relation.

There is an intimate connection between satisfiable formulas and tautologies.

Lemma Let $\varphi$ be a propositional formula. The the following are equivalent:

  • The formula $\varphi$ is satisfiable. ($\text{Sat} \varphi$.)
  • The formula $\neg \varphi$ is not valid. ($\not\models \neg \varphi$.)

Proof The proof is as follows. Assume $\varphi$ is satisfiable. Then there exists a variable assignment $\beta$ such that $\beta \mymodels \varphi$. The semantics of propositional formulas implies $\beta \not\mymodels \neg \varphi$, from which follows that $\neg \varphi$ is not valid. Conversely, assume $\neg \varphi$ is not valid. Then there is a variable assignment $\beta$ such that $\beta \not\mymodels \neg \varphi$. The semantics of propositional formulas implies $\beta \mymodels \varphi$, which means $\varphi$ is satisfiable.—This concludes the proof.

There are several ways of stating the above equivalence. Another way is to say the following statements are equivalent:

  • The formula $\neg \varphi$ is satisfiable.
  • The formula $\varphi$ is not valid.

In this version, there is exactly one negation in each of the two statements.

Sets of formulas

A set of propositional formulas $\Phi$ is satisfiable if there is a variable assignment $\beta$ such that $\beta \mymodels \varphi$ for every $\varphi \in \Phi$. In other words, $\Phi$ is satisfiable if there is a simultaneous 1-assignment for all the formulas in $\Phi$. In symbols: $\text{Sat} \Phi$.

Satisfiability of finite sets can be reduced to satisfiability of a single formula:

Remark Let $\varphi_0, \dots, \varphi_{n-1}$ be propositional formulas. Then the following are equivalent:

  • $\text{Sat} \{\varphi_0, \dots, \varphi_{n-1}\}$.
  • $\text{Sat} \bigwedge(\varphi_0, \dots, \varphi_{n-1})$.

Satisfiability ordering

When comparing 1-assignments of formulas with each other, then the following pre ordering relation is useful.

Definition Let $\varphi$ and $\varphi'$ be propositional formulas. We write $\varphi \sqsubseteq \varphi'$ if the following three conditions are satisfied:

  • $\text{vars}(\varphi) \subseteq \text{vars}(\varphi')$.
  • For every variable assignment $\beta'$ with $\beta' \mymodels \varphi'$, $\beta' \mymodels \varphi$.
  • For every $\beta \colon \text{vars}(\varphi) \to \{0,1\}$ with $\beta\mymodels \varphi$, there is some variable assignment $\beta'$ such that $\beta \subseteq \beta'$ and $\beta' \mymodels \varphi'$.

Example We have $X_0 \sqsubseteq (X_0 \vee X_1) \wedge \neg X_1 \wedge X_2$. We have $X_0 \vee \neg X_0 \SemEquiv X_1 \vee \neg X_1$, but we have $X_0 \vee \neg X_0 \not\sqsubseteq X_1 \vee \neg X_1$ and $ X_1 \vee \neg X_1 \not\sqsubseteq X_0 \vee \neg X_0$.

Remark Let $\varphi$ and $\varphi'$ be propositional formulas. If $\varphi \sqsubseteq \varphi'$, then

  • $\text{Sat} \varphi$ iff $\text{Sat} \varphi'$ and
  • $\varphi' \models \varphi$ ($\varphi'$ entails $\varphi$).

Satisfiability solvers and satisfiability tests

An algorthim that checks, for a given finite set of propositional formulas, whether it is satisfiable is called a satisfiability test. When it outputs a simultaneous 1-assignment for satisfiable sets of formulas it is called a satisfiability solver.

Pointers

There is an intimate connection between satisfiability and entailment.

An important property of satisfiability is compactness.

Exercises

Exercise Gegeben seien folgende Formeln: \begin{align*} \varphi_0 & = X_0 \to (\neg X_0\to X_1)&\\ \varphi_1 & = (X_1 \wedge X_2)\vee X_3 \;\to\; \neg X_1 \vee \neg X_2 \vee \neg X_3&\\ \varphi_2 & = X_1\leftrightarrow (X_1\to X_2)\wedge (X_1\to \neg X_2)&\\ \varphi_{3,n} & = \dot{\bigvee}_{i=1}^n (X_{i}\wedge X_{i-1})\leftrightarrow \bigoplus_{i=1}^n (X_{i}\wedge X_{i-1}) & \text{für $n\geq 1$}\\ \end{align*}

  1. Geben Sie zu jeder der oben genannten Formeln an, ob diese erfüllbar, unerfüllbar oder eine Tautologie sind.
  2. Geben Sie für die erfüllbaren Formeln jeweils eine 1-Belegung, für Formeln, die keine Tautologie sind, jeweils eine 0-Belegung und zu jeder Tautologie und Kontradiktion eine vollständige Wertetabelle als Beleg für Ihre Antwort bei 1. an.



Lösung

  • $\varphi_0 = X_0 \to (\neg X_0\to X_1)$ ist eine Tautologie und damit erfüllbar. Eine 1-Belegung wäre $\beta=\{X_0\mapsto 0, X_1\mapsto 1\}$.
    \(\beta(X_0)\) \(\beta(X_1)\) \(\llbracket\neg X_0\rrbracket_{\beta}\) \(\llbracket\neg X_0\to X_1\rrbracket_{\beta}\) \(\llbracket X_0 \to (\neg X_0\to X_1)\rrbracket_\beta\)
    0 0 1 0 1
    0 1 1 1 1
    1 0 0 1 1
    1 1 0 1 1
  • $\varphi_1=(X_1 \wedge X_2)\vee X_3 \;\to\; \neg X_1 \vee \neg X_2 \vee \neg X_3$ ist erfüllbar aber weder eine Tautologie, noch eine Kontradiktion. Eine 1-Belegung wäre $\beta=\{X_1\mapsto 0, X_2\mapsto 0, X_3\mapsto 0\}$ und eine 0-Belegung wäre $\beta=\{X_1\mapsto 1, X_2\mapsto 1, X_3\mapsto 1\}$.
  • $\varphi_2 = X_1\leftrightarrow (X_1\to X_2)\wedge (X_1\to \neg X_2)$ ist eine Kontradiktion und damit unerfüllbar. Eine 0-Belegung wäre $\beta=\{X_1\mapsto 0, X_2\mapsto 0\}$.
    \(\beta(X_1)\) \(\beta(X_2)\) \(\llbracket\neg X_2\rrbracket_{\beta}\) \(\llbracket X_1\to X_2\rrbracket_{\beta}\) \(\llbracket X_1\to \neg X_2\rrbracket_{\beta}\) \(\llbracket (X_1\to X_2)\wedge (X_1\to \neg X_2)\rrbracket_{\beta}\) \(\llbracket X_1\leftrightarrow (X_1\to X_2)\wedge (X_1\to \neg X_2)\rrbracket_{\beta}\)
    0 0 1 1 1 1 0
    0 1 0 1 1 1 0
    1 0 1 0 1 0 0
    1 1 0 1 0 0 0
  • Für $n\leq 2$ ist $\varphi_{3,n} = \dot{\bigvee}_{i=1}^n (X_{i}\wedge X_{i-1})\leftrightarrow \bigoplus_{i=1}^n (X_{i}\wedge X_{i-1})$ eine Tautologie und damit erfüllbar. Eine 1-Belegung wäre $\beta=\{X_0\mapsto 0, X_1\mapsto 0, X_2\mapsto 0\}$. Es ergeben sich folgende Wertetetabellen.
    • $n=1$:
      \(\beta(X_0)\) \(\beta(X_1)\) \(\llbracket X_1\wedge X_0\rrbracket_{\beta}\) \(\llbracket \dot{\bigvee}(X_1\wedge X_0)\rrbracket_{\beta}\) \(\llbracket \oplus(X_1\wedge X_0)\rrbracket_{\beta}\) \(\llbracket \dot{\bigvee}_{i=1}^1 (X_{i}\wedge X_{i-1})\leftrightarrow \bigoplus_{i=1}^1 (X_{i}\wedge X_{i-1})\rrbracket_{\beta}\)
      0 0 0 0 0 1
      0 1 0 0 0 1
      1 0 0 0 0 1
      1 1 1 1 1 1
    • $n=2$:
      \(\beta(X_0)\) \(\beta(X_1)\) \(\beta(X_2)\) \(\llbracket X_1\wedge X_0\rrbracket_{\beta}\) \(\llbracket X_2\wedge X_1\rrbracket_{\beta}\) \(\llbracket \dot{\bigvee}_{i=1}^2 (X_{i}\wedge X_{i-1})\rrbracket_{\beta}\) \(\llbracket \bigoplus_{i=1}^2 (X_{i}\wedge X_{i-1})\rrbracket_{\beta}\) \(\llbracket \dot{\bigvee}_{i=1}^2 (X_{i}\wedge X_{i-1})\leftrightarrow \bigoplus_{i=1}^2 (X_{i}\wedge X_{i-1})\rrbracket_{\beta}\)
      0 0 0 0 0 0 0 1
      0 0 1 0 0 0 0 1
      0 1 0 0 0 0 0 1
      0 1 1 0 1 1 1 1
      1 0 0 0 0 0 0 1
      1 0 1 0 0 0 0 1
      1 1 0 1 0 1 1 1
      1 1 1 1 1 0 0 1
  • Für $n\geq 3$ ist $\varphi_{3,n} = \dot{\bigvee}_{i=1}^n (X_{i}\wedge X_{i-1})\leftrightarrow \bigoplus_{i=1}^n (X_{i}\wedge X_{i-1})$ jedoch keine Tautologie, aber erfüllbar. Eine $1$-Belegung wäre $\beta_1$ mit $\beta(X_i)=0$ für alle $i\in\mathbb{N}$, eine $0$-Belegung wäre $\beta_1$ mit $\beta(X_0)=\beta(X_1)=\beta(X_2)=\beta(X_3) = 1$ und $\beta(X_i)=0$ für alle $i\in\mathbb{N}_{>3}$.

Exercise Geben Sie zu jeder der folgenden Formelmengen an, ob diese erfüllbar oder unerfüllbar ist. Geben Sie im Falle einer erfüllbaren Formel eine simultane $1$-Belegung und im Falle einer unerfüllbaren Formel eine kurze Begründung an. \begin{align*} \Phi_1 & = \{X_1 \vee X_2, \neg X_1 \vee X_3, \neg X_1 \vee X_2, \neg X_2 \vee \neg X_3\}\\ \Phi_{2,n} & = \{ X_i \to X_{i+1}, \neg X_i \to \neg X_{i+1} \mid 0\leq i \leq n-1\}\cup\{X_n\to \neg X_0\} & \text{für $n\geq 1$}\\ \Phi_{3,n} & = \Phi_{2,n}\cup \{ \neg X_n \to X_0\} & \text{für $n\geq 1$}\\ \end{align*}



Lösung

  • Die Formelmenge $\Phi_1$ ist erfüllbar. Eine simultane $1$-Belegung ist $\beta=\{X_1\mapsto 0, X_2\mapsto 1, X_3\mapsto 0\}$.
  • Die Formelmenge $\Phi_{2,n}$ ist für alle $n\geq 1$ erfüllbar. Eine simultane $1$-Belegung ist $\beta$ mit $\beta(X_i)=0$ für $0\leq i < n$
  • Die Formelmenge $\Phi_{3,n}$ ist für alle $n\geq 1$ unerfüllbar.
    Begründung:
    Stellen wir die Formelmenge als Graph da, wobei die Variablen oder negierten Variablen die Knoten und die einzelnen Formeln gerichtete Kanten darstellen, so erhalten wir einen Kreis. Wird nun eine Variable durch eine Belegung wahr, müssen alle Folgeknoten, also alle Knoten auf dem Kreis, durch $\beta$ zu $1$ ausgewertet werden, damit jede Folgerung der Formel zu $1$ ausgewertet werden und $\beta$ somit eine simultane $1$-Belegung wäre. Da nun aber für jede Variable $X_i$ auf dem Kreis auch $\neg X_i$ auf dem Kreis liegt und $\llbracket X_i\rrbracket_\beta=1 - \llbracket \neg X_i\rrbracket_\beta$ muss es mindestens auch einen Knoten geben der zu $1$ ausgewertet wird und einen, der zu $0$ ausgewertet wird. Dies kann aber nicht passieren, da ja alle Knoten zu $1$ ausgewertet werden müssen, damit eine Belegung eine simultane $1$-Belegung ist.

    Eine weniger anschauliche Begründung:
    Da sowohl $X_i\to X_{i+1}, \neg X_{i}\to\neg X_{i+1}\in\Phi_{3,n}$ für alle $i< n$ gilt, folgt, sofern es eine erfüllende Belegung $\beta$ gibt, dass für eine erfüllende Belegung $\beta(X_0)\leq \beta(X_1)\leq \dots\leq \beta(X_n)$ und $\beta(X_0)\geq \beta(X_1)\geq \dots\geq \beta(X_n)$ also $\beta(X_0)= \beta(X_1)= \dots= \beta(X_n)$ gilt. Dies ließe sich induktiv und mithilfe der Semantik von $\rightarrow$ zeigen. Außerdem würde aus $X_n\to\neg X_0,\neg X_n\to X_0\in\Phi_{3,n}$, dass $\beta(X_n)\leq 1-\beta(X_0)$, $1-\beta(X_n)\leq\beta(X_0)$ und somit $1-\beta(X_n)=\beta(X_0)$. Da jedoch $\beta(X_n)=\beta(X_0)$ gelten müsste, kann dies nicht der Fall sein und somit kann es keine simultane $1$-Belegung geben.

    Beachte, dass beide Begründungen kein vollständiger Beweis, der in dieser Aufgabe auch nicht gefordert ist, wären.