DPLL Algorithm

Question

In this DPLL algorithm, is that possible to set another value to x0 and x1. 

When i tried, 

{x0, ¬b}, {x0, ¬c}, {b, c, ¬x0} 

{x0, ¬x1}, {x1, ¬a, ¬x0},

 {a, ¬x1} {x1, ¬b}

set x1 = true, 

{x0, ¬b}, {x0, ¬c}, {b, c, ¬x0} 

{x0}

 {a} 

a = true, x0 = true, b = c = true or b = false or c = true

Is that a valid solution ? As per my understanding we should not get anything like {} which will be a conflict. When i gave these values i did not get any conflicts 

Answer 1

That is certain possible in general, and in this example, it also generates a model of the formula. If we compute the BDD of the formula, we can also see all the possible models (but I think you should have written b or c must be true):

Comments

Thanks for the clarification.