This Article 
 Bibliographic References 
 Add to: 
Solving Satisfiability with Less Searching
April 1984 (vol. 6 no. 4)
pp. 510-513
Paul W. Purdom, Department of Computer Science, Indiana University, Bloomington, IN 47405.
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. When this occurs, knowledge that the first subtree does not have a solution can be used to reduce the searching in the second subtree. Only the part of the second subtree which is different from the first needs to be searched. The pure literal rule 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).
Paul W. Purdom, "Solving Satisfiability with Less Searching," IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 6, no. 4, pp. 510-513, April 1984, doi:10.1109/TPAMI.1984.4767555
Usage of this product signifies your acceptance of the Terms of Use.