%Fred Annexstein (fred@annexstein.csm.uc.edu - contact author),
%John Franco (franco@franco.csm.uc.edu - alternate contact author),
%R. Swaminathan (swamy@jupiter.csm.uc.edu)
%University of Cincinnati
%Computer Science Department
%Cincinnati, OH 45221-0008
%==============================proposal==========================
\documentstyle[12pt]{article}
\title{
Distributed Implementation of Algorithms for Satisfiability Problems
}
\author{
Fred S. Annexstein\\
John V. Franco\\
R. Swaminathan\\
\\
{\it Department of Computer Science}\\
{\it University of Cincinnati}\\
{\it Cincinnati, OH 45221-0008}\\
}
\parskip 6pt
\topmargin -.5in
\textheight 8.5in
\textwidth 6in
\oddsidemargin .15in
\evensidemargin .15in
\begin{document}
\maketitle

\section{\bf Introduction}
We shall be concerned with distributed implementations of algorithms for
Satisfiability problems (SAT) in commonly available networked environments.
These days, a typical industrial, research laboratory, or
university site has dozens of Sparc Stations or DOS machines on LANs.  Such
networks represent great computational power that is often underused,
especially after hours.  Moreover, the future promises to add more
communication power, for example, high-bandwidth networks, in addition
to increased computational power, but probably with little special software for
distributed computing.  It would not surprise us if UNIX and X windows will
become the backbone operating system for most sites.  Although UNIX may have
the capacity to allow a user to distribute load to other sites (with
permission) by means of a special language, we do not foresee that it will
perform such functions automatically.  The proposed research aims at
gaining insight into the performance of distributed solutions to propositional
SAT in a garden-variety environment of networked UNIX workstations.

For a given SAT problem, we will harness unused distributed power using
the {\it shotgun approach}, that is, 
initially assigning different algorithms to different machines and then,
over time, reallocating machine cycles to give priority to the more promising
algorithms.  The nature of the resulting communication is oriented more
toward performance monitoring than computational requests and results;
we expect such communication to be more efficient than the type of
communication resulting from exclusively decomposing the computation of
one algorithm over many machines.  It is natural to try the above approach
on SAT because there are so many different algorithms for SAT.  The
performance of these algorithms depends heavily on properties of a given
problem instance, but the relationship between performance and properties
is not yet well understood.  Hence, experimenting with the shotgun approach
is justified.

The goals of our study are to answer the following questions:
\begin{itemize}
\item Are algorithms for SAT communication bound or computation bound?
\item Are there good evaluators for determining how far away the search is
from a solution?
\item Are there scalable parallel algorithms for SAT?
\item How well does the workstation-network environment support distributed
solutions to combinatorial problems such as SAT?
\end{itemize}

\section{\bf Algorithms}

As much as possible we shall try to include algorithms which exhibit
{\it orthogonality} with respect to performance.  The hope is that at least
one of a collection of such algorithms finds a solution to a given instance
of SAT quickly.  Orthogonality seems to depend somewhat on instance
properties such as the degree to which an instance is satisfiable or
unsatisfiable and structural properties of a given CNF instance.
In this framework, we start our investigation with two algorithms: a version of
the Davis-Putnam-Procedure (DPP) using the heuristic studied by Johnson in
1974 and a version of Bryant's algorithm.  We include DPP because analytic
and experimental results, including those from a recent contest held
in Paderborn, Germany, suggest that DPP is useful on instances of SAT which
are probably satisfiable.   In contrast, Bryant's algorithm is designed for
logic verification and so, is probably more useful in verifying
unsatisfiability.  As the project continues, we expect to add other algorithms
to the collection.

\section{\bf Hardware and Distributed Languages}

We will experiment with our faculty's SUN network consisting of 14 Sparc
IPC workstations connected by ethernet.  Two public domain distributed
languages are currently implemented on this network: a public domain version
of C-LINDA called POSYBL, and PCN.  POSYBL provides a high degree of 
control over the inter-node communication using a small number of language
primitives: the programmer designs POSYBL fragments explicitly.  On the
other hand, PCN provides a more professional programming environment: it is
actually a compiler of a high-level parallel language (the PCN language)
to object code and distributes control code automatically.  Although
there are public domain languages other than POSYBL and PCN available,
these appear to be harder to use, so we will refrain from investigating these
for now.

\section{\bf Qualifications of the Authors}

Fred Annexstein has published several papers in the area of distributed and
parallel computing.  He is mainly interested in emulations among
fixed-connection networks.  John Franco has extensive experience in the
probabilistic analysis of algorithms for the Satisfiability problem and
has published numerous papers on this subject.  R. Swaminathan is an expert
in combinatorial optimization and graph theory.  Some of his results on
graph-realization problems connect Satisfiability with graph theory.

\end{document}