Examen Parcial Lògica Informàtica 2014 (2014)

Examen Inglés
Universidad Universidad Politécnica de Cataluña (UPC)
Grado Ingeniería Informática - 3º curso
Asignatura Lògica Informàtica
Año del apunte 2014
Páginas 2
Fecha de subida 16/06/2014
Descargas 4

Descripción

Parcial de primavera 2014, examen i resolució d'aquest

Vista previa del texto

L´ ogica en la Inform´ atica / Logic in Computer Science Tuesday April 22nd, 2014 Time: 1h55min. No books, lecture notes or formula sheets allowed.
1A) Let F and G be two propositional formulas such that F |= G. Is it true that F ≡ F ∧ G? Prove it using only the formal definitions of propositional logic.
Solution: It is true. The proof has two parts: A) Let I be any model of F . We prove that then I |= F ∧ G. If I |= F and F |= G, we have I |= G (by definition of F |= G). Then evalI (F ) = evalI (G) = 1. And then I |= F ∧ G because evalI (F ∧ G) = min(evalI (F ), evalI (G)) = min(1, 1) = 1.
B) Let I be any model of F ∧ G. We prove that then I |= F . I |= F ∧ G implies evalI (F ) = evalI (G) = min(evalI (F ), evalI (G)), which implies that evalI (F ) = evalI (G) = 1 and therefore I |= F .
1B) Given two propositional formulas F and G, is it true that either F |= G or F |= ¬G? Prove it using only the formal definitions of propositional logic.
Solution: It is false. A counterexample is as follows: let F be the formula p and G be the formula q.
Then F |= G: for example, if we define I s.t. I(p) = 1 and I(q) = 0 then we have I |= F but I |= G.
And F |= ¬G: now, if we define I(p) = 1 and I(q) = 1 then again I |= F but I |= ¬G.
2) If S is a set of clauses, let us denote by UP (S) the set of all literals that can be obtained from S by zero or more steps of unit propagation. Imagine you have a C++ program P that does unit propagation in linear time, taking as input any set of clauses S and returning UP (S). Explain your answers to the following questions: 2A): Is it true that l ∈ UP (S) implies S |= l? Solution: Yes, if I is a model of given a clause l ∨ l1 ∨ . . . ∨ ln and unit clauses ¬l1 , . . . ¬ln then also I |= l, since 1 = evalI (l ∨ l1 ∨ . . . ∨ ln ) = max{evalI (l), evalI (l1 ), . . . evalI (ln )} = max{evalI (l), 0 . . . 0} which implies evalI (l) = 1.
2B): Let l be any literal. Is it true that S |= l implies l ∈ UP (S)? Solution: No. Counterexample: if S = {p ∨ q, ¬p ∨ q}, then S |= q but q ∈ / UP (S).
2C): Can you use your program P to decide 2-SAT in polynomial time? Solution: No. The program by itself cannot.
2D): Can you use your program P to decide Horn-SAT in polynomial time? Solution: Yes, because a set of Horn clauses is satisfiable if and only if the output UP (S) of P contains any pair of contradictory literals l and ¬l (see also exercise 25 of “3. Deduccion en Logica Proposicional”): If for some l, we have UP (S) ⊇ {l, ¬l} then by 2A), we have S |= l and S |= ¬l and hence S |= l∧¬l so S is unsatisfiable.
For the reverse implication: if there is no l such that UP (S) ⊇ {l, ¬l}, then S is satisfiable, since it has the model I defined as I(l) = 1 iff l is a unit clause in UP (S). This is true because Horn clauses have at most one positive literal, so there are only two possible kinds of clauses: A) (one positive literal): for evey clause l ∨ C in S, if I |= C then by unit propagation we have l ∈ UP (S) and I |= l ∨ C. and B) (no positive literals): for every clause clause C of the form ¬l1 ∨ . . . ∨ ¬ln in S, if I |= C then I |= li for all i, so li ∈ UP (S). But then by unit propagation also ¬li would belong to UP (S).
3A) Write all clauses needed to express the cardinality constraint x1 + · · · + x6 ≤ 4 without using any auxiliary variables (do not write any unnecessary clauses).
Solution: Of all subsets of 5 at least one is false: ¬x1 ∨ ¬x2 ∨ ¬x3 ∨ ¬x4 ∨ ¬x5 ¬x1 ∨ ¬x2 ∨ ¬x3 ∨ ¬x4 ∨ ¬x6 ¬x1 ∨ ¬x2 ∨ ¬x3 ∨ ¬x5 ∨ ¬x6 ¬x1 ∨ ¬x2 ∨ ¬x4 ∨ ¬x5 ∨ ¬x6 ¬x1 ∨ ¬x3 ∨ ¬x4 ∨ ¬x5 ∨ ¬x6 ¬x2 ∨ ¬x3 ∨ ¬x4 ∨ ¬x5 ∨ ¬x6 3B) Write all clauses needed to express the Pseudo-Boolean constraint 1x + 3y + 4z + 5u + 8v ≥ 14 without using any auxiliary variables (do not write any unnecessary clauses). Hint: write one clause for each (minimal) subset S of the variables such that not all variables of S can be false.
Solution: v, u ∨ z, u ∨ y, z ∨ y ∨ x.
4) We want to use a SAT solver to do factoring: given a natural number n, find two natural numbers p and q with p ≥ 2 and q ≥ 2, such that n = p · q. Of course, the SAT solver will return “unsatisfiable” if and only if n is a prime number. (Curiosity: if we could factor large n, we could break many cryptographic systems!).
4A) Let a and b be bits (propositional variables). Write the seven clauses meeded to express that the two-bit number c d is the result of the sum a+b, that is, c is the “carry” (c = a ∧ b) and d means “exactly one of a, b is 1” (exclusive or: c = xor(a, b)).
Solution: ¬c ∨ a ¬c ∨ b c ∨ ¬a ∨ ¬b ¬d ∨ ¬a ∨ ¬b ¬d ∨ a ∨ b d ∨ a ∨ ¬b d ∨ ¬a ∨ b 4B) Here we will factor numbers n of four bits n3 n2 n1 n0 only, so n ≤ 15. This means that, since we want to find p ≥ 2 and q ≥ 2, we know that p < 8 and q < 8 so for p and for q three bits each are sufficient, which we will call p2 p1 p0 and q2 q1 q0 . Graphically, we can express the multiplication as we would do it “by hand”: p2 p1 p0 q2 q1 q0 x2 x1 x0 y2 y1 y0 0 z2 z1 z0 0 0 0 n3 n2 n1 n0 using 9 intermediate auxiliary variables (called x, y, z, with subindices), where in fact we already know that z2 must be 0. Using these auxiliary variables, and a few other auxiliary variables expressing the “carries” (please call them c∗ ), write here the expressions, like n1 = xor(x1 , y0 ), cardinality constraints, etc., needed to ensure that indeed n = p · q. After that, write the concrete clauses needed for each expression.
Solution: Since x0 = n0 , we can directly define n0 = and(q0 , p0 ). Every and of this kind generates three clauses as we wrote above for c = a ∧ b. We also have: x1 = and(q0 , p1 ), x2 = and(q0 , p2 ), y0 = and(q1 , p0 ), y1 = and(q1 , p1 ), y2 = and(q1 , p2 ), z0 = and(q2 , p0 ), z1 = and(q2 , p1 ).
Since z2 must be 0, we need the clause ¬q2 ∨ ¬p2 .
We need two carry bits: c0 = and(x1 , y0 ), c1 = atleasttwo(c0 , x2 , y1 , z0 ), and also one clause ¬c0 ∨ ¬x2 ∨ ¬y1 ∨ ¬z0 ) (otherwise the sum is too large) and the bits for the result: n1 = xor(x1 , y0 ) (four clauses as above), n2 = odd(c0 , x2 , y1 , z0 ), and n3 = or(c1 , y2 , z1 ). This last sum must give no carry: atmostone(c1 , y2 , z1 ). To encode this into CNF: c1 = atleasttwo(c0 , x2 , y1 , z0 ) can be expressed, e.g., making c1 be the second output bit of a 4-bit sorting network, or with clauses: ¬c0 ∨ ¬x2 ∨ c1 , ¬c0 ∨ ¬y1 ∨ c1 , ... ¬y1 ∨ ¬z0 ∨ c1 , and c0 ∨ x2 ∨ y1 ∨ ¬c1 , c0 ∨ x2 ∨ zo ∨ ¬c1 , c0 ∨ y1 ∨ zo ∨ ¬c1 , x2 ∨ y1 ∨ zo ∨ ¬c1 .
n2 = odd(c0 , x2 , y1 , z0 ) can be expressed by all 16 cases: ¬c0 ∨ ¬x2 ∨ ¬y1 ∨ ¬zo ∨ ¬n2 , ¬c0 ∨ ¬x2 ∨ ¬y1 ∨ zo ∨ n2 , ... c0 ∨ x2 ∨ y1 ∨ zo ∨ ¬n2 .
n3 = or(c1 , y2 , z1 ) can be expressed similarly to a binary or, with clauses: n3 ∨ ¬c1 n3 ∨ ¬y2 n3 ∨ ¬z1 ¬n3 ∨ ¬c1 ∨ ¬y2 ∨ ¬z1 .
...