# Parcial LI (2014)

Apunte EspañolUniversidad | Universidad Politécnica de Cataluña (UPC) |

Grado | Ingeniería Informática - 3º curso |

Asignatura | LI |

Año del apunte | 2014 |

Páginas | 2 |

Fecha de subida | 06/12/2014 |

Descargas | 2 |

Subido por | gbaiona |

### 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 .

Powered by TCPDF (www.tcpdf.org)
...