Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

928 questions

1k answers

1.4k comments

441 users

0 votes

At first, the unit clause {x3} demands the assignment x3 := true, which propagates to the other clauses as follows: 

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

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

{x1, ¬x2, ¬a}, {¬x1, x2}, {x2, a}

{¬x2, c}, {x2, ¬c} 

We now have four clauses with only two literals and an occurrence of x0, so that we make the case split x0 := true (instead of false as per the solution), which yields the following clauses:

{b}, {c} 

{¬x1}

{x1, ¬x2, ¬a}, {¬x1, x2}, {x2, a}

{¬x2, c}, {x2, ¬c}

The new unit clauses {b}, {c} , {¬x1} demand assignments of   b := c:= true and x1 := false. Propagating this yields:

{}, {} 

{}

{¬x2, ¬a}, {x2, a}

{x2}

Do we backtrack here and make x0 := false due to the empty clauses and then continue? 

Proceeding otherwise means x2 := true and the following:

{¬a}

{}

which demands a:= false

The final assignments obtained are x3 := x0 := x2 := b :=c := true and x1 := a := false 

(compared, the exam solution : x3 := x1 := x2 := c := true and x0 := b := false , a:= arbitrary)

in * TF "Emb. Sys. and Rob." by (480 points)
edited by

1 Answer

+1 vote
 
Best answer

When assigning  b := c := true and x1 := false, the clauses {b}, {c},{¬x1} do not become empty clauses, the clauses are just removed. What happens precisely is the unit clause propagation rule. Therefore, the only way to proceed is to assign x2:=true as another unit clause propagation, and the get the model.

Bytheway, looking at the BDD of the clause set shows the possible models you could get:

by (143k points)
selected by
Thank you Professor. So, both these are valid models. Is my understanding correct?
Right, both are satisfying assignments, and each one is as good as the other one.
Imprint | Privacy Policy
...