This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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).
Citation:
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.