home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / sci / math / 14645 < prev    next >
Encoding:
Internet Message Format  |  1992-11-09  |  3.6 KB
  1. Xref: sparky sci.math:14645 comp.ai:4208 comp.lang.lisp:2834
  2. Path: sparky!uunet!news.tek.com!uw-beaver!cs.ubc.ca!destroyer!caen!spool.mu.edu!hri.com!snorkelwacker.mit.edu!stanford.edu!CSD-NewsHost.Stanford.EDU!CS.Stanford.EDU!pehoushe
  3. From: pehoushe@CS.Stanford.EDU (Dan Pehoushek)
  4. Newsgroups: sci.math,comp.ai,comp.lang.lisp
  5. Subject: Satisfiability program available, common lisp
  6. Message-ID: <1992Nov9.013145.175@CSD-NewsHost.Stanford.EDU>
  7. Date: 9 Nov 92 01:31:45 GMT
  8. Sender: news@CSD-NewsHost.Stanford.EDU
  9. Organization: Computer Science Department, Stanford University
  10. Lines: 63
  11.  
  12.  
  13.  
  14. I am making the source code to a satisfiability program available, and
  15. if there's enough interest, I will post it in comp.lang.lisp (1500
  16. lines of code). Mail to pehoushe@sail.stanford.edu.
  17.  
  18. The program is competitive with the fastest complete algorithms that I
  19. know of.  If you use a propositional inference engine in your work, give
  20. this one a try.  If you haven't put a significant amount of time an
  21. effort into your inference system, this program is probably faster in a
  22. majority of cases.
  23.  
  24. On Mitchell, Selman, Levesque hard spot problems, the program takes
  25. from 1 minute to 15 minutes on 150 variable instances, including
  26. unsatisfiable instances, averaging under 10 minutes.  The program
  27. appears to run in time N*2^(N/22) on MSL hard spot instances. 
  28.  
  29. Easy Instances: Using the program, the author (me) discovered
  30. empirically that almost all randomly generated 4-regular graphs (and
  31. indeed, almost all randomly generated k-regular graphs, with
  32. sufficiently many vertices), are 3-colorable.  Instances with
  33. thousands of vertices were translated to 3-sat and then colored.
  34. There is a fairly simple counting argument that proves this empiricaal
  35. result.  Empirically, the 3-coloring problem on almost all (in
  36. Bollobas sense) 4-regular graphs is easy (near linear time).
  37.  
  38. However, the main potential practical result is that, given a random
  39. instance of an NP-complete problem, and then translating it to 3-sat,
  40. does not necessarily make the resulting instance hard. The program
  41. appears to run in near O(N) time on almost all of these 3-coloring
  42. instances.  Please note, however, these so-called "easy" instances appear
  43. to be quite hard for the Davis-Putnam algorithm.
  44.  
  45.  
  46. Fairly Hard Instances: There is a simple method to generate instances
  47. that are significantly harder than the MSL hard spot.  Generate random
  48. 3-clauses such that each variable appears 5 times positively and 5
  49. times negatively. The resulting 3-cnf formulae tend to be harder and
  50. smaller than MSL hard spot formulae, but also tend to be almost always
  51. satisfiable, given more than 100 or so variables.  The program tends
  52. to run in time 2^(N/17) or so on these instances, but they could get
  53. even harder as N gets larger.  These "5-5-regular" instances are the
  54. hardest, almost always satisfiable, 3-CNF problems that I know of.
  55.  
  56. Hardest Known Instances: The hardest (based on size of 3-CNF formulae)
  57. of any instances are 6-5-regular (each variable occurs 6 times
  58. positively and 5 times negatively), with many of these being
  59. unsatisfiable.  150 variable instances of these problems can take
  60. several hours.
  61.  
  62.  
  63. I'm very interested in "in practice" kinds of instances.  I wonder how
  64. hard the NP-complete instances that actually arise in areas outside of
  65. CS theory really are.
  66.  
  67. If you'd like to trade "hard" instances, let me know.
  68.  
  69. I may not be on the net after Christmas, because the job hunting
  70. situation in this area is very bad.  So if you'd like the source code
  71. for the program, let me know soon. Also, if you have any pointers to
  72. "research programming" type jobs, I'd very much appreciate them.
  73.  
  74. Dan Pehoushek
  75.