27 Soundness and Completeness of Resolution Calculus, NP and SAT problem

Lecture from: 18.12.2024 | Video: Videos ETHZ

Let us briefly recap where we are. We were given a set of formulas $M$ and wanted to see if a formula $F$ is logically entailed from the set of formulas, meaning if $M\models F$. In the extreme case, we can also ask if $F$ is a tautology, meaning it is logically entailed from no assumptions, i.e., $\varnothing \models F$ (or simply $\models F$). Note that the aim is to prove things with as few assumptions as possible.

We also introduced a second formalism where we syntactically derive things, denoted as $M{⊢}_{K}F$, in a calculus $K$. The idea is that syntactic derivation steps should indeed preserve logical entailment (if the premises are true, the derived formula should also be true). This property is called soundness. Conversely, we also want that if something can be logically entailed, there exists a finite sequence of derivation steps to show that we can derive it syntactically. This property is called completeness.

These concepts (soundness and completeness) are generally true for all logical calculi. Last time, we focused on propositional logic and said that instead of dealing with logical connectives like $\wedge$, $\vee$, $\neg$, $\to$, etc., we can convert our formula to Conjunctive Normal Form (CNF) and look at it as a clause set in the context of the resolution calculus.

We also observed that checking the satisfiability of a formula in CNF corresponds to the SAT problem. We are particularly interested in unsatisfiability, as it’s generally a harder problem (for satisfiability, we just need to provide a single interpretation that makes the clause set true).

The current belief is that SAT $\in$ NP, but UNSAT $\notin$ NP (or more precisely, UNSAT is co-NP-complete), meaning there is likely no efficient proof system that can provide short, easily verifiable proofs of unsatisfiability for arbitrary CNF formulas (unless P = NP, which is considered highly unlikely). This means given a clause set, while a “yes” answer to the SAT problem can be verified efficiently, a “no” answer is, in general, believed not to be verifiable in polynomial time.

Resolution Calculus

Let $\mathcal{K}$ be a clause set. A clause $C$ is entailed by a clause set $\mathcal{K}$, written $\mathcal{K}\models C$, if for any interpretation $\mathcal{A}$ that makes all clauses in $\mathcal{K}$ true (i.e., $\mathcal{A}(\mathcal{K})=1$), $C$ must also be true (i.e., $\mathcal{A}(C)=1$). In other words, if every clause in $\mathcal{K}$ evaluates to 1 under $\mathcal{A}$, then $C$ must also evaluate to 1 under $\mathcal{A}$.

We also have the property that if $C\subseteq C^{\prime }$, then $\{C\}\models C^{\prime }$. This holds because if $\mathcal{A}(C)=1$, then at least one literal in $C$ must be true under the interpretation $\mathcal{A}$. Since $C^{\prime }$ contains all the literals of $C$ (and possibly more), that same literal will also be present in $C^{\prime }$, and therefore $\mathcal{A}(C^{\prime })=1$. This shows that adding arbitrary literals to a clause results in a weaker (or equally strong) clause, as it becomes easier to satisfy. This is referred to as weakening.

If we have $\mathcal{K}\subseteq {\mathcal{K}}^{\prime }$, then ${\mathcal{K}}^{\prime }\models \mathcal{K}$. More generally, if for every clause $C\in \mathcal{K}$, we have ${\mathcal{K}}^{\prime }\models C$, then we write ${\mathcal{K}}^{\prime }\models \mathcal{K}$. This means that any interpretation that satisfies all clauses in ${\mathcal{K}}^{\prime }$ will also satisfy all clauses in $\mathcal{K}$. In terms of satisfiability, this also implies that if ${\mathcal{K}}^{\prime }$ is satisfiable, then so is $\mathcal{K}$. The other way around is not true in general.

Resolution Rule

Recall the resolution rule. If we are given two clauses $C_1$ and $C_2$ such that there exists a literal $L$ where $L\in C_1$ and $\neg L\in C_2$, then we can apply the resolution rule. The resolvent $C$ of $C_1$ and $C_2$ with respect to $L$ is defined as:

$C=(C_1\cup C_2)\setminus \{L,\neg L\}$

The resolvent can maximally have a size of $|C_1|+|C_2|-2$. We write the application of the resolution rule as:

$\{C_1,C_2\}{⊢}_{\text{res}}C$

The resolution calculus has only this single rule, i.e., $\text{Res}=\{\text{res}\}$.

Lemma 6.5: Soundness

If a clause $C$ can be derived from a clause set $\mathcal{K}$ using the resolution rule, then $C$ is logically entailed by $\mathcal{K}$. Formally:

$\mathcal{K}{⊢}_{\text{Res}}C⟹\mathcal{K}\models C$

This is a lemma, and we need to prove it.

It suffices to show that a single application of the resolution rule preserves entailment. Let $\{C_1,C_2\}{⊢}_{\text{res}}C$. We want to show that $\{C_1,C_2\}\models C$. If this is true, we can extend to any sequence of resolution steps, demonstrating $\mathcal{K}\models C$.

Let us now justify the first part, i.e., show that $\{C_1,C_2\}\models C$.

Let $\mathcal{A}$ be an arbitrary interpretation such that $\mathcal{A}(C_1)=1$ and $\mathcal{A}(C_2)=1$. Since $\{C_1,C_2\}{⊢}_{\text{res}}C$, there exists a literal $L$ such that $L\in C_1$ and $\neg L\in C_2$, and $C=(C_1\cup C_2)\setminus \{L,\neg L\}$. We can perform a case distinction on the truth value of $L$ under $\mathcal{A}$:

• Case 1: $\mathcal{A}(L)=1$: Since $\mathcal{A}(C_2)=1$ and $\mathcal{A}(\neg L)=0$, there must exist another literal $L^{\prime }\in C_2$ such that $L^{\prime }\ne \neg L$ and $\mathcal{A}(L^{\prime })=1$. Since $L^{\prime }\in C_2$ and $L^{\prime }\ne \neg L$, it follows that $L^{\prime }\in C$. Therefore, $\mathcal{A}(C)=1$.

• Case 2: $\mathcal{A}(L)=0$: Since $\mathcal{A}(C_1)=1$ and $\mathcal{A}(L)=0$, there must exist another literal $L^{\prime \prime }\in C_1$ such that $L^{\prime \prime }\ne L$ and $\mathcal{A}(L^{\prime \prime })=1$. Since $L^{\prime \prime }\in C_1$ and $L^{\prime \prime }\ne L$, it follows that $L^{\prime \prime }\in C$. Therefore, $\mathcal{A}(C)=1$.

In both cases, $\mathcal{A}(C)=1$. Thus, under any interpretation $\mathcal{A}$ where $\mathcal{A}(C_1)=1$ and $\mathcal{A}(C_2)=1$, we also have $\mathcal{A}(C)=1$. Therefore, $\{C_1,C_2\}\models C$. Because $\{C_1,C_2\}\subseteq \mathcal{K}⟹\mathcal{K}\models \{C_1,C_2\}$, by transitivity $\mathcal{K}\models C$.

Theorem 6.6: Completeness of Resolution

We want to show that if a clause set is unsatisfiable, then we can derive the empty clause using resolution.

Let $\mathcal{K}$ be a clause set. Then $\mathcal{K}$ is unsatisfiable if and only if $\mathcal{K}{⊢}_{\text{Res}}\square$. (Recall that $\square$ denotes the empty clause).

Proof:

"$\Leftarrow$": (Soundness, already proven in Lemma 6.5, but we recap the argument for clarity.) Assume $\mathcal{K}{⊢}_{\text{Res}}\square$. From Lemma 6.5 (soundness of the resolution rule), we know that $\mathcal{K}{⊢}_{\text{Res}}\square$ implies $\mathcal{K}\models \square$. The empty clause $\square$ is unsatisfiable (vacuously false), since there exists no interpretation that can make it true. Since $\mathcal{K}$ entails an unsatisfiable clause, $\mathcal{K}$ must also be unsatisfiable.

"$\Rightarrow$": (Completeness, this is what we show by induction) Assume $\mathcal{K}$ is unsatisfiable. We want to prove that $\mathcal{K}{⊢}_{\text{Res}}\square$ using induction on the number of distinct propositional variables (atoms) appearing in $\mathcal{K}$.

• Base Case (Induction Base): Let $n$ be the number of distinct propositional variables in $\mathcal{K}$.

  • If $n=0$, then $\mathcal{K}$ is either $\{\}$ (the empty set of clauses, which is satisfiable) or $\{\square \}$ (contains the empty clause). Since we assumed $\mathcal{K}$ is unsatisfiable, $\mathcal{K}$ must be $\{\square \}$, and trivially $\mathcal{K}{⊢}_{\text{Res}}\square$.

  • If $n=1$, $\mathcal{K}$ contains only one propositional variable, say $A_1$. The possible clauses are $\{A_1\}$, $\{\neg A_1\}$, $\{A_1,\neg A_1\}$ and $\square$. The only unsatisfiable sets of clauses from those are $\{\{A_1\},\{\neg A_1\}\}$ and any set containing $\square$. If we are in a set containing $\square$, then we are already done. Otherwise, $\mathcal{K}$ must contain both $\{A_1\}$ and $\{\neg A_1\}$ (or clauses that can be weakened to these). Applying resolution to $\{A_1\}$ and $\{\neg A_1\}$ yields $\square$. Thus, $\mathcal{K}{⊢}_{\text{Res}}\square$.

• Induction Hypothesis (I.H.): Assume that for any unsatisfiable clause set ${\mathcal{K}}^{\prime }$ containing at most $n$ distinct propositional variables, ${\mathcal{K}}^{\prime }{⊢}_{\text{Res}}\square$.

• Inductive Step: Let $\mathcal{K}$ be an unsatisfiable clause set containing $n+1$ distinct propositional variables. Let $A$ be one of these variables. We construct two new clause sets, ${\mathcal{K}}_A$ and ${\mathcal{K}}_{\neg A}$, as follows:

  • ${\mathcal{K}}_A$: From $\mathcal{K}$, remove all clauses containing $A$, and remove $\neg A$ from the remaining clauses.
  • ${\mathcal{K}}_{\neg A}$: From $\mathcal{K}$, remove all clauses containing $\neg A$, and remove $A$ from the remaining clauses.

  Formally, ${\mathcal{K}}_A=\{C\setminus \{\neg A\}\mid C\in \mathcal{K}\text{ and }A\notin C\}$ and ${\mathcal{K}}_{\neg A}=\{C\setminus \{A\}\mid C\in \mathcal{K}\text{ and }\neg A\notin C\}$.

  Since $\mathcal{K}$ is unsatisfiable, both ${\mathcal{K}}_A$ and ${\mathcal{K}}_{\neg A}$ are also unsatisfiable. (If either ${\mathcal{K}}_A$ or ${\mathcal{K}}_{\neg A}$ were satisfiable, we could extend that satisfying interpretation to satisfy $\mathcal{K}$ by assigning the appropriate truth value to $A$). Furthermore, ${\mathcal{K}}_A$ and ${\mathcal{K}}_{\neg A}$ each contain at most $n$ distinct propositional variables (since we’ve eliminated $A$).

  By the induction hypothesis, ${\mathcal{K}}_A{⊢}_{\text{Res}}\square$ and ${\mathcal{K}}_{\neg A}{⊢}_{\text{Res}}\square$.

  Now, we want to show that $\mathcal{K}{⊢}_{\text{Res}}\square$. Since ${\mathcal{K}}_A{⊢}_{\text{Res}}\square$, there exists a sequence of resolution steps starting from clauses in ${\mathcal{K}}_A$ that derives $\square$. We can “lift” this derivation to a derivation from $\mathcal{K}$: Replace each clause $C$ in the derivation from ${\mathcal{K}}_A$ with $C\cup \{\neg A\}$ if $C\cup \{\neg A\}$ was not a step of the derivation. The same sequence of resolution steps will now derive $\{\neg A\}$ (instead of $\square$) from clauses in $\mathcal{K}$.

  Similarly, since ${\mathcal{K}}_{\neg A}{⊢}_{\text{Res}}\square$, we can lift a derivation of $\square$ from ${\mathcal{K}}_{\neg A}$ to a derivation of $\{A\}$ from clauses in $\mathcal{K}$.

  Finally, we can resolve $\{A\}$ and $\{\neg A\}$ (which we derived from $\mathcal{K}$) to obtain $\square$. Therefore, $\mathcal{K}{⊢}_{\text{Res}}\square$.

This completes the proof by induction.

3-SAT

The 3-SAT problem is a special case of the SAT problem where each clause contains exactly three literals. A formula in 3-CNF is a conjunction of clauses, where each clause is a disjunction of three literals.

Surprisingly, 3-SAT is also NP-complete. This means that although it appears more restricted than the general SAT problem (where clauses can have any number of literals), it is equally difficult in terms of computational complexity. In other words, there is no known polynomial-time algorithm for 3-SAT (unless P = NP), and any algorithm that can solve 3-SAT in polynomial time could be adapted to solve any other problem in NP in polynomial time. This equivalence in difficulty is established by showing that any SAT instance (with arbitrary clause lengths) can be converted into a 3-SAT instance in polynomial time, such that the 3-SAT instance is satisfiable if and only if the original SAT instance is satisfiable.

NP-Completeness

A problem is NP-complete if it satisfies two conditions:

1. It is in NP: A problem is in the class NP (Nondeterministic Polynomial time) if a proposed solution (“yes” instance) can be verified in polynomial time. This means that given a potential solution, we can check whether it’s correct in a time that grows at most polynomially with the size of the input. For example, for SAT, given an assignment of truth values to variables, we can easily check in polynomial time if that assignment satisfies all clauses.

2. It is NP-hard: A problem is NP-hard if every problem in NP can be reduced to it in polynomial time. This means that for any problem in NP, we can find a polynomial-time algorithm that transforms an instance of that problem into an instance of the NP-hard problem, such that the answer (“yes” or “no”) is preserved. In other words, the NP-hard problem is at least as difficult as any other problem in NP.

A problem that satisfies both of these conditions is called NP-complete. NP-complete problems are, in a sense, the “hardest” problems in NP. If we could find a polynomial-time algorithm for any NP-complete problem, we would have proven that P = NP, which would imply that all problems in NP have polynomial-time solutions.

This was the last lecture…