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.