-------------------------------------------------------------------------------------------------- Logic in Computer Science, April 1st, 2022. Time: 1h30min. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- -Insert your answers on the dotted lines ... below, and only there. -Do NOT modify the problems or the @nota lines. -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 etc., 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. (4 points). @n@nota1: 1a) Let F and G be propositional formulas such that G |= F. Is it true that then always F |= G or F |= -G ? Prove it as simply as you can using only the definitions of propositional logic. Answer: This is false. Let F be the formula p v -p and let G be the formula p. Then G |= F, because for the only model I of G, the interpretation I where I(p)=1, we have I|=F (in fact, F is a tautology). But F not|= G: if I(p)=0 we have I |= F but I not|= G. And F not|= -G: if I(p)=1 we have I |= F but I not|= -G. 1b) Let F and G be propositional formulas. Is it true that F |= G iff F & -G is unsatisfiable? Prove it using only the definitions of propositional logic. Answer: F |= G iff [by definition of logical consequence] for all I, I not|= F or I |= G iff [by definition of satisfaction] for all I, eval_I(F)=0 or eval_I( G)=1 iff [by property of -] for all I, eval_I(F)=0 or 1-eval_I( G)=0 iff [by definition of eval] for all I, eval_I(F)=0 or eval_I(-G)=0 iff [by definition of min] for all I, min( eval_I(F), eval_I(-G) ) = 0 iff [by definition of eval] for all I, eval_I(F & -G)=0 iff [by definition of satisfaction] for all I, I not|= F & -G iff [by definition of satisfiable] F land -G is unsatisfiable -------------------------------------------------------------------------------------------------- Problem 2. (3 points). @n@nota2: 2a) Explain in a few words why propositional SAT is in NP. Answer: Propositional SAT is the following problem. Input: a propositional formula F. Question: Is F satisfiable? It is in NP because if the answer is "yes" there is a polynomial-size certificate of this fact, a model I, and we can check whether I |= F in polynomial time. 2b) Explain in a few words why 3-SAT is NP-complete. You may assume that SAT is NP-hard. Answer: for 3-SAT to be NP-complete, we need: a) 3-SAT is in NP. For the same reason as a). b) 3-SAT is NP-hard. Because using the (linear) Tseitin transformation we can reduce SAT to 3-SAT: transform any formula F into an equisatisfiable 3-SAT formula. 2c) Let F be an UNsatisfiable propositional formula built over n different predicate symbols. Give the name of some method to express a proof (or certificate) of unsatisfiability (like a model is a certificate of satisfiability). Do you think that every unsatisfiable F has such an unsatisfiability proof of size polynomial in n? Answer: For example, the full backtracking tree of a backtracking-based SAT algorithm is an unsatisfiability certificate. Another example: a resolution proof. For example, if a set of clauses S includes (possibly among many others) the clauses pvq, -pvq, pv-q, -pv-q, a resolution proof of unsatisfiability of S is a tree like this: pvq -pvq pv-q -pv-q --------- ------------ q -q ------------------ [] Resolution proofs are not polynomial: there is no polynomial P such that every unsatisfiable F has a resolution proof of size P(|F|). In fact, it is widely believed (but not known) that no kind of polynomial unsatisfiability certificates exists (i.e, that NP != co-NP and hence P != NP ). -------------------------------------------------------------------------------------------------- Problem 3. (2 points). @n@nota3: Here just give the answer, giving no explanations. Use a^b to denote "a to the power b". 3a) How many Boolean functions with n input bits f: {0,1}^n --> {0,1} are there in terms of n? Answer: 2^(2^n). 3b) Any propositional formula F represents a Boolean function. List the names of the other methods you know to represent Boolean functions. Answer: Boolean circuits, truth tables, BDDs, ... Note: F represents the Boolean function that returns 1 iff its input bits are a model of F. 3c) Is it true that two formulas F and G are logically equivalent iff they represent the same Boolean function? Answer: yes -------------------------------------------------------------------------------------------------- Problem 4. (1 point ). @n@nota4: 4) The published Sudoku puzzles are usually designed in such a way that exactly one solution exists. Explain *very* briefly how you would use a SAT solver to decide if a given Sudoku has exactly one solution. Answer: -Call the SAT solver with input S, the set of the usual clauses for the given Sudoku. -If unsatisfiable, output "no". -If satisfiable with model I, where I(x_1)=0,...,I(x_n)=0, and I(y_1)=1,...,I(y_m)=1, -add to S the clause x_1 v...v x_n v -y_1 v...v -y_m that "forbids" I, and call the solver again: -if satisfiable, output "no" else output "yes". --------------------------------------------------------------------------------------------------