Proving Conjectures in Propositional Logic (SAT)

Propositional logic corresponds to the satisfiability problem (SAT). It is known to be NP-complete. Only, the special case of 2-SAT is polynomial solvable (by converting the problem to computing the strongly connected components).

Ingredients

• The basic unit of propositional logic is the proposition, which may be either true or false.
• A set of operators, viz. conjunction $\land$, disjunction $\lor$ and negation $\neg$ (equivalence and implication are derived from these ones).

An example of implication, If Jack knows Julie, Julie knows Jack.

PROPOSITIONAL LOGIC IS DECIDABLE. Proof. For any statement you can use a truth table!

Let's find a more efficient method than computing truth tables.

Definitions

• A proposition $l$ is also called a literal.
• A clause $C$ is a disjunction of literals $l_1\lor l_2\lor\dots\lor l_n$ or equivalently a set of literals $\{l_1,l_2,\dots,l_n\}$.
• A clausal form (expressed in conjuctive normal form, CNF) $\Sigma$ is a conjuction of clauses $C_1\land\dots\land C_c$ or equivalently a set of clauses (a set of sets) $\{C_1,\dots,C_c\}$.
• Given a clausal form $\Sigma$, a refutation is the derivation of a contradiction $\perp$, namely $\Sigma\vdash\perp$.

Now we want to define an inference rule which is used for refutation of clauses. Consider two clauses $C_1=\{l,a,\dots\}$ and $C_1=\{\neg l,b,\dots\}$. These two clauses are said to clash. Therefore, we can define the resolvent of the two clashing clauses as $C=C_1\setminus\{l\}\cup C_2\setminus\{\neg l\}$

Resolution. Given a clausal form $\Sigma$, resolution takes two clashing clauses $C_1,C_2$ computes the resolvent $C$ and add it to the clausal form. We can easily prove that $\{C_1,C_2,C\}$ preserves the truth of $\Sigma$.

Note that resolution allows to derive a contradiction, in fact if $C_1=\{a\}$ and $C_2=\{\neg a\}$, then the resolvent is $C=\{\perp\}$.

Theorem. Resolution is sound and complete for refutation. In fact, if resolution derives a contradiction, then the statement logically entails a contradiction $\Sigma\vdash\perp\implies\Sigma\models\perp$ (soundness) and if a statement is contradictory, resolution admits a refutation (completeness) $\Sigma\models\perp\implies\Sigma\vdash\perp$.
Proof of soundness. Trivially obtained by the fact that resolution preserves the truth of clauses.

It is important to mention that in this case there is a finite number of possible resolution steps, which is bounded above by the number of possible combinations of literals (as there is a limit on the possible number of clauses that can be added). Therefore, resolution is guaranteed to find a contradiction if the statement is unsatisfiable. Furthermore, if no contradiction is found, the statement is satisfiable.

RESOLUTION REFUTATION IS A METHOD TO DECIDE ABOUT SATISFIABILITY IN PROPOSITIONAL LOGIC AND IS IN GENERAL MORE EFFICIENT THAN COMPUTING TRUTH TABLES.

Example

Problems

Note also that (i) resolution increases the set of clauses and (ii) it can increase the number of literals in the clauses. This creates problems of inefficiency when trying to detect unsatisfiable statements. Smarter selection of clauses can improve the convergence to refutation. Nevertheless, if a statement is satisfiable, you need to check ALL POSSIBLE RESOLUTION STEPS.