home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / theory / 1783 < prev    next >
Encoding:
Internet Message Format  |  1992-08-19  |  1.3 KB
  1. Path: sparky!uunet!charon.amdahl.com!pacbell.com!mips!darwin.sura.net!Sirius.dfn.de!zrz.tu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!corton!loria!loria.crin.fr!eker
  2. From: eker@loria.crin.fr (Steven Eker)
  3. Newsgroups: comp.theory
  4. Subject: Re: boolean satisfiability problem
  5. Message-ID: <445@muller.loria.fr>
  6. Date: 19 Aug 92 17:25:05 GMT
  7. References: <Bt5Mz6.3xs@research.canon.oz.au>
  8. Sender: news@news.loria.fr
  9. Organization: CRIN (CNRS) Nancy - INRIA Lorraine
  10. Lines: 22
  11.  
  12. In article <Bt5Mz6.3xs@research.canon.oz.au>, naylor@research.canon.oz.au (William Naylor) writes:
  13. |> I am looking for information on algorithms to solve the
  14. |> "boolean satisfiability problem".  What is the largest problem that
  15. |> can be solved routinely?  What is the best known algorithm?  
  16. |> Any good references?
  17. |> 
  18.  
  19. Well BDDs are fashionable for this sort of boolean equivalence (to false
  20. in your case) problem - especially in the hardware community.
  21.  
  22. The classic ref is
  23.  
  24. R. E. Bryant, Graph-Based Algorithms for Boolean Fuction Manipulation,
  25. IEEE Trans. on Computers, Vol. C-35, No. 8, pp677-691, 1986.
  26.  
  27. There are many refinements on this idea eg
  28.  
  29. S. H. Horeth, Improving the performance of a BDD-based tautology checker,
  30. Proceedings of the Advanced Workshop on Correct Hardware Design Methodologies, Turin, Italy, 1991.
  31.  
  32.  
  33. Steven
  34.