Question

(b) Using the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, determine whether the following formula is satisfiable. Show each step. [3 marks] (c) Give an example of a conjunctive normal form (CNF) formula where the pure literal rule can be applied, but the unit propagation rule cannot. The formula must have at least 3 clauses. [3 marks

Answer 1

b

Definition 1. The Basic DPLL system consists of the following transition rules: UnitPropagate: l is undefined in M Decide: l or -l occurs in a clause of F l is undefined in M M F Fail: M는-C M contains no decision literals MIF,C fail if Backjump: there is some clause C VI s.t.: if l' is undefined in M or occurs in a clause of F

Here,

a DPLL procedure will be modeled by a transition system: a set of states together with a relation, called the transition relation, over these states. States will be denoted by (possibly subscripted) SS.... A state is either fail or a pair M∥FM∥F, where FF is a finite set of clauses and MM is a sequence of annotated literals.... We will not go into a complete formalization of annotated literals; it suffices to know that some literals ll will be annotated as being decision literals; this fact will be denoted here by writing ldld (roughly, decision literals are the ones that have been added to MM by the Decide rule given below). Most of the time the sequence MM will be simply seen as a set of literals, denoting an assignment, i.e., ignoring both the annotations and the fact that MM is a sequence and not a set.

C.

All of the following formulas in the variables A, B, C, D, E, and F are in conjunctive normal form:

• {\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
• {\displaystyle (A\lor B)\land C}${\displaystyle (A\lor B)\land C}$
• {\displaystyle A\lor B}$A\lor B$
• {\displaystyle A}

The third formula is in conjunctive normal form because it is viewed as a "conjunction" with just one conjunct, namely the clause {\displaystyle A\lor B}$A\lor B$. Incidentally, the last two formulas are also in disjunctive normal form.