%\documentstyle[epsf,12pt]{article} 
\documentclass[11pt]{article} 

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{algorithm}[theorem]{Algorithm}
\newtheorem{procedure}[theorem]{Procedure}
\newtheorem{conjecture}[theorem]{Conjecture}

\newenvironment{oldtheorem}[1]{\smallskip\noindent{\bf Theorem #1}\em}{}
\newenvironment{oldlemma}[1]{\smallskip\noindent{\bf Lemma #1}\em}{}
\newenvironment{oldproposition}[1]{\smallskip\noindent{\bf Proposition #1}\em}{}
\newenvironment{oldcorollary}[1]{\smallskip\noindent{\bf Corollary #1}\em}{}
\newenvironment{oldalgorithm}[1]{\smallskip\noindent{\bf Algorithm #1}\em}{}
\newenvironment{oldprocedure}[1]{\smallskip\noindent{\bf Procedure #1}\em}{}

\newcommand{\dblspace}{\baselineskip=19.3pt}
\newcommand{\nodblspace}{\baselineskip=\normalbaselineskip}

%this defines that little box at the end of proofs.
%\def\square{\vrule height6pt width6pt depth0pt}
\def\sqr#1#2{{\vcenter{\hrule height.#2pt
      \hbox{\vrule width.#2pt height#1pt \kern#1pt
	\vrule width.#2pt}
     \hrule height.#2pt}}}
\def\square{\mathchoice\sqr34\sqr34\sqr{2.1}3\sqr{1.5}3}
\def\proofend{\mbox{\nobreak\qquad$\square$\medskip}}
\def\endproof{\vrule height6pt width6pt depth0pt}

%this defines the (single-spaced, not indented) proofs.
\def \proof{\noindent{\bf Proof.}\enspace}

%here are some mathematical symbols
\def\emptyset{{\hbox{\rm \O}}}
\def\set#1{\{#1\}}
\newcommand{\type}[1]{\mbox{\tt #1}}
\def\powset{{\cal P}}

\newcommand{\codesize}{\footnotesize}

\newcommand{\eq}[1]{(\ref{e.#1})}
\newcommand{\chap}[1]{Chapter~\ref{c.#1}}
\newcommand{\secn}[1]{Section~\ref{s.#1}}
\newcommand{\fig}[1]{Figure~\ref{f.#1}}
\newcommand{\defn}[1]{Definition~\ref{d.#1}}
\newcommand{\thm}[1]{Theorem~\ref{t.#1}}
\newcommand{\tab}[1]{Table~\ref{t.#1}}
\newcommand{\prop}[1]{Proposition~\ref{p.#1}}
\newcommand{\lem}[1]{Lemma~\ref{l.#1}}
\newcommand{\cor}[1]{Corollary~\ref{c.#1}}
\newcommand{\alg}[1]{Algorithm~\ref{a.#1}}
\newcommand{\proc}[1]{Procedure~\ref{p.#1}}
\newcommand{\prc}[1]{Procedure~\ref{p.#1}}
\newcommand{\lin}[1]{line~\ref{l.#1}}

\usepackage{jair}
\usepackage{theapa}
%\usepackage{twoside}
\usepackage{clrscode}
\usepackage{graphics}
\usepackage{graphicx}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{requirement}[theorem]{Requirement}

\jairheading{21}{2004}{193-243}{09/03}{02/04}
\ShortHeadings{Boolean Satisfiability Survey}
{Dixon, Ginsberg \& Parkes}
\firstpageno{193}

\begin{document}

\title{Generalizing Boolean Satisfiability I: Background and Survey of
Existing Work}

\author{\name Heidi E. Dixon \email dixon@cirl.uoregon.edu \\
       \addr CIRL \\
       Computer and Information Science \\
       1269 University of Oregon \\
       Eugene, OR  97403 USA
       \AND
       \name Matthew L. Ginsberg \email ginsberg@otsys.com \\
       \addr On Time Systems, Inc. \\
       1850 Millrace, Suite 1 \\
       Eugene, OR  97403 USA
       \AND
       \name Andrew J. Parkes \email parkes@cirl.uoregon.edu \\
       \addr CIRL \\
       1269 University of Oregon \\
       Eugene, OR  97403 USA}

\newcommand{\bs}{Boolean satisfiability}
\newcommand{\up}{unit propagation}
\newcommand{\Up}{Unit propagation}
\newcommand{\php}{pigeonhole problem}
\newcommand{\pb}{pseudo-Boolean}
\newcommand{\Pb}{Pseudo-Boolean}
\newcommand{\dpll}{{\sc dpll}}
\newcommand{\qprop}{{\sc qprop}}
\newcommand{\zchaff}{{\sc zChaff}}
\newcommand{\prs}{{\sc prs}}
\newcommand{\Prs}{{\sc Prs}}
\newcommand{\pbchaff}{{\sc pbchaff}}
\newcommand{\Pbchaff}{{\sc Pbchaff}}
\newcommand{\zap}{{\sc zap}}
\newcommand{\Zap}{{\sc Zap}}
\newcommand{\wsat}{{\sc wsat}}
\newcommand{\wsatu}{{\sc wsat(U)}}
\newcommand{\wsatub}{{\sc wsat(UB)}}
\newcommand{\Wsat}{{\sc Wsat}}
\newcommand{\csp}{{\sc csp}}
\newcommand{\asp}{{\sc asp}}
\newcommand{\sat}{{\sc sat}}
\newcommand{\Sat}{{\sc Sat}}
\newcommand{\solve}{\type{solve}}
\newcommand{\unit}{\type{unit-propagate}}
\newcommand{\true}{\type{true}}
\newcommand{\false}{\type{false}}
\newcommand{\pbar}{\overline p}
\newcommand{\xbar}{\overline x}
\newcommand{\lbar}{\overline l}
\newcommand{\curr}{\type{curr}}
\newcommand{\poss}{\type{poss}}
\newcommand{\mod}{\mbox{\rm mod}}
\newcommand{\floor}[1]{\lfloor #1 \rfloor}
\newcommand{\at}{\type{at}}
\newcommand{\duration}{\type{duration}}
\newcommand{\between}{\type{between}}
\newcommand{\learn}{\type{learn}}
\newcommand{\plane}{\type{aboard}}
\newcommand{\ploc}{\type{plane-at}}


\maketitle

\begin{abstract}
  This is the first of three planned papers describing \zap, a
satisfiability engine that substantially generalizes existing tools
while retaining the performance characteristics of modern
high-performance solvers.  The fundamental idea underlying \zap\ is
that many problems passed to such engines contain rich internal
structure that is obscured by the Boolean representation used; our
goal is to define a representation in which this structure is apparent
and can easily be exploited to improve computational performance.
This paper is a survey of the work underlying \zap, and discusses
previous attempts to improve the performance of the
Davis-Putnam-Logemann-Loveland algorithm by exploiting the structure
of the problem being solved.  We examine existing ideas including
extensions of the Boolean language to allow cardinality constraints,
\pb\ representations, symmetry, and a limited form of quantification.
While this paper is intended as a survey, our research results are
contained in the two subsequent articles, with the theoretical
structure of \zap\ described in the second paper in this series, and
\zap's implementation described in the third.
\end{abstract}

\section{Introduction}

This is the first of a planned series of three papers describing \zap,
a satisfiability engine that substantially generalizes existing tools
while retaining the performance characteristics of modern
high-performance solvers such as \zchaff~\cite{zchaff}.\footnote{The
second two papers have been published as technical reports
\cite{Ginsberg:zap2,Ginsberg:zap3} but have not yet been peer
reviewed.}  Many \bs\ problems incorporate a rich structure that
reflects properties of the domain from which the problems themselves
arise, and \zap\ includes a representation language that allows this
structure to be described and a proof engine that exploits the
structure to improve performance.  This first paper describes the work
on which \zap\ itself is based, and is intended to be a survey of
existing results that attempt to use problem structure to improve the
performance of satisfiability engines.  The results we discuss include
generalizations from \bs\ to include cardinality constraints, \pb\
representations, symmetry, and a limited form of quantification.  The
second paper in this series~\cite{Ginsberg:zap2} describes the
theoretical generalization that subsumes and extends these ideas, and
the third paper~\cite{Ginsberg:zap3} describes the \zap\ system
itself.

Our intention is to review work on satisfiability from the
introduction of the Davis-Putnam-Logemann-Loveland algorithm
\cite{DPLL} to the present day.  Not all of this work (thankfully),
but only that portion of the work that can be thought of as an attempt
to improve the performance of systematic methods by exploiting the
general structure of the problem in question.

We therefore include a description of recent work extending the
language of \bs\ to include a restricted form of quantification
\cite{Ginsberg:qprop} or \pb\ constraints
\cite{Barth:pseudo,Barth:01,Chandru:logic_book,Dixon:AIOR,Hooker:genres,OR:cut};
in each case, the representational extension corresponds to the
existence of structure that is hidden by the Boolean axiomatization.
We discuss at length the interplay between the desire to speed search
by exploiting structure and the danger of slowing search by using
unwieldy representations.  Somewhat surprisingly, we will see that the
most effective representational extensions appear to incur little or
no overhead as a result of implementation concerns.  It was this
observation -- that better representations can have better
implementations -- that led us to search for the general sort of
structure that \zap\ exploits.

We will also discuss the attempts that have been made to exploit the
symmetrical structure of some satisfiability problems
\cite{Brown:symmetry,Crawford:symmetry,Ginsberg:symmetry,Joslin:symmetry,krish:symmetry,Puget:symmetry}.
This work appears to have had only a modest impact on the development
of satisfiability engines generally, and we explain why: Most authors
\cite{Crawford:symmetry,Ginsberg:symmetry,Joslin:symmetry,krish:symmetry,Puget:symmetry}
exploit only global symmetries, and such symmetries are vanishingly
rare in naturally occurring problems.  The methods that have been
described for exploiting local or emergent symmetries
\cite{Brown:symmetry,Szeider:symmetry} incur unacceptable
computational overhead at each node of the search.  Our general
arguments regarding the interplay between representation and search
suggest that one should identify local symmetries when a problem is
formulated, and then exploit those symmetries throughout the search.

We will {\em not\/} discuss heuristic search or any of the substantial
literature relating to it.  To our collective eye, just as a Boolean
axiomatization can obscure the natural structure in a search problem,
so can heuristics.  We have argued elsewhere \cite{Ginsberg:metalevel}
that domain-dependent search control rules can never be more than a
poor man's standin for general principles based on problem structure.
Our selection of survey material reflects this bias.

We have remarked that this entry in the \zap\ series is a survey
paper; to the extent that there is a research contribution, it is in
the overall (and, we believe, novel) focus we are taking.  Our basic
view is that the target of new work in this area should not be a
specific representational extension such as a \pb\ or first-order
encoding, but a direct exploitation of the underlying problem
structure.  This paper is original in describing existing work in this
way, for the first time viewing the first-order and \pb\ extensions
purely as structure-exploitation techniques.  First-order and \pb\
representations are effective not because of their history of
usefulness, but because -- and to our mind {\em only\/} because --
they allow the identification and capture of two particular types of
structure inherent in many classes of problems.  It is our hope that
the reader views the material we are presenting here (and in the
companion papers as well) in this light: Recent progress in \bs\ is
best thought of in terms of structure exploitation.  That is the
perspective with which we approach this paper, and we hope that you,
the reader, will come to share it.

\bigskip

But let us return to the Davis-Putnam-Logemann-Loveland procedure
itself~\cite{DPLL}, which appears to have begun the body of work on
the development of solvers that are sufficiently powerful to be used
in practice on a wide range of problems.  Descendants of the \dpll\
algorithm are now the solution method of choice on many such problems
including microprocessor testing and verification
\cite{Biere:verify,sat-mtv,Velev:verify}, and are competitive in other
domains such as planning \cite{satplan}.

We will return to the pure algorithmics of \dpll\ and its successors
shortly, but let us begin by noting that in spite of impressive
engineering successes on many difficult problems, there are many {\em
easy\/} problems with which \bs\ engines struggle.  These include
problems involving parity, the well known ``\php'' (stating that you
cannot put $n+1$ pigeons into $n$ holes if each pigeon needs its own
hole), and problems that are described most naturally using a
first-order as opposed to a ground representation.

In all of these cases, there is structure to the problem being solved
and this structure is lost when the ground encoding is built.  While
it is a testament to the power of Boolean methods that they can solve
large and difficult problems without access to this underlying
structure, it seems reasonable to expect that incorporating and using
the structure would improve performance further.  Our survey of
techniques that improve \dpll\ will suggest that this is in fact the
case, since all of the techniques that underpin the performance of
modern \bs\ engines can be well understood in this way.

Before turning to the details of this analysis, however, let us flesh
out our framework a bit more.  If {\em any\/} computational procedure
is to have its performance improved, there seem to be only three ways
in which this can be done:
\begin{enumerate}
\item Replace the algorithm.
\item Reduce the time spent on a single iteration of the inner loop.
\item Reduce the number of times the inner loop must be executed.
\end{enumerate}
 The first approach is not our focus here; while there are many
potential competitors to \dpll, none of them seems to outperform
\dpll\ in practice.\footnote{Systematic alternatives include the
original Davis-Putnam \citeyear{Davis-Putnam} method, polynomial
calculus solvers \cite{Clegg:Groebner} based on Buchberger's
\citeyear{Groebner65,Groebner85} Groebner basis algorithm, methods
based on binary decision diagrams or {\sc bdd}s
\cite{Bryant:bdd1,Bryant:bdd2}, and direct first-order methods such as
those employed by {\sc otter} \cite{Otter}.  Nonsystematic methods
include the \wsat\ family \cite{Selman:wsat}, which received a great
deal of attention in the 1990's and still appears to be the method of
choice for randomly generated problems and some specific other sets of
instances.  In general, however, systematic algorithms with their
roots in \dpll\ tend to outperform the alternatives.}  Work on the
second approach has historically focused on reducing the amount of
time spent in unit propagation, which does indeed appear to represent
the inner loop of most \dpll\ implementations.

There are a variety of techniques available for reducing the number
of calls to the inner loop, which we will divide as follows:
\begin{itemize}
\item[3a.] Algorithmic improvements that do not require
representational changes.
\item[3b.] Algorithmic improvements requiring representational
changes.
\end{itemize}
 Attempts to improve \dpll\ without changing the underlying Boolean
representation have focused on (i)~the development of a mechanism for
retaining information developed in one portion of the search for
subsequent use (caching or, more commonly, {\em learning}) and
(ii)~the development of search heuristics that can be expected to
reduce the size of the space being examined.  In all such work,
however, using \dpll\ to analyze problems where no solution exists is
equivalent to building a resolution proof of the unsatisfiability of
the underlying theory, so that the number of inference steps is
bounded by the number of inferences in the shortest such proof
\cite{Mitchell:hard}.  These lengths are generally exponential in
problem size in the worst case.

Work involving representation change can overcome this difficulty by
reducing the length of the proof that \dpll\ or a similar algorithm is
implicitly trying to construct.  Representations are sought for which
certain problems known to require proofs of exponential length in the
Boolean case admit proofs of polynomial length after the
representational shift is made.  This leads to a hierarchy of
representational choices, where one representation $r_1$ is said to
polynomially simulate or {\em $p$-simulate\/} another $r_2$ if proofs
using the representation $r_2$ can be converted to proofs using $r_1$
in polynomial time.  In general, representations that lead to
efficient proofs do so via more efficient encodings, so that a single
axiom in the improved representation corresponds to exponentially many
in the original.  There are many excellent surveys of the proof
complexity literature
\cite{Beame:complexity,Pitassi:complexity,urquhart:complexity}, and we
will generally not repeat that material here.

Of course, it is not sufficient to simply improve the epistemological
adequacy of a proof system; its heuristic adequacy must be maintained
or improved as well \cite{McCarthy77}.  We therefore assume that any
representation introduced for the purposes of navigating the
$p$-simulation hierarchy also preserves the basic inference mechanism
of \dpll\ (resolution) and maintains, and ideally builds upon, the
improvements made in propagation performance (2) and learning (3a).
It is in this context that our survey shall consider these
representational changes.

The representations that we will consider are the following:
\begin{itemize} 
\item Boolean axiomatizations.  This is the original representation
used in \dpll, and provides the basic setting in which progress in
propagation, learning and branching has taken place.
\item Cardinality constraints.  If a disjunctive Boolean axiom states
that at least one of the disjuncts is true, a cardinality constraint
allows one to state that at least $n$ of the disjuncts are true for
some integer $n$.
\item \Pb\ constraints.  Taken from operations research, a \pb\
constraint is of the form 
\[\sum_i w_i l_i \geq k\]
where the $w_i$ are positive integral weights, the $l_i$ are literals,
and $k$ is a positive integer.  Cardinality constraints are the
special case where $w_i = 1$ for all $i$; a Boolean constraint has
$k=1$ as well.
\item Symmetric representations.  Some problems (such as the
pigeonhole problem) are highly symmetric, and it is possible to
capture this symmetry directly in the axiomatization.  A variety of
authors have developed proof systems that exploit these symmetries to
reduce proof size
\cite{Brown:symmetry,Crawford:symmetry,Ginsberg:symmetry,Joslin:symmetry,krish:symmetry,Puget:symmetry}.
\item Quantified representations.  While there are many approaches to
quantified satisfiability, we will focus only on those that do not
change the underlying complexity of the problem being
solved.\footnote{Problems involving quantified Boolean formulae, or
{\sc qbf}, are {\sc pspace}-complete \cite{Cadoli:qbf} as opposed to
the {\sc np}-complete problems considered by \dpll\ and its direct
successors.}  This requires that all domains of quantification be
finite, and is the focus of a ``propositional'' restriction of
first-order logic known as \qprop~\cite{Ginsberg:qprop}.
\end{itemize}

Given the arguments regarding heuristic adequacy generally, our goal
in this survey is to complete the following table:

\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& {\bf representational} & {\bf p-simulation} && {\bf unit} & \\
& {\bf efficiency} & {\bf hierarchy} & {\bf inference} 
 & {\bf propagation} & {\bf learning} \\
\hline
\footnotesize\bf SAT &&&&& \\ 
\bf{cardinality} &&&&& \\
\bf{\pb} &&&&& \\
\bf{symmetry} &&&&& \\
\footnotesize\bf QPROP &&&&& \\
\hline
\end{tabular}
\end{center}

The first column simply names the representational system in question.
Then for each, we describe:
\begin{itemize}
\item Representational efficiency (3b): How many Boolean axioms can be
captured in a single axiom in the given representation?
\item $p$-simulation hierarchy (3b): Where is the representation
relative to others in the $p$-simulation hierarchy?
\item Inference: Is it possible to lift the basic \dpll\ inference
mechanism of resolution to the new representation without incurring
significant additional computational expense?
\item \Up\ (2): Can the techniques used to speed \up\ be lifted to the
new setting?  Are new techniques available that are not available in
the Boolean case?
\item Learning (3a): Can existing learning techniques be lifted to the
new setting?  Are new techniques available that are not available in
the Boolean case?
\end{itemize}

We cannot overstress the fact that no single column in our table is
more important than the others.  A reduction in proof length is of
little practical value if there is no associated reduction in the
amount of computation time required to find a proof.  Speeding the
time needed for a single inference is hardly useful if the number of
inferences required grows exponentially.

The \bs\ community has pioneered many techniques used to reduce
per-inference running time and to understand learning in a declarative
setting.  In spite of the fact that resolution and \bs\ are among the
weakest inference systems in terms of representational efficiency and
their position in the $p$-simulation hierarchy \cite{clique}, almost
none of the more powerful proof systems is in wide computational use.
Finding proofs in these more sophisticated settings is difficult; even
direct attempts to lift \dpll\ to a first-order setting
\cite{Baumgartner:fdpll} seem fraught with complexity and an inability
to exploit recent ideas that have led to substantial improvements in
algorithmic performance.  The most usable proof systems are often not
the theoretically most powerful.

This paper is organized along the rows of the table we are trying to
complete.  Boolean techniques are described in the next section; we
recount the demonstration that the \php\ is exponentially difficult in
this setting \cite{Haken}.  We go on in \secn{pseudo} to discuss
cardinality constraints and \pb\ methods, showing that the earlier
difficulties with the \php\ can be overcome using either method but
that similar issues remain in other cases.  Following the descriptions
of implemented \pb\ reasoning systems \cite{Barth:pseudo,Dixon:AIOR},
we show that the key computational ideas from the Boolean case
continue to be applicable in a \pb\ setting.

Axiomatizations that attempt to exploit symmetry directly are
discussed in \secn{symmetry}.  We draw a distinction between
approaches that require the existence of global symmetries, which tend
not to exist in practice, and those that use only local ones, which
exist but are difficult to find as inference proceeds.

In \secn{qprop}, we discuss axiomatizations that are Boolean
descriptions of problems that are more naturally represented using
quantified axioms.  We discuss the problems arising from the fact that
the ground theories tend to be exponentially larger than their lifted
counterparts, and show that working with the first-order
axiomatization directly can lead to large improvements in the
efficiency of the overall system~\cite{Ginsberg:qprop}.

Concluding remarks are contained in \secn{conclusion}.

\section{Boolean Satisfiability}
\label{s.bool}

\begin{definition} A {\em variable\/} is simply a letter (e.g., $a$)
that can be either true or false.  A {\em literal\/} is either a
variable or the negation of a variable.  A {\em clause\/} is a
disjunction of literals, and a {\em \bs\ problem (in conjunctive
normal form)}, or a \sat\ problem, is a conjunction of clauses.

A {\em solution\/} to a \sat\ problem $C$ is an assignment of values to
each of the letters so that every clause in $C$ is satisfied.  
 \end{definition}

None of this should be new.  Satisfiability of \sat\ instances is
well-known to be NP-complete~\cite{Cook:sat}, and the language is a
reasonably natural one for encoding real-world problems.  As we
remarked in the introduction, the classic algorithm for solving these
problems is depth-first search augmented with an ability to set
variables whose values are forced:

\begin{procedure}[Davis-Putnam-Logemann-Loveland]
Given a \sat\ problem $C$ and a partial assignment $P$ of values to
variables, to compute $\proc{dpll}(C,P)$:\em

\begin{codebox}
\li  $P \gets \proc{Unit-Propagate}(P)$
\li  \If $P$ contains a contradiction  
\li    \Then 
           \Return  \const{failure}
        \End

\li  \If $P$ assigns a value to every variable 
\li  \Then  \Return \const{success} 
     \End

\li  $l \gets $ a literal not assigned a value by $P$
\li  \If $\proc{dpll}(C,P \cup \set{l = \true}) = \const{success}$
\li  \Then \Return \const{success}
\li  \Else  \Return $\proc{dpll}(C,P \cup \set{l = \false})$
     \End
\end{codebox}
\label{p.dp}
\end{procedure}

Variables are assigned values in two ways.  In the first, \up, the
clause set is examined under the existing partial assignment and new
consequential assignments are identified.  Somewhat more specifically
(see below), clauses are found that have no satisfied literals and
exactly one unvalued literal.  In each such clause, the unvalued
literal is valued so as to satisfy the clause.  This process is
repeated until a contradiction is encountered, a solution is found, or
no more clauses meet the necessary conditions.  If the \up\ function
terminates without reaching a contradiction or finding a solution,
then a variable is selected and assigned a value, and the procedure
recurs.

In practice, the choice of branch literal is crucial to the
performance of the algorithm. (Note that by choosing a branch literal
$\neg l$ instead of $l$, we can also select the order in which values
are tried for the underlying variable.)  Relatively early work on
\dpll\ focused on the selection of branch variables that produced as
many \up s as possible, thus reducing the size of the residual
problems that had to be solved recursively.  As we will see in
\secn{branch}, however, more recent ideas appear to be more effective.

Missing from \prc{dp}, however, is a description of the propagation
process.  Here it is:

\begin{procedure}[\Up] To compute $\proc{Unit-Propagate}(P)$:\em
\begin{codebox}
\li \While no contradiction is found \kw{and} there is a $c\in C$ that
	 under $P$  \\
            has no satisfied literals and exactly  one unassigned literal 
\li \Do $v \gets $ the variable in $c$ unassigned by $P$
\li     $P \gets P \cup \{ v = V : \mbox{$V$ is selected so that $c$ 
	  is satisfied} \}$
	\End
\li \Return $P$
\end{codebox}
\label{p.unit}
\end{procedure}

{\sc Dpll} has a variety of well-known theoretical properties.  It is
sound and complete in that every candidate solution returned is a
solution of the original problem, and such a solution will be returned
if one exists (and failure eventually reported if no solution exists).

From a practical point of view, the running time of \dpll\ is
obviously potentially exponential in the size of the problem, since at
each iteration, possibly only a single variable is assigned a value
before the routine is invoked recursively.  In practice, of course,
\up\ can reduce the number of branch points substantially, but the
running time remains exponential on difficult instances
\cite{Crawford:exp}.

We also point out that on difficult problem instances, most of the
running time is necessarily spent exploring portions of the search
space in which there are no solutions.  After all, if $P$ is a partial
assignment that can be extended to a solution, the algorithm will
never backtrack away from $P$.  (Indeed, it cannot and retain
completeness, since $P$ may be the only variable assignment that
extends to a full solution at this point.)  Given that there can be no
backtrack away from a satisfiable partial assignment, and that the
number of backtracks is exponential in the problem size, it is clear
that most of the time spent by the program is indeed in evaluating
unsatisfiable regions of the search space.

\subsection{Unit Propagation: The Inner Loop}
\label{s.inner}

\begin{figure}[bt!]
\begin{center}
\scalebox{0.50}{\resizebox{\textwidth}{!}
	{\includegraphics{up-frac}}} % use epstopdf to make both versions!
  \vspace*{-5mm}
\end{center}
\caption{Fraction of CPU time spent in unit propagation}
\label{f.up-time}
\end{figure}

When the \dpll\ algorithm \ref{p.dp} is implemented and run on
practical problems, the bulk of the running time is spent in \up.  As
an example, \fig{up-time} gives the amount of time spent by \zchaff\
on a variety of microprocessor test and verification examples made
available by Velev ({\sf
http://www.ece.cmu.edu/\~{}mvelev}).\footnote{The examples used to
generate the graph are those solved by \zchaff\ within 100 seconds
using an Intel Pentium 4M running at 1.6GHz.  For those not solved
within the 100 second limit, an average of 89.4\% of the time was
spent unit propagating.}  As the problems become more difficult, an
increasing fraction of the computational resources are devoted to
unit propagation.  For this reason, much early work on improving the
performance of \dpll\ focused on improving the speed of \up.

Within the \up\ procedure \ref{p.unit}, the bulk of the time is spent
identifying clauses that propagate; in other words, clauses that are
not satisfied by the partial assignment and contain at most one
unvalued literal:

\begin{observation} Efficient implementations of \dpll\ typically
spend the bulk of their effort searching for clauses satisfying the
conditions required for \up.\label{o.1}\end{observation}

Before we go on to examine the techniques that have been used to speed
\up\ in practice, let us remark that other implementations of \sat\
solvers have similar properties.  Nonsystematic solvers such as \wsat\
\cite{Selman:wsat}, for example, spend the bulk of their time looking
for clauses containing no satisfied or unvalued literals (or,
equivalently, maintaining the data structures needed to make such
search efficient).  We can generalize Observation \ref{o.1} to get:

\begin{observation} Efficient implementations of \sat\ solvers
typically spend the bulk of their effort searching for clauses
satisfying specific syntactic conditions relative to a partial or
complete truth assignment.
\end{observation}
 While the focus of our survey is on systematic methods, we remark
that because of the similarity of the techniques used in \dpll\ and in
\wsat, techniques that speed the inner loop of one are likely to speed
the inner loop of the other as well.

That said, let us describe the series of ideas that have been employed
in speeding the process of identifying clauses leading to \up s:

\begin{enumerate}

\item After binding a variable $v$, examine each clause to determine
whether or not it satisfies the conditions of Procedure \ref{p.unit}.

\item Slightly more sophisticated is to restrict the search for a
suitable clause to those clauses $c\in C$ that include $\neg
v$ as one of the disjuncts (assuming that $v$ has been assigned the
value true).  After all, if $v$ appears in $c$, $c$ is satisfied after
$v$ is set to true; if $v$ is not mentioned in $c$ there can be no
change in $c$'s ability to unit propagate when $v$'s value is set.

\item When we set $v$ to true above, as we examine clauses containing
$\neg v$, we have to walk each such clause to determine just which
literals are satisfied (if any) and which are still unbound.  It is
more efficient to keep a record, for each clause $c$, of the number
$s(c)$ of satisfied and the number $u(c)$ of unbound literals.

In order to keep these counts current when we set a variable $v$ to
true, we need to increment $s(c)$ and decrement $u(c)$ for each clause
where $v$ appears, and to simply decrement $u(c)$ for each clause
where $\neg v$ appears.  If we backtrack and unset $v$, we need to
reverse these adjustments.

Compared to the previous approach, we need to examine four times as
many clauses (those where $v$ appears with either sign, and both when
$v$ is set and unset), but each examination takes constant time
instead of time proportional to the clause length.  If the average
clause length is greater than four, this approach, due to Crawford and
Auton \citeyear{Crawford:exp}, will be more effective than its
predecessor.

\item Currently, the most efficient scheme for searching for \up s is the
{\em watched literals}  family of implementations \cite{zchaff,Zhang:watch}. 
For each clause $c$, we identify two
``watched'' literals $l_1(c)$ and $l_2(c)$; the basic idea is that as
long as these two literals are both either unvalued or satisfied, the
clause cannot produce a \up.

It is only when one of the watched literals is set to false that the
clause must be examined in detail.  If there is another unset (and
unwatched) literal, we watch it.  If there is a satisfied literal in
the clause, we need do nothing.  If there is no satisfied literal, the
clause is ready to unit propagate.

If the average clause length is $l$, then when we set a variable $v$
(say to true), the probability is approximately $2/l$ that we will
need to analyze a clause in which $\neg v$ appears, and the work
involved is proportional to the length of the clause.  So the expected
amount of work involved is twice the number of clauses in which $\neg
v$ appears, an improvement on the previous methods.  In fact, the
approach is somewhat more efficient than this cursory analysis
suggests because the adjustment of the watched literals tends to favor
watching those that are set deep in the search tree.

\end{enumerate}

Before we move on to discuss learning in \bs, let us remark briefly on
the so-called ``pure literal'' rule.  To understand the rule itself,
suppose that we have a theory $T$ and some partial variable assignment
$P$.  Suppose also that while a literal $q$ appears in some of the
clauses in $T$ that are not yet satisfied by $P$, the negation $\neg
q$ does not appear in any such clauses.  Now while $q$ may not be a
consequence of the partial assignment $P$, we can clearly set $q$ to
true without removing any solutions from the portion of the search
space that remains.

The pure literal rule is not generally included in implementations of
either the \dpll\ or the \up\ procedure because it is relatively
expensive to work with.  Counts of the number of unsatisfied clauses
containing variables and their negations must be maintained at all
times, and checked to see if a literal has become pure.  In addition,
we will see in \secn{branch} that many branching heuristics obviate
the need for the pure literal rule to be employed.

\subsection{Learning and Relevance}
\label{s.relevance}

Let us now turn to the final column of our table, considering the
progress that has been made in avoiding rework in \bs\ engines.  The
basic idea is to avoid situations where a conventional implementation
will ``thrash'', solving the same subproblem many times in different
contexts.

To understand the source of the difficulty, consider an example
involving a \sat\ problem $C$ with variables $v_{1},v_{2},
\ldots,v_{100}$, and suppose also that the subset of $C$ involving
only variables $v_{50},\dots,v_{100}$ in fact implies that $v_{50}$
must be true.

Now imagine that we have constructed a partial solution that values
the variables $v_{1},\ldots ,v_{49}$, and that we initially set
$v_{50}$ to false.  After some amount of backtracking, we realize that
$v_{50}$ must be true.  Unfortunately, if we subsequently change the
value of one of the $v_i$'s for $i<50$, we will ``forget'' that
$v_{50}$ needs to be true and are in danger of setting it to false
once again, followed by a repetition of the search that showed
$v_{50}$ to be a consequence of $C$.  Indeed, we are in danger of
solving this subproblem not just twice, but once for each search node
that we examine in the space of $v_i$'s for $i<50$.

As we have indicated, the solution to this problem is to cache the
fact that $v_{50}$ needs to be true; this information is generally
saved in the form of a new clause called a {\em nogood\/}.  In this
case, we record the unary clause $v_{50}$.  Modifying our original
problem $C$ in this way will allow us to immediately prune any
subproblem for which we have set $v_{50}$ to false.  This technique
was introduced by Stallman and Sussman \citeyear{Sussman:ddb} in {\em
dependency directed backtracking\/}.

Learning new constraints in this way can prevent thrashing.  When a
contradiction is encountered, the set of assignments that caused the
contradiction is identified; we will call this set the {\em conflict
set}.  A new constraint can then be constructed that excludes the
assignments in the conflict set.  Adding this constraint to the
problem will ensure that the faulty set of assignments is avoided in
the future.

This description of learning is fairly syntactic; we can also give a
more semantic description.  Suppose that our partial assignment
contains $\set{a,\neg b,d,\neg e}$ and that our problem contains the
clauses
 \begin{equation}
\neg a \vee b \vee c \vee \neg d \vee e
 \label{e.res1}
 \end{equation}
 and
 \begin{equation}
\neg c \vee \neg d.
 \label{e.res2}
\end{equation}
The first clause unit propagates to allow us to conclude $c$; the
second allows us to conclude $\neg c$.  This contradiction causes us
to backtrack, learning the nogood
\begin{equation}
\neg a \vee b \vee \neg d \vee e.
\label{e.res}
\end{equation}
 From a semantic point of view, the derived nogood~\eq{res} is simply
the result of resolving the reason~\eq{res1} for $\neg c$ with the
reason~\eq{res2} for $c$.

This is a general phenomenon.  At any point, suppose that $v$ is a
variable that has been set in the partial assignment $P$.  If $v$'s
value is the result of a branch choice, there is no associated reason.
If $v$'s current value is the result of a \up, however, we associate
to $v$ as a reason the clause that produced the propagation.  If $v$'s
value is the result of a backtrack, that value must be the result of a
contradiction identified for some subsequent variable $v'$ and we set
the reason for $v$ to be the result of resolving the reasons for $v'$
and $\neg v'$.  At any point, any variable whose value has been forced
will have an associated reason, and these accumulated reasons will
avoid the need to reexamine any particular portion of the search
space.

Modifying \dpll\ to exploit the derived information requires that we
include the derived clauses in the overall problem $C$, thus enabling
new unit propagations and restricting subsequent search.  But there is
an implicit change as well.

In our earlier example, suppose that we have set the variables
$v_1,\dots,v_{49}$ in that order, and that we have learned the nogood
\begin{equation} v_7 \vee \neg v_9 \label{e.nogood} \end{equation}
(presumably in a situation where $v_7$ is false and $v_9$ is true).
Now as long as $v_7$ remains false and $v_9$ remains true, \up\ will
fail immediately because~\eq{nogood} is unsatisfied.  This will allow
us to backtrack directly to $v_9$ in this example.  This is the
semantic justification for a technique known as {\em
backjumping\/}~\cite{Gaschnig:bj} because the search ``jumps back'' to
a variable that is relevant to the problem at hand.\footnote{In this
particular example, it is also possible to backtrack over $v_8$ as
well, although no reason is recorded.  The branch point for $v_8$ is
removed from the search, and $v_9$ is set to false by \up.  The
advantage of this is that there is now flexibility in either the
choice of value for $v_8$ or the choice of branch variable itself.
This idea is related to Baker's \citeyear{Baker:fancy} work on the
difficulties associated with some backjumping schemes, and is employed
in \zchaff~\cite{zchaff}.}

While attractive in theory, however, this technique is difficult to
apply in practice.  The reason is that a new nogood is learned with
every backtrack; since the number of backtracks is proportional to the
running time of the program, an exponential number of nogoods can be
learned.  This can be expected both to overtax the memory available on
the system where the algorithm is running, and to increase the time
for each node expansion.  As the number of clauses containing any
particular variable $v$ grows without bound, the \up\ procedure
\ref{p.unit} will grind to a halt.

Addressing this problem was the primary focus of work on systematic
\sat\ solvers during the 1990's.  Since it was impractical to retain
all of the nogoods that had been learned, some method needed to be
found that would allow a polynomial number of nogoods to be retained
while others were discarded.  The hope was that a relatively small
number of nogoods could still be used to prune the search space
effectively.\footnote{Indeed, the final column of our table might
better be named ``forgetting'' than ``learning''.  Learning
(everything) is easy; it's forgetting in a coherent way that's hard.}

\paragraph{Length-bounded Learning}  The first method used to
bound the size of the set of learned clauses was to only retain
clauses whose length is less than a given bound $k$
\cite{Dechter:bj,Dechter:length}.  In addition to providing a
polynomial bound on the number of nogoods retained, this approach was
felt likely to retain the most important learned clauses, since a
clause of length $l$ will in general prune $\frac{1}{2^l}$ of the
possible assignments of values to variables.  Length-bounded learning
draws from this observation the conclusion that short clauses should
be retained in preference to long ones.

\paragraph{Relevance-bounded Learning}  Unfortunately,
length may not be the best indicator of the value of a particular
learned clause.  If we restrict our attention to any particular
subproblem in the search, some short clauses may not be applicable at
all, while other longer clauses may lead to significant pruning.  As
an example, consider a node defined by the partial assignment $P =
\set{a,b,c}$ together with the two learned clauses:
\begin{eqnarray}
& a \vee b \vee e & \label{e.short} \\
&\neg a \vee \neg b \vee \neg c \vee d \vee e & \label{e.long}
\end{eqnarray}
As long as the assignments in $P$ are retained, the clause \eq{short}
cannot be used for pruning because it is satisfied by $P$ itself.  In
fact, this clause will not be useful until we backtrack and change the
values for both $a$ and for $b$.  The clause \eq{long} is more likely
to be useful in the current subproblem, since it will lead to a unit
propagation if either $d$ or $e$ is set to \false.  If the subproblem
below the node given by $P$ is large, \eq{long} may be used many
times.  Within the context of this subproblem, the longer clause is
actually the more useful.

At some level, the appearance of $\neg a$, $\neg b$, and $\neg c$
in~\eq{long} shouldn't contribute to the effective length of the
learned clause because that all of these literals are currently false.
Length-bounded learning cannot make this distinction.

We see from this example that it is useful to retain clauses of
arbitrary length provided that they are relevant to the current search
context.  If the context subsequently changes, we can remove some
clauses to make room for new ones that are more suitable to the new
context.  This is what relevance-bounded learning does.

In relevance-bounded learning, the effective length of a clause is
defined in terms of the current partial assignment.  The {\em
irrelevance} of a clause is defined as one less than the number of
unvalued or satisfied literals it contains.  For example, the clause
\eq{long} under the partial assignment $P$ has an irrelevance of 1.
The idea of relevance-bounded learning originated in dynamic
backtracking \cite{Ginsberg:dynamic}, in which clauses were deleted if
their irrelevance exceeded $1$.  This idea was generalized by Bayardo
and Miranker~\citeyear{Bayardo:relsat}, who defined a general
relevance bound and then deleted all clauses whose irrelevance
exceeded that bound.  This generalization is implemented in the {\sc
relsat} satisfiability engine \cite{Schrag:relsat}.

Like length-bounded learning, relevance-bounded learning retains all
clauses of length less than the irrelevance bound $k$, since the
irrelevance of a clause can never exceed its length.  But the
technique of relevance-bounded learning also allows the retention of
longer clauses if they are applicable to the current portion of the
search space.  Such clauses are only removed when they are no longer
relevant.

Returning to our example, if we backtrack from the original partial
assignment with $\set{a,b,c}$ and find ourselves exploring $\set{\neg
a,\neg b,\neg c}$, the short nogood~\eq{short} will be 0-irrelevant
(since we can unit propagate to conclude $e$) and the long
one~\eq{long} will be 4-irrelevant.  Using a relevance bound of 3 or
less, this nogood would be discarded.

The condition that nogoods are only retained until their irrelevance
exceeds a bound $k$ is sufficient to ensure that only a polynomial
number of nogoods are retained at any point.\footnote{Although
accepted wisdom, we know of no proof in the literature of this result;
Bayardo and Miranker's \citeyear{Bayardo:relsat} proof appears to
assume that the order in which branch variables are chosen is fixed.
We present a general proof in the next paper in this series
\cite{Ginsberg:zap2}.}  Experimental results~\cite{Bayardo:relsat}
show that relevance-bounded learning is more effective than its
length-bounded counterpart and, even with a relevance bound of 1, the
results are comparable to those of learning without
restriction.\footnote{Results such as these necessarily become
somewhat suspect as algorithmic methods mature; an unfortunate
consequence of the extremely rapid progress in satisfiability engines
over recent years is the lack of careful experimental work evaluating
the host of new ideas that have been developed.}

\paragraph{Hybrid Approaches} Finally, we note that some solvers
employ a hybrid approach.  The {\sc chaff} algorithm~\cite{zchaff}
uses both a relevance bound and a (larger) length bound.  Clauses must
meet both the relevance bound and the length bound to be retained.

Yet another approach is taken by the {\sc berkmin} algorithm
\cite{berkmin}.  Here, the set of nogoods is partitioned into two
separate groups based on how recently the nogoods were acquired;
$\frac{15}{16}$ of the nogoods are kept in a ``recent'' group and the
remaining $\frac{1}{16}$ in an ``old'' group.  A relatively large
length bound is used to cull the recently acquired nogoods while a
smaller length bound is used to aggressively cull the smaller group of
older nogoods.  We are not aware of any studies comparing these hybrid
approaches to pure length-bounded or relevance-bounded methods.

\subsection{Branching Heuristics}
\label{s.branch}

Let us now turn to an examination of the progress that has been made
in the development of effective heuristics for the selection of branch
variables in \dpll.  As discussed in the introduction, we focus not on
specific heuristics that work in selected domains, but on general
ideas that attempt to exploit the structure of the axiomatization
directly.

Prior to the development of successful learning techniques, branching
heuristics were the primary method used to reduce the size of the
search space.  It seems likely, therefore, that the role of branching
heuristics is likely to change significantly for algorithms that prune
the search space using learning.  While the heuristics used in
\zchaff\ appear to be a first step in this direction, very little is
known about this new role.

Initially, however, the primary criterion for the selection of a
branch variable was to pick one that would enable a cascade of unit
propagations; the result of such a cascade is a smaller and more
tractable subproblem.\footnote{This idea tends to obviate the need for
use of the pure literal rule, as well.  If $p$ is a pure literal,
there is no particular reason to hurry to set $p$ to true; the key
thing is to avoid setting it to false.  But if $p$ is pure, $\neg p$
cannot generate any unit propagations, so $p$ will tend not to be
selected as a branch variable.  Pure literals can obviously never be
set false by unit propagation, so heuristics based on unit propagation
counts tend to achieve most of the advantages of the pure literal rule
without incurring the associated computational costs.}

The first rule based on this idea is called the {\sc moms} rule, which
branches on the variable that has \underline Maximum \underline
Occurrences in clauses of \underline Minimum \underline Size
\cite{Crawford:exp,Dubois:branch,Hooker:branching,Jeroslow:branching,Pretolani:branching}.
{\sc Moms} provides a rough but easily computed approximation to the
number of unit propagations that a particular variable assignment
might cause.

Alternatively, one can use a ``unit propagation rule''
\cite{Crawford:exp,Freeman:SAT}, and compute the exact number of
propagations that would be caused by a branching choice.  Given a
branching candidate $v_{i}$, the variable is separately fixed to true
and to false and the \up\ procedure is executed for each choice.  The
precise number of \up s caused is then used to evaluate possible
branching choices.  Unlike the {\sc moms} heuristic, this rule is
obviously exact in its attempt to judge the number of \up s caused by
a potential variable assignment.  Unfortunately, it is also
considerably more expensive to compute because of the expense of unit
propagation itself.  This led to the adoption of composite approaches
\cite{li:unitprop} where {\sc moms} is used to identify a small number
of branching candidates, each of which is then evaluated exactly using
the more expensive \up\ heuristic.  On randomly generated problems,
the composite technique outperforms either heuristic in isolation.

Another strategy is to branch on variables that are likely to be {\em
backbone} variables~\cite{Dubois:backbone}.  A {\em backbone\/}
literal (also often referred to as a {\em unary prime implicate\/} of
a theory) is one that must be true in all solutions to a given
problem.  Given a problem $C$ and a partial assignment $P$, the
backbone heuristic attempts to branch on variables that are backbones
of the subset of those clauses in $C$ that are satisfied by $P$; the
likelihood that any particular variable is a backbone literal is
approximated by counting the appearances of that literal in the
satisfied clauses in $C$.  This heuristic outperforms those discussed
in the previous paragraphs.

The heuristics described thus far were developed when the community's
research emphasis was focused on the solution of randomly generated
satisfiability problems.  The development of bounded learning methods
enabled solvers to address the issue of thrashing, and caused a
natural shift in focus toward more structured, realistic problems.
There are no formal studies comparing the previously discussed
heuristics on structured problems, and the value of the studies that
do exist is reduced because all of the implementations were of \dpll\
in isolation and without the learning techniques that have since
proved so important.  Branching techniques and learning are deeply
related, and the addition of learning to a \dpll\ implementation will
have a significant effect on the effectiveness of any of these
branching strategies.  As new clauses are learned, the number of \up s
an assignment will cause can be expected to vary; the reverse is also
true in that the choice of branch variable can affect which clauses
the algorithm learns.  A formal comparison of branching techniques'
performance on structured problems and in the presence of learning
would be extremely useful.

Branching heuristics that are designed to function well in the context
of a learning algorithm generally try to branch on variables about
which things have been learned recently.  This tends to allow the
implementation to keep ``making progress'' on a single section of the
search space as opposed to moving from one area to another; an
additional benefit is that existing nogoods tend to remain relevant,
avoiding the inefficiencies associated with losing the information
present in nogoods that become irrelevant and are deleted.  In
\zchaff, for example, a count is maintained of the number of times
each literal occurs in the theory being solved.  When a new clause is
added, the count associated with each literal in the clause is
incremented.  The branch heuristic then selects a variable that
appears in as many clauses as possible.  By periodically dividing all
of the counts by a constant factor, a bias is introduced toward
branching on variables that appear in recently learned clauses.  Like
the {\sc moms} rule, this rule is inexpensive to calculate.

The heuristic used in {\sc berkmin}~\cite{berkmin} builds on this idea
but responds more dynamically to recently learned clauses.  The {\sc
berkmin} heuristic prefers to branch on variables that are unvalued in
the most recently learned clause that is not yet satisfied, with a
\zchaff-like heuristic used to break ties.

All told, there are many competing branching heuristics for
satisfiability solvers, and there is still much to be done in
evaluating their relative effectiveness.  The most interesting
experiments will be done using implementations that learn, and on
realistic, structured problems as opposed to randomly generated ones.

\subsection{Proof Complexity}
\label{s.complexity}

We have already commented briefly on the fact that proof systems can
be evaluated based on provable bounds on the proofs of certain classes
of formulae, or by the development of polynomial transformations from
proofs in one system into proofs in another.

With regard to the first metric, there are at least three classes of
problems known to be exponentially difficult for conventional
resolution-based provers (including any \dpll\
implementation):\footnote{There are other hard problems as well, such
as Haken's \citeyear{Haken:mosquito} {\em broken mosquito screen\/}
problem.  The three examples quoted here are sufficient for our
purposes.}
\begin{enumerate}
\item Pigeonhole problems \cite{Haken}
\item Parity problems \cite{Tseitin:complexity}
\item Clique coloring problems \cite{bonet-pb-clique,krajicek-pb-clique,clique}
\end{enumerate}

Before turning to a discussion of these problems specifically,
however, let us point out that there are many proof systems that are
known to be more powerful than any of the ones we discuss in this
paper.  From our perspective, the most interesting is {\em extended
resolution\/} and involves the introduction of new variables that
correspond to arbitrary logical expressions built up out of the
original variables in the theory.

Since such logical expressions can always be built up term-by-term,
it suffices to allow the introduction of new variables corresponding
to pairwise combinations of existing ones; since disjunction can be
replaced with conjunction using de~Morgan's laws, it suffices to
introduce new variables of the form
\begin{equation}
w \equiv x \wedge y
\label{e.extend}
\end{equation}
for literals $x$ and $y$.  Writing \eq{extend} in disjunctive normal
form, we get:

\begin{definition}{\bf \cite{Tseitin:complexity}} An {\em extended resolution
proof\/} for a theory $T$ is one where $T$ is first augmented by a
collection of groups of axioms, each group of the form
\begin{eqnarray}
& \neg x \vee \neg y \vee w & \nonumber \\
& x \vee \neg w & \label{e.extend-example} \\
& y \vee \neg w & \nonumber
\end{eqnarray}
where $x$ and $y$ are literals in the (possibly already extended)
theory $T$ and $w$ is a new variable.  Following this, derivation
proceeds using conventional resolution on the augmented theory.
\end{definition}

There is no proof system known to be stronger than extended
resolution; in fact, there is no class of problems for which there are
known to be no polynomially sized proofs in extended resolution.

As we have stressed, however, the fact that a proof system is strong
does not mean that it works well in practice.  We know of {\em no\/}
implementation of extended resolution for the simple reason that
virtually nothing is known about how to select new variables so as to
shorten proof length.

Understanding {\em why\/} the introduction of these new variables can
reduce proof length is considerably simpler.  As an example, suppose
that during a resolution proof, we have managed to derive the nogood
$a\vee x$, and that we have also derived $a\vee y$.  In order to
complete the proof, we need to perform lengthy -- but identical --
analyses of each of these nogoods, eventually deriving simply $x$ from
the first and $y$ from the second (and then resolving against $\neg x
\vee \neg y$, for example).

If we could replace the pair of nogoods $a\vee x$ and $a \vee y$ with
the single nogood $a\vee w$ using~\eq{extend-example}, the two proofs
from $a\vee x$ and $a\vee y$ could be collapsed into a single proof,
potentially halving the size of the proof in its entirety.
Introducing still more variables can repeat the effect, resulting in
exponential reductions in proof size.

Another way to look at this is as an improvement in expressivity.
There is simply no way to write $(a\vee x)\wedge (a\vee y)$ or the
equivalent $a\vee(x\wedge y)$ as a single Boolean axiom in disjunctive
normal form.  The power of extended resolution rests on the fact that
subexpression substitution makes it possible to capture expressions
such as $a\vee(x\wedge y)$ in a single axiom.

None of the proof systems being considered in this survey is as
powerful as extended resolution, and we will therefore evaluate them
based on their performance on the three problems mentioned at the
beginning of this section.  Let us therefore describe each of those
problems in some detail.

\subsubsection{Pigeonhole problems}

The \php\ involves showing that it is impossible to put $n+1$ pigeons
into $n$ holes if each pigeon must go into a distinct hole.  If we
write $p_{ij}$ for the fact that pigeon $i$ is in hole $j$, then a
straightforward axiomatization says that every pigeon must be in at
least one hole: \begin{equation} p_{i1} \vee p_{i2} \vee \cdots \vee
p_{in} \mbox{ for $i=1,\dots,n+1$} \label{e.php1} \end{equation} and
that no two pigeons can be in the same hole: \begin{equation} \neg
p_{ik} \vee \neg p_{jk} \mbox{ for $1\leq i<j\leq n+1$ and
$k=1,\dots,n$} \label{e.php2} \end{equation} Note that there are in
all $\Theta(n^3)$ axioms of the form~\eq{php2}.

It is well known that there is no polynomial-sized proof of the
unsatisfiability of the axioms~\eq{php1}--\eq{php2}~\cite{Haken}.  The
proof is technical, but the essential reason is that the \php\ is
``all about'' counting.  At some point, proving that you can't put
$n+1$ pigeons into $n$ holes requires saying that you can't put $n$
pigeons into the last $n-1$ holes, thus $n-1$ pigeons into the last
$n-2$ holes, and so on.  Saying this in the language of \sat\ is
awkward, and it is possible to show that no proof of the \php\ can be
completed without, at some point, working with extremely long
individual clauses.  Once again, we see the connection to expressive
efficiency; for readers interested in additional details, Pitassi's
\citeyear{Pitassi:complexity} explanation is reasonably accessible.

\subsubsection{Parity problems}

By a {\em parity problem}, we will mean a collection of axioms
specifying the parity of sets of inputs.  So we will write, for
example,
\begin{equation}
x_1\oplus\cdots\oplus x_n = 1
\label{e.parity}
\end{equation}
to indicates that an odd number of the $x_i$ are true; a right hand
side of zero would indicate that an even number were true.  The
$\oplus$ here indicates exclusive or.

Reduction of \eq{parity} to a collection of Boolean axioms is best
described by an example.  The parity constraint $x\oplus y \oplus z=1$
is equivalent to
\begin{eqnarray*}
& x\vee y\vee z & \\
& x \vee \neg y \vee \neg z & \\
& \neg x \vee y \vee \neg z & \\
& \neg x \vee \neg y \vee z &
\end{eqnarray*}
In general, the number of Boolean axioms needed is exponential in the
length of the parity clause \eq{parity}, but for clauses of a fixed
length, the number of axioms is obviously fixed as well.

For the proof complexity result of interest, suppose that $G$ is a
graph, where each node in $G$ will correspond to a clause and each
edge to a literal.  We label the edges with distinct literals, and
label each node of the graph with a zero or a one.  Now if $n$ is a
node of the graph that is labeled with a value $v_n$ and the edges
$e_{1n},\dots,e_{i(n),n}$ incident on $n$ are labeled with literals
$l_{1n},\dots,l_{i(n),n}$, we add to our theory the Boolean version of
the clause
\begin{equation}
l_{1n}\oplus\cdots\oplus l_{i(n),n} = v_n
\label{e.tseitin}
\end{equation}

Since every edge connects two nodes, every literal in the theory
appears exactly twice in axioms of the form~\eq{tseitin}.  Adding all
of these constraints therefore produces a value that is equivalent to
zero mod 2 and must be equal to $\sum_n v_n$ as well.  If $\sum_n v_n$
is odd, the theory is unsatisfiable.  Tseitin's
\citeyear{Tseitin:complexity} principal result is to show that this
unsatisfiability cannot in general be proven in a number of resolution
steps polynomial in the size of the Boolean encoding.

\subsubsection{Clique coloring problems}

The last examples we will consider are known as ``clique coloring
problems.''  These are derivatives of \php s where the exact nature of
the \php\ is obscured.  Somewhat more specifically, the problems
indicate that a graph includes a clique of $n+1$ nodes (where every
node in the clique is connected to every other), and that the graph
must be colored in $n$ colors.  If the graph itself is known to be a
clique, the problem is equivalent to the \php.  But if we know only
that the clique can be embedded into the graph, the problem is more
difficult.

In the axiomatization, we use $e_{ij}$ to describe the edges of the
graph, $c_{ij}$ to describe the coloring of the graph, and $q_{ij}$ to
describe the embedding of the cli\underline{Q}ue into the graph.  The
graph has $m$ nodes, the clique is of size $n+1$, and there are $n$
colors available.  So the axiomatization is:
\begin{eqnarray}
\neg e_{ij} \vee \neg c_{il} \vee \neg c_{jl} && \mbox{for $1\leq i<j\leq m$, $l=1,\dots,n$} \label{e.okcolor}\\
c_{i1} \vee \cdots \vee c_{in} && \mbox{for $i=1,\dots,m$} \label{e.color}\\
q_{i1} \vee \cdots \vee q_{im} && \mbox{for $i=1,\dots,n+1$} \label{e.clique}\\
\neg q_{ij} \vee \neg q_{kj} && \mbox{for $1\leq i<k\leq n+1$, $j=1,\dots,m$} \label{e.map}\\
e_{ij} \vee \neg q_{ki} \vee \neg q_{lj} && \mbox{for $1\leq i<j\leq m$, $1\leq k \neq l \leq n+1$} \label{e.okmap}
\end{eqnarray}
 Here $e_{ij}$ means that there is an edge between graph nodes $i$ and
$j$, $c_{ij}$ means that graph node $i$ is colored with the $j$th
color, and $q_{ij}$ means that the $i$th element of the clique is
mapped to graph node $j$.  Thus the first axiom \eq{okcolor} says that
two of the $m$ nodes in the graph cannot be the same color (of the $n$
colors available) if they are connected by an edge.  \eq{color} says
that every graph node has a color.  \eq{clique} says that every
element of the clique appears in the graph, and \eq{map} says that no
two elements of the clique map to the same node in the graph.
Finally, \eq{okmap} says that the clique is indeed a clique -- no two
clique elements can map to disconnected nodes in the graph.

Since there is no polynomially sized resolution proof of the \php\ in
\bs, there is obviously no polynomially sized proof of the clique
coloring problems, either.  But as we shall see, clique coloring
problems can in some cases be used to distinguish among elements of
the proof complexity hierarchy.

\subsection{Boolean Summary}

We summarize the results of this section by completing the first row
of our table as follows:

\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& & {\bf p-simulation} && {\bf unit} & \\
& {\bf rep. eff.} & {\bf hierarchy} & {\bf inference} 
 & {\bf propagation} & {\bf learning} \\
\hline
\footnotesize\bf SAT & 1 & EEE& resolution & watched literals&relevance \\ 
\bf{cardinality} &&&&& \\
\bf{PB} &&&&& \\
\bf{symmetry} &&&&& \\
\footnotesize\bf QPROP &&&&& \\
\hline
\end{tabular}
\end{center}

The entries are really just an informal shorthand:
\begin{itemize}
\item {\bf Representational efficiency:} \bs\ is the benchmark against
which other languages will be measured; we give here the relative
savings to be had by changing representation.
\item {\bf $p$-simulation hierarchy:} We give the proof complexity for
the three problem classes discussed in \secn{complexity}.  For \bs,
all of the problems require proofs of exponential length.
\item {\bf Inference:} The basic inference mechanism used by 
\dpll\ is resolution.
\item {\bf Propagation:} Watched literals lead to the most efficient
implementation.
\item {\bf Learning:} Relevance-based learning appears to be more
effective than other poly-sized methods.
\end{itemize}

\section{\Pb\ and Cardinality Constraints}
\label{s.pseudo}

The entries in the previous table summarize the fact that \bs\ is a
weak method that admits efficient implementations.  The representation
is relatively inefficient, and none of our canonical problems can be
solved in polynomial time.  Some of these difficulties, at least, can
be overcome via a representational shift.

To understand the shift, note that we can write an axiom such as
\[x \vee y \vee \neg z\]
as
\begin{equation}
x+y+\overline z \geq 1
\label{e.pb-basic}
\end{equation}
where we are now thinking of $x,y$ and $z$ as variables with value
either 0 (false) or 1 (true) and have written $\overline z$ for $1-z$
or, equivalently, $\neg z$.  If $v$ is a variable, we will continue to
refer to $\overline v$ as the negation of $v$.

All of the familiar logical operations have obvious analogs in this
notation.  If, for example, we want to resolve
 \[a \vee \neg b \vee c\]
with
 \[b \vee \neg d\]
to get $a\vee c \vee \neg d$, we simply add
 \[a+\overline b+c \geq 1\]
to
 \[ b+\overline d \geq 1\]
 and simplify using the identity $b+\overline b=1$ to get
 \[a+c+\overline d \geq 1\]
as required.

What's nice about this notation is that it extends easily to more
general descriptions.  If the general form of a disjunction $\vee l_i$
of literals is $\sum l_i \geq 1$ as in~\eq{pb-basic}, we can drop the
requirement that the right-hand side be 1:

\begin{definition} A {\em cardinality constraint} or {\em extended 
clause} is a constraint of the form
\[\sum_i l_i \geq k\]
where $k$ is an integer and each of the $l_i$ is required to have
value 0 or 1.
\label{d.cardinality}
\end{definition}
The cardinality constraint simply says that at least $k$ of the
literals in question are true.

\begin{proposition}[Cook, Coullard and Turan \citeyear{Cook:php}] There is
an unsatisfiability proof of polynomial length of the \php\ using
cardinality constraints.
\label{p.php}
\end{proposition}

\proof Cook et~al.~\citeyear{Cook:php} give a derivation in $o(n^3)$
steps; we have presented an $o(n^2)$ derivation elsewhere
\cite{Dixon:AIOR}.\proofend

Of course, the fact that this extension to the \sat\ language allows
us to find polynomial-length derivations of \php\ does not necessarily
show that the change will have computational value; we need to examine
the other columns of the table as well.  In the remainder of this
section, we will show this and will go further, describing new
computational techniques that can only be applied in the broader
setting that we are now considering.  Experimental results are also
presented.  But let us begin by examining the first column of the
table:

\begin{proposition}{\bf \cite{benhamou:dpc}} The cardinality constraint
 \begin{equation}
x_1 + \cdots + x_m \geq k
 \label{e.card1}
 \end{equation}
 is logically equivalent to the set of $m \choose {k-1}$ axioms
 \begin{equation}
x_{i_1} + \cdots + x_{i_{m-k+1}} \geq 1
 \label{e.card2}
 \end{equation}
 for every set of $m-k+1$ distinct variables
$\set{x_{i_1},\dots,x_{i_{m-k+1}}}$.  Furthermore, there is no more
compact Boolean encoding of \eq{card1}.
\label{p.card}
 \end{proposition}

\proof We first show that \eq{card1} implies \eq{card2}.  To see this,
suppose that we have a set $S$ of $m-k+1$ variables.  Suppose also
that $T$ is the set of $x_i$'s that are true, so that $T$ is of size
at least $k$.  Since there are only $m$ variables, $S\cap T \neq
\emptyset$ and at least one $x_i\in S$ must be true.

To see that \eq{card2} implies \eq{card1}, suppose that~\eq{card2} is
true for all appropriate sets of $x_i$'s.  Now if~\eq{card1} were
false, the set of false $x_i$'s would be of size at least $m-k+1$, so
that some instance of~\eq{card2} would be unsatisfied.

To see that there is no more efficient encoding, first note that
if \eq{card1} implies a Boolean axiom
\[x_1\vee\cdots\vee x_k\vee \neg x_{k+1}\vee\cdots\vee \neg x_m\]
then it must also imply
\[x_1\vee\cdots\vee x_k\]
since we can always change an $x_i$ from false to true without
reducing the satisfiability of~\eq{card1}.

Next, note that no axiom of length less than $m-k+1$ is a consequence
of \eq{card1}, since any such axiom can be falsified while satisfying
\eq{card1} by setting every unmentioned variable to true and the rest
to false.

Finally, suppose that we leave out a single instance $i$ of \eq{card2}
but include all of the others as well as every clause of length
greater than $m-k+1$.  By setting the variables in $i$ to false and
every other variable to true, all of the given clauses will be
satisfied but \eq{card1} will not be.  It follows that any Boolean
equivalent of \eq{card1} must include at least the $m \choose {k-1}$
instances of~\eq{card2}.\proofend 
 
\noindent It follows from \prop{card} that provided that no new
variables are introduced, cardinality constraints can be exponentially
more efficient than their Boolean counterparts.

Before discussing the other columns in the table, let us consider
further extending our representation to include what are known as {\em
pseudo}-Boolean constraints:

\begin{definition} A {\em pseudo-Boolean constraint\/} is an axiom of 
the form
\begin{equation}
\sum_i w_i l_i \geq k
\label{e.pb}
\end{equation}
 where each $w_i$ and $k$ is a positive integer and each of the $l_i$
is required to have value 0 or 1.
\label{d.pb}
\end{definition}

Pseudo-Boolean representations typically allow both linear
inequalities and linear equalities over Boolean variables.  Linear
equalities can easily be translated into a pair of inequalities of the
form in the definition; we prefer the inequality-based description
\cite[also known as \pb\ {\em normal
form}]{Barth:01,Chandru:logic_book} because of the better analogy with
\bs\ and because \up\ becomes unmanageable if equality constraints are
considered.  Indeed, simply determining if an equality clause is
satisfiable subsumes subset-sum and is therefore (weakly) NP-complete
\cite{Garey&Johnson}.

Compare \eq{pb} with \defn{cardinality}; the $w_i$ are the weights
attached to various literals.  The \pb\ language is somewhat more
flexible still, allowing us to say (for example)
\[2a + b + \overline c \geq 2\]
indicating that either $a$ is true or both $b$ and $\neg c$ are
(equivalent to the crucial representational efficiency obtained in
extended resolution).  As we will see shortly, it is natural to make
this further extension because the result of resolving two cardinality
constraints can be most naturally written in this form.

\subsection{Unit Propagation}

Let us begin by discussing propagation techniques in a cardinality or
\pb\ setting.\footnote{As we have remarked, our table is designed to
reflect the issues involved in lifting \dpll\ to a more expressive
representation.  Extending a nonsystematic search technique such as
\wsat\ to a \pb\ setting has been discussed by Walser
\citeyear{Walser:WSATPB} and Prestwich \citeyear{Prestwich:pb}.}

A \pb\ version of \up\ was first presented by Barth
\citeyear{Barth:01} and is described in a number of papers
\cite{Aloul:PBS,Dixon:AIOR}. In the Boolean case, we can describe a
clause as unit if it contains no satisfied literals and at most one
unvalued one.  To generalize this to the \pb\ setting, we make the
following definition, where we view a partial assignment $P$ simply as
the set of literals that it values to true:

\begin{definition} Let $\sum_i w_i l_i \geq k$ be a \pb\ clause, which 
we will denote by $c$.  Now suppose that $P$ is a partial assignment
of values to variables.  We will say that the {\em current value of
$c$ under $P$\/} is given by \[\curr(c,P) = \sum_{\set{i|l_i\in P}}
w_i - k\] If no ambiguity is possible, we will write simply $\curr(c)$
instead of $\curr(c,P)$.  In other words, $\curr(c)$ is the sum of the
weights of literals that are already satisfied by $P$, reduced by the
required total weight $k$.

In a similar way, we will say that the {\em possible value of $c$
under $P$\/} is given by \[\poss(c,P) = \sum_{\set{i|\neg l_i\not\in
P}} w_i - k\] If no ambiguity is possible, we will write simply
$\poss(c)$ instead of $\poss(c,P)$.  In other words, $\poss(c)$ is the
sum of the weights of literals that are either already satisfied or
not valued by $P$, reduced by the required total weight
$k$.\footnote{Chai and Kuehlmann \citeyear{Chai:pb} refer to \poss\ as
{\em slack}.}
\label{d.poss}
\end{definition}

\begin{definition} Let $c$ be a clause, and $P$ a partial assignment.
We will say that $c$ is {\em unit\/} if there is a variable $v$ not
appearing in $P$ such that either $P\cup\set v$ or $P\cup\set{\neg
v}$ cannot be extended to an assignment that satisfies $c$.
\label{d.unit}
\end{definition}
In this situation, the variable $v$ is forced to take a value that
will help satisfy the clause.  This creates a new consequential
assignment.  Note that if $c$ is already unsatisfiable, we can meet
the conditions of the definition by choosing $v$ to be any variable
not assigned a value by $P$.  Note also that in the \pb\ case, a
clause may actually contain more than one variable that is forced to a
specific value.  It should be clear that in the Boolean case, this
definition duplicates the conditions of the original \up\ procedure
\ref{p.unit}.

\begin{lemma}  A partial assignment $P$ can be extended in a way
that satisfies a clause $c$ if and only if $\poss(c,P)\geq 0$.
 \end{lemma}

\proof Assume first that $\poss(c,P)\geq 0$, and suppose that we value
every remaining variable in a way that helps to satisfy $c$.  Having
done so, every literal in $c$ that is not currently made false by $P$
will be true, and the resulting value of $c$ will be
\[\sum_{i} w_i l_i = \sum_{\set{i|\neg l_i \not\in P}} w_i = \poss(c,P) + k \geq k\] so
that $c$ becomes satisfied.

Conversely, suppose that $\poss(c,P)<0$.  Now the best we can do is
still to value the unvalued literals favorably, so that the value of
$c$ becomes
 \[\sum_{i} w_i l_i = \sum_{\set{i|\neg l_i \not\in P}} w_i = \poss(c,P) + k < k\] 
 and $c$ is unsatisfiable.\proofend

\begin{proposition} A clause $c$ containing at least one unvalued
literal is unit if and only if $c$ contains an unvalued literal $l_i$
with weight $w_i > \poss(c)$.\label{p.up}  \end{proposition}

\proof If there is a literal with weight $w_i > \poss(c)$, setting
that literal to false will reduce $\poss(c)$ by $w_i$, making it
negative and thus making the $c$ unsatisfiable.  Conversely, if there
is no such literal, then $\poss(c)$ will remain positive after any
single unvalued literal is set, so that $c$ remains satisfiable and is
therefore not unit.\proofend

Given the above result, there is little impact on the time needed to
find unit clauses.  We need simply keep the literals in each clause
sorted by weight and maintain, for each clause, the value of $\poss$
and the weight of the largest unvalued literal.  If we value a literal
with different weight, we can apply the test in \prop{up} directly.
If we value a literal of the given weight, a short walk along the
clause will allow us to identify the new unvalued literal of maximum
weight, so that the proposition continues to apply.

\paragraph{Watched literals} Generalizing the idea of watched literals
is no more difficult.  We make the following definition:

\begin{definition} Let $c$ be a clause.  A {\em watching set for $c$\/}
is any set $S$ of variables with the property that $c$ cannot be unit
as long as all of the variables in $S$ are either unvalued or
satisfied.\end{definition}

\begin{proposition} Given a clause $c$ of the form $\sum_i w_i l_i \geq k$,
let $S$ be any set of variables.  Then $S$ is a watching set for $c$
if and only if
\begin{equation}
\sum_i w_i - \max_i w_i \geq k
 \label{e.watch}
 \end{equation}
 where the sum and maximum are taken over literals involving variables in
$S$.\end{proposition}

\proof Suppose that all of the variables in $S$ are unvalued or
satisfied.  Now let $l_j$ be any unvalued literal in $c$.  If
$l_j\not\in S$, then $\poss(c) \geq w_j + \sum_i w_i - k$ and thus
$\poss(c) \geq w_j$ since $\sum_i w_i \geq \sum_i w_i - \max_i w_i
\geq k$.  If, on the other hand, $l_j\in S$, then
\[\poss(c) \geq \sum_i w_i - k\]
 and
 \[\sum_i w_i - w_j \geq \sum_i w_i - \max_i w_i \geq k\]
 Combining these, we get
 \[\poss(c) \geq w_j\]
 Either way, we cannot have $\poss(c) < w_j$ and \prop{up} therefore
implies that $c$ cannot be unit.  It follows that $S$ is a watching set.

The converse is simpler.  If $\sum_i w_i - \max_i w_i < k$, value
every literal outside of $S$ so as to make $c$ false.  Now $\poss(c) =
\sum_i w_i - k$, so if $l_j$ is the literal in $S$ with greatest
weight, the associated weight $w_j$ satisfies $w_j > \poss(c)$ and $c$
is unit.  Thus $S$ cannot be a watching set.\proofend

This generalizes the definition from the Boolean case, a fact made
even more obvious by:

\begin{corollary} Given a cardinality constraint $c$ requiring at
least $k$ of the associated literals to be true, $S$ is a watching set
for $c$ if and only if it includes at least $k+1$ literals in
$c$.\end{corollary}

\proof  The expression~\eq{watch} becomes
 \[\sum_i 1 - \max_i 1 \geq k\]
or
 \[|S| - 1 \geq k.\proofend\]

\subsection{Inference and Resolution}

As with \up, resolution also lifts fairly easily to a \pb\ setting.
The general computation is as follows:

\begin{proposition} Suppose that we have two clauses $c$ and $c'$, with
$c$ given by
 \begin{equation}
\sum_i w_i l_i + wl \geq k
 \label{e.resolve1}
 \end{equation}
and $c'$ given by
 \begin{equation}
\sum_i w'_i l'_i + w'\overline l \geq k'
 \label{e.resolve2}
 \end{equation}
 Then it is legitimate to conclude
 \begin{equation}
\sum_i w'w_i l_i + \sum_i ww'_i l'_i \geq w'k + wk' - ww'
 \label{e.resolved}
 \end{equation}
\label{p.resolution}
\end{proposition}

\proof This is immediate.  Multiply~\eq{resolve1} by $w'$, multiply
\eq{resolve2} by $w$, add and simplify using $l+\overline l=1$.\proofend

If all of the weights, $k$ and $k'$ are 1, this generalizes
conventional resolution provided that the sets of nonresolving
literals in $c$ and $c'$ are disjoint.  To deal with the case where
there is overlap between the set of $l_i$ and the set of $l'_i$, we
need:

\begin{lemma} Suppose that $c$ is clause $\sum_i w_i l_i \geq k$.
Then $c$ is equivalent to $\sum_i w'_i l_i \geq k$, where the $w'_i$
are given by:
  \[w'_i(j)=\cases{w_i,& if $w_i<k$;\cr
  		   k,& otherwise.\cr}\]
\label{l.round}
\end{lemma}

\proof If $l_j$ is a literal with $w_j\geq k$, then both $c$ and the
rewrite are true if $l_j$ is satisfied.  If $l_j = 0$, then $c$ and
the rewrite are equivalent.\proofend

In other words, we can reduce any coefficient that is greater than 
what is required to satisfy the clause in its entirety, for example
rewriting
\[3x+y+\overline z \geq 2\]
as
\[2x+y+\overline z \geq 2\]
because either is equivalent to $x\vee(y\wedge \neg z)$.

\begin{proposition}{\bf \cite{Cook:php,Hooker:genres}} The construction of
\prop{resolution} generalizes conventional
resolution.\label{p.pb-res}\end{proposition}

\proof We have already discussed the case where the sets of $l_i$ and
$l'_i$ are disjoint.  If there is a literal $l_i$ in $c$ that is the
negation of a literal in $c'$, then we will have $l_i + \neg l_i$ in
\eq{resolved}, which we can simplify to 1 to make the resolved
constraint trivial; resolution produces the same result.  If there is
a literal $l_i$ in $c$ that also appears in $c'$, the coefficient of
that literal in the resolvent~\eq{resolved} will be 2 but can be
reduced to 1 by virtue of the lemma.\proofend

Cardinality constraints are a bit more interesting.  Suppose that
we are resolving the two clauses
 \[\begin{array}{ccccccccc}
a & + & b & + & c &&& \geq & 2 \\
a & + &   &   & \overline c & + & d & \geq & 1
\end{array}\]
 which we add to get
 \begin{equation}
2a + b + d \geq 2
 \label{e.noncard}
 \end{equation}
 In other words, either $a$ is true or $b$ and $d$ both are.  The 
problem is that this is not a cardinality constraint, and cannot
be rewritten as one.

One possibility is to rewrite~\eq{noncard} as a pair of cardinality
constraints
 \begin{eqnarray}
a+b & \geq & 1 \label{e.iscard1} \\
a+d & \geq & 1 \label{e.iscard2}
\end{eqnarray}
If, however, we want the result of ``resolving'' a pair of constraints
to be a single axiom, we must either select one of the above axioms or
extend our language further.

\subsection{Learning and Relevance Bounds}
\label{s.pb-learn}

The idea of relevance also has a natural generalization to the \pb\
setting.  Recall the basic definition from \secn{relevance}:

\begin{definition} Let $c$ be a clause and $P$ a partial assignment.
Then $c$ is {\em $i$-irrelevant\/} if the number of literals in $c$
that are either unvalued or true under $P$ is at least
$i+1$.\end{definition}

\begin{proposition} Given a partial assignment $P$ and a Boolean clause
$c$, $c$ is $i$-irrelevant if and only if $\poss(c,P) \geq
i$.\end{proposition}

\proof In the Boolean case, the number of literals in $c$ that are
either unvalued or true is $\poss(c,P)+1$ since the right hand side of
the constraint is always 1.  So the irrelevance condition is
 \[\poss(c,P)+1 \geq i+1\]
 and the result follows.\proofend

In the \pb\ case, additional learning techniques are also possible.
Before we present these ideas in detail, however, let us point out
that {\em some\/} sort of inferential extension is needed if we are to
overcome the shortcomings of \dpll\ as revealed by the pigeonhole and
other problems.  After all, recall \prop{pb-res}: \pb\ inference
generalizes Boolean resolution.  So if we begin with a Boolean
axiomatization (as we did in the \php), any derivation using our
techniques will be reproducible using conventional resolution-based
methods, and will therefore be of exponential length.  (A majority of
the inference steps in the various proofs of \prop{php} are not
resolution steps in that no literal cancellations occur.)

\paragraph{Strengthening} The specific method that we will discuss
is from operations research and is used to preprocess mixed integer
programming problems
\cite{Guignard:strengthening,Savelsbergh:preprocess}.

Suppose that after setting $l_0$ to true and applying some form of
propagation to our constraint set, we discover that under this
assumption a constraint $c$ given by \mbox{$\sum w_i l_i \geq r$}
becomes oversatisfied by an amount $s$ in that the sum of the left
hand side is greater (by $s$) than the amount required by the right
hand side of the inequality; in the terms of \defn{poss}, $\curr(c) =
s$.  The oversatisfied constraint $c$ can now be replaced by the
following:
\begin{equation}
	s\lbar_0 + \sum w_i l_i \geq r + s  \label{e.strengthened}
\end{equation}
If $l_0$ is true, we know that $\sum w_i l_i \geq r + s$, so
\eq{strengthened} holds.  If $l_0$ is false, then $s\lbar_0 = s$ and
we still must satisfy the original constraint $\sum w_i l_i \geq r$,
so~\eq{strengthened} still holds.  The new constraint implies the
original one, so no information is lost in the replacement.  

As we have remarked, the OR community uses this technique during
preprocessing.  A literal is fixed, propagation is applied, and any
oversatisfied constraint is strengthened.  Consider the following set
of clauses:
\begin{eqnarray*}
& a + b \geq 1 & \\
& a + c \geq 1 & \\
& b + c \geq 1 &
\end{eqnarray*}
If we set $a$ to false, we must then value both $b$ and $c$ true in
order to satisfy the first two constraints.  The third constraint is
now oversatisfied and can thus be replaced by
\[a + b + c \geq 2 \]
The power of this method is that it allows us to build more complex
axioms from a set of simple ones.  The strengthened constraint will
often subsume some or all of the constraints involved in generating
it.  In this case, the new constraint subsumes all three of the
generating constraints.

\begin{proposition} Let $c$ be a constraint and $P$ a partial assignment.
Then if we can conclude that $\curr(c)\geq s$ for any solution to
our overall problem that extends $P$, we can replace $c$ with
\begin{equation}
 s \sum_P \lbar_i + \sum w_i l_i \geq r + s  \label{e.strengthened2}
\end{equation}
 where the first summation is over literals $l_i\in P$.
\end{proposition}

\proof For any truth assignment that extends $P$,~\eq{strengthened2}
follows from the fact that $\curr(c)\geq s$.  For any truth assignment
$P'$ that does not extend $P$, there is some $l_j\in P$ that is false
in $P'$, and so 
\[s \sum_P \lbar_i \geq s\]
 Combining this with the original constraint $c$ once again produces
\eq{strengthened2}.\proofend

\paragraph{Learning and inference} Before we present some experimental
results related to the effectiveness of \pb\ inference, we should
point out one additional problem that can arise in this setting.  It
is possible that for some branch variable $v$, the result of resolving
the reasons for $v$ and $\neg v$ is a new nogood that is not falsified
by the partial assignment above $v$ in the search space.

As an example \cite{Dixon:strengthen}, suppose that we have a partial
assignment $\set{\neg a,\neg b,c,d}$ and constraints
\begin{eqnarray}
2e+a+c & \geq & 2 \label{e.bad1} \\
2\overline e+b+d & \geq & 2 \label{e.bad2}
\end{eqnarray}
Now we can unit propagate to conclude $e$ by virtue of \eq{bad1} and
$\neg e$ by virtue of \eq{bad2}; it isn't hard to conclude that the
conflict set is $a\vee b$ in that either $a$ or $b$ must be true if
\eq{bad1} and \eq{bad2} are to be simultaneously satisfiable.  But if
we simply add \eq{bad1} and \eq{bad2} and simplify, we get
\[a+b+c+d\geq 2\]
which still allows $a$ and $b$ to both be false.  This difficulty can
be addressed by deriving a cardinality constraint that is guaranteed
to be falsified by the current partial solution being investigated
\cite{Dixon:strengthen}; Chai and Kuehlmann \citeyear{Chai:pb} have
developed a still stronger method.

\paragraph{Experimental results} Many of the ideas that we have
described have been implemented in the \pbchaff\ satisfiability
solver. In an earlier paper \cite{Dixon:strengthen}, we compared
results obtained using {\sc prs}, a \pb\ version of {\sc relsat}, and
those obtained using {\sc relsat}~\cite{Bayardo:relsat}.  {\sc
Pbchaff} is an updated version of {\sc prs} that is modeled closely on
\zchaff~\cite{zchaff}. It implements watched literals for cardinality
constraints and applies the strengthening idea.  Here we compare
\pbchaff's performance to its Boolean counterpart \zchaff.

\begin{table}
\begin{center}
\begin{tabular}{|c|  cc | cc |}
\hline
	& \multicolumn{2}{c|}{\zchaff}	&\multicolumn{2}{c|}{\pbchaff} \\
Instance 	& sec	& nodes		& sec	& nodes\\
\hline 
\type{2pipe} & 0 & 8994 & 0 & 8948 \\
\type{2pipe-1-ooo} & 1 & 10725 & 1 & 9534 \\
\type{2pipe-2-ooo} & 0 & 6690 & 0 & 6706 \\
\type{3pipe} & 7 & 48433 & 12 & 57218 \\
\type{3pipe-1-ooo} & 6 & 33570 & 9 & 36589 \\
\type{3pipe-2-ooo} & 9 & 41251 & 16 & 45003 \\
\type{3pipe-3-ooo} & 11 & 46504 & 19 & 57370 \\
\type{4pipe} & 244 & 411107 & 263 & 382750  \\
\hline
\end{tabular}
\caption{Run time (seconds) and nodes expanded}
\label{t.unsat}
\end{center}
\end{table}

Results on some (unsatisfiable) problem instances from the Velev suite
discussed at the beginning of \secn{inner} are shown in Table
\ref{t.unsat}.  As can be seen, performance is comparable; \pbchaff\
pays a small (although noticeable) cost for its extended expressivity.
The experiments were run on a 1.5 GHz AMD Athlon processor, and both
solvers used the same values for the various tuning parameters
available (relevance and length bounds, etc.).

\begin{table}
\begin{center}
\begin{tabular}{|l|  r r | c r r |}
\hline
  & \multicolumn{2}{c|}{\zchaff} & Preprocess &\multicolumn{2}{c|}{\pbchaff} \\
Instance 	& sec	& nodes		& sec	& sec	& nodes\\
\hline 
hole8.cnf	& 0	& 3544		& 0	& 0	& 11 \\
hole9.cnf	& 1	& 8144		& 0	& 0	& 12  \\
hole10.cnf	& 17	& 27399		& 0	& 0	& 17  \\
hole11.cnf	& 339	& 126962	& 0	& 0	& 15  \\
hole12.cnf	&	&		& 0	& 0	& 20  \\
hole20.cnf	&	&		& 0	& 0	& 34  \\
hole30.cnf	&	&		& 4	& 0	& 52  \\
hole40.cnf	&	&		& 25	& 0	& 75  \\
hole50.cnf  	& 	& 		& 95 	& 0	& 95  \\
\hline
\end{tabular}
\caption{Run time (seconds) and nodes expanded}
\label{t.pigeon}
\end{center}
\end{table}

Results for the \php\ appear in Table \ref{t.pigeon}.  In this case,
\pbchaff\ was permitted to preprocess the problem using strengthening
as described earlier in this section.  {\sc ZChaff} was unable to
solve the problem for twelve or more pigeons with a 1000-second
timeout using a 1.5 GHz Athlon processor.  Not surprisingly, \pbchaff\
with preprocessing dramatically outperformed \zchaff\ on these
instances.\footnote{Without preprocessing, the two systems perform
comparably on this class of problems.  As we have stressed,
representational extensions are of little use without matching
modifications to inference methods.}

\subsection{Proof Complexity}

We have already shown in \prop{php} that \pb\ or cardinality-based
axiomatizations can produce polynomially sized proofs of the \php.  It
is also known that these methods do not lead to polynomially sized
proofs of the clique coloring
problem~\cite{bonet-pb-clique,krajicek-pb-clique,clique}.  The
situation with regard to parity constraints is a bit more interesting.

Let us first point out that it is possible to capture parity
constraints, or modularity constraints generally in a \pb\ setting:

\begin{definition} A {\em modularity constraint\/} is a constraint
$c$ of the form
\begin{equation}
\sum_i w_i l_i~\equiv n (\mod\ m)
\label{e.mod}
\end{equation}
for positive integers $w_i$, $n$ and $m$.
\end{definition}

In the remainder of this section, we show that modularity constraints
can be easily encoded using \pb\ axioms, and also that constraint sets
consisting entirely of mod 2 constraints are easily solved either
directly or using the above encoding, although it is not clear how to
recover the \pb\ encodings from the Boolean versions.

\paragraph{Modularity constraints and \pb\ encodings}  To encode
a modularity constraint in this way, we first note that we can
easily capture an equality axiom of the form
 \begin{equation}
\sum_i w_i l_i = k
 \label{e.equals}
 \end{equation}
 in a \pb\ setting, simply by rewriting~\eq{equals} as the pair of
constraints
\begin{eqnarray*}
\sum_i w_i l_i & \geq & k \\ 
\sum_i w_i \overline l_i & \geq & \sum_i w_i - k
\end{eqnarray*}
 In what follows, we will therefore feel free to write axioms of the
form \eq{equals}.

We now denote by $\floor x$ the floor of $x$, which is to say
the smallest integer not greater than $x$, and have:

\begin{proposition}  Suppose that we have a modularity constraint 
of the form~\eq{mod}.  We set $w=\sum_i w_i$ and introduce new
variables $s_i$ for $i=1,\dots,\floor{\frac wm}$.  Then~\eq{mod} is
equivalent to 
\begin{equation}
\sum_i w_i l_i + \sum_i ms_i = 
  m\Bigl\lfloor \frac wm \Bigr\rfloor + n \label{e.pb-mod} 
\end{equation}
\end{proposition}

\proof Reducing both sides of~\eq{pb-mod} mod m shows that~\eq{pb-mod}
clearly implies~\eq{mod}.  For the converse, note if~\eq{mod} is
satisfied, there is some integer $s$ such that $\sum_i w_i l_i = sm +
n$.  Further, since $\sum_i w_il_i \leq \sum_i w_i = w$, it follows
that $sm+n \leq w$, so that $s\leq \frac{w-n}m\leq \frac wm$ and thus
$s\leq \floor{\frac wm}$.  We can therefore satisfy~\eq{pb-mod} by
valuing exactly that many of the $s_i$ to be true.\proofend

Understand that the introduction of new variables here is not part of
any intended inference procedure; it is simply the fashion in which
the modularity constraints can be captured within a \pb\ setting.

In the case where all of the constraints are parity constraints, we
have:

\begin{proposition}  A set of mod 2 constraints can be solved in
polynomial time.\end{proposition}

\proof An individual constraint (recall that $\oplus$ corresponds to
exclusive or, or addition mod~2)
\[l\oplus \oplus_i l_i = n\]
can be viewed simply as defining
\[ l=n\oplus\oplus_i l_i\]
and this definition can be inserted to remove $l$ from the remaining
constraints.  Continuing in this way, we either define all of the
variables (and can then return a solution) or derive $1=0$ and can
return failure.\proofend

This result, which can be thought of as little more than an
application of Gaussian elimination, is also an instance of a far more
general result of Schaefer's~\citeyear{Schaefer:complexity}.

\begin{proposition}  A set of mod 2 constraints can be solved in
polynomial time using the \pb\ axiomatization given by
\eq{pb-mod}.\end{proposition}

\proof The technique is unchanged.  When we combine
\[l+\sum_i l_i + 2\sum_i s_i = n\]
and
\[l+\sum_i l'_i + 2\sum_i s'_i = n'\]
 we get
\[\sum_i l_i + \sum_i l'_i + 2(\sum_i s_i + \sum_i s'_i + l) = n+n'\]
and can now treat $l$ as one of the auxiliary $s$ variables.  Eventually,
we will get 
\[2 \sum_i s_i = n\]
for a large (but polynomially sized) set $S$ of auxiliary variables
and some $n$ that is either even or odd.  If $n$ is even, we can value
the variables and return a solution; if $n$ is odd and there are $k$
auxiliary variables, we have
\[ \sum_i s_i = \frac n2\]
so
\begin{equation}
\sum_i s_i \geq \frac{n+1}2
\label{e.frac1}
\end{equation}
since each $s_i$ is integral.  But we also have
\[2 \sum_i \overline s_i \geq 2k-n\]
so that
\begin{equation}
\sum_i \overline s_i \geq k - \frac{n-1}2
\label{e.frac2}
\end{equation}
 Adding~\eq{frac1} and~\eq{frac2} produces $k\geq k+1$, a
contradiction.\proofend

Let us point out, however, that if a mod 2 constraint is encoded in a
normal Boolean way, so that $x\oplus y \oplus z=1$ becomes
\begin{eqnarray}
& x\vee y\vee z & \label{e.mod2a} \\
& x \vee \neg y \vee \neg z & \nonumber \\
& \neg x \vee y \vee \neg z & \nonumber \\
& \neg x \vee \neg y \vee z & \label{e.mod2b}
\end{eqnarray}
it is not obvious how the \pb\ analog can be reconstructed.  Here is
the problem we mentioned at the beginning of this section: it is not
enough to simply extend the representation; we need to extend the
inference methods as well.  In fact, even the question of whether
families of mod 2 constraints can be solved in polynomial time by \pb\
methods without the introduction of auxiliary variables as in
\eq{pb-mod} is open.  Other authors have also considered the problem
of reasoning with these constraints directly \cite{Li:mod2}.

\paragraph{\Pb\ constraints and extended resolution}  Finally, let
us clarify a point that we made earlier.  Given that there is an
encoding of $a\vee (b\wedge c)$ as a single \pb\ clause, how can it be
that \pb\ inference is properly below extended resolution in the
$p$-simulation hierarchy?

The answer is as follows.  While the fact that $a\vee (b\wedge c)$ is
logically equivalent to \mbox{$2a+b+c\geq 2$} allows us to remove one
of the variables introduced by extended resolution, we cannot combine
this encoding with others to remove subsequent variables.  As a
specific example, suppose that we learn both
\[a\vee (b\wedge c)\]
and
\[d\vee (b\wedge c)\]
and wish to conclude from this that
\begin{equation}
(a\wedge d)\vee (b\wedge c)
\label{e.pb-bad}
\end{equation}
There is no single \pb\ axiom that is equivalent to \eq{pb-bad}.

\subsection{Summary}
\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& & {\bf p-simulation} && {\bf unit} & \\
& {\bf rep. eff.} & {\bf hierarchy} & {\bf inference} 
 & {\bf propagation} & {\bf learning} \\
\hline
\footnotesize\bf SAT & 1 & EEE& resolution & watched literals&relevance \\ 
\bf{cardinality} & exp & P?E & not unique & watched literals & relevance \\
\bf{PB} & exp & P?E & uniquely defined & watched literals & + strengthening \\
\bf{symmetry} &&&&& \\
\footnotesize\bf QPROP &&&&& \\
\hline
\end{tabular}
\end{center}

As before, a few notes are in order:
\begin{itemize}
\item While both cardinality and \pb\ representations can be exponentially
more efficient than their Boolean counterpart, it is not clear how often
compressions of this magnitude will occur in practice.
\item The entries in the $p$-simulation column indicate that the \php\
is easy, clique coloring remains hard, and the complexity of parity
problems is unknown if no new variables are introduced.
\item The cardinality entry for ``inference'' is intended to reflect
the fact that the natural resolvent of two cardinality constraints
need not be one.
\item \Pb\ systems can use existing learning techniques, augmented
with the strengthening idea.
\end{itemize}

\section{Symmetry}
\label{s.symmetry}  

Given that the \php\ and clique-coloring problems involve a great deal
of symmetry in their arguments, a variety of authors have suggested
extending Boolean representation or inference in a way that allows
this symmetry to be exploited directly.  We will discuss the variety
of approaches that have been proposed by separating them based on
whether or not a modification to the basic resolution inference rule
is suggested.  In any event, we make the following definition:

\begin{definition} Let $T$ be a collection of axioms.  By a {\em
symmetry\/} of $T$ we will mean any permutation $\rho$ of the
variables in $T$ that leaves $T$ itself unchanged.
\end{definition}

As an example, if $T$ consists of the single axiom $x\vee y$, then
$T$ is clearly symmetric under the exchange of $x$ and $y$.  If $T$
contains the two axioms
\[a\vee x\]
and
\[a\vee y\]
then $T$ is once again symmetric under the exchange of $x$ and $y$.

\paragraph{Exploiting symmetry without changing inference}  One way
to exploit symmetry is to modify the set of axioms in a way that
captures the power of the symmetry.  In the \php, for example, we can
argue that since there is a symmetry under the exchange of pigeons or
of holes, we can assume ``without loss of generality'' that pigeon 1
is in hole 1, and then by virtue of a residual symmetry that pigeon 2
is in hole 2, and so on.

The basic idea is to add so-called {\em symmetry-breaking axioms\/} to
our original theory, axioms that break the existing symmetry without
affecting the overall satisfiability of the theory itself.  This idea
was introduced by Crawford et~al.~\citeyear{Ginsberg:symmetry}.

While attractive in theory, there are at least two fundamental
difficulties with the symmetry-breaking approach:

\begin{enumerate}
\item Luks and Roy \citeyear{Luks:symmetry} have shown that breaking
all of the symmetries in any particular problem may require the
introduction of a set of symmetry-breaking axioms of exponential size.
This problem can be sidestepped by breaking only ``most'' of the
symmetries, although little is known about how the set of broken
symmetries is to be selected.
\item Far more serious, the technique can only be applied if the
symmetry in question is global.  This is because the basic argument
that satisfiability is unaffected by the introduction of the new
axioms requires that there be no additional axioms to consider.
\end{enumerate}

In theoretical problems, global symmetries exist.  But in practice,
even the addition of asymmetric axioms that constrain the problem
further (e.g., you can't put pigeon 4 in hole 7) will break the
required global symmetry and render this method inapplicable.  More
problematic still is the possibility of the symmetries being
``obscured'' by replacing the single axiom
\begin{equation}
\neg p_{11} \vee \neg p_{21}
\label{e.breaking}
\end{equation}
with the equivalent pair
\[a\vee \neg p_{11} \vee \neg p_{21}\]
and
\[\neg a\vee \neg p_{11} \vee \neg p_{21}\]
from which \eq{breaking} can obviously be recovered using resolution.
Once again, the symmetry in the original problem has vanished and the
method cannot be applied.

These arguments could perhaps have been anticipated by consideration
of our usual table; since the inference mechanism itself is not
modified (and it is possible to break global symmetries), none of the
entries has changed.  Let us turn, then, to other techniques that
modify inference itself.

\paragraph{Exploiting symmetry by changing inference}

Rather than modifying the set of clauses in the problem, it is also
possible to modify the notion of inference, so that once a particular
nogood has been derived, symmetric equivalents can be derived in a
single step.  The basic idea is due to Krishnamurthy
\citeyear{krish:symmetry} and is as follows:

\begin{lemma} Suppose that $T\models q$ for some theory $T$ and
nogood $q$.  If $\rho$ is a symmetry of $T$, then $T\models
\rho(q)$.\proofend
\end{lemma}

It is not hard to see that this technique allows the \php\ to be
solved in polynomial time, since symmetric versions of specific
conclusions (e.g., pigeon 1 is not in hole 1) can be derived without
repeating the analysis that led to the original.  The dependence on
global symmetries remains, but can be addressed by the following
modification:

\begin{proposition} Let $T$ be a theory, and suppose that  $T'\models q$
for some $T'\subseteq T$ and nogood $q$.  If $\rho$ is a symmetry of
$T'$, then $T\models \rho(q)$.\proofend
\end{proposition}

\noindent Instead of needing to find a symmetry of the theory $T$ in
its entirety, it suffices to find a ``local'' symmetry of the subset
of $T$ that was actually used in the proof of $q$.

This idea, which has been generalized somewhat by Szeider
\citeyear{Szeider:symmetry}, allows us to avoid the fact that the
introduction of additional axioms can break a global symmetry.  The
problem of symmetries that have been obscured as in \eq{breaking}
remains, however, and is accompanied by a new one, the need to
identify local symmetries at each inference step
\cite{Brown:symmetry}.

While it is straightforward to identify the support of any new nogood
$q$ in terms of a subtheory $T'$ of the original theory $T$, finding
the symmetries of any particular theory is equivalent to the graph
isomorphism problem \cite{Crawford:symmetry}.  The precise complexity
of graph isomorphism is unknown, but it is felt likely to be properly
between $P$ and $NP$ \cite{Babai95}.  Our basic table becomes:
\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& & {\bf p-simulation} && {\bf unit} & \\
& {\bf rep. eff.} & {\bf hierarchy} & {\bf inference} 
 & {\bf propagation} & {\bf learning} \\
\hline
\footnotesize\bf SAT & 1 & EEE& resolution & watched literals&relevance \\ 
\bf{cardinality} & exp & P?E & not unique & watched literals & relevance \\
\bf{PB} & exp & P?E & unique & watched literals & + strengthening \\
\bf{symmetry} & 1 & EEE$^*$ & not in P& same as {\sc sat} &
 same as {\sc sat} \\
\footnotesize\bf QPROP &&&&& \\
\hline
\end{tabular}
\end{center}

\begin{itemize}
\item It is not clear how the representational efficiency of this
system is to be described, since a single concluded nogood can serve
as a standin for its image under the symmetries of the proof that
produced it.
\item While specific instances of the \php\ and clique coloring
problems can be addressed using symmetries, even trivial modifications
of these problems render the techniques inapplicable.  Hence the
appearance of the asterisk in the above table: ``Textbook'' problem
instances may admit polynomially sized proofs, but most instances
require proofs of exponential length.  Parity problems do not seem to
be amenable to these techniques at all.
\item As we have remarked, inference using Krishnamurthy's or related
ideas appears to require multiple solutions of the graph isomorphism
problem, and is therefore unlikely to remain in $P$.
\end{itemize}

We know of no implemented system based on the ideas discussed in this
section.

\section{Quantification and QPROP}
\label{s.qprop}

We conclude our survey with an examination of ideas that have been
used in trying to extend the Boolean work to cope with theories that
are most naturally thought of using quantification of some sort.
Indeed, as \bs\ engines are applied to ever larger problems, many of
the theories in question are produced in large part by constructing
the set of ground instances of quantified axioms such as
\begin{equation}
\forall{xyz}.[a(x,y) \wedge b(y,z) \rightarrow c(x,z)]
\label{e.qprop}
\end{equation}
If $d$ is the size of the domain from which $x$, $y$ and $z$ are
taken, this single axiom has $d^3$ ground instances.  Researchers have
dealt with this difficulty by buying machines with more memory or by
finding clever axiomatizations for which ground theories remain
manageably sized~\cite{Selman:blackbox}.  In general, however, memory
and cleverness are both scarce resources and a more natural solution
needs to be found.

We will call a clause such as~\eq{qprop} {\em quantified\/}, and
assume throughout this section that the quantification is universal as
opposed to existential, and that the domains of quantification are
finite.\footnote{There appears to be no effective alternative but to
treat existentially quantified clauses as simple disjunctions, as in
\eq{php1}.}

As we remarked at the beginning of this section, quantified clauses
are common in encodings of realistic problems, and these problems have
in general been solved by converting quantified clauses to standard
propositional formulae.  The quantifiers are expanded first (possible
because the domains of quantification are finite), and the resulting
set of predicates is then ``linearized'' by relabeling all of the
atoms so that, for example, $a(2,3)$ might become $v_{24}$.  The
number of ground clauses produced is exponential in the number of
variables in the quantified clause.

\subsection{Unit Propagation}

Our primary goal here is to work with the quantified formulation
directly, as opposed to its much larger ground translation.
Unfortunately, there are significant constant-factor costs incurred in
doing so, since each inference step will need to deal with issues
involving the bindings of the variables in question.  Simply finding
the value assigned to $a(2,3)$ might well take several times longer
than finding the value assigned to the equivalent $v_{24}$.  Finding
all occurrences of a given literal can be achieved in the ground case
by simple indexing schemes, whereas in the quantified case this is
likely to require a unification step.  While unification can be
performed in time linear in the length of the terms being unified, it
is obviously not as efficient as a simple equality check.  Such
routine but essential operations can be expected to significantly slow
the cost of every inference undertaken by the system.

Our fundamental point here is that while there are costs associated
with using quantified axioms, there are significant savings as well.
These savings are a consequence of the fact that the basic \up\
procedure uses an amount of time that scales roughly linearly with the
size of the theory; use of quantified axioms can reduce the size of
the theory so substantially that the constant-factor costs can be
overcome.

We will make this argument in two phases.  In \secn{subsearch}, we
generalize a specific computational subtask that is shared by \up\ and
other satisfiability procedures such as \wsat.  We will show this
generalization to be NP-complete in a formal sense, and we call it
{\em subsearch\/} for that reason.  The specific procedures for \up\
and as needed by \wsat\ encounter this NP-complete subproblem at each
inference step, and we show that while subsearch is generally not a
problem for randomly generated theories, the subsearch cost can be
expected to dominate the running time on more realistic instances.

In \secn{quantify}, we discuss other consequences of the fact that
subsearch is NP-complete.  Search techniques can be used to speed the
solution of NP-complete problems, and subsearch is no exception.  We
show that quantified axiomatizations support the application of simple
search techniques to the subsearch problem, and argue that realistic
examples are likely to lead to subsearch problems of only polynomial
difficulty although existing \up\ implementations solve them
exponentially.

\subsubsection{Subsearch}
\label{s.subsearch}

Each iteration of \dpll\ (or \wsat) involves a search through the
original theory for clauses that satisfy some numeric property.  The
specific examples that we have already seen of this are the following:
\begin{enumerate}
\item In Procedure \ref{p.dp} (\dpll) (and similarly in \wsat), we
need to determine if $P$ is a solution to the problem at hand. This
involves searching for an unsatisfied clause.
\item In Procedure \ref{p.unit} (\up), we need to find unsatisfied
clauses that contain at most one unvalued literal.
\end{enumerate}
 In addition, \wsat\ needs to compute the number of clauses that will
become unsatisfied when a particular variable is flipped.

All of these tasks can be rewritten using the following:

\begin{definition} Suppose $C$ is a set of quantified clauses, and $P$
is a partial assignment of values to the atoms in those clauses.  We
will denote by $S_u^s(C,P)$ the set of ground instances of $C$ that
have $u$ literals unvalued by $P$ and $s$ literals satisfied by the
assignments in $P$.\footnote{In interpreting the expression
$S_u^s(C,P)$, the set $C$ of clauses and partial assignment $P$ should
generally be clear from context.  The superscript refers to the number
of satisfied literals because satisfied literals are ``super good''
and the subscript refers to the unvalued literals because unvalued
literals aren't so good.}

We will say that the {\em checking problem\/} is that of determining
whether $S_u^s(C,P) \neq \emptyset$.  By a {\em subsearch problem}, we
will mean an instance of the checking problem, or the problem of
either enumerating $S_u^s(C,P)$ or determining its size.
\label{d.subsearch}
\end{definition}

\begin{proposition} For fixed $u$ and $s$, the checking problem is
NP-complete.
\label{p.np}
\end{proposition}

\proof Checking is in NP, since a witness that $S_u^s(C,P) \neq
\emptyset$ need simply give suitable bindings for the variables in
each clause of $C$.

To see NP-hardness, we assume $u=s=0$; other cases are not
significantly different.  We reduce from a binary constraint
satisfaction problem (\csp), producing a single clause $C$ and set of
bindings $P$ such that $S_0^0(C,P) \neq \emptyset$ if and only if the
original binary \csp\ was satisfiable.  The basic idea is that each
variable in the constraint problem will become a quantified variable
in $C$.

Suppose that we have a binary \csp\ $\Sigma$ with variables
$v_1,\ldots,v_n$ and with $m$ binary constraints of the form
$(v_{i1},v_{i2}) \in c_i$, where $(v_{i1},v_{i2})$ is the pair of
variables constrained by $c_i$.  For each such constraint, we
introduce a corresponding binary relation $r_i(v_{i1},v_{i2})$, and
take $C$ to be the single quantified clause \mbox{$\forall
v_1,\ldots,v_n. \vee_i r_i(v_{i1},v_{i2})$}.  For the assignment $P$,
we set $r_i(v_{i1},v_{i2})$ to false for all $(v_{i1},v_{i2}) \in
c_i$, and to true otherwise.

Now note that since $P$ values every instance of every $r_i$,
$S_0^0(C,P)$ will be nonempty if and only if there is a set of values
for $v_i$ such that every literal in $\vee_i r_i(v_{i_1},v_{i_2})$ is
false.  Since a literal $r_i(v_{i_1},v_{i_2})$ is false just in the
case the original constraint $c_i$ is satisfied, it follows that
$S_0^0(C,P) \neq \emptyset$ if and only if the original \csp\ $\Sigma$
was satisfiable.\proofend

Before moving on, let us place this result in context.  First, and
most important, note that the fact that the checking problem is
NP-complete does not imply that \qprop\ is an unwieldy representation;
the subsearch problem does indeed appear to be exponential in the size
of the \qprop\ axioms, but there are exponentially fewer of them than
in the ground case.  So, as for similar results elsewhere
\cite{smallok,Papadimitriou:smallok}, there is no net effect on
complexity.

Second, the result embodied in \prop{np} appears to be a general
phenomenon in that propagation is more difficult for more compact
representations.  Our earlier discussion of cardinality and \pb\
axioms, for which the complexity of \up\ was unchanged from the
Boolean case, appears to be much more the exception than the rule.  As
we have already remarked, if we extend the \pb\ representation only
slightly, so that in addition to axioms of the form
\begin{equation}
\sum_i w_i l_i \geq k
\label{e.pbx}
\end{equation}
as in \defn{pb} we allow axioms such as
\[\sum_i w_i l_i = k\]
(replacing the inequality in \eq{pbx} with an equality), determining
whether a single axiom is satisfiable becomes weakly NP-complete.
Symmetry, the other example we have examined, involves no effective
change in the representational power of a single axiom.

Here is a recasting of \up\ in terms of \defn{subsearch}:

\begin{procedure}[\Up] To compute $\proc{Unit-Propagate}(P)$:\em
\begin{codebox}
\li \While $S_0^0(C,P) = \emptyset$ \kw{and} $S_1^0(C,P) \neq \emptyset$
\li \Do select $c\in S_1^0(C,P)$ 
\li	$v \gets $ the variable in $c$ unassigned by $P$ 
\li     $P \gets P \cup \{ v = V : \mbox{$V$ is selected so that $c$ 
	 is satisfied} \}$  
	\End
\li \Return $P$
\end{codebox}
\end{procedure}
 It is important to recognize that this recasting is not changing the
procedure in any significant way; it is simply making explicit the
subsearch tasks that were previously described only implicitly.  The
procedure itself is unchanged, and other procedural details such as
variable and value choice heuristics are irrelevant to the general
point that \up\ depends on solving a subsearch instance at every step.
\Wsat\ is similar.

\subsubsection{Subsearch and quantification}
\label{s.quantify}

As we discussed in \secn{inner}, efficient implementations of \sat\
solvers go to great lengths to minimize the amount of time spent
solving subsearch problems.  While the watched literal idea is the
most efficient mechanism known here, we will discuss the problem in
terms of a simpler scheme that maintains and updates \poss\ and \curr\
counts for each clause.  As discussed earlier, this scheme is about
half as fast as the watched literal approach, and the general
arguments that we will make can be expected to lead to more than
constant-factor improvements.\footnote{We know of no effective way to
lift the watched literal idea to the \qprop\ setting.  But as we will
see when we discuss the \zap\ implementation \cite{Ginsberg:zap3}, a
still broader generalization allows watched literals to return in an
elegant and far more general way.}

For notational convenience in what follows, suppose that $C$ is a
quantified theory and that $l$ is a ground literal.  By $C_l$ we will
mean that subset of the clauses in $C$ that include terms of which $l$
is an instance.  If $C$ contains quantified clauses, then $C_l$ will
as well; the clauses in $C_l$ can be found by matching the literal $l$
against the clauses in $C$.

As discussed in \secn{inner}, it is possible to compute $S_u^s(C,P)$
once during an initialization phase, and then update it incrementally.
In terms of \defn{subsearch}, the update rule might be one such as
\[S_0^0(C,P') = S_0^0(C,P) \cup S_1^0(C_{\neg l},P)\] if the literal
$l$ is changed from unvalued to true.  $P'$ here is the partial
assignment after the update; $P$ is the assignment before.  To compute
the number of fully assigned but unsatisfied clauses after the update,
we start with the number before, and add newly unsatisfied clauses
(unsatisfied clauses previously containing the single unvalued literal
$\neg l$).

As we argued previously, reorganizing the computation in this way
leads to substantial speedups because the subsearch problem being
solved is no longer NP-complete in the size of $C$, but only in the
size of $C_l$ or $C_{\neg l}$.  These incremental techniques are
essential to the performance of modern search implementations because
the runtime of these implementations is dominated by the time spent in
propagation (i.e., subsearch).

Given that the subsearch computation time is potentially exponential
in the size of the subtheory $C_l$ when the literal $l$ is valued or
unvalued, let us now consider the questions of how much of a concern
this is in practice, and of what (if anything) can be done about it.
After all, one of the primary lessons of recent satisfiability
research is that problems that are NP-hard in theory tend strongly not
to be exponentially difficult in practice.

Let us begin by noting that subsearch is {\em not\/} likely to be much
of an issue for the randomly generated satisfiability problems that
were the focus of research in the 1990's and drove the development of
algorithms such as \wsat.  The reason for this is that if $n$ is the
number of clauses in a theory $C$ and $v$ is the number of variables
in $C$, then random problems are difficult only for fairly narrow
ranges of values of the ratio $n/v$ \cite{Coarfa:3sat}.  For 3-SAT
(where every clause in $C$ contains exactly three literals), difficult
random problems appear at $n/v \approx 4.2$ \cite{Selman:science}.
For such a problem, the number of clauses in which a particular
literal $l$ appears will be small (on average $3 \times 4.2 / 2 = 6.3$
for random 3-SAT).  Thus the size of the relevant subtheory $C_l$ or
$C_{\neg l}$ will also be small, and while subsearch cost still tends
to dominate the running time of the algorithms in question, there is
little to be gained by applying sophisticated techniques to reduce the
time needed to examine a relative handful of clauses.

For realistic problems, the situation is dramatically different.  Here
is an axiom from a logistics domain encoded in {\sc satplan} style
\cite{satplan}:

\vbox{
\begin{eqnarray}
  && \at(o,l,t) \wedge \duration(l,l',dt) \wedge \nonumber \\
  &&  \qquad \qquad \between(t,t',t + dt) \rightarrow \neg\at(o,l',t')
  \label{e.long-qprop}
\end{eqnarray}}
\noindent This axiom says that if an object $o$ is at location $l$ at
time $t$ and it takes time $dt$ to fly from $l$ to $l'$, and $t'$ is
between $t$ and $t+dt$, then $o$ cannot be at $l'$ at $t'$.

A given ground atom of the form $\at(o,l,t)$ will appear in $|t|^2|l|$
clauses of the above form, where $|t|$ is the number of time points or
increments and $|l|$ is the number of locations.  Even if there are
only 100 of each, the $10^6$ axioms created seem likely to make
computing $S_u^s(C_l,P)$ impractical.

Let us examine this computation in a bit more detail.  Suppose that we
do indeed have a variable $a = \at(O,L,T)$ for fixed $O$, $L$ and $T$,
and that we are interested in counting the number of unit propagations
that will be possible if we set $a$ to true.  In other words, we want
to know how many instances of~\eq{long-qprop} will be unsatisfied and
have a single unvalued literal after we do so.

Existing implementations, faced with this problem (or an analogous one
if \wsat\ or another approach is used), will now consider axioms of
the form \eq{long-qprop} for $o$, $l$ and $t$ bound and as $l'$, $t'$
and $dt$ are allowed to vary.  They examine every axiom of this form
and simply count the number of possible unit propagations.

The watched literal idea in isolation cannot help with this problem.
If, for example, we watch only the \duration\ and \between\ predicates
in \eq{long-qprop}, we reduce by half the probability that we need to
solve a subsearch problem when a particular variable is valued, but in
those cases where the problem is encountered, it is as fierce as ever.

The existing approach to solving subsearch problems is taken because
existing systems use not quantified clauses such as~\eq{long-qprop},
but the set of ground instances of those clauses.  Computing
$S_u^s(C,P)$ for ground $C$ involves simply checking each axiom
individually; indeed, once the axiom has been replaced by its set of
ground instances, no other approach seems possible.

Set against the context of a quantified axiom, however, this seems
inappropriate.  Computing $S_u^s(C,P)$ for a quantified $C$ by
reducing $C$ to a set of ground clauses and then examining each is
equivalent to solving the original NP-complete problem by generate and
test -- and if there is one thing that we can state with confidence
about NP-complete problems, it is that generate and test is not in
general an effective way to solve them.

Returning to our example with $\at(O,L,T)$ true, we are looking for
variable bindings for $l'$, $dt$ and $t'$ such that,
amongst $\neg\duration(L,l',dt)$, $\neg\between(T,t',T + dt)$ and
$\neg\at(O,l',t')$,
precisely  two of these literals  are false and the third is unvalued.  \prop{np}
suggests that subsearch will be exponentially hard (with
respect to the number of quantifiers) in the worst case, 
but what is it likely to be like in practice?

In practice, things are going to be much better.  Suppose that for
some possible destination $l'$, we know that $\duration(L,l',dt)$ is
false for all $dt$ except some specific value $D$.  We can
immediately ignore all bindings for $dt$ except for $dt=D$,
reducing the size of the subsearch space by a factor of $|t|$.  If
$D$ depended on previous choices in the search (aircraft loads,
etc.), it would be impossible to perform this analysis in advance and
thereby remove the unnecessary bindings in the ground theory.

Pushing this example somewhat further, suppose that $D$ is so small
that $T+D$ is the time point immediately after $T$.  In other words,
$\between(T,t',T + D)$ will always be false, so that
$\neg\between(T,t',T + D)$ will always be true and no unit propagation
will be possible for any value of $t'$ at all.  We can ``backtrack''
away from the unfortunate choice of destination $l'$ in our
(sub)search for variable bindings for which unit propagation is
possible.  Such backtracking is not supported by the generate-and-test
subsearch philosophy used by existing implementations.

This sort of computational savings is likely to be possible in
general.  For naturally occurring theories, most of the variables
involved are likely to be either unvalued (because we have not yet
managed to determine their truth values) or false (by virtue of the
closed-world assumption, \citeR{Reiter:cwa}, if nothing else).  Domain
constraints will typically be of the form $a_1 \wedge \cdots \wedge
a_k \rightarrow l$, where the premises $a_i$ are variables and the
conclusion $l$ is a literal of unknown sign.  Unit propagation (or
other likely instances of the subsearch problem) will thus involve
finding a situation where at most one of the $a_i$ is unvalued, and
the rest are true.  If we use efficient data structures to identify
those instances of relational expressions that are true, it is not
unreasonable to expect that most instances of the subsearch problem
will be soluble in time polynomial in the length of the clauses
involved, as opposed to exponential in that length.

\subsection{Inference and Learning}

As in \secn{pseudo}, working with a modified representation allows
certain inference techniques that are not applicable in the Boolean
case.

As an example, suppose that we are resolving
\[\neg a(A,B) \vee \neg b(B,C) \vee c(C)\]
with
\[\neg c(C) \vee d(C,D)\]
to conclude 
\begin{equation}
\neg a(A,B) \vee \neg b(B,C) \vee d(C,D)
\label{e.qpres}
\end{equation}
where the capital letters indicate ground elements of the domain as
before and the resolvents are actually ground instances of
\begin{equation}
\neg a(x,y) \vee \neg b(y,C) \vee c(C)
\label{e.qpres1}
\end{equation}
and
\begin{equation}
\neg c(z) \vee d(z,w)
\label{e.qpres2}
\end{equation}
It is obviously possible to resolve \eq{qpres1} and \eq{qpres2} directly
to obtain
\begin{equation}
\neg a(x,y) \vee \neg b(y,C) \vee d(C,w)
\label{e.general}
\end{equation}
which is more general than \eq{qpres}.  For a procedure that learns
new nogoods and uses them to prune the resulting search, the impact of
learning the more general \eq{general} can be substantial and can
easily outweigh the cost of the unification step required to conclude
that $c(C)$ and $\neg c(z)$ resolve if $z=C$.  We have also discussed
this elsewhere~\cite{Parkes:thesis}.

There are two new difficulties that arise when we implement these
ideas.  The first is a consequence of the fact that resolution can be
ambiguously defined for two quantified clauses.  Consider resolving
\begin{equation}
a(A,x) \vee a(y,B)
\label{e.ambig1}
\end{equation}
with
\begin{equation}
\overline a(A,B) \vee b(A,B)
\label{e.ambig2}
\end{equation}
 If we unify the first term in \eq{ambig2} with the first term in
\eq{ambig1}, we obtain $a(y,B) \vee b(A,B)$ as the resolvent; if we
unify with the second term of \eq{ambig1}, we obtain $a(A,x) \vee
b(A,B)$.

In practice, however, this need not be a problem:

\begin{proposition} Let $c_1$ and $c_2$ be two lifted clauses, and
$g_1$ and $g_2$ ground instances that resolve to produce $g$.  Then
there is a unique natural resolvent of $c_1$ and $c_2$ of which $g$ is
a ground instance.\end{proposition}

\proof If there is more than one pair of resolving literals in $g_1$
and $g_2$ the result of the resolution will be vacuous, so we can
assume that there is a single literal $l$ in $g_1$ with $\neg l$ in
$g_2$.  If $l$ is the $i$th literal in $g_1$ and $\neg l$ the $j$th
literal in $g_2$, it follows that we can resolve the original $c_1$
and $c_2$ by unifying the $i$th literal in $c_1$ and the $j$th literal
in $c_2$.  It is clear that this resolution will be a generalization
of $g$.\proofend

What this suggests is that the reasons being associated with literal
values be not the lifted nogoods that are retained as clauses, but
ground instances thereof that were initially used to prune the search
space and can subsequently be used to break ambiguities in learning.

The second difficulty is far more substantial.  Suppose that
we have the axiom
\[\neg a(x,y) \vee \neg a(y,z) \vee a(x,z)\]
or, in a more familiar form, the usual transitivity axiom
\[a(x,y) \wedge a(y,z) \rightarrow a(x,z)\]
 This might be used in reasoning about a logistics problem, for
example, if it gave conditions under which two cities were connected
by roads.

Now suppose that we are trying to prove $a(A,B)$ for an
$A$ and a $B$ that are ``far apart'' given the skeleton
of the relation $a$ that we already know.  It is possible that we
use resolution to derive
\[a(A,x) \wedge a(x,B) \rightarrow a(A,B)\]
 as we search for a proof involving a single intermediate location,
and then
\[a(A,x) \wedge a(x,y) \wedge a(y,B) \rightarrow a(A,B)\]
as we search for a proof involving two such locations, and so on,
eventually deriving the wonderfully concise
\begin{equation}
a(A,x_1) \wedge \cdots \wedge a(x_n,B) \rightarrow a(A,B)
\label{e.bad}
\end{equation}
for some suitably large $n$.

The problem is that if $d$ is the size of our domain, \eq{bad} will
have $d^n$ ground instances and is in danger of overwhelming our \up\
algorithm even in the presence of reasonably sophisticated subsearch
techniques.  Some technique needs to be adopted to ensure that this
difficulty is sidestepped in practice.  One way to do this is to learn
not the fully general \eq{bad}, but a partially bound instance that
has fewer ground instances.

\begin{procedure} To construct $\learn(c,g)$, the nogood that
will be learned after a clause $c$ has been produced in response to a
backtrack, with $g$ the ground reason associated with $c$:\em
\begin{codebox}
\li \While $c$ has a ground instance that is $i$-irrelevant
\li	\Do
		$v \gets $ a variable in $c$
\li		bind $v$ to its value in $g$ 
	\End
\li \Return $c$
\end{codebox}
\label{p.learn}		
\end{procedure}

We may still learn a nogood with an exponential number of ground
instances, but at least have some reason to believe that each of these
instances will be useful in pruning subsequent search.  Note that
there is a subsearch component to Procedure \ref{p.learn}, since we
need to find ground instances of $c$ that are irrelevant.  This cost
is incurred only once when the clause is learned, however, and not at
every unit propagation or other use.

It might seem more natural to learn the general \eq{bad}, but to
modify the subsearch algorithm used in \up\ so that only a subset of
the candidate clauses is considered.  As above, the most natural
approach would likely be to restrict the subsearch to clauses of a
particular irrelevance or better.  Unfortunately, this won't help,
since irrelevant clauses cannot be unit.  Restricting the subsearch to
relevant clauses is no more useful in practice than requiring that any
search algorithm expand only successful nodes.

Before moving on, let us note that a similar phenomenon occurs in the
\pb\ case.  Suppose we have a partial assignment $\set{\neg b,c,\neg
d,e}$ and constraints
\begin{eqnarray}
a+d+ \overline{e}& \geq& 1 \label{e.c1} \\
\overline{a} + b + c& \geq& 2 \label{e.c2}
\end{eqnarray}
Unit propagation now causes the variable $a$ to be simultaneously true
(by virtue of \eq{c1}) and false (because of \eq{c2}).  Resolving these
reasons together as in \prop{resolution} gives us
\begin{equation}
b+c+d + \overline{e} \geq 2
\label{e.c3}
\end{equation}

The conflict set here is easily seen to be $\set{\neg b,\neg d,e}$,
and this is indeed prohibited by the derived constraint \eq{c3}.  But
\eq{c3} eliminates some additional bad assignments as well, such as
$\set{\neg c,\neg d,e}$.  Just as in the lifted case, we have learned
something about a portion of the search space that has yet to be
examined.

\subsection{Summary}
\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& & {\bf p-simulation} && {\bf unit} & \\
& {\bf rep. eff.} & {\bf hierarchy} & {\bf inference} 
 & {\bf propagation} & {\bf learning} \\
\hline
\footnotesize\bf SAT & 1 & EEE& resolution & watched literals&relevance \\ 
\bf{cardinality} & exp & P?E & not unique & watched literals & relevance \\
\bf{PB} & exp & P?E & unique & watched literals & + strengthening \\
\bf{symmetry} & 1 & EEE$^*$ & not in P& same as {\sc sat} &
 same as {\sc sat} \\
\footnotesize\bf QPROP & exp & ??? & in P using reasons & exp improvement &
 + first-order \\
\hline
\end{tabular}
\end{center}

As usual, there are a few points to be made.
\begin{itemize}
\item There is an important difference in practice between the
exponential savings in representation provided by \qprop\ and the
savings provided by \pb\ or cardinality encodings.  While the
exponential savings in previous cases were mathematical possibilities
that were of uncertain use in practice, the savings provided by
\qprop\ can be expected to be achieved in any axiomatization that is
constructed by grounding out a relative handful of universally
quantified physical laws.
\item It is not clear whether \qprop\ leads to polynomially sized
solutions to the pigeonhole and clique coloring problems.  It appears
at first blush that it should, since quantification over pigeons or
holes is the \qprop\ analog of the identification of the corresponding
symmetry as in the previous section.  We know of no detailed proof in
the literature, however, and our attempts to construct one have been
unsuccessful.  Similar remarks apply to parity problems.
\item Inference in \qprop\ requires the introduction of a (linear
complexity) unification step, and is only uniquely defined if
reasons are maintained for the choices made in the search.
\item The exponential savings claimed for \up\ are obviously an
average case result, as opposed to a worst case one.  They are a
consequence of the fact that it is possible to use subsearch as part
of \up, as opposed to the ``generate and test'' mechanism used by
ground methods.
\item In addition to the usual idea of relevance-based learning,
quantified methods can extend the power of individual nogoods by
resolving quantified clauses instead of their ground instances.
\end{itemize}

Finally, we remark that a representation very similar to \qprop\ has
also been used in Answer Set Programming (\asp)
\cite{Marek:stable,Niemela:ASP} under the name ``propositional
schemata'' \cite{East:propositional,East:PS}.  The approach used in
\asp\ resembles existing satisfiability work, however, in that clauses
are always grounded out.  The potential advantages of intelligent
subsearch are thus not exploited, although we expect that many of the
motivations and results given here would also apply in \asp.  In fact,
\asp\ has many features in common with \sat:
\begin{itemize}
\item In the most commonly used semantics, that of (non-disjunctive)
stable model logic programming \cite{Gelfond:stable}, the
representational power is precisely that of NP (or $NP^{NP}$ for
disjunctive programming).
\item Cardinality constraints are allowed \cite{East:PS,Simons:stable}.
\item Solution methods \cite{dlv02,Niemela:ASP,Simons:stable} use
\dpll\ and some form of propagation.
\end{itemize}

The most significant difference between conventional satisfiability
work and \asp\ with stable model semantics is that the relevant logic
is not classical but the ``logic of here and there''
\cite{Pearce:LHT}.  In the logic of here and there, the law of the
excluded middle does not hold, only the weaker $\neg p \vee \neg \neg
p$. This is sufficient for \dpll\ to be applied, but does imply that
classical resolution is no longer valid.  As a result, there seems to
be no proof theory for the resulting system, and learning within this
framework is not yet understood.  Backjumping is used, but the
mechanism does not seem to learn new rules from failed subtrees in the
search.  In an analogous way, cardinality constraints are used but
cutting plane proof systems are not.  Despite the many parallels
between \sat\ and \asp, including the approach in this survey seems to
be somewhat premature.

\section{Conclusion}
\label{s.conclusion}

Satisfiability algorithms have too often been developed against the
framework provided by either random instances or, worse still,
instances that have been designed solely to show that the technique
being proposed has computational merit.  The algorithms themselves
have thus tended to ignore problem features that dominate the
computational requirements when they are applied to real problems.

On such realistic problems, it is possible to both improve the speed
of the algorithms' inner loops (via \qprop\ and subsearch) and to
reduce the number of times that the inner loops need to be executed
(via learning and a move up the $p$-simulation hierarchy).  Both of
these classes of improvements arise because the problems in question
have {\em structure}.  The structure can be learned as nogoods, or
used to re-represent the problem using \pb\ or quantified expressions.

It is true that the table in the previous subsection can be viewed as
a survey of recent work on satisfiability, and it is also true that the
table can be viewed as a rational reconstruction of the goals of the
researchers who have investigated various representational extensions.
But to our mind, the table is more accurately viewed as a report on
the extent to which these linguistic or semantic modifications
successfully capture problem structure.

Every column in the table is about structure.  Improved
representational efficiency is only possible if the problem itself has
structure that a Boolean axiomatization typically obscures.  It is
structure that allows progress to be made in terms of proof
complexity.  The structure must be preserved by the basic inference
mechanism of the system in question if it is to remain useful, and
\qprop's ability to speed the inner loop of \up\ is a direct
consequence of the structure present in the subsearch problem.
Finally, learning itself can be thought of as a search for reasonably
concise descriptions of large sections of the search space that
contain no solutions -- in other words, learning is the discovery of
structure in the search space itself.

This is the setting against which the next two papers in this series
are set.  If so much of the progress in satisfiability techniques can
be thought of as structure exploitation, then surely it is natural to
attempt to understand and to exploit that structure directly.  As we
will see, not only do the techniques we have discussed work by
exploiting structure, but they all exploit different instances of a
{\em single\/} structure.  The \zap\ work is an attempt to understand,
generalize and streamline previous results by setting them in this
uniform setting.

\section*{Acknowledgments}

We would like to thank the members of {\sc cirl}, the technical staff
of On Time Systems, and Eugene Luks and David Hofer from the CIS
department at the University of Oregon for their assistance with the
ideas in this series of papers.  We would also like to thank the
anonymous reviewers for their comments and suggestions, which we found
extremely valuable.

This work was sponsored in part by grants from Air Force Office of
Scientific Research ({\sc afosr}) number F49620-92-J-0384, the Air
Force Research Laboratory ({\sc afrl}) number F30602-97-0294, Small
Business Technology Transfer Research, Advanced Technology Institute
({\sc sttr-ati}) number 20000766, Office of Naval Research ({\sc onr})
number N00014-00-C-0233, and the Defense Advanced Research Projects
Agency ({\sc darpa}) and the Air Force Research Laboratory, Rome, NY,
under agreements numbered F30602-95-1-0023, F30602-97-1-0294,
F30602-98-2-0181, F30602-00-2-0534, and F33615-02-C-4032.  The views
expressed are those of the authors.

\bibliography{bib}
\bibliographystyle{theapa}

\end{document}
