-------------------------------------------------------------------------------------------------- Logic in Computer Science, April 7th, 2026. Time: 2h. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- - Insert your answers on the dotted lines ... below, and only there. - When finished, upload this file with the same name: exam.txt - Use the text symbols: & v - -> |= A E === for AND OR NOT IMPLIES "SATISFIES" FORALL EXISTS LOGICAL EQUIV., etc like in: I |= p & (q v -r) (the interpretation I satisfies the formula p & (q v -r) ). You can write not (I |= F) to express "I does not satisfy F", or not (F |= G) to express "G is not a logical consequence of F" Also you can use subindices with "_". For example write x_i to denote x-sub-i. -------------------------------------------------------------------------------------------------- Problem 1. (2.5 points). Consider the following statement. For all propositional formulas F, G, H, (F -> G) & (H -> G) is satisfiable iff -G |= -F & -H. Use only the definitions of propositional logic in the following subexercises. 1a) Is the ==> implication of this iff statement true? >>> Answer 1a): ... It is not true. Counterexample: Let F = G = p and H = q. Then (F -> G) & (H -> G) is satisfiable (any interpretation where p is true is a model), but not (-G |= -F & -H): if I(p) = 0 and I(q) = 1 then I |= -G but not (I |= -F & -H). 1b) Is the <== implication of this iff statement true? >>> Answer 1b): ... It is true. -G |= -F & -H implies [by def. of logical consequence] AI, if I is a model of -G then I is a model of -F & - G implies [by definition of model] AI, if (I |= -G) then I |= -F & -H implies [by definition of if-then] AI, either not (I |= -G) or I |= -F & -H implies [by def of |=] AI, either eval_I(-G) = 0 or eval_I(-F & -H) = 1 implies [by def of eval_I(-), eval_I(&)] AI, either 1-eval_I(G) = 0 or min(eval_I(-F), eval_I(-H)) = 1 implies [by def of eval_I and min] AI, either eval_I(G) = 1 or eval_I(-F) = eval_I(-H) = 1 implies [by def of max] AI, max(eval_I(-F), eval_I(G)) = 1 and max(eval_I(-H), eval_I(G)) = 1 implies [by def of eval_I(v)] AI, eval_I(-F v G) = 1 and eval_I(-H v G) = 1 implies [by def of min] AI, min(eval_I(-F v G), eval_I(-H v G)) = 1 implies [by def of eval_I(&)] AI, eval_I((-F v G) & (-H v G)) = 1 implies [by def of ->] AI, eval_I((F -> G) & (H -> G)) = 1 implies [by def of |=] AI, I |= (F -> G) & (H -> G) implies [by def of model] AI, I is a model of (F -> G) & (H -> G) implies [by def of tautology] (F -> G) & (H -> G) is a tautology, so it is satisfiable. -------------------------------------------------------------------------------------------------- Problem 2. (2.5 points). Let P be a set of propositional predicate symbols. Let S be a set of clauses over P and let N be a subset of P. We define flip(N, S) to be the set of clauses obtained from S by flipping (changing the sign) of all literals with symbols in N. For example, if N = {p,q}: flip( {p,q}, {p v -q v -r, q v r} ) is {-p v q v -r, -q v r}. A clause is called Horn if it has at most one positive literal. A set of clauses S is called *renamable Horn* if there is some N subset of P such that flip(N, S) is a set of Horn clauses. 2a) Explain in three lines: given S and N such that flip(N, S) is a set of Horn clauses, what would you do to efficiently decide whether S is satisfiable, and why? What is the cost of your algorithm? >>> Answer 2a): ... One can compute flip(N, S) and apply on it the well-known algorithm based on unit resolution for deciding the satisfiability of a set of Horn clauses. The cost is linear: computing flip(N, S) is linear, and deciding if it is satisfiable is linear too. S and flip(N, S) are equi-satisfiable because it is Horn. S and flip(N, S) are equi-satisfiable because if I is a model of one of them, then I′ is a model of the other one, where I′(p) = I(p) iff p not in N. 2b) Given an arbitrary set of clauses S, we want to decide whether it is *renamable Horn*, and, if so, find the corresponding N. We will do this using an algorithm based on... SAT! For each p in P, we introduce a SAT variable flipped(p) meaning that "symbol p is in N". Then we add clauses for every clause C of S and every pair of literals l and l' in C, forbidding that after doing all flips, l and l' both *become positive* in the clause C. For every pair of literals l and l' appearing in the same clause of S, we add one clause depending on whether l and l' are positive or negative. Explain in three lines: which clauses do you need, what is the cost of the resulting SAT-based algorithm and why? >>> Answer 2b): ... a) if both l and l' are positive symbols p and q then we add the clause: flipped(p) v flipped(q) b) if both are negative, of the form -p and -q, then we add: -flipped(p) v -flipped(q) c) otherwise they are of the form -p and q, and we add: -flipped(p) v flipped(q) This gives a quadratic number of 2-SAT clauses, so using the linear 2-SAT algorithm we get a quadratic algorithm for deciding whether S is *renamable Horn* and, if so, finding the corresponding N. -------------------------------------------------------------------------------------------------- Problem 3. (2.5 points). Consider the following particular case of the resolution rule, ResUnit (unitary resolution): p -p v C -------------- C where p is a propositional symbol (which appears positive in the unitary clause on the left). Complete the following proof that shows that unitary resolution is refutationally complete for Horn clauses, i.e., if a set of Horn clauses S is unsatisfiable then [] in ResUnit(S). By contrapositive, it is sufficient to see that if [] is not in ResUnit(S), then ResUnit(S) (and therefore S, since ResUnit(S) includes S) has a model I, that is, S is satisfiable. Define I as I(p) = 1 if and only if p is a (single literal) clause in ResUnit(S), and prove that I |= ResUnit(S) by induction on the number of literals of the clauses. Now we will show that I |= Resunit(S). For this it is enough to prove that I |= C for every clause C in ResUnit(S). We do this by induction on |C|, the number of literals of C. >>> Answer 3): ... Base case: |C| = 0. Clearly I |= C for any clause C in Res(S) of zero literals, since that [] does not belong to ResUnit(S). Induction step: |C| > 0. If C is a clause of a single positive literal p, we have that I |= C by definition of I. Otherwise, dealing with Horn clauses, C must necessarily contain some negative literal, that is, C is of the form -p v C'. * If I(p) = 0, we have that I |= C. * If I(p) = 1, this is because there is a unitary clause p in ResUnit(S) (by the way we have defined I). But then, as we have -p v C' belongs to ResUnit(S) and p in ResUnit(S), we have that C' belongs to ResUnit(S). Since |C'| = |C| - 1, by induction hypothesis we have that I |= C', which implies I |= C. -------------------------------------------------------------------------------------------------- Problem 4. (2.5 points). Using the Tseitin transformation, we can transform an arbitrary propositional formula F into a set of clauses T(F) (a CNF with auxiliary variables) that is equisatisfiable: F is SAT iff T(F) is SAT. Moreover, the size of T(F) is linear in the size of F. 4a) Is there any transformation T' into an equisatisfiable linear-size DNF? If yes, which one? If not, why? >>> Answer 4a): ... No (unless P = NP). If such a similar transformation existed, then we could solve an NP-complete problem (is F SAT?) by transforming F in linear time into the DNF T'(F), and then deciding whether the DNF T'(F) is satisfiable (which, as we know, can be done in linear time for DNFs). 4b) Is there any similar transformation T'' into a linear-size DNF, such that F is a tautology iff T′'(F) is a tautology? If yes, which one? If not, why? >>> Answer 4b): ... Yes. F is a tautology iff -F is unsatisfiable iff the normal Tseitin transformation T(-F) is unsatisfiable iff -T(-F) is a tautology. And indeed -T(-F) can be easily transformed into a DNF: T(-F) is a conjunction of clauses C1 & ... & Cn. Its negation -(C1 & ... & Cn) is equivalent to -C1 v ... v -Cn, and each -Ci is of the form -(l1 v ... v lm) which is equivalent to -l1 & ... & -lm. Note that, unlike what happened in the previous case, here we transform an NP-complete problem into another NP-complete problem.