Question

The length of a clause is the number of literals in the clause. The length of a CNF formula is the sum of the length of its clauses. The number of excess literals in a CNF formula is the length of the formula minus the number of clauses in the formula. (a) Show that if an unsatisfiable set \(S\) of clauses contains only clauses of length 0 and 1 , it has a resolution refutation. (Hint: Prove the following: If \(S\) contains a clause of length 0 , it has [trivially] a resolution refutation. If, for some proposition letter \(p, S\) contains both \(p\) and \(\neg p,\) then \(S\) has a resolution refutation. Otherwise, \(S\) is satisfiable.) (b) Show that if a set \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k} \vee \lambda_{k+1}+\cup S(k \geq 1)\right.\) of clauses is un- satisfiable, so are \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \lambda_{k}\right\\} \cup S\) and \(\left\\{\lambda_{k+1}\right\\} \cup S\). (Hint: For the first half, prove that if an interpretation \(I\) satisfies \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k}\right\\} \cup S,\) it also satisfies \(\left.\left\\{\lambda_{1} \vee \lambda_{2} \vee \cdots \vee \lambda_{k} \vee \lambda_{k+1}\right\\} \cup S_{.}\right)\) (c) Show that for \(k \geq 1,\) the number of excess literals in \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \cdots \vee \lambda_{k}\right\\} \cup S\) and the number of excess literals in \(\left\\{\lambda_{k+1}\right\\} \cup S\) are both less than the number of excess literals in \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k} \vee \lambda_{k+1}\right\\} \cup S\). (d) A resolution derivation of a clause \(r_{k}\) from a set \(S\) of clauses is a sequence \(r_{0}, r_{1}, r_{2}, \ldots, r_{k}\) of clauses where each \(r_{l}\) is either an element of \(S\) or a resolvant of two previous \(r\) 's. (Thus, resolution refutation of \(S\) is just a resolution derivation of \(F\) from \(S .\) ) Show that if there is a resolution derivation of \(\lambda\) from \(S\) and a resolution refutation of \(S \cup\\{\lambda\\},\) then there is a resolution refutation of \(S .\) (e) Prove that if there is a resolution refutation \(\rho\) of \(\left\\{\lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k}\right\\} \cup S,\) then either (i) there is a resolution refutation of \(\left.\mid \lambda_{1} \vee \lambda_{2} \vee \cdots \vee \lambda_{k} \vee \lambda_{k+1}\right\\} \cup S\) or (ii) there is a resolution derivation of \(\lambda_{k+1}\) from \(\lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k} \vee \lambda_{k+1} \cup S\). (Hint: Prove this by induction on the length \(\rho\). You will have to add \(\lambda_{k+1}\) as a disjunct to some of the clauses in \(\rho\). It is not true in general that if \(S \models \lambda\), then there is a resolution derivation of \(\lambda\) from \(S .\) ) (f) Prove that resolution refutation is complete.

Short answer

Resolution refutation is complete for unsatisfiable clause sets.

Step-by-step solution

Understanding Clause Length and Excess Literals

Consider a CNF formula consisting of clauses. Each clause has a certain number of literals, and the length of the formula is the sum of the lengths of all its clauses. The number of excess literals is the length of the formula minus the number of its clauses. Understanding these definitions will help in solving the given problem.

Resolution Refutation for Clauses of Length 0 and 1

Any clause of length 0 (i.e., \(\bot\) or false) in a set of clauses leads to the entire set being unsatisfiable, as there is no interpretation that can satisfy it. If the set contains a clause like \(p\) and its negation \(eg p\), resolution between them produces a null clause (false), leading to unsatisfiability.

Showing Unsatisfiability When a Clause is Split

Given the unsatisfiable CNF formula \( \{ \lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k} \vee \lambda_{k+1} \} \cup S \,\), breaking it into two parts \( (\{ \lambda_{1} \vee \lambda_{2} \vee \ldots \vee \lambda_{k} \} \cup S) \) and \( (\{ \lambda_{k+1} \} \cup S) \) must also be unsatisfiable. Any interpretation that satisfies these parts also satisfies the original clause when combined, proving them unsatisfiable too.

Comparing Excess Literals Between Different Splits

If \(k \geq 1\), the split into \( \{ \lambda_{1} \vee \ldots \vee \lambda_{k} \} \) and \( \{ \lambda_{k+1} \} \) decreases the combined length because you reallocated one literal to a separate clause, reducing excess literals compared to the original set.

Resolution Derivation of a Clause and its Effects

If you can derive a clause \( \lambda\) from a set \( S \,\) and a resolution refutation of \( S \cup\{ \lambda \}\), you perform a sequence of resolutions leading to a false clause within the original set \( S \,\) thus proving \( S \) itself is unsatisfiable by resolution.

Using Induction to Prove Refutation Completeness

Applying induction on the length of the refutation sequence \( \rho\) demonstrates that, given \( \{ \lambda_{1} \vee \ldots \vee \lambda_{k} \} \cup S\), adding \( \lambda_{k+1} \) creates a refutation path ensuring either a larger clause remains unsatisfiable or a derivation occurs for \( \lambda_{k+1} \) demonstrating the completeness of the resolution refutation.

Resolution Refutation Completeness Proof

The completeness of resolution is shown by demonstrating any unsatisfiable CNF can be resolved into a contradiction through finite logical implications, ensuring that resolution refutation can effectively demonstrate unsatisfiability.

Key concepts

Clause Length

In the realm of logic and computing, a clause is a fundamental part of a Boolean formula expressed in Conjunctive Normal Form (CNF). The length of a clause is essentially the count of literals contained within that clause. For instance, if you have a clause like \( p \vee q \vee eg r \), its length is 3, as there are three literals involved.

Similarly, the length of a CNF formula is calculated by adding together the lengths of its constituent clauses. Imagine a formula comprised of several clauses: the formula length would be the total number of literals across all these clauses. The concept of clause length is crucial as it significantly affects the complexity and structure of logical proofs, like resolution refutation.

Excess Literals

The notion of excess literals arises when analyzing CNF formulas. The term 'excess literals' refers to the difference between the total number of literals in the formula and the number of clauses within that formula. In simple terms, you calculate it by subtracting the number of clauses from the total length of the formula.

Let's say you have a formula with a length of 10 and it consists of 4 clauses. The number of excess literals would be \(10 - 4 = 6 \). This metric helps in assessing how the literals are distributed across the clauses. It is particularly useful when determining the potential for simplification and checking unsatisfiability of a formula through resolution refutation.

Unsatisfiability

The concept of unsatisfiability hinges on whether a set of logical clauses can be simultaneously satisfied. A set is considered unsatisfiable if no interpretation of the variables within those clauses makes them all true simultaneously.

Consider a scenario where you have clauses such as \(p \) and \( eg p \). Clearly, there is no possible interpretation that can satisfy both, hence the set is unsatisfiable. When a CNF formula is unsatisfiable, it implies that through logical deductions and operations, we will find contradictions. This unsatisfiability can be systematically verified using methods like resolution refutation, which involves deriving contradictions from the available clauses.

Complete Proof of Resolution Refutation

Resolution refutation is an effective logical method used to demonstrate the unsatisfiability of a CNF formula. It involves using a series of logical operations to derive a contradiction, thus proving that the formula cannot be true under any interpretation.

To achieve a complete proof of resolution refutation, you start by applying resolution steps iteratively. If at any point you produce an empty clause, equivalent to false in logical terms, the original formula is unsatisfiable. This method is 'complete', meaning it is guaranteed to find a contradiction if one exists.

• First, identify a pair of clauses where one contains a literal \(p\) and another contains \(eg p\).
• Use these clauses to generate a new clause that omits \(p\) and \(eg p\).
• Continue resolving until an empty clause is obtained.

Hence, resolution refutation serves as a robust tool for confirming the unsatisfiability of logical formulas.