%This file is onefile.tex, for the 2nd DIMACS Implementation Challenge

\documentstyle[11pt]{article}
%\pagestyle{empty}

%Springer LNCS formatting
%interpolation for 11pt fonts
\setlength{\textwidth}{5.8in}
\setlength{\textheight}{8.5in}
\setlength{\topmargin}{0in}
\setlength{\headheight}{.25in}
\setlength{\abovedisplayskip}{2.5mm}
\setlength{\belowdisplayskip}{2.5mm}
\setlength{\abovedisplayshortskip}{0mm}
\setlength{\belowdisplayshortskip}{1.7mm}

\renewcommand{\textfraction}{.1}

\def\null{\makebox[0mm]{}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{proposition}{Proposition}

\hyphenation{re-write com-ple-tion}


\begin{document}
%\begin{titlepage}

\title{Proposed Work on Satisfiability for the Second DIMACS International Algorithm Implementation Challenge}
\author{Jeffrey A. Ward\\
        Department of Computer and Information Science\\
        The Ohio State University \\
        Columbus, OH 43210-1277\\
        {\small $\langle$ward@cis.ohio-state.edu$\rangle$}
}

%\date{}
\maketitle

\begin{abstract}
This work concerns the SAT and MAX-SAT problems.
A formula generator will be created which can generate CNF formulas from
distributions outside the domain of the standard constant-probability and fixed clause-length models.
The generator will be used to generate formulas from both standard models and one additional model.
Measurements will be taken on these formulas concerning the likelihood of being satisfiable and the average number of solutions.
Performance measurements will also be obtained for existing SAT and MAX-SAT algorithms and some novel variants of these algorithms.
\end{abstract}

\thispagestyle{empty}
%\end{titlepage}


\section{Alternative Models for Random Formulas}

The standard models from which random CNF fmlas are drawn are the constant-probability model and the fixed clause-length model.
Mitchell, Selman, and Levesque \cite{MitchellSelmanLevesque:92}
in particular compare these two models.
Both models take as parameters the number of variables $N$, and the
number of clauses $L$.
The fixed clause-length model takes as its third parameter $K$,
the number of literals per clause.
Frequently the value of $K$ is taken to be 3.
In contrast, the constant-probability model takes as its third parameter
$P$, the probability that a given variable will be mentioned in a given clause.
In both models the likelihood of a literal being negated is 50\%.
Both of these models are instances of a more general model
which I will refer to as the random clause size model.
This model again takes $N$ and $L$ as parameters but takes as its
third parameter a discrete probability distribution function $f$
from which the lengths of clauses are independently determined.
Under the random clause-length model we can obtain a fixed clause-length
or constant-probability model by allowing $f$ to correspond to a constant or
binomial distribution, respectively.
I plan to write a formula generator which allows the user to insert
a procedure for generating values according to a chosen $f$
and which will then generate formulas from the
corresponding instantiation of the random clause size model.

I will refer to instances of the random clause size model where $f$
corresponds to a discrete uniform distribution as uniform distribution models.
The motivation for considering uniform distribution models comes from the
observation that formulas generated according to the fixed clause-length
and constant-probability models tend in some sense to be rather homogenous:
all variables tend to be mentioned roughly the same number of times,
all literals are negated with likelihood 0.5,
and all clauses tend towards roughly the same length.
One might expect that examples from a large number of applications would
not exhibit these characteristics.
Using a uniform distribution for $f$ addresses the last of these three sources of homogeneity:
the lengths of clauses will vary in a more extreme manner.
Of course, the lengths of clauses vary more in the constant-probability model
than in the fixed clause-length model but I am interested in investigating
trends that occur as models with more and more variance are considered.

I also plan to submit a version of the formula generator which will take
pdf's $f$, $g$, and $h$ as parameters.
In this case, if $v_1,...,v_N$ are the propositional variables
then $g(i)$ and $h(i)$ are computed before each formula is generated.
Then, for a given clause $c$ whose size has already been determined using $f$,
$g(i)$ will specify the relative probability (with respect to the other
variables) of $v_i$ being included in $c$.
Similarly, $h(i)$ would specify the likelihood that a given literal mentioning
$v_i$ will be negated.
I do not, however, expect to use this version of the formula generator
in the experiments that I will perform for the Challenge.

\section{Experiments}
\subsection{Hard problems for DP}
Mitchell, Selman, and Levesque found that for the fixed clause size model with
clause size $K$ = 3 and a fixed number of variables $N \leq 140$, formulas
could be generated with a close to 50\% likelihood of being satisfiable
by setting the number of clauses $ L \approx 4.3 N$ (modulo a slight
boundary effect for small values of $N$).
They also found that such a ratio between $L$ and $N$ resulted in the
hardest problems for the Davis-Putnam procedure (DP) \cite{DavisPutnam:60},
which so far seems to remain the standard procedure for solving
SAT decision problems.

I intend to repeat these experiments for different values of $K$,
checking whether the hard problems for DP are still generated
near the ``50\% satisfiability point'' in terms of the ratio $N/L$.
I will also keep an eye out for a general relationship between the
``50\% satisfiability point'' and $K$ and the possibility of analytically
suggesting why the relationship might exist.
I plan to test formulas derived from the constant-probability
and uniform distribution models for combinations of parameters which,
for a given number of variables, yield a 50\% likelihood of satisfiability
or hard problems for DP.
Mitchell et al.\ produced empirical work which suggests that,
for a given number of variables ($V=20$ in their experiments),
random 3-SAT formulas are considerably harder for DP than formulas
obtained from the Random P-SAT model.
(Random P-SAT is a variant of the constant probability model in which empty and unit clauses are disallowed.)
They concluded that ``the constant-probability model is not suitable for the evaluation of satisfiability testing procedures.''
On the other hand, Prof. Paul Purdom and his collaborators have done
seemingly all of their work on SAT using the constant-probability
model.
In \cite{Purdom:90} Purdom gives analytical results indicating
combinations of parameters which asymptotically lead to average
case exponential computing time for various versions of DP.
For $V=50$ he gives detailed empirically derived contours indicating
parameters which result in the maximal average number of solutions and
the maximal average number of recursive calls for DP.
I hope to investigate further, for different values of $V$ up to say 50 or 100,
the extent (great or small as it may be) to which formulas from the
constant-probability model can be generated which are as hard for DP
as formulas from the fixed clause-length model.
I would also like to perform this comparison for formulas generated
from uniform distribution models.
I note that in their empirical work, Mitchell et al.\ report the
{\em median} number of DP calls whereas Purdom reports the {\em mean}
number of DP calls.
I plan to compile and contrast results for both statistics.

\subsection{Local search (GSAT)}
I also plan to perform tests of algorithms for (approximate)
MAX-SAT on the above mentioned models.
Algorithms for MAX-SAT can include simulated annealing, genetic algorithms,
steepest ascent/mildest descent \cite{HansenJaumard:90},
GSAT \cite{SelmanLevesqueMitchell:92}, and
two greedy algorithms due to Johnson \cite{Johnson:74}
(referred to by Hansen and Jaumard in \cite{HansenJaumard:90}
as JOHN1 and JOHN2).
Simulated annealing, steepest ascent/mildest descent, and GSAT
are all examples of local search methods.
Hansen and Jaumard made an empirical comparison of the performance of
JOHN1, JOHN2, simulated annealing, and steepest ascent/mildest descent
on random 3-SAT formulas and obtained the best results from
steepest ascent/mildest descent.
I plan to test JOHN2 and GSAT on formulas generated from 3-SAT,
constant probability, and uniform distribution models.
I hypothesize that JOHN2 will compare more favorably to the local
search method on the later two models than it does on 3-SAT.
I make this hypothesis because JOHN2 takes the size of a clause into account
when assigning it a weight whereas GSAT assigns all clauses equal weight.

Selman, Levesque, and Mitchell \cite{SelmanLevesqueMitchell:92}
found that GSAT is remarkably effective at finding satisfying assignments
for satisfiable random 3-SAT formulas.
I hypothesize that GSAT will not be as effective in finding satisfying
assignments for formulas generated from constant probability
and uniform distribution models because
I expect GSAT to have some difficulty in dealing with smaller (especially unit)
clauses.
I would like to look for models and parameter combinations
which produce formulas that (1) have a relatively large number of local
optima which are not global optima,
(2) have local optima which fall relatively far short of being global optima
(in terms of the objective function), and/or
(3) have local optima which differ greatly from global optima
in terms of which variables are assigned which values.
One would naturally expect these formulas to be hard instances for
local search methods.



\subsection{Variants of GSAT}

I plan to test variants of GSAT on satisfiable formulas on
which GSAT itself has difficulty in finding satisfying assignments.
These variants will involve modifying the way in which the algorithm
assigns weights to clauses.
One variant will utilize the clause weighting scheme used in JOHN2:
$weight = 2^{-length}$.
Another variant will use a dynamic weighting scheme:
clauses are originally weighted equally, but each time the algorithm reaches
a local optimum it multiplies the weight of each clause by
$(1-\epsilon)^{m-1}$, where $\epsilon$ is a small positive constant and $m$
is the number of currently satisfied literals in the clause.
This will cause unsatisfied clauses to become progressively
heavier and oversatisfied clauses to become progressively lighter.
Given sufficient time I might also implement a dynamic weighting scheme
which uses timestamps.
In this scheme clauses have their timestamps updated when their status
changes from satisfied to unsatisfied or vice versa.
Among those clauses which are unsatisfied, those with older timestamps
are considered heavier.
Among satisfied clauses, those with older timestamps
are considered lighter.
It would seem that any of the above three weighting schemes could
be incorporated into genetic algorithms, simulated annealing, or
steapest ascent/mildest descent, although I don't expect to have time
to implement and test such methods before the end of the Challenge.

\subsection{Variant of DP}

Another idea that I plan to try is using approximate solutions
to MAX-SAT to order the variables for the Davis-Putnam procedure in solving SAT.
My idea is to take the variables mentioned in the unsatisfied clauses and
place them at the top of DP's search tree.
This idea may not be entirely baked but my intuition
is that a formula may have a harder part and an easier part and
that by placing these variables at the top of the search tree
we are forcing DP to commit to its choice on the hard part earlier
rather than asking it to solve the hard part repeatedly.



\bibliographystyle{alpha}
\begin{thebibliography} {99999}
\bibitem[DP60]{DavisPutnam:60}
M. Davis and H. Putnam,
``A Computing Procedure for Quantification Theory'',
{\em Journal of the ACM}, Vol. 7, pp. 201-215, 1960.

\bibitem[HJ90]{HansenJaumard:90}
Pierre Hansen and Brigitte Jaumard,
``Algorithms for the maximum satisfiability problem'',
{\em Computing}, Vol. 44, pp. 279-303, 1990.

\bibitem[Joh74]{Johnson:74}
 D. S. Johnson,
``Approximation algorithms for combinatorial problems'',
{\em Journal of Computer and System Sciences}, Vol. 9, pp. 256-278, 1974.

\bibitem[MSL92]{MitchellSelmanLevesque:92}
David Mitchell, Bart Selman, and Hector Levesque,
``Hard and easy distributions of SAT problems'',
{\em Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92)}, 1992.

\bibitem[Pur90]{Purdom:90}
Paul Purdom,
``A survey of average time analyses of satisfiability algorithms'',
{\em Journal of Information Processing}, Vol. 13, No. 4, pp. 449-455, 1990.

\bibitem[SLM92]{SelmanLevesqueMitchell:92}
Bart Selman, Hector Levesque, and David Mitchell,
``A new method for solving hard satisfiability problems'',
{\em Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI-92)}, 1992.

\end{thebibliography}

\end{document}