-------------------------------------------------------------------------------------------------- Logic in Computer Science, Juny 15th, 2023. Time: 2h30min. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- Note on evaluation: eval(propositional logic) = max(eval(Problems 1,2,3), eval(midterm exam)) eval(first-order logic) = eval(Problems 4,5,6). - Insert your answers on the dotted lines ... below, and only there. - Do NOT modify the problems - 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, like in: I |= p & (q v -r) (the interpretation I satisfies the formula p & (q v -r) ). You can write subindices using "_". For example write x_i to denote x-sub-i. -------------------------------------------------------------------------------------------------- Problem 1. (3 points). For each one of the following statements, indicate if it is true or false for propositional logic. Answer T (true) or F (false) on each dotted line ... Give no explanations why. Below always F,G,H are formulas and I is an interpretation. Note: Wrong answers subtract 0.4 points. Unanswered questions subtract 0.2 points. Answer: 1) ... It is decidable in polynomial time whether a given formula is a tautology. 2) ... If F is unsatisfiable, then for every G we have F |= G. 3) ... The Tseitin transformation can be used for reducing SAT to 3-SAT. 4) ... The formula p is a logical consequence of (p v r) & (-q v r) & (q v r). 5) ... Given a formula F, the Tseitin transformation of F always has a number of clauses that is linear in the size of F. 6) ... If F is tautology, then -F |= F. 7) ... There are infinitely many different formulas that are not logically equivalent, even if there is only one predicate symbol. 8) ... F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. 9) ... If there are n propositional symbols, there are 2^(2n) (2 to the power 2n) different clauses. 10) ... Given I and F, it is decidable in linear time whether I |= F. 11) ... If F v G |= H then F & -H is unsatisfiable. 12) ... The closure under resolution Res(S) of a finite set of clauses S is always a finite set of clauses. 13) ... If F is a tautology, then for every G we have G |= F. 14) ... It is decidable in polynomial time whether a given formula in DNF is satisfiable. 15) ... Given a formula F, the Tseitin transformation of F is a set of clauses that is logically equivalent to F. 16) ... The formula (p v q) & (-p v q) & (-p v -q) & (-q v p) is unsatisfiable. 17) ... Given a set of Horn clauses S, we can find in linear time a minimal model I of S, that is, a model I with the minimal |{ p | I(p)=1 }|. 18) ... There are infinitely many different formulas, even if there is only one predicate symbol. -------------------------------------------------------------------------------------------------- Problem 2. (4 points). 2a) My friend John says that he has found a new way to speed up SAT solving. Before starting his SAT solver, he removes from the set of clauses S some clauses he calls "unnecessary": A: if there is some variable x that appears only in positive literals of clauses of S, then he removes from S all clauses containing x. B: similarly, if some variable y appears in S only in negative literals then he removes from S all clauses containing y. Note that after eliminating some "unnecessary" clauses, step A or B may be (or become) applicable for other variables, so John continues doing this until no more variables of type A or B exist and then launches his solver on a (hopefully) much smaller set of clauses. Is John's idea correct? Explain why (in approximately 50 words). Answer: ... 2b) Given two clauses C, D, in what follows we will denote the resolution of C and D by Res(C, D). Given a set of clauses S and a clause C, a literal l in C *blocks* C with respect to S if for each clause C' in S with -l in C', the conclusion (resolvent) Res(C, C') is a tautology We can identify the *blocked* clauses and remove them from the initial set of clauses S while preserving satisfiability. So we need to prove the following result: if clause C in S is blocked by l with respect to S, and S - {C} is satisfiable, then so is S. Beginning of the prove: Let I be such that I |= S - {C}. If I |= C then S is obviously satisfiable. So let us assume that not(I |= C). Define I' so that I'(l) = 1 - I(l), I'(l') = I(l') if var(l') != var(l). Since l in C and not(I |= C), it must be I(l) = 0. So I'(l) = 1 - I(l) = 1 and I' |= C. In what follows we will prove that I' |= S - {C}. To that end, let us consider C' in S, C' != C. We want to prove that I' |= C'. Complete the prove: ... -------------------------------------------------------------------------------------------------- Problem 3. (3 points). Consider the following decision problem, called "MaxSAT": Input: A natural number k and a set S of n propositional clauses {C_1,...,C_n} over propositional symbols P. Question: Is there any interpretation I: P -> {0, 1} that satisfies at least k clauses of S? 3a) Do you think that MaxSAT is polynomial? NP-complete? Exponential? Why? Answer: ... 3b) How would you use a SAT solver to decide it? Hint: use new auxiliary variables x1,...,xn. Answer: ... -------------------------------------------------------------------------------------------------- _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 4. (4 points). 4a) Let F be the FOLE formula: Ez p(z) & Ax (p(x) -> Ey (-p(y) & x=f(y,y))) - Let I be the interpretation with domain D_I = R (the real numbers), and p_I(x) = 1 iff x > 0 f_I(x,y) = x·y (the product in R) Do we have I |= F? Prove it informally Answer: ... - If I' |= F, how many elements has at least I'? Prove it. Answer: ... 4b) Let F and G be the FOL formulas: F = Ax p(a,x) & Ey -q(y) G = Ez Eu (-q(u) & p(z,a)) Do we have F |= G? Prove it. Answer: ... ------------------------------------------------------------------------------------ Problem 5. (3 points). An injective function is a function f that maps distinct elements of its domain to distinct elements in the codomain; that is, f(x1) = f(x2) implies x1 = x2. An exhaustive/surjective function is a function f such that every element of the function's codomain is the image of at least one element of its domain. Consider the following formula of FOLE: ( A x E y (x = f(y))) & - ( Ax Ay (f(x) = f(y) -> x = y) ) 5a) Prove that it is satisfiable by giving a model with domain N (the natural numbers). Answer: ... 5b) Is there any model with a finite domain? Why? Answer: ... ------------------------------------------------------------------------------------ Problem 6. (4 points). A *unital magma* is a set S equipped with a binary operation p: S x S -> S satisfying that there exists an element e in S such that for every element x in S, the equalities equal(p(e, x), x) and equal(p(x, e), x) hold. This element is called the identity element. Prove in **FOL** that the identity element is unique. Use that equality is transitive and symmetric. NOTE: Here the "equal" predicate is a "standard" predicate of FOL, NOT the "built-in" predicate of FOLE. Hint: write formulas A,B,... and U (where U expresses "the identity element e is unique"), and prove with resolution that A & B & ... |= U. Answer: ... ------------------------------------------------------------------------------------