From: gu@enel.ucalgary.ca (Jun Gu)
Subject: Satisfiability (I)
Date: Thu, 03 Sep 92 22:18:30 GMT
Organization: ECE Department, U. of Calgary, Calgary, Alberta, Canada
Keywords: Average time complexity, local search, satisfiability 

Since last January, I have been receiving messages from many researchers.  
A typical message was one from Paul Purdom on Sept. 1, 1992.  Some of the 
questions are fairly interesting.  I have been asked by many people and  
I would be happy to share my opinion on some questions in this group.  

The first set of questions I sorted out from numerous messages include: why 
we had chosen this algorithm (i.e., SAT) to study, what are other results 
from the past and present research, what are the other SAT algorithm(s),
how to evaluate the hardness of the SAT problem instances.  I will discuss 
these questions soon. 

Jun Gu

---------------------------------------------------------------------------

The following two manuscripts were written last year and were submitted for
review.  You may ask a copy from Ruchir Puri:

			puri@enel.UCalgary.CA


---------------------------------------------------------------------------

                       Average Time Complexities of 
       Several Local Search Algorithms for the Satisfiability Problem 

                         Jun Gu and Qian Ping Gu
              Dept. of Electrical and Computer Engineering 
                     Univ. of Calgary, Canada T2N 1N4

		    	         1991

                         Abstract (LaTex format)

The satisfiability (SAT) problem is a basic problem in computing theory. 
It is fundamental in solving many practical application problems in logic 
programming, inference, machine learning, and VLSI engineering.  Recently, 
many families of local search algorithms for the SAT problem have been 
developed.  In this report, we analyze the average time complexities of 
three basic algorithms in the $SAT1$ family.  For the randomly generated 
{\it conjunctive normal form} ($CNF$) formulae with $n$ clauses, $m$ variables,
and $l$ literals in each clause, we give a qualitative analysis of the average
time complexity of the $SAT1.1$ and  $SAT1.2$ algorithms, and a quantitative 
analysis of the average time complexity of the $SAT1.3$ algorithm.  For 
$l\geq \log m-\log\log m-c$ and $n/m\leq 2^{l-1}/l$, where $c\geq 0$ is any 
constant, we show that $SAT1.1$ exhibits a polynomial average time complexity 
of $O(m^{O(1)}n)$. For $l\geq 3$ and $n/m=O(2^l/l)$, we show that $SAT1.2$ 
exhibits a polynomial average time complexity of $O(m^{O(1)}n^2)$. The average
run time of the $SAT1.3$ algorithm is $O(m\log n(ln+m))$ for $l\geq 3$ and 
$n/m=O(2^l/l)$. For $l=o(m)$, while all $SAT1.1$, $SAT1.2$, and $SAT1.3$ 
algorithms have the polynomial average time complexity, the well-known Davis-
Putnam algorithm demonstrates a superpolynomial average run time 
($O(n^{O(m/l)})$).  Thus the $SAT1.1$, $SAT1.2$ and $SAT1.3$ algorithms
have significantly improved on the Davis-Putnam algorithm for certain classes 
of $CNF$ formulae.


           Average Time Complexity of the SAT1.3 Algorithm

                     Jun Gu and Qian Ping Gu
           Dept. of Electrical and Computer Engineering 
                 Univ. of Calgary, Canada T2N 1N4

		      1991, Rev. Feb. 1992

                     Abstract (LaTex format)


The satisfiability (SAT) problem is a basic problem in computing theory. 
It is fundamental in solving many practical application problems in logic 
programming, inference, machine learning, and VLSI engineering. In this paper, 
we analyze the average time complexity of the $SAT1.3$ algorithm. For the 
randomly generated $CNF$ formulae with 	$n$ clauses, $m$ variables, and 
average $l$ literals in each clause, the average run time of the $SAT1.3$ 
algorithm is $O(m\log n(ln+m))$ for $l\geq 3$ and $n/m=O(2^l/l)$. This result 
improves significantly on the well-known Davis-Putnam algorithm which has an 
$O(n^{O(m/l)})$ average time complexity.  Numerous real algorithm executions
were performed which indicate that the $SAT1.3$ algorithm is much more 
efficient than the Davis-Putnam algorithm for certain classes of 
{\it conjunctive normal form} ($CNF$) formulae. 


Newsgroups: comp.theory