Why is unit-propagation performed first in DPLL algorithm?

Question

Why is the pure-literal rule performed after the unit propagation and not before?

Because it can give rise to more elements in _I_. – alias Apr 17 '22 at 19:26 — alias, Apr 17 '22 at 19:26
@alias can you clarify what you mean with an example? – Ronald Apr 17 '22 at 20:08 — Ronald, Apr 17 '22 at 20:08
What Kyle said in his answer, essentially. – alias Apr 17 '22 at 22:17 — alias, Apr 17 '22 at 22:17

score 2 · Accepted Answer · answered Apr 17 '22 at 21:43

Unit propagation is done first because it might produce pure literals. DPLL might then recurse on the variables associated with these literals, wasting potentially exponential time uselessly backtracking over them in the future. By eliminating pure literals after unit propagation the function is assured of recursing on a variable whose value legitimately might be either TRUE or FALSE. A pure literal can always be immediately set to TRUE.

Why is unit-propagation performed first in DPLL algorithm?

1 Answers1