Actually, the third clause is (x2 + x3 + x4'), and we haven't assigned x3
yet, so it's not actually conflicting. But after assigning x4=1, deduce()
will either try to set x3=0 and get a conflict with clause 3, or it will
try to set x3=1 and get a conflict with clause 1. (Exactly which case
happens depends on the order deduce() looks at the clauses. If it goes
through them from first to last, then it will set x3=0 because the unit
literal rule will apply in clause 1, and then reach a conflict in clause
3.) Either interpretation is correct, and in any case it's going to return
CONFLICT immediately anyways. So, I guess you could pencil in either x3=0
or x3=1 underneath the x4=1 if you wanted.
Alexander
Post by Steve C, C = CoolNo because once X1=0, X2=0 and X4=1, a conflict exists in clause number 3.
The conflict rule then kicks in and the program backtracks. Assignment of X3
won't happen because the program won't care as long as an UNSAT clause
exists.