Chapter 2

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.

Simplify the following boolean expressions: (a) \((x \wedge y) \vee(x \wedge \neg y) \vee(\neg x \wedge y) \vee(\neg x \wedge \neg y)\) (b) \((x \wedge y \wedge z) \vee(x \wedge \neg y \wedge z) \vee(\neg x \wedge y \wedge \neg z) \vee(\neg x \wedge \neg y \wedge z)\) (c) \((x \wedge y \wedge \neg z) \vee(x \wedge \neg y \wedge z) \vee(x \wedge \neg y \wedge \neg z)\)

Find formulas equivalent to the following formulas with all the negations "pushed inward to the proposition letters": (a) \(\neg(p \wedge T)\) (b) \(((p \rightarrow q) \rightarrow r) \rightarrow F\) (c) \(((p \rightarrow q) \rightarrow r) \rightarrow T\) (d) \((p \leftrightarrow q) \leftrightarrow r\) (c) \((p \leftrightarrow q) \leftrightarrow F\) (Hint: Look for a way to simplify this last one.) (Note: The method given to "push negations inward" does not always give the shortest formula that is equivalent to the given formula and has \(\neg\) applied only to proposition letters.)

Find a formula in negation normal form equivalent to the negation of $$ \forall x \exists y((P(x, y) \wedge Q(x, y)) \rightarrow R(x, y)) $$.

Prove that a combinatorial network for $$ (x \wedge y \wedge z) \vee(\neg x \wedge y \wedge z) \vee(x \wedge \neg y \wedge z) \vee(x \wedge y \wedge \neg z) $$ can be simplified to a combinatorial network representing $$ (x \wedge y) \vee(x \wedge z) \vee(y \wedge z) $$

(a) The conjunction of \(n\) formulas \(p_{1}, p_{2}, \ldots, p_{n}\) is defined to be the formula \(\left(\ldots\left(\left(p_{1} \wedge p_{2}\right) \wedge p_{3}\right) \wedge \ldots\right) \wedge p_{n} .\) For \(n=0,\) there is a special case: The conjunction of zero formulas is defined to be \(T\). For \(n=1\), that conjunction simplifies to \(p_{1}\). Let \(\phi\) be the conjunction of \(p_{1}, p_{2}, \ldots, p_{n} .\) Prove that for any interpretation \(I, I(\phi)=T\) if and only if \(I\left(p_{i}\right)=T\) for each \(i\) such that \(1 \leq i \leq n .\) (Hint: Use induction.) (b) Let \(\phi\) be the formula $$ \left(\ldots\left(\left(p_{1} \leftrightarrow p_{2}\right) \leftrightarrow p_{3}\right) \leftrightarrow \ldots\right) \leftrightarrow p_{n} $$ for \(n \geq 1 .\) For what interpretations \(I\) is \(I(\phi)=T ?\) (Hint: The answer involves counting how many of the \(p_{i}\) 's are true in \(I\). Prove the result by induction on \(n\).)

Given an array Values with \(n\) elements Values[0], Values[1],.... Values \([n-1 \mid\) each containing a real number, the following algorithm finds the sum of all the positive values in Values. Write an invariant for the loop. rollingSum \(=0\) for \(i=\phi, 2, \ldots, n-1\) if Values \([t]>0\) rolling Sum \(=\) rollingSum \(+\) Values \([i]\) Output rollingSum.

(a) Show that \((p \vee q)\) is an alphabetic variant of \((q \vee p)\). (b) Show that the relation of being an alphabetic variant is an equivalence relation. (c) Show that if \(\psi\) is an alphabetic variant of \(\phi .\) then \(\phi\) is a tautology (respectively, is satisfiable, is unsatisfiable) if and only if \(\psi\) is a tautology (respectively, is satisfiable, is unsatisfiable). (d) Show that \(\phi\) being an alphabetic variant of \(\psi\) does not imply that \(\phi\) and \(\psi\) are tautologically equivalent.

The first stage of the method described to "push negations inward" was a method to climinate \(\rightarrow\) 's and \(\leftrightarrow\) 's. Prove that in the method to eliminate them, the process of substituting always stops, Consider, for example, the substitution in the formula $$ (p \leftrightarrow q) \leftrightarrow(r \leftrightarrow s) $$ If the substitution is first performed on the second \(\leftrightarrow\), the resultant formula is $$ ((p \leftrightarrow q) \rightarrow(r \leftrightarrow s)) \wedge((r \leftrightarrow s) \rightarrow(p \leftrightarrow q)) $$ which has more \(\leftrightarrow\) 's to replace than in the original formula! At first sight, one might expect that if the substitutions are made in the wrong order, the process might continue generating more \(\leftrightarrow\) 's at each stage, and the process might continue forever. (Hint: One method is to, instead of just counting the number of \(\leftrightarrow\) symbols, put a weight on each \(\leftrightarrow\) symbol, with the weight of the \(\leftrightarrow\) symbol in \(\psi \leftrightarrow x\) being dependent on the number of \(\leftrightarrow\) 's in \(\psi\) and \(\chi\). If the correct method of calculating weights is used, it can be shown that the total weight of the \(\leftrightarrow\) 's decreases with each substitution.

The second stage of the procedure to "push negations inward" started with a formula whose only logical connectives are \(\neg, v,\) and \(\wedge\) and constructed a tautologically equivalent formula with negations applied only to proposition letters. (a) Write an algorithm describing exactly what is done. The algorithm should work on formulas as strings of symbols. To avoid what in this case is irrelevant detail, the program should assume that all proposition letters are one character long and that any symbol encountered, except for \((.), \wedge, v,\) and \(\neg,\) is a proposition letter. Assume that the formula contains no blanks. (It is perhaps easiest to consider the program as a function that is passed the original formula - a string-as a parameter, and then returns the equivalent formula with all the negations pushed inward. It is casiest to use recursion to handle many subformulas.) (b) Prove that your program from part (a) works. (Hint: if your program in part (a) uses recursion to handle subformulas, it is natural to do this proof by induction on formulas. However, the induction may not be straightforward.)