%Contact: ltuncel@watdragon.uwaterl
%Enclosed is the LaTex file for a preliminary abstract by
%Cheriyan, Cunningham, Wang and myself to be reviewed
%for the DIMACS Challenge.

%Sincerely,


%--Levent Tuncel


\documentstyle[11pt]{article}
 \oddsidemargin 0.25in \evensidemargin 0.25in
 \marginparwidth 40pt \marginparsep 10pt
 \topmargin -.25in \headsep .5in
 \textheight 8.175in \textwidth 6.25in
 \brokenpenalty=10000
 \renewcommand{\baselinestretch}{1.3}
\newlength{\sspace}
\setlength{\sspace}{\baselineskip}
\newcommand{\slineskip}{\setlength{\baselineskip}{1.3\sspace}}
\newcommand{\ssspace}{\setlength{\baselineskip}{1.0\sspace}}
\let\Huge=\large
\let\huge=\large
\let\LARGE=\large
\let\Large=\normalsize
\pagestyle{empty}
\begin{document}

\begin{center}

{\LARGE \bf SAT and MAX-SAT: Computational Behavior of Optimization Algorithms}

\medskip


{J. Cheriyan, W.H.Cunningham, L. Tun\c{c}el, Y. Wang}

{Department of Combinatorics and Optimization}


{University of Waterloo}



{Waterloo, Ontario, N2L 3G1 CANADA}

\end{center}



\medskip


We propose to conduct a computational study of the SAT and MAX-SAT
problems, focusing on the behavior of combinatorial optimization
algorithms on these problems.

We first plan to study the MAX-k-SAT problem, the restricted version
of MAX-SAT, where each clause has exactly k literals per clause (we
would be interested in small values of k, e.g. k=2,3,4), and to study
algorithms that achieve a guaranteed approximation ratio in polynomial
running time.  One such example is the recent algorithm of Yannakakis [1]
that achieves a 3/4 approximation ratio, using network flow methods.
We plan to implement some variants of this algorithm, focusing on issues
such as the empirical approximation ratios achieved on particular distributions
of MAX-k-SAT instances, and the empirical behavior of the running time
for achieving better and better approximation ratios, such as 1/2,
0.62, 3/4, etc.  In a related direction, we plan to study recent
multicommodity flow algorithms that have applications to solving
MAX-2-SAT, such as the algorithm by Klein, Agrawal, Ravi and Rao [2],
and improved algorithms by other researchers; also, we would take into account t
he
recent empirical
study by Leong, Shor and Stein on multicommodity flow algorithms [3].


We would also like to utilize a polyhedral approach as follows:
any weighted MAX-SAT problem with $m$ clauses and $n$
  variables can be formulated as a 0-1 integer linear
  program (ILP).
Using different formulations,
LP-based cutting plane approaches for the MAX-SAT
problem could be developed. For this purpose,
we will first try to identify polynomially separable
classes of facet-inducing inequalities for the ILP.
Next, we develop an LP-based cutting-plane
solution procedure to find a heuristic solution to
the MAX-SAT as well as a tight upper bound.
Finally, we will compare the empirical
performance ratios
of our heuristic with those of other
existing heuristics on a sample of
{\em hard} instances, for instance, those $50\% $
  satisfiable formulas (see [4]).


We would be interested in studying other issues pertaining to specific
distributions of SAT instances, such as the existence and value of a
``threshold ratio'' of number of clauses to number of variables in
random MAX-k-SAT instances, such that below the threshold almost every
instance is satisfiable whereas above the threshold almost every
instance is unsatisfiable, see eg., Mitchell, Selman and Levesque [4],
and Chvatal and Reed [5].

We plan to use instance generators available from DIMACS, such as the
MWFF generator of Selman.  If a number of different instance generators
were to be made available through DIMACS, then that would be helpful
for us.  Also, we would be interested in comparing our implementations
with those of others, such as the GSAT ``local search'' code of
Selman,  Levesque and Mitchell [6], and possibly other implementations;
we hope that some such implementations would be available through
DIMACS.


\medskip


{\bf References}

[1] M.Yannakakis,
On the approximation of maximum satisfiability,
preliminary version in Proc. 3rd Annual ACM-SIAM Sympos. on
Discr. Algorithms (1992), pp.1--9;

[2] P.Klein, A.Agrawal, R.Ravi and S.Rao,
Approximation through multicommodity flow,
Proc. 31st IEEE Sympos. on Foundations of Computer Science (1990),
pp.726--737.

[3] T.Leong, P.Shor and C.Stein,
Implementation of a Combinatorial Multicommodity Flow Algorithm,
Proc. 1st DIMACS Implementation Challenge: Network Flows and Matching
(1992), AMS, to appear.

[4] D.Mitchell, B.Selman, H.Levesque,
Hard and Easy Distributions of SAT Problems,
Proc. 10th Nat. Conf. on Artificial Intelligence (AAAI-92),
San Jose, CA, (1992), pp.459--465.

[5] V.Chvatal and B.Reed,
Mick Gets Some (the Odds Are on His Side),
Proc. 33st IEEE Sympos. on Foundations of Computer Science (1992),
pp.620--627.

[6] H.Levesque, B.Selman, and D.Mitchell,
A New Method for Solving Hard Satisfiability Problems (AAAI-92),
Proc. 10th Nat. Conf. on Artificial Intelligence,
San Jose, CA, (1992), pp.440--446.



 \end{document}