\documentstyle [12pt]{article}
\baselineskip 12pt
\onecolumn
\pagenumbering{arabic}
\pagestyle{plain}
\textwidth 16.5cm
\textheight 24cm
\hoffset=-1.5cm
\voffset=-2cm
\setlength{\parindent}{0.0cm}

\title{ Can a very simple algorithm \\
be efficient for solving the SAT problem ? }
\author{O. Dubois$^{\dagger}$, P. Andre$^{\dagger}$, Y. Boufkhad$^{\dagger}$ and J. Carlier$^{\ddagger}$ \\
\scriptsize $\dagger$ LAFORIA, CNRS-Universit\'e Paris 6, 4 place Jussieu, 75252 Paris cedex 05, FRANCE. {  }  {\bf Email} : dubois@laforia.ibp.fr \\
\scriptsize $\ddagger$ HEUDIASYC, D\'epartement G\'enie Informatique, Universit\'e de Technologie de Compi\`egne, 60206 Compi\`egne, FRANCE}
\date{}

\begin{document}
\maketitle  

\begin{quote}
\em~~~We present a very simple algorithm for solving the problem of Satisfiability and we ask if a significantly more efficient algorithm may be found.
\end{quote}

We give below a backtracking algorithm which solves the SAT problem using a simple branching rule.

\paragraph{}
We consider a SAT instance as a set of clauses (see definition of the SAT problem in the document satreview.tex of DIMACS) and we denote by $S$ any SAT instance. The rule used is~:

\paragraph{}
{\bf Branching rule} : select the variable $x$ having the greatest number of occurrences in the shortest clauses of S, and split $S$ in two simplified subinstances by setting $x$ to true and false respectively.

\paragraph{}
The following backtracking algorithm implements this rule.

\paragraph{Algorithm A}
\begin{quote}
Let $I$ be the input SAT instance \\
Let $L$ be a working list containing SAT instances \\
$L$ is initialized as \{$I$\}
\begin{enumerate}
\item if $L$ is empty, then return $I$ unsatisfiable (stop), else choose a SAT instance $S$ in $L$
\item if $S$ is empty, then return $I$ satisfiable (stop)
\item if $S$ contains an empty clause, $S$ is not satisfiable, then go to 1.
\item if $S$ contains a clause with only one variable then set this variable to the value which satisfies the clause, simplify S and go to 2.
\item {\bf Branching rule} : select the variable $x$ having the greatest number of occurrences in the shortest clauses of $S$. Add to $L$ the simplified instance $S'$ obtained by setting $x$ to false. Set $x$ to true and simplify $S$. Go to 2.
\end{enumerate}
\end{quote}

\paragraph{}
This algorithm is "naive". It is a backtracking search of a solution, driven by a simple function of choice of the branching variables. Intuitively this function tries to bring out as fast as possible the greatest number of fixed variables.

\paragraph{}
We tested algorithm A on so called random r-SAT instances with a constant length of clauses equal to $r$ in order to obtain hard instances (see Franco and Paull 1983, Mitchell $et$ $al.$ 1992). The following model is used. First one fixes the values $n$ of the number of variables, $p$ of the number of clauses and $r$ of the number of literals per clause, then one chooses independently and uniformly $p$ clauses with $r$ distinct literals defined over a set of $n$ variables. It can be observed experimentally that the difficulty of SAT instances generated according to that model, depends strongly on the ratio $p/n$. For example, the hardest 3-SAT instances  wchich can be solved actually, have a ratio varying between 4.1 and 4.5. These results can be explained by probabilistic arguments (Simon $et$ $al.$ 1986).

\paragraph{}
The table below gives results of experiments of the algorithm A on 3-SAT instances for $p/n$ equal to 4.1, 4.3 and 4.5 and some values of $n$ from 100 to 300 variables. The algorithm has been implemented in C programming language and performed on a SUN SPARC 2 workstation under UNIX operating system (the load program is provided, to obtain it see the end of the abstract). For every couple of values ($n,p/n$) of the table, 10 random 3-SAT instances have been generated. Every square contains two lines. The upper line gives results for satisfiable instances and the lower line for unsatisfiable ones. Each line contains firstly, in parentheses, the number of instances (satisfiable in the upper line -Y is for yes-, unsatisfiable in the lower line -N is for no-), secondly, the average time (rounded to the nearest number of seconds, so 0 may be written) for solving these instances, thirdly, the average number (rounded to the nearest tens) of branches of the backtrack trees constructed by the algorithm A, i.e the double of the number of calls to the Branching rule in case of unsatisfiable instances.\vspace{6mm}

\begin{tabular}{|l|ccc|ccc|ccc|}
\hline
~~~~$p/n$ & \multicolumn{3}{c|}{4.1} & \multicolumn{3}{c|}{4.3} & \multicolumn{3}{c|}{4.5} \\
~$n$ & & & & & & & & & \\ \hline \hline
100 & (8Y) & 0" & 160 & (5Y) & 0" & 160 & (0Y) & . & . \\
 & (2N) & 0" & 820 & (5N) & 0" & 500 & (10N) & 0" & 430 \\ \hline \hline
150 & (7Y) & 1" & 800 & (5Y) & 1" & 1700 & (0Y) & . & . \\
 & (3N) & 4" & 7290 & (5N) & 3" & 4940 & (10N) & 2" & 2860 \\ \hline \hline
200 & (9Y) & 10" & 12450 & (4Y) & 19" & 25420 & (0Y) & . & . \\
 & (1N) & 25" & 32300 & (6N) & 21" & 26700 & (10N) & 18" & 21030 \\ \hline \hline
250 & (7Y) & 59" & 58930 & (2Y) & 1'38" & 102230 & (0Y) & . & . \\
 & (3N) & 7'44" & 468990 & (8N) & 3'43" & 233410 & (10N) & 1'58" & 116470 \\ \hline \hline
300 & (10Y) & 8'54" & 494980 & (3Y) & 9'11" & 491220 & (0Y) & . & . \\
 & (0N) & . & . & (7N) & 24'04" & 1283590 & (10N) & 20'00" & 751430 \\ \hline
\end{tabular}

\paragraph{}

Algorithm A is so simple that common sense suggests that it is possible to find a more elaborate algorithm which solves the Satisfiability problem much more efficiently. Indeed for many combinatorial problems for example the Travelling Salesman problem, the Jobshop problem ..., it have been shown that new methods more sophisticated than previous ones or refinements carried out for existing algorithms have improved considerably the solution of those problems. In the case of the SAT problem, common sense seems to be caught out. Relaxing techniques have been introduced as the 2-SAT relaxation (Stamm 1992) or the Horn-SAT relaxation (Gallo and Urbani 1989), integer programming methods have been adapted (Hooker 1988, Kamath $et$ $al.$ 1990), backtracking algorithms with sophisticated heuristics have been proposed (Purdom 1984, Monien and Speckenmeyer 1985, Zabih and McAllester 1988, Andre and Dubois 1992, B\"{o}hm 1992), mixed methods associating backtrack with resolution have also been implemented (Billionnet and Sutter 1992) ... but it does not seem from the reported results that significant improvements in computing time have been obtained even comparing with the results of the very simple algorithm A. Nevertheless concerning parameters others than the computing time such as, for example, the size of search trees, large improvements have been obtained. However, the comparisons between the different sets of results are difficult to make, because the conditions of experiments are not normalized : generator models of random instances, programming languages, computers, etc. can be very different.

\paragraph{}
If the algorithm A is as or is more efficient than other sophisticated algorithms for solving the SAT problem, its efficiency comes probably from its simplicity which permits the implementation to be really optimized with regard to data structures or programming instructions. But if we do not observe significant differences, in terms of computing time, between existings algorithms, the reason may be that the size of the instances which can be solved at present, is limited. If very large instances (1000, 10000 or more variables) could be solved, significant differences might be observed.

\paragraph{}
Algorithm A is surely improvable. For example, if the SAT instance is satisfiable, a solution could be found faster if, in the Branching rule, the selected variable is first set to the truth value satisfying the most number of clauses. Likewise, when there are several variables which may be selected because they have the greatest number of occurrences in the shortest clauses, if one chooses among them the variable $x$ such that the difference between the numbers of occurences of literals $x$ and -$x$ is the smallest, the performance of A is enhanced. But these improvements remain insignificant.

\paragraph{}
The short preceding discussion, leads us to ask the following question. Is it possible to find a more elaborate algorithm than A which solves the problem of satisfiability significantly more efficiently ? It might be considered, for example, as a significant improvement, to solve in the same computing times as A, random SAT instances having 100 variables more, the random instances processed being the hardest ones according to the ratio $p/n$, and the conditions of experiments for the comparison being equivalent : same generator, same programming language, same computer, same kind of implementation with regard to optimization. We are working on the question mentionned above.

\paragraph{}
To permit comparisons, we provide the load program of our C implementation of the algorithm A (this implementation is due to Pascal Andre). We also provide the C source of our generator of random r-SAT instances. Appendix gives the conditions for using these modules. They are available in: pub/challenge/sat/contributed/dubois through FTP to DIMACS.

\newpage
\paragraph{References}

\begin{description}
\item[\small\sc Andre, P. {\normalsize and} Dubois, O.] (1992) Using the expected number of solutions to optimize the resolution of a SAT instance, {\em Compte Rendu de l'Acad\'emie des Sciences de Paris}, tome 315, s\'erie I, 1992, 217-220. 
\item[\small\sc Billionnet, A. {\normalsize and} Sutter, A.] (1992) An efficient algorithm for the 3-satisfiability problem, {\em Operations Research Letters}, 12, 1992, 29-36.
\item[\small\sc B\"{o}hm, H.] (1992) Report on a SAT competition, Universit\"{a}t Paderborn, Germany, Nr. 110, November 1992.
\item[\small\sc Franco, J. {\normalsize and} Paull, M.] (1983) Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. {\em Discrete Applied Math.}, 1983, 77-87.
\item[\small\sc Gallo, G. {\normalsize and} Urbani, G.] (1989) Algorithms for testing the satisfiability of propositional formulae. {\em Journal of Logic Programming}, 7, 1989, 45-61.
\item[\small\sc Hooker, J.N.] (1988) Resolution vs cutting plane solution of inference problems : some computational experience. {\em Operations Research Letter}, 7(1), 1988.
\item[\small\sc Kamath, A.P., Karmarkar, N.K., Ramakrishnan, K.G. {\normalsize and} Resende, M.G.C.] (1990)\\Computational experience with an interior point algorithm on the satisfiability problem. {\em Proceedings, Integer Programming {\normalsize and} Combinatorial Optimization}, Waterloo, Canada, Mathematical Programming Society, 1990, 333-349.
\item[\small\sc Mitchell, D., Selman, B. {\normalsize and} Levesque, H.J.] (1992) Hard and easy distributions of SAT problems. {\em Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92)}, San Jose, CA, July 1992, 440-446.
\item[\small\sc Monien, B. {\normalsize and} Speckenmeyer, E.] (1985) Solving satisfiability in less than $2^n$ steps, {\em Discrete Applied Mathematics}, 10, 1985, 287-295.
\item[\small\sc Purdom, P.] (1984) Solving satisfiability with less searching, {\em IEEE Trans. Pattern. Anal. Machine Intell.}, 6(4), 1984, 510-515.
\item[\small\sc Simon, J.C., Carlier, J., Dubois, O. {\normalsize and} Moulines, O.] (1986) Etude statistique de l'ex-\\istence de solutions de probl\'emes SAT, {\em Compte Rendu de l'Acad\'emie des Sciences de Paris}, tome 302, s\'erie I, 1986, 283-286.
\item[\small\sc Stamm, H.] (1992) Report on a SAT competition, Universit\"{a}t Paderborn, Germany, Nr. 110, November 1992.
\item[\small\sc Zabih, R. {\normalsize and} McAllester, D.] (1988) A rearrangement search strategy for determining propositional satisfiability. {\em Proceedings AAAI-88}, 1988, 155-160.
\end{description}

\newpage
\paragraph{Appendix}

\paragraph{}
Here we give informations for using our random SAT generator "gensat" and our load program "Asat"~:
\begin{itemize}
\item "gensat.c" is the source C file of our generator of random r-SAT instances. this generator is asking as input for~:
\begin{quote}
. n $=$ the number of variables (int) \\
. p $=$ the number of clauses (int) \\
. r $=$ the number of variables per clause (int) \\
. g $=$ the seed of the random SAT instance (unsigned long int)
\end{quote}
Its output is the text file "in.dat".

{\it In the experiments reported page 2, for every couple of values ($n,p/n$) of the table of results, 10 random instances have been generated with the ten following seeds: 123+$k$456 with $k$ = 0, 1, ...,9.}

 
\item the text file "in.dat" is automatically generated by the generator "gensat" with the following format~:
\begin{quote}
. the first line contains the number of variables (n) \\
. the second line contains the number of clauses (p) \\
. the third line contains the number of variables per clause (r) \\
. the fourth line contains the seed (g) \\
. each of the next p lines contains the values of the r literals per clause, separated with a blank ; each literal is represented by an integer value between -n and n (except 0)
\end{quote}
\item the executable file "Asat" is the implementation of the algorithm A. It takes as input the file "in.dat" and return as output a line of 7 integer values separated with blanks, corresponding to~:
\begin{quote}
. the seed of the SAT instance (g) \\
. the number of variables (n) \\
. the number of clauses (p) \\
. the number of variables per clause (r) \\
. the value of the satisfiability, 1 if yes and 0 if no \\
. the number of branches of the resolution tree \\
. the time needed to solve the instance in seconds (using time() function)
\end{quote}  
\end{itemize}

\end{document}