-------------------------------------------------------------------------------------------------- Logic in Computer Science, April 2nd, 2025. Time: 2h00min. 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). 1a) Is it true that for any two propositional formulas F and G, we have that F is a logical consequence of G iff G & -F is unsatisfiable? Prove it using only the definition of propositional logic. >>> Answer: ... G |= F iff [by def. of logical consequence] AI, if I |= G then I |= F iff [by def. of if ... then ...] AI, either not (I |= G) or I |= F iff [by def. |=, and eval_I] AI, either eval_I(G) = 0 or eval_I(F) = 1 iff [by arithmetic] AI, either eval_I(G) = 0 or 1-eval_I(F) = 0 iff [by def. of eval(-)] AI, either eval_I(G) = 0 or eval_I(-F) = 0 iff [by def. of min] AI, min(eval_I(G), eval_I(-F)) = 0 iff [by def. of eval_I(&)] AI, eval_I(G & -F) = 0 iff [by def. of |=] AI, not I |= G & -F iff [by def. of unsatisfiable] G & -F is unsatisfiable 1b) Is it true that for any three propositional formulas F, G, H, we have that F & (G v H) is a tautology iff (-G & H) v -F is unsatisfiable? Prove it using only the deļ¬nition of propositional logic. >>> Answer: ... No. Counter example: Let F be p v -p, let G be p and let H be -p. Then F & (G v H) is the formula (p v -p) & (p v -p) which is a tautology. But (-G & H) v -F is the formula (-p & -p) v -(p v -p), which is satisfiable, because any interpretation I with I(p) = 0 is a model. -------------------------------------------------------------------------------------------------- Problem 2. (2.5 points). We define: - a literal in a formula in CNF is *pure* if it appears either always positive or always negative. - In addition, a clause C is said to be *redundant* if it contains at least one *pure* literal. Prove that, if C' is a *redundant* clause, then {C_1, ..., C_n, C'} is satisfiable if and only if {C_1, ..., C_n} is satisfiable, i.e. they are equisatisfiable. a) {C_1, ..., C_n, C'} is satisfiable ==> {C_1, ..., C_n} is satisfiable: >>> Answer 2a: ... If C_1 & ... & C_n & C' is satisfiable, the same model also satisfies {C_1, ..., C_n}. b) Let's see the reverse implication. {C_1, ..., C_n, C'} is satisfiable <== {C_1, ..., C_n} is satisfiable. Suppose {C_1, ..., C_n} is satisfiable. Then, there exists a model I such that I |= C_i for each i in 1..n. Let's build an interpretation I' that satisfies {C_1, ..., C_n, C'}. Let l be a *pure* literal of C'. We distinguish two cases: * If eval_I(l) = 1, >>> Answer 2b1: ... then eval_I(C') = 1, and I |= {C_1, ..., C_n, C'}. So we can take I' = I. * If eval_I(l) = 0, >>> Answer 2b2: HINT: define I', and use the fact that I |= C_i for each i in 1..n. ... let I' be the interpretation that is exactly equal to I *except* for the predicate symbol l, so that eval_I'(l) = 1. Let's see that I' |= C_i for each i in 1..n. Since I |= C_i then there exists at least one literal l' in C_i such that eval_I(l') = 1. Like eval_I'(l) = 0 and the literal l is *pure*, necessarily l and l' do not have the same propositional symbol. So eval_I'(l') = 1 too, and I' |= C_i. As, for construction, eval_I'(l) = 1, then eval_I'(C') = 1, and therefore I |= {C_1, ..., C_n, C'}. Note: The *redundant* clauses in a CNF can be safely removed in order to determine its satifiablity. -------------------------------------------------------------------------------------------------- Problem 3. (2.5 points). Let: - x be a propositional symbol/variable. - S be a set of clauses defined over propositional variables in the set of symbols P U {x} (with x not in P). - Sp be the subset of S consisting of all those clauses where literal x occurs but -x does not. - Sn be the subset of S consisting of all those clauses where literal -x occurs but x does not. - Sr be the set of all clauses that can be obtained by applying resolution on symbol x (wrt. symbol x) between a clause in Sp and a clause in Sn. Prove that, if Sr is satisfiable (has a model I) then (Sp & Sn) is also satisfiable (have a model I'). Let I: P -> {0, 1} be a model of Sr. 3a) Let us assume that for any clause x v C in Sp we have I |= C. Define the interpretation I' : P U {x} -> {0, 1} as I'(p) = I(p) for p in P, and I'(x) = 0. Prove that I' |= Sp and I' |= Sn. >>> Answer: ... Any clause of Sp is of the form x v C, with C defined over P. By hypothesis I |= C, so I |= x v C. Hence I' |= Sp. Any clause of Sn is of the form -x v D, with D defined over P. Since I'(x) = 0, we have I' |= -x v D. Hence I' |= Sn. 3b) Let us assume that there is a clause x v C in Sp such that not(I |= C). Define the interpretation I' : P U {x} -> {0, 1} as I'(p) = I(p) for p in P, and I'(x) = 1. Prove that I' |= Sp and I' |= Sn. >>> Answer: ... Any clause of Sp is of the form x v C, with C defined over P. Since I'(x) = 1, we have I' |= x v C. Hence I' |= Sp. Any clause of Sn is of the form -x v D, with D defined over P. By applying resolution with clause x v C we get clause C v D, which belongs to Sr. By hypothesis I |= Sr. In particular, I |= C v D. But we have that not(I |= C). So it must be I |= D, which implies I' |= D. Hence I' |= Sn. Note: this is part of the proof of refutational completeness of resolution. It gives a *constructive* way of defining a model for a set of clauses S such that the empty clause is not in the closure by resolution of S, Res(S). -------------------------------------------------------------------------------------------------- Problem 4. (2.5 points). Encodings of cardinality constraints x_1 + ... + x_n <= K, for K=2 (AMT(x_1, ..., x_n)) 4a) Write the clauses needed for expressing x1+x2+x3+x4 <= 2 without using auxiliary variables. >>> Answer ... -x1 v -x2 v -x3 -x1 v -x2 v -x4 -x1 v -x3 v -x4 -x2 v -x3 v -x4 Depending on n, how many clauses are generated in this encoding of AMT(x_1, ..., x_n)? >>> Answer ... The number of clauses is equal to the binomial coeficient C(n,K+1) 4b) Which auxiliary variables are needed, and which clauses are generated for expressing x1+x2+x3+x4 <= 2 using the ladder encoding of AMT. >>> Answer ... Variables: x1 x2 x3 x4 Auxiliary 'a' vars: a1 a2 a3 a4 Auxiliary 'b' vars: b1 b2 b3 b4 Clauses: x1 -> a1 -x1 v a1 a1 -> a2 -a1 v a2 b1 -> b2 -b1 v b2 a1 & x2 -> b2 -a1 v -x2 v b2 b1 -> -x2 -b1 v -x2 x2 -> a2 -x2 v a2 a2 -> a3 -a2 v a3 b2 -> b3 -b2 v b3 a2 & x3 -> b3 -a2 v -x3 v b3 b2 -> -x3 -b2 v -x3 x3 -> a3 -x3 v a3 a3 -> a4 -a3 v a4 b3 -> b4 -b3 v b4 a3 & x4 -> b4 -a3 v -x4 v b4 b3 -> -x4 -b3 v -x4 x4 -> a4 -x4 v a_4 Depending on n, how many auxiliary variables are needed, and how many clauses are generated using the ladder encoding of AMT(x_1, ..., x_n)? >>> Answer ... 2n auxiliary variables 5n-4 clauses