%
% satreview.tex A selection of problem definitions, suggested
% readings, and possible projects on satisfiability and maximum
% satisfiability. 
%
\documentstyle[12pt]{article}
\title{Satisfiability and Maximum Satisfiability\\Descriptions,
Readings, Problems}
\author{}
\date{Last revision: December 3, 1992}
\begin{document}
\maketitle 

{\narrower{\it This a work in progress, intended as a solely to
define the problems, suggest some introductory readings and offer some
suggested problems.  Feel free to send us any suggested additions or
clarifications, or additional project suggestions.  The email address
for suggestions is} 

\centerline{\tt challenge@dimacs.rutgers.edu}.  

{\it\noindent Also, any researchers with recent papers or surveys are encouraged to
contact that address to arrange for their papers to be made available
by ftp.}}

\section{Introduction and Problem Definitions}

The {\it Satisfiability Problem (SAT)} and its close relative, the
{\it Maximum Satisfiability Problem (MAX--SAT)} are central problems
in artificial intelligence, logic, and computational complexity.
These problems can be defined as follows:

A boolean {\it variable} $x$ is a variable that can assume only the
values {\it true} or {\it false} (sometimes denoted 1 or 0
respectively).  A boolean formula is a combination of boolean
variables using the logical connectives {\it not} ($\bar{x}$), {\it
or} ($\vee$), and {\it and} ($\wedge$).  A variable or a negation of a
variable is called a {\it literal}.  A disjunction of literals is
called a {\it clause}.

Given a set of clauses $C_1, C_2,\ldots, C_m$ on the variables $x_1,
x_2, \ldots, x_n$, the satisfiability problem is to determine if the
formula

$$C_1\wedge C_2\wedge\ldots\wedge C_m$$

\noindent is satisfiable.  That is, is there an assignment of values to the
variables so that the above formula evaluates to {\it true}.  Clearly,
this requires that each $C_j$ evaluate to {\it true}.

The maximum satisfiability problem is to find an assignment of values
to the variables so that the largest number of clauses evaluate to
{\it true}.

\section{Suggested Readings}

Both SAT and MAX--SAT have a large literature.  Here we simply list a
few of the relevant papers according to a rough classification
scheme.  These papers provide many pointers to other papers and areas
of interest.  A more detailed review is in preparation.

{\bf SAT: Symbolic and Heuristic Methods.} Since artificial
intelligence is a large generator of SAT problems, it is not
surprising that symbolic methods have been generated to solve these
problems.  The best known of these is Robinson's resolution algorithm
(\cite{Ro65}, though see
\cite{Lo78} for some refinements and additional description).  The
most widely known variant is that of Davis and Putnam \cite{DaPu60}.
Most large expert systems seem to use heuristic solution methods
(\cite{BaFe82}).  One heuristic approach, based on local search, is
that of Selman, Levesque and Mitchell \cite{SLM92} (available in the
ftp directory {\tt pub/challenge/sat/contributed/selman}).

{\bf SAT: Mathematical Programming Methods.} A wonderful exposition of
using such mathematical programming techniques as cutting planes and
branch and bound is Hooker \cite{Ho88}.  This work summarizes a large
number of other papers and gives an overview of the field suitable for
someone trained in mathematical programming.  Other relevant papers
include Jeroslow and Wang \cite{JeWa90} and Hooker \cite{Ho88b}.  Kamath
et. al. \cite{KKRR90} apply interior point methods to the problem and
report some computational results.

{\bf SAT: Solvable Special Cases.} There are a number of known special
cases that can be solved quickly.  These include 2--satisfiability
(each clause has at most two literals), Horn systems (that have at
most one non--negated variable per clause), hidden Horn systems (that
are Horn after suitable definitions of the variables) and so on.  In
all these cases, not only are there polynomial algorithms for
satisfiability, but there are extremely fast algorithms (often
linear).  Methods for these problems have been used as heuristics for
unstructured problems (for instance, chaining methods that work for
Horn systems are also used for more general systems, see \cite{Ni80}).

{\bf SAT: Probabilistic Results.}  There are a number of results about
the likelihood of randomly generated problems being solvable as well
as the likely performance of algorithms on such problems.  Some
suggested papers are Franco \cite{Fr86}, Franco and Paull
\cite{FrPa83}, and Chv\'atal and Reed \cite{ChRe92}.  A discussion of
how to generate hard random problems is given in Mitchell, Selman, and
Levesque \cite{MSL92} (available in the ftp directory
{\tt pub/challenge/sat/contributed/selman}).


{\bf MAX--SAT: Heuristic Techniques.}  Hansen and Jaumard
\cite{HaJa90}  have a recent paper that does a nice job of summarizing
heuristics available for MAX--SAT.  In addition to reviewing work on
the general problem, they also review heuristics for the case when
there are just two literals per clause (MAX--2--SAT).  The also
examine some local search schemes including a variation on simulated
annealing.  The heuristic method of Selman et. al. \cite{SLM92} is
actually a local search method for solving MAX--SAT (with a particular
emphasis on cases where all clauses can be satisfied).

{\bf MAX--SAT: Worst Case Bounds.} It is possible to find a solution
to MAX--SAT that is within a constant bound of optimal (that is, is
guaranteed to find a truth assignment that satisfies at least a
constant number times the optimal number of clauses.  Yannakakis
\cite{Ya92} gives an algorithm that has a guaranteed ratio of 3/4.
Arora et. al. \cite{ALMSS92} show that there is some threshold $c < 1$
such that no polynomial time algorithm can guarantee a solution
satisfying at least $c$ times the optimal number of clauses.


\section{Suggested Projects}

There are a many directions computational--oriented research could go.
Here are a number of suggestions.

\begin{enumerate}

\item Construct interesting test beds.  One idea is to use NP-completeness
transformations, from, for example, from graph coloring and clique,
the other problems covered by this Challenge.

\item Examine practical instances.  SAT and MAX--SAT are reputed to
have many applications, but there is only a limited number of real
instances available.  Expert systems and other logic machines should
be generating many, many instances.  Do these instances ``look''
different from random problems?  Are such instances easier or harder
to solve in practice?  Can aspects of such instances be embedded in
random generators to allow for generating larger random instances.?  Are
there applications that ``typically'' generate very hard instances?

\item Find an application that yields "easy" instance in practice, and test
behavior of exact algorithms on very large instances of this type.

\item  Explore the question of satisfiability/non-satisfiability for
various types of random k-SAT instances.  There is already a fair
amount of research on this subject, but a computational approach may
provide insights that are not yet noticed.

\item  Examine heuristics for MAX-SAT.  Here there is a substantial theory,
but perhaps less experimental data.  How much better than worst-case
are these in practice?

\item  Selman and others have had reasonable success with local search.
Can you do better with simulated annealing, tabu search and other
variations?

\item  Test how best to use various parallel architectures to speed up the
search in exact algorithms.

\item  Develop new algorithms for (exact) satisfiability, and test them.

\item  Compare LP and interior point approaches with other more
traditional approaches.  One approach suggested in Hooker \cite{Ho88}
is to replace general purpose linear programming codes with a
specialized code that exploits the structure inherent in
satisfiability problems.

\item Examine mathematical programming techniques for MAX--SAT.  While
computational approaches to SAT have received a lot of attention
recently, little work has yet been published on similar methods for
MAX--SAT.  Are similar approaches too much the same to be interesting
or are there some interesting variations?

\end{enumerate}
%
% If you want to use BibTeX, using the file satreview.bib for
% references, uncomment the next three lines and remove the current
% bibliography. 

%\nocite{*}
%\bibliographystyle{plain}
%\bibliography{satreview}
\begin{thebibliography}{10}

\bibitem{ALMSS92}
S.~Arora, C.~Lund, R.~Motwani, M.~Sudan, and M.~Szegedy.
\newblock Proof verification and hardness of approximation problems.
\newblock In {\em Proceedings 33rd {IEEE} {S}ymposium on the {F}oundations of
  {C}omputer {S}cience}, pages 14--23, Los Angeles, CA, 1992. IEEE Computer
  Society.

\bibitem{BaFe82}
A.~Barr and E.A. Feigenbaum.
\newblock {\em The Handbook of Artificial Intelligence}.
\newblock William Kaufman, 1982.

\bibitem{ChRe92}
Vasek Chv\'atal and Bruce Reed.
\newblock Mick gets some (the odds are on his side).
\newblock In {\em Proceedings on the Foundations of Computer Science},
  Pittsburgh, 1992.

\bibitem{DaPu60}
M.~Davis and H.~Putnam.
\newblock A computing procedure for quantification theory.
\newblock {\em Journal of the {ACM}}, 7:201--215, 1960.

\bibitem{Fr86}
John Franco.
\newblock On the probabilistic performance of algorithms for the satisfiability
  problem.
\newblock {\em Information Processing Letters}, 23:103--106, 1986.

\bibitem{FrPa83}
John Franco and M.~Paull.
\newblock Probabilistic analysis of the davis putnam procedure for solving the
  satisfiability problem.
\newblock {\em Discrete Applied Mathematics}, 5:77--87, 1983.

\bibitem{HaJa90}
Pierre Hansen and Brigitte Jaumard.
\newblock Algorithms for the maximum satisfiability problem.
\newblock {\em Computing}, 44:279--303, 1990.

\bibitem{Ho88}
John~N. Hooker.
\newblock A quantitative approach to logical inference.
\newblock {\em Decision Support Systems}, 4:45--69, 1988.

\bibitem{Ho88b}
John~N. Hooker.
\newblock Resolution vs. cutting plane solution of inference problems: Some
  computational results.
\newblock {\em Operations Research Letters}, 7:1--7, 1988.

\bibitem{JeWa90}
Robert~E. Jeroslow and J.~Wang.
\newblock Solving propositional satisfiability problems.
\newblock {\em Annals of Mathematics and AI}, 1:167--187, 1990.

\bibitem{KKRR90}
A.P. Kamath, N.K. Karmarkar, K.G. Rmakrishnan, and M.G.C. Resende.
\newblock Computational experience with an interior point algorithm on the
  satisfiability problem.
\newblock {\em Annals of Operations Research}, 25:43--58, 1990.

\bibitem{Lo78}
D.W. Loveland.
\newblock {\em Automated Theorem Proving: A Logical Basis}.
\newblock North--Holland, 1978.

\bibitem{MSL92}
David Mitchell, Bart Selman, and Hector Levesque.
\newblock Hard and easy distributions of {SAT} problems.
\newblock In {\em Proceedings of the Tenth National Conference on Artificial
  Intelligence ({AAAI}--92)}, San Jose, CA, 1992.

\bibitem{Ni80}
N.J. Nilsson.
\newblock {\em Principles of Artificial Intelligence}.
\newblock Tioga Publishing Company, 1980.

\bibitem{Ro65}
J.A. Robinson.
\newblock A machine--oriented logic based on the resolution principle.
\newblock {\em Journal of the ACM}, 1965:23--41, 1965.

\bibitem{SLM92}
Bart Selman, Hector Levesque, and David Mitchell.
\newblock A new method for solving hard satisfiability problems.
\newblock In {\em Proceedings of the Tenth National Conference on Artificial
  Intelligence ({AAAI}--92)}, San Jose, CA, 1992.

\bibitem{Ya92}
Mihalis Yannakakis.
\newblock On the approximation of maximum satisfiability.
\newblock In {\em Proceedings of the Third {ACM--SIAM} Symposium on Discrete
  Algorithms}, pages 1--9, 1992.

\end{thebibliography}

\end{document}