home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #19 / NN_1992_19.iso / spool / comp / theory / 1861 < prev    next >
Encoding:
Text File  |  1992-09-03  |  4.5 KB  |  96 lines
  1. Newsgroups: comp.theory
  2. Path: sparky!uunet!decwrl!sdd.hp.com!wupost!gumby!destroyer!ubc-cs!unixg.ubc.ca!kakwa.ucs.ualberta.ca!acs.ucalgary.ca!gu
  3. From: gu@enel.ucalgary.ca (Jun Gu)
  4. Subject: Satisfiability (I)
  5. Sender: news@acs.ucalgary.ca (USENET News System)
  6. Message-ID: <92Sep03.221830.18724@acs.ucalgary.ca>
  7. Date: Thu, 03 Sep 92 22:18:30 GMT
  8. References: <1992Sep1.183853.5844@news.cs.indiana.edu>
  9. Nntp-Posting-Host: eneli.enel.ucalgary.ca
  10. Organization: ECE Department, U. of Calgary, Calgary, Alberta, Canada
  11. Keywords: Average time complexity, local search, satisfiability 
  12. Lines: 82
  13.  
  14. Since last January, I have been receiving messages from many researchers.  
  15. A typical message was one from Paul Purdom on Sept. 1, 1992.  Some of the 
  16. questions are fairly interesting.  I have been asked by many people and  
  17. I would be happy to share my opinion on some questions in this group.  
  18.  
  19. The first set of questions I sorted out from numerous messages include: why 
  20. we had chosen this algorithm (i.e., SAT) to study, what are other results 
  21. from the past and present research, what are the other SAT algorithm(s),
  22. how to evaluate the hardness of the SAT problem instances.  I will discuss 
  23. these questions soon. 
  24.  
  25. Jun Gu
  26.  
  27. ---------------------------------------------------------------------------
  28.  
  29. The following two manuscripts were written last year and were submitted for
  30. review.  You may ask a copy from Ruchir Puri:
  31.  
  32.             puri@enel.UCalgary.CA
  33.  
  34.  
  35. ---------------------------------------------------------------------------
  36.  
  37.                        Average Time Complexities of 
  38.        Several Local Search Algorithms for the Satisfiability Problem 
  39.  
  40.                          Jun Gu and Qian Ping Gu
  41.               Dept. of Electrical and Computer Engineering 
  42.                      Univ. of Calgary, Canada T2N 1N4
  43.  
  44.                          1991
  45.  
  46.                          Abstract (LaTex format)
  47.  
  48. The satisfiability (SAT) problem is a basic problem in computing theory. 
  49. It is fundamental in solving many practical application problems in logic 
  50. programming, inference, machine learning, and VLSI engineering.  Recently, 
  51. many families of local search algorithms for the SAT problem have been 
  52. developed.  In this report, we analyze the average time complexities of 
  53. three basic algorithms in the $SAT1$ family.  For the randomly generated 
  54. {\it conjunctive normal form} ($CNF$) formulae with $n$ clauses, $m$ variables,
  55. and $l$ literals in each clause, we give a qualitative analysis of the average
  56. time complexity of the $SAT1.1$ and  $SAT1.2$ algorithms, and a quantitative 
  57. analysis of the average time complexity of the $SAT1.3$ algorithm.  For 
  58. $l\geq \log m-\log\log m-c$ and $n/m\leq 2^{l-1}/l$, where $c\geq 0$ is any 
  59. constant, we show that $SAT1.1$ exhibits a polynomial average time complexity 
  60. of $O(m^{O(1)}n)$. For $l\geq 3$ and $n/m=O(2^l/l)$, we show that $SAT1.2$ 
  61. exhibits a polynomial average time complexity of $O(m^{O(1)}n^2)$. The average
  62. run time of the $SAT1.3$ algorithm is $O(m\log n(ln+m))$ for $l\geq 3$ and 
  63. $n/m=O(2^l/l)$. For $l=o(m)$, while all $SAT1.1$, $SAT1.2$, and $SAT1.3$ 
  64. algorithms have the polynomial average time complexity, the well-known Davis-
  65. Putnam algorithm demonstrates a superpolynomial average run time 
  66. ($O(n^{O(m/l)})$).  Thus the $SAT1.1$, $SAT1.2$ and $SAT1.3$ algorithms
  67. have significantly improved on the Davis-Putnam algorithm for certain classes 
  68. of $CNF$ formulae.
  69.  
  70.  
  71.            Average Time Complexity of the SAT1.3 Algorithm
  72.  
  73.                      Jun Gu and Qian Ping Gu
  74.            Dept. of Electrical and Computer Engineering 
  75.                  Univ. of Calgary, Canada T2N 1N4
  76.  
  77.               1991, Rev. Feb. 1992
  78.  
  79.                      Abstract (LaTex format)
  80.  
  81.  
  82. The satisfiability (SAT) problem is a basic problem in computing theory. 
  83. It is fundamental in solving many practical application problems in logic 
  84. programming, inference, machine learning, and VLSI engineering. In this paper, 
  85. we analyze the average time complexity of the $SAT1.3$ algorithm. For the 
  86. randomly generated $CNF$ formulae with     $n$ clauses, $m$ variables, and 
  87. average $l$ literals in each clause, the average run time of the $SAT1.3$ 
  88. algorithm is $O(m\log n(ln+m))$ for $l\geq 3$ and $n/m=O(2^l/l)$. This result 
  89. improves significantly on the well-known Davis-Putnam algorithm which has an 
  90. $O(n^{O(m/l)})$ average time complexity.  Numerous real algorithm executions
  91. were performed which indicate that the $SAT1.3$ algorithm is much more 
  92. efficient than the Davis-Putnam algorithm for certain classes of 
  93. {\it conjunctive normal form} ($CNF$) formulae. 
  94.  
  95.  
  96.