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 {x2} demands the assignment x2 := true, which propagates to the other clauses as follows: 

{x0, ¬b}, {x0, ¬c}, {b, c, ¬x0}
{x0, ¬x1}, {x1, ¬a, ¬x0}, {a, ¬x1}
{x1, ¬b}
-> x0 := true
{b, c} {x1, ¬a}, {a, ¬x1} {x1, ¬b}
-> x1 := true
{b, c}
{a}
->  b := true
{a}

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

(compared to the exam solution: x0 := b := c := x1 := false, a := arbitrary)

Is my solution correct?
in * TF "Emb. Sys. and Rob." by (460 points)

1 Answer

+1 vote
 
Best answer
Yes, I think it is correct. However, in the last step, you should have first assigned a true, since that is a unit clause. Since a propositional logic formula has usually many satisfying assignments, there are typically also many solutions for SAT solving.
by (143k points)
selected by
Imprint | Privacy Policy
...