logicsatsat-solversdpll

Why is unit-propagation performed first in DPLL algorithm?


enter image description here

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


Solution

  • 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.