Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP21111

PAGE 2 OF 4

1.

a) Apply the splitting algorithm to check whether the following formula is satisfiable.

¬(q → r) → ¬p ↔ (p → r) ∧ q ∧ p

Split on the variable p first. Show the splitting tree. (6 marks)

b) Convert the formula ¬((p → (q ∧ ¬r)) ↔ ¬q) into clausal normal form using the defini-tional clausal form transformation. (6 marks)

c) Explain briefly how to check validity and equivalence of propositional formulas using a procedure for checking satisfiability. (2 marks)

d) Let A be a propositional formula over variables p1, . . . , pn−1. What is the number of models of the formula pn ↔ A? Explain your answer. (3 marks)

e) Explain how to extend a branch in the tableau for the following formulas. (3 marks)

1. (A → B) = 1

2. (A → B) = 0

2.

a) Consider the process of generating random clauses over n variables as was described in the lectures.

What is the probability of generating the clause: p1 ∨ ¬p2 ∨ p3 ? Briefly explain your answer. (2 marks)

b) Present the GSAT algorithm for propositional satisfiability as a pseudo-code. (4 marks)

c) Integrate the OBDD for the formula q ∨ p → q into the OBDD below and mark the corresponding node as (G). (4 marks)

Apply conjunction and disjunction algorithms for OBDDs to nodes (G) and (F). Draw the resulting OBDD and indicate nodes corresponding to conjunction (G)∧(F) and disjunction (G) ∨ (F). (4 marks)

d) Based on an OBDD representation of a formula F, in each of the following cases explain how to check that F is:

i. valid;

ii. satisfiable;

iii. equivalent to a formula G represented in the same OBDD structure.                                   (3 marks)

e) A variable x in propositional logic of finite domains (PLDF) has the domain {u, v, h}. Translate the following PLFD formula into a formula in propositional logic:

¬(x = v ∨ x = u ↔ x = h).                         (3 marks)

3.

a) Consider the following QBF formula in CNF (7 marks)

Evaluate this formula using the DPLL algorithm. Show all steps of the algorithm. Is this formula true or false?

b) The following picture describes the semantics of the temporal operator :

Draw pictures describing the semantics of temporal operators  and U. (3 marks)

c) In each case below state whether the equivalence holds or does not hold. Briefly explain your answers.

d) Consider a transition system with the state transition graph shown below.

i Write down 1) the set of all states reachable from the inital state and 2) a symbolic representation of this set. (2 marks)

ii Write down 1) the set of all single step transitions starting from the initial state and 2) a symbolic representation of this transition set. (2 marks)