Unit clause propagation variable from 4 to 3

Question

How many variables are assigned in the formula below in an exhaustive application of the 'unit clause' rule from the DPLL SAT-solving algorithm?

Recall that the rule can propagate, i.e., after cleaning up after one application, a new application may be possible.

𝐹=(𝑥1)∧(¬𝑥1∨𝑥2)∧(𝑥2∨𝑥3)∧(¬𝑥2∨𝑥4)

I can so far get to 4, but how can I get it to 3?

Answer 1

Initially

F = (x1)∧(¬x1∨x2)∧(x2∨x3)∧(¬x2∨x4)

The first unit clause yields the first assignment x1=T.

After substituting that

F = (x2)∧(x2∨x3)∧(¬x2∨x4)

The new unit clause yields the second assignment x2=T.

After substituting that

F = (T∨x3)∧(x4)

The new unit clause yields the third assignment x4=T.

After substituting that

F = (T∨x3)

There is no assignment to x3, because F is satisfied with any value for x3.