--------------------------------------------------------------------------------------------------
Logic in Computer Science, November 5th, 2024. Time: 1h45min. 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 points).

1a) Let F and G be propositional formulas such that G |= F.  Is it true that then always  F |= G  or  F |= -G ?
    Prove your answer as simply as you can using only the definition of propositional logic.

>>> Answer:
    ...
    
1b) Let F, G, H be formulas. Prove that if F v G |= H then F & -H is unsatisfiable,
    using only the definition of propositional logic.

>>> Answer:
    ...


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

Problem 2. (3 points).

Given S a set of clauses (CNF) over n propositional symbols, and Resolution the deductive rule:

                 p v C          -p v D
                 ---------------------      for some symbol p
                         C v D

2a) Is Resolution a correct deductive rule:  (p v C) & (-p v D) |= C v D  for any p, C, D?
    Prove your answer.

>>> Answer:
    ...

2b) Is Resolution a complete deductive rule? Prove your answer.

>>> Answer:
    ...

2c) Explain what it means that Resolution is a refutationally complete deductive rule.

>>> Answer:
    ...


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

Problem 3. (2 points).

Let us remember the Ladder encoding for at-most-one (amo), that is, for expressing in CNF
that at most one of the literals x_1 ... x_n is true, also written x1 + ... + xn <= 1.
It uses new auxiliary variables a_i that mean "some of x_1 ... x_i is true".

3a) Depending on n, how many auxiliary variables a_i will be needed?

>>> Answer:
    ...

3b) Which clauses are generated by this encoding, and, in total, how many there are.

>>> Answer:
    ...


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

Problem 4. (3 points).

4a) UNIQUE-SAT is the problem of determining whether a given set of clauses S has exactly one model.
    Explain very briefly how you would use a SAT solver to decide UNIQUE-SAT.

>>> Answer
    We need at most two calls to the SAT solver:
    ...

4b) Assuming you can use a SAT solver or any other algorithm, explain very briefly what you would do
    and what the computational cost would be and why, to decide the following problem:
    Given a formula F in disjunctive normal form (DNF), decide whether F is a satisfiable

>>> Answer
    ...