Question

This problem investigates resolution, a method for proving the unsatisfiability of cnf-formulas. Let $\varphi =C_1\wedge C_2\wedge \dots \wedge C_m$be a formula in cnf, where the $C_i$are its clauses. Let $C=\left\{C_i\left|C_i \mathrm{is} \mathrm{a} \mathrm{clause} \mathrm{of} \varphi \right.\right\}$. In a resolution step, we take two clauses $C_a$and $C_b$in C, which both have some variable occurring positively in one of the clauses and negatively in the other. Thus, $C_a=\left(x\vee y_1\vee y_2\vee \dots \vee y_k\right)$and $C_b=\left(\overline{x}\vee z_1\vee z_2\vee \dots \vee z_l\right)$, where the and are literals. We form the new clause $\left(y_1\vee y_2\vee \dots \vee y_k\vee z_1\vee z_2\vee \dots \vee z_l\right)$and remove repeated literals. Add this new clause to C. Repeat the resolution steps until no additional clauses can be obtained. If the empty clause ( ) is in C, then declare $\varphi$unsatisfiable. Say that resolution is sound if it never declares satisfiable formulas to be unsatisfiable. Say that resolution is complete if all unsatisfiable formulas are declared to be unsatisfiable.

a. Show that resolution is sound and complete.

b. Use part (a) to show that $2SAT\in P$.

Short answer

1. It can be shown that the resolution is sound and complete.

Step-by-step solution

Explain the problem resolution.

Consider the cnf-formula $\varphi =C_1\wedge C_2\wedge \dots \wedge C_m$, where its clauses are referred as $C_i$. Consider that role="math" localid="1663224346961" $C=\left\{C_i\left|C_i \mathrm{is} \mathrm{a} \mathrm{clause} \mathrm{of} \varphi \right.\right\}$, take the two clauses which have some variable x occurring positively in one of the clauses and negatively in the other, where $C_a=\left(x\vee y_1\vee y_2\vee \dots \vee y_k\right)$and$C_b=\left(\overline{x}\vee z_1\vee z_2\vee \dots \vee z_l\right)$. Form the new clause, $\left(y_1\vee y_2\vee \dots \vee y_k\vee z_1\vee z_2\vee \dots \vee z_l\right)$and remove the repeated literals. Add the new clause to C and repeat the resolution step until no additional clauses are obtained.

Explain unsatisfiability

If a Boolean formula is not satisfied for the given values, then the formula is said to be unsatisfiable.

Show that resolution is sound and complete.

a)

Consider the clause H, $H=H_1\backslash \left\{L\right\}\cup C_2\backslash \left\{\neg L\right\}$. If a clause H is produced by the application of the resolution rule under the valuation of Q, then from the hypothesis of the rule $H_1\wedge H_2$, is false.

Assume that H is false under Q to prove the above lemma. The conjunction hypothesis $H_1\wedge H_2$gives the true value under Q. $H_1$gives the disjunction behaviour, then one of its literals will be true under Q.

The literals in H, other than L exists and the H shows true and it is a contradiction. If literal L is taken and then$\neg L$is false under Q.

Under Q, $H_2$is true and it consist of literals other than $\neg L$. This proves that it exists in H and shows true nature in Q. This is in contradiction.

Thus, $H_1\wedge H_2$is false under Q. By induction, it has been shown that a satisfiable formula can never be declared as unsatisfiable.

Therefore, it has been shown that the resolutionis sound.

By using induction, prove the complete property of the resolution as follows:

Consider that the excess number of literals has been defined as follows,

$excess\left(H\right)=\left\{0 \mathrm{if} \left|H\right|<2 \mathrm{and}\left|H\right|-1 \mathrm{if} \left|H\right|>2\right\}$

In every clause, the number of excess literals in a clause set is the sum of excess literals as follows,

$excess\left(H\right)=\sum _{i=1}^{n}excess\left(H_i\right)$

Therefore, by applying induction, the resolutionis complete.