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


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 definition of propositional logic.
>>> Answer:
    ...



--------------------------------------------------------------------------------------------------

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

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

         * If eval_I(l) = 0,
>>> Answer 2b2:
	         HINT: define I', and use the fact that I |= C_i for each i in 1..n.
           ...


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


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


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

    Depending on n, how many clauses are generated in this encoding of AMT(x_1, ..., x_n)?
>>> Answer
    ...


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

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