--------------------------------------------------------------------------------------------------
Logic in Computer Science, April 7th, 2026. Time: 2h. 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).

Consider the following statement. For all propositional formulas F, G, H,
     (F -> G) & (H -> G) is satisfiable  iff  -G |= -F & -H.
Use only the definitions of propositional logic in the following subexercises.

1a) Is the ==> implication of this iff statement true?

>>> Answer 1a):
    ...

1b) Is the <== implication of this iff statement true?

>>> Answer 1b):
    ...


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

Problem 2. (2.5 points).

Let P be a set of propositional predicate symbols.
Let S be a set of clauses over P and let N be a subset of P.
We define  flip(N, S)  to be the set of clauses obtained from S by flipping
(changing the sign) of all literals with symbols in N.

For example, if N = {p,q}:
   flip( {p,q}, {p v -q v -r, q v r} )   is   {-p v q v -r, -q v r}.
   
A clause is called Horn if it has at most one positive literal.
A set of clauses S is called *renamable Horn* if there is some N subset of P
such that flip(N, S) is a set of Horn clauses.

2a) Explain in three lines: given S and N such that flip(N, S) is a set of Horn clauses,
    what would you do to efficiently decide whether S is satisfiable, and why?
    What is the cost of your algorithm?

>>> Answer 2a):
    ...

2b) Given an arbitrary set of clauses S, we want to decide whether it is *renamable Horn*,
    and, if so, find the corresponding N.

    We will do this using an algorithm based on... SAT!
    For each p in P, we introduce a SAT variable flipped(p) meaning that "symbol p is in N".
    Then we add clauses for every clause C of S and every pair of literals l and l' in C,
    forbidding that after doing all flips, l and l' both *become positive* in the clause C.
    
    For every pair of literals l and l' appearing in the same clause of S, we add one clause
    depending on whether l and l' are positive or negative.
    Explain in three lines: which clauses do you need, what is the cost of the
    resulting SAT-based algorithm and why?

>>> Answer 2b):
    ...


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

Problem 3. (2.5 points).

Consider the following particular case of the resolution rule, ResUnit (unitary resolution):
                   p       -p v C
                   --------------
                         C
where p is a propositional symbol (which appears positive in the unitary clause on the left).

Complete the following proof that shows that unitary resolution is refutationally
complete for Horn clauses, i.e., if a set of Horn clauses S is unsatisfiable then [] in ResUnit(S).

By contrapositive, it is sufficient to see that if [] is not in ResUnit(S), then ResUnit(S)
(and therefore S, since ResUnit(S) includes S) has a model I, that is, S is satisfiable.

Define I as I(p) = 1 if and only if p is a (single literal) clause in ResUnit(S),
and prove that I |= ResUnit(S) by induction on the number of literals of the clauses.

Now we will show that I |= Resunit(S). For this it is enough to prove that I |= C
for every clause C in ResUnit(S).
We do this by induction on |C|, the number of literals of C.

>>> Answer 3):
    ...


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

Problem 4. (2.5 points).

Using the Tseitin transformation, we can transform an arbitrary propositional formula F
into a set of clauses T(F) (a CNF with auxiliary variables) that is equisatisfiable:
F is SAT iff T(F) is SAT. Moreover, the size of T(F) is linear in the size of F.

4a) Is there any transformation T' into an equisatisfiable linear-size DNF?
    If yes, which one? If not, why?

>>> Answer 4a):
    ...

4b) Is there any similar transformation T'' into a linear-size DNF, such that
    F is a tautology iff T′'(F) is a tautology? If yes, which one? If not, why?

>>> Answer 4b):
    ...