\documentstyle{article}
\textheight 23.0cm
\textwidth  16.0cm
\topmargin -0.18in
\oddsidemargin 0.5in
\evensidemargin 0.5in
\begin{document}

\centerline{\Large\bf Announcement and Call for Participation:}
$\newline$
\centerline{\Large\bf The International Competition on SAT Testing}
$\newline$
\centerline{\bf March 15--17, 1996, Beijing, China}
$\newline$

\begin{enumerate}
\item {\large\sl Goals} 

The goal of this competition is to evaluate and compare the performance of 
the latest SAT procedures, and to provide a forum for academic exchange on the
SAT problem.

\item {\large\sl General Information and Policy}

\begin{itemize}

\item This competition is sponsored by China's "863" High-Tech R\&D Project for
Intelligent Computing Systems.

\item The basic unit of participation in the competition is a {\it team}.
Each team has one or more members. 

\item Each team should notify at least one of the Competition co-chairs
by JANUARY 31st, 1996 of their intention to participate.

\item the competition will be held from 9am March 15, 1996 to 6pm March 17, 
1996, in Beijing, China. Teams with at least one member present at the
competition site will be given preference, and remote participation is also
allowed. (The total number of places is limited by the available machine resources. 
We expect to have room for about 20 teams.) The registration and submission of
 executable programs must be done by 9am, March 15.

\item At the start of the competition, each team must submit a description of
its procedures. Each team will be given an opportunity to present a description
 of its approach at the workshop.

\item In order to keep a balance among different approaches towards solving 
the SAT problem, the following three parts of benchmarks will be provided at
the competition: (1) randomly generated 3SAT instances; (2) industrial instances--I
and (3) industrial instances--II. For benchmarks of part (1), the random seeds
are randomly determined, and the source code of the generator will be released
at Dec. 1st, 1995. Benchmarks of part (2) will not be released until the beginning
of the competition, but similar instances will be avalable by Dec. 1st.
Benchmarks of part (3) will be released at Dec. 1st, 1995, with variables and
clauses reordered by randomly generated permutations at th beginning of the
competition. Each team can submit different procedures for different types of
benchmarks. 

\item The executables of the winning programs with a description of the
approach will be made available via anonymous ftp at the end of the competition.
The winning teams will also be invited to submit a paper on their approach to the
special journal issue devoted to the SAT Symposium.

\item The competition will be notarized by a notary public office.
\end{itemize}

\item {\large\sl Environments}

\qquad The competition will be performed on several SUN Sparc 20 
WorkStations (80 MIPS, 32M memory and UNIX Operating System). 
The control program will start each program sequentially, and
ensure that each program is excecuted in the same environment.

\item {\large\sl Further Information}

For further information, contact James Crawford at jc@cs.uoregon.edu and
DingXin Wang at dcswdx@tsinghua.edu.cn
\end{enumerate}
\end{document}