= Unit propagation
If all but one <literal> of a <Boolean clause> are false under a partial <Boolean valuation>, the remaining <literal> must be true in any extension satisfying the clause. Repeatedly make such forced assignments, remove satisfied <Boolean clauses> and remove false <literals> from the others. An empty <Boolean clause> proves that the current partial <Boolean valuation> has no satisfying extension. This is sound because every step is forced by an original or already implied <Boolean clause>; it is not by itself a complete <SAT> decision procedure.
Back to article page
