The DPLL algorithm constructs a decision tree in order to determine if a given propositional formula is satisfiable. For example consider the decision tree presented in the lecture notes with 6 leaves for the simple formula 

Your task is to construct a decision tree for the following propositional formula by applying the DPLL algorithm:

,

How many leaves the your decision tree have?

Important:

• Always apply Boolean Constraint Propagation (BCP) as soon as possible.

• When a decision is necessary, choose variables in alphabetical order: for example, split on variable a before b, b before c, etc.