zbMATH — the first resource for mathematics

Solving satisfiability with less searching. (English) Zbl 0545.68052
A new technique, complement searching, is given for reducing the amount of searching required to solve satisfiability (constraint satisfaction) problems. Search trees for these problems often contain subtrees that have approximately the same shape. Knowledge that the first subtree does not have a solution can be used to reduce the searching in the second subtree. The pure literal of the Davis-Putnam procedure is a special case of complement searching. The new technique greatly reduces the amount of searching required to solve conjunctive normal form predicates that contain almost pure literals (literals with a small number of occurrences).

68P10 Searching and sorting
Full Text: DOI