\documentstyle[12pt]{article}
\setlength{\topmargin}{-.5in}
\addtolength{\textheight}{1.5in}
\addtolength{\textwidth}{\evensidemargin}
\addtolength{\textwidth}{\oddsidemargin}
\setlength{\oddsidemargin}{.25in}
\setlength{\evensidemargin}{.25in}
\addtolength{\textwidth}{-1.0\oddsidemargin}
\addtolength{\textwidth}{-1.0\evensidemargin}
\begin{document}
\setlength{\baselineskip}{20pt}

\title{
Solving the Satisfiability Problem on an MIMD Computer}
\author{ 
Wei-Chieh Lee, Wen-Jer Wu and Chuan-Yi Tang\\
\\
Institute of Computer Science \\
National Tsing Hua University, Hsinchu, Taiwan\\
e-mail: {\tt cytang@cs.nthu.edu.tw}
} 
\date{December 31, 1992}

\maketitle 

\noindent {\it We shall implement an MIMD program in hypercube 
architecture to solve satisfiability (SAT) problem.}

\section{Introduction}

We select the implementation of a parallel algorithm for the 
SAT problem on hypercube to participate the Implementation Challenge. 
There are three main characteristics in our implementation:
\begin{enumerate}
  \item Based upon branching technique and using {\bf autark} 
        property to prevent unnecessary expansions [1].
  \item Dividing work load evenly during startup time.
  \item Using dynamic load balancing technique to balance work load
        during subsequent execution [2] [3].
\end{enumerate}
Our goal is to gain good speedup and high scalibility [3]. The following 
three sections will be organized to describe the three main 
characteristics in detail, and our current status will be given 
in the last section.


\section{Branching Technique}

Let $F$ be a formula which contains clauses $C_{i}=X_{1}\vee X_{2} 
\vee\cdots\vee X_{l}$ for $i=1,2,\ldots ,n$ , where 
$X_{i} (1\leq i\leq l)$ is a literal. We can split $F$ into the following 
$l$ formulas $F_{1},F_{2}, \ldots ,F_{l}$, which can be solved by checking
if the following $k$th assignments satisfy $F_{k}$ :

\begin{verse}
$F_{1}:X_{1}=true$\\
$F_{2}:X_{1}=false,X_{2}=true$\\
$\vdots$ \\
$F_{l}:X_{1}=\cdots =X_{l-1}=false,X_{l}=true$\\
\end{verse}

For the above $l$ assignments, if there exists an assignment such that 
every clause in $F$ is either made true by this assignment or does not
contain the same literals, we call this assignment an {\bf autark}
. Using autark property, $F$ can be solely reduced to $F_{i}$ 
that is computed from this assignment, and thus needn't to expand 
another $l-1$ branchs. Surely, if there exists no {\bf autark} truth
assignment, $l$ branchs are necessary [1].


\section{Divide Initial Work Load}

How to divide initial work load evenly for all processors is always 
a headache. Taking long time to saturate all processors will lead to 
poor speedup and low scalibility, especially when numerous processors 
are applied.
\paragraph{}
We design a heuristic method to distribute work load among processors
in hypercube more evenly. The following is a brief description:
\begin{verse}
Let $n$ be the dimension number of hypercube we use. We can 
represent each processor id as an $n$-digit binary number. And we can 
make use of these $n$ binary digits as the initial assignment, 
say $0$ for $false$ and $1$ for $true$, for binding the 
first $n$ heavy used literals. 
\end{verse}
This method is rather simple, but it works fine especially when 
communication or broadcasting is expansive. There are still 
problems in this method, some processors will discover the initial
assignment unsatisfiable and stop execution very quickly. The
compensative solution will be dynamic load balancing or find the
better $n$ literals for inital assignments. 


\section{Dynamic Load Balancing}

During execution there will be some processors that find unsatisfiability
very quickly and stop execution. If we let them idle, time will be 
wasted. So we would like to design a protocol for sharing work load 
among processors. Initially, we wish to adopt the load balancing concepts 
presented in [3]. The basic ideas are:
\begin{itemize}
  \item Partition work load within a processor into sharable 
        pieces that can be done independently by another processor, and
  \item Design a protocol for exchange information and work pieces.
\end{itemize}
The first item is easy to achieve by using the stack elements, but 
the second is more complexity.


\section{Current Status}

We have already completed this program with the first two characteristics,
and are planning to add the dynamic load balancing recently. This program 
works fine and correctly.


\section{References}

\begin{enumerate}
  \item[[1]] B. Monien and E. Speckenmeyer, {\it Solving Satisfiability
              in Less Than $2^{n}$ Steps}, Discrete Applied Mathematics 10
              (1985) 287-295
  \item[[2]] Ananth Y. Grama, Vipin Kumar and Vemparty Nageshwara Rao,
             {\it Experimental Evaluation of Load Balancing Techniques
             for The Hypercube}, Parallel Computing '91, 497-514

  \item[[3]] R. L\"{u}ling and B. Monien, {\it Load Balancing for Distributed 
             Branch \& Bound Algorithm}, International Parallel Processing
             Symposium (IPPS-92)
\end{enumerate}

\end{document}