%\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}{}
\newenvironment{olddefinition}[1]{\smallskip\noindent{\bf Definition #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\squar{\mathchoice\sqr34\sqr34\sqr{2.1}3\sqr{1.5}3}
\def\proofend{\mbox{\nobreak\qquad$\squar$\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{amsfonts}
\usepackage{clrscode}
\usepackage{graphics}
\usepackage{graphicx}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{requirement}[theorem]{Requirement}

\jairheading{22}{2004}{481-534}{08/04}{12/04}
\ShortHeadings{ZAP 2: Theory}
{Dixon, Ginsberg, Luks \& Parkes}
\firstpageno{481}

\begin{document}

\title{Generalizing Boolean Satisfiability II: Theory}

\author{\name Heidi E. Dixon \email dixon@otsys.com \\
       \addr On Time Systems, Inc. \\
       1850 Millrace, Suite 1 \\
       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 Eugene M. Luks \email luks@cs.uoregon.edu \\
       \addr Computer and Information Science \\
       University of Oregon \\
       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{\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{\cnf}{{\sc cnf}}
\newcommand{\zap}{{\sc zap}}
\newcommand{\Zap}{{\sc Zap}}
\newcommand{\zapz}{{\sc zap1}}
\newcommand{\wsat}{{\sc wsat}}
\newcommand{\wsatu}{{\sc wsat(U)}}
\newcommand{\wsatub}{{\sc wsat(UB)}}
\newcommand{\Wsat}{{\sc Wsat}}
\newcommand{\csp}{{\sc csp}}
\newcommand{\sat}{{\sc sat}}
\newcommand{\Sat}{{\sc Sat}}
\newcommand{\rbl}{{\sc rbl}}
\newcommand{\Rbl}{{\sc Rbl}}
\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{\Sym}{\mbox{\rm Sym}}
\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}}
\newcommand{\resolve}{\type{resolve}}
\newcommand{\ext}{\type{extn}}
\newcommand{\sext}{\type{stab}}
\newcommand{\grp}[1]{\langle #1 \rangle}
\newcommand{\cgt}{computational group theory}

\maketitle

\begin{abstract}
  This is the second 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
presents the theoretical basis for the ideas underlying \zap, arguing
that existing ideas in this area exploit a single, recurring structure
in that multiple database axioms can be obtained by operating on a
single axiom using a subgroup of the group of permutations on the
literals in the problem.  We argue that the group structure precisely
captures the general structure at which earlier approaches hinted, and
give numerous examples of its use.  We go on to extend the
Davis-Putnam-Logemann-Loveland inference procedure to this broader
setting, and show that earlier computational improvements are either
subsumed or left intact by the new method.  The third paper in this
series discusses \zap's implementation and presents experimental
performance results.
\end{abstract}

\section{Introduction}

This is the second of a planned series of three papers describing
\zap, a satisfiability engine that substantially generalizes existing
tools while retaining the performance characteristics of existing
high-performance solvers such as \zchaff~\cite{zchaff}.\footnote{The
first paper has appeared in {\sc jair}; the third is currently
available as a technical report \cite{Ginsberg:zap3} but has not yet
been peer reviewed.}  In the first paper \cite{Ginsberg:zap1}, to
which we will refer as \zapz, we discussed a variety of existing
computational improvements to the Davis-Putnam-Logemann-Loveland
(\dpll) inference procedure, eventually producing the following table.
The rows and columns are described on this page and the next.

\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& {\bf efficiency} & {\bf proof} & & {\bf propagation}& {\bf learning} \\
& {\bf of rep'n} & {\bf length} & {\bf resolution} 
 & {\bf technique} & {\bf method} \\
\hline\hline
\footnotesize\bf SAT & --- & EEE& --- & watched literals&relevance \\ \hline
\bf{cardinality} & exponential & P?E & not unique & watched literals & relevance \\ \hline
\bf{\parbox{.8in}{\vspace*{.03in}pseudo-\hspace*{.2in}Boolean\vspace*{.03in}}} & exponential & P?E & unique & watched literals & + strengthening \\ \hline
\bf{symmetry} & --- & EEE$^*$ & not believed in P& same as {\sc sat} &
 same as {\sc sat} \\ \hline
\footnotesize\bf QPROP & exponential & ??? & in P using reasons & exp improvement &
 + first-order \\
\hline
\end{tabular}
\end{center}

The rows of the table correspond to observations regarding existing
representations used in satisfiability research, as reflected in the
labels in the first column:\footnote{Please see the preceding paper
\zapz\ \cite{Ginsberg:zap1} for a fuller explanation and for a
relatively comprehensive list of references where the earlier work is
discussed.}
\begin{enumerate}
\item {\small\bf SAT} refers to conventional \bs\ work, representing
information as conjunctions of disjunctions of literals (\cnf).
\item {\bf cardinality} refers to the use of ``counting'' clauses;
if we think of a conventional disjunction of literals $\vee_i l_i$ as
\[\sum_i l_i \geq 1\]
then a cardinality clause is one of the form
\[\sum_i l_i \geq k\]
for a positive integer $k$.
\item {\bf \pb} clauses extend cardinality clauses by allowing the
literals in question to be weighted:
\[\sum_i w_i l_i \geq k\]
Each $w_i$ is a positive integer giving the weight to be assigned to
the associated literal.
\item {\bf symmetry} involves the introduction of techniques that are
designed to explicitly exploit local or global symmetries in the
problem being solved.
\item {\small\bf QPROP} deals with universally quantified formulae
where all of the quantifications are over finite domains of known
size.
\end{enumerate}

The columns in the table measure the performance of the various
systems against a variety of metrics:
\begin{enumerate}
\item {\bf Efficiency of representation\/} measures the extent to
which a single axiom in a proposed framework can replace many in \cnf.
For cardinality, \pb\ and quantified languages, it is possible that
exponential savings are achieved.  We argued that such savings were
possible but relatively unlikely for cardinality and \pb\ encodings
but were relatively likely for \qprop.
\item {\bf Proof length\/} gives the minimum proof length for the
representation on three classes of problems: the \php, parity problems
due to Tseitin \citeyear{Tseitin:complexity} and clique coloring
problems \cite{clique}.  An E indicates exponential proof length; P
indicates polynomial length.  While symmetry-exploitation techniques
can provide polynomial-length proofs in certain instances, the method
is so brittle against changes in the axiomatization that we do not
regard this as a polynomial approach in general.
\item {\bf Resolution\/} indicates the extent to which resolution can
be lifted to a broader setting.  This is straightforward in the \pb\
case; cardinality clauses have the problem that the most natural
resolvent of two cardinality clauses may not be a cardinality clause,
and there may be many cardinality clauses that could be derived as a
result.  Systems that exploit local symmetries must search for such
symmetries at each inference step, a problem that is not believed to
be in P.  Provided that reasons are maintained, inference remains well
defined for quantified axioms, requiring only the introduction of a
linear complexity unification step.
\item {\bf Propagation technique\/} describes the techniques used to
draw conclusions from an existing partial assignment of values to
variables.  For all of the systems except \qprop, Zhang and Stickel's
watched literals idea \cite{zchaff,Zhang:watch} is the most efficient
mechanism known.  This approach cannot be lifted to \qprop, but a
somewhat simpler method can be lifted and average-case exponential
savings obtained as a result \cite{Ginsberg:qprop}.
\item {\bf Learning method\/} gives the technique typically used to
save conclusions as the inference proceeds.  In general,
relevance-bounded learning
\cite{Bayardo:relsat,Schrag:relsat,Ginsberg:dynamic} is the most
effective technique known here.  It can be augmented with
strengthening \cite{Guignard:strengthening,strengthen} in the \pb\
case and with first-order reasoning if quantified formulae are
present.
\end{enumerate}

Our goal in the current paper is to add a single line to the above
table:

\begin{center}
\small
\begin{tabular}{|r||c|c|c|c|c|}
\hline
& {\bf efficiency} & {\bf proof} & & {\bf propagation}& {\bf learning} \\
& {\bf of rep'n} & {\bf length} & {\bf resolution} 
 & {\bf technique} & {\bf method} \\
\hline\hline
\footnotesize\bf SAT & --- & EEE& --- & watched literals&relevance \\ \hline
\bf{cardinality} & exponential & P?E & not unique & watched literals & relevance \\ \hline
\bf{\parbox{.8in}{\vspace*{.03in}pseudo-\hspace*{.2in}Boolean\vspace*{.03in}}} & exponential & P?E & unique & watched literals & + strengthening \\ \hline
\bf{symmetry} & --- & EEE$^*$ & not believed in P& same as {\sc sat} &
 same as {\sc sat} \\ \hline
\footnotesize\bf QPROP & exponential & ??? & in P using reasons & exp improvement &
 + first-order \\
\hline
\hline
\footnotesize\bf ZAP & exponential & PPP & in P using reasons & \parbox{1.14in}{\begin{center}watched literals, exp improvement\end{center}} & \parbox{1in}{\begin{center}\mbox{+ first-order} \mbox{+ parity} \mbox{+ others}\end{center}} \\
\hline
\end{tabular}
\end{center}

\Zap\ is the approach to inference that is the focus of this series of
papers.  The basic idea in \zap\ is that in realistic problems, many
Boolean clauses are ``versions'' of a single clause.  We will make
this notion precise shortly; at this point, one might think of all of
the instances of a quantified clause as being versions of any
particular ground instance.  The versions, it will turn out,
correspond to permutations on the set of literals in the problem.

As an example, suppose that we are tying to prove that it is impossible
to put $n+1$ pigeons into $n$ holes if each pigeon is to get its own
hole.  A Boolean axiomatization of this problem will include the axioms
\[\begin{array}{cccc}
\neg p_{11} \vee \neg p_{21} & \neg p_{12} \vee \neg p_{22} & \cdots & \neg p_{1n} \vee \neg p_{2n} \\
\neg p_{11} \vee \neg p_{31} & \neg p_{12} \vee \neg p_{32} & \cdots & \neg p_{1n} \vee \neg p_{3n} \\
\vdots & \vdots & & \vdots \\
\neg p_{11} \vee \neg p_{n+1,1} & \neg p_{12} \vee \neg p_{n+1,2} & \cdots & \neg p_{1n} \vee \neg p_{n+1,n} \\
\neg p_{21} \vee \neg p_{31} & \neg p_{22} \vee \neg p_{32} & \cdots & \neg p_{2n} \vee \neg p_{3n} \\
\vdots & \vdots & & \vdots \\
\neg p_{21} \vee \neg p_{n+1,1} & \neg p_{22} \vee \neg p_{n+1,2} & \cdots & \neg p_{2n} \vee \neg p_{n+1,n} \\
\vdots & \vdots & & \vdots \\
\neg p_{n1} \vee \neg p_{n+1,1} & \neg p_{n2} \vee \neg p_{n+1,2} & \cdots & \neg p_{nn} \vee \neg p_{n+1,n} \\
  \end{array}
\]
 where $p_{ij}$ says that pigeon $i$ is in hole $j$.  Thus the first
clause above says that pigeon one and pigeon two cannot both be in
hole one.  The second clause in the first column says that pigeon one
and pigeon three cannot both be in hole one.  The second column refers
to hole two, and so on.  It is fairly clear that all of these axioms
can be reconstructed from the first by interchanging the pigeons and
the holes, and it is this intuition that \zap\ attempts to capture.

What makes this approach interesting is the fact that instead of
reasoning with a large set of clauses, it becomes possible to reason
with a single clause instance and a set of permutations.  As we will
see, the sets of permutations that occur naturally are highly
structured sets called {\em groups}, and exploiting this structure can
lead to significant efficiency gains in both representation and
reasoning.

Some further comments on the above table:
\begin{itemize}
\item Unlike cardinality and \pb\ methods, which seem unlikely to
achieve exponential reductions in problem size in practice, and
\qprop, which seems likely to achieve such reductions, \zap\ is {\em
guaranteed\/}, when the requisite structure is present, to replace a
set of $n$ axioms with a single axiom of size at most $v \log(n)$,
where $v$ is the number of variables in the problem (\prop{rsize}).

\item The fundamental inference step in \zap\ is in NP with respect to
the \zap\ representation, and therefore has complexity no worse than
exponential in the representation size (i.e., polynomial in the number
of Boolean axioms being resolved).  In practice, the average case
complexity appears to be low-order polynomial in the size of the \zap\
representation (i.e., polynomial in the logarithm of the number of
Boolean axioms being resolved) \cite{Ginsberg:zap3}.
\item \Zap\ obtains the savings attributable to subsearch in the
\qprop\ case while casting them in a general setting that is
equivalent to watched literals in the Boolean case.  This particular
observation is dependent on a variety of results from computational
group theory and is discussed in the third paper in this series
\cite{Ginsberg:zap3}.
\item In addition to learning the Boolean consequences of resolution,
\zap\ continues to support relevance-bounded learning schemes while
also allowing the derivation of first-order consequences, conclusions
based on parity arguments, and combinations thereof.
\end{itemize}

In order to deliver on these claims, we begin in \secn{bs} by
summarizing both the \dpll\ algorithm and the modifications that
embody recent progress, casting \dpll\ into the precise form that is
needed in \zap\ and that seems to best capture the architecture of
modern systems such as \zchaff.  \secn{group-intro} is also a summary
of ideas that are not new with us, providing an introduction to some
ideas from group theory.

In \secn{group}, we describe the key insight underlying \zap.  As
mentioned above, the structure exploited in earlier examples
corresponds to the existence of particular groups of permutations of
the literals in the problem.  We call the combination of a clause and
such a permutation group an {\em augmented clause}, and the {\bf
efficiency of representation} column of our table corresponds to the
observation that augmented clauses can use group structure to improve
the efficiency of their encoding.

\secn{resolution} ({\bf resolution}) describes resolution in this
broader setting, and \secn{example} ({\bf proof length}) presents a
variety of examples of these ideas at work, showing that the \php,
clique-coloring problems, and Tseitin's parity examples all admit
short proofs in the new framework.  \secn{describe} ({\bf learning
method}) recasts the \dpll\ algorithm in the new terms and discusses
the continued applicability of relevance in our setting.  Concluding
remarks are contained in \secn{conclusion}.  Implementation details,
including a discussion of {\bf propagation techniques}, are deferred
until the third of this series of papers \cite{Ginsberg:zap3}.  This
third paper will also include a presentation of performance details;
at this point, we note merely that \zap\ does indeed exhibit
polynomial performance on the natural encodings of pigeonhole, parity
and clique-coloring problems.  This is in sharp contrast with other
methods, where theoretical best-case performance (let alone
experimental average-case performance) is known to be exponential on
these problems classes.

\section{Boolean Satisfiability Engines}
\label{s.bs}

In \zapz, we presented descriptions of the standard
Davis-Putnam-Logemann-Loveland (\dpll) \bs\ algorithm and described
informally the extensions to \dpll\ that deal with learning.  Our goal
in this paper and the next is to describe an implementation of our
theoretical ideas.  We therefore begin here by being more precise
about \dpll\ and its extension to relevance-bounded learning, or \rbl.
We present some general definitions that we will need throughout this
paper, and then give a description of the \dpll\ algorithm in a
learning/reason-maintenance setting.  We prove that an implementation
of these ideas can retain the soundness and completeness of \dpll\
while using an amount of memory that grows polynomially with problem
size.  Although this result has been generally accepted since
1-relevance learning (``dynamic backtracking,''
\citeR{Ginsberg:dynamic}) was generalized by Bayardo, Miranker and
Schrag \cite{Bayardo:relsat,Schrag:relsat}, we know of no previous
proof that \rbl\ has the stated properties.

\begin{definition} A {\em partial assignment\/} is an ordered sequence
\[\langle l_1,\dots,l_n\rangle\]
of distinct and consistent literals.
\end{definition}

\begin{definition} Let $\vee_i l_i$ be a clause, which we will denote 
by $c$, and suppose that $P$ is a partial assignment.  We will say
that the {\em possible value of $c$ under $P$\/} is given by
\[\poss(c,P) = |\set{l\in c|\neg l\not\in P}| - 1\] If no ambiguity is
possible, we will write simply $\poss(c)$ instead of $\poss(c,P)$.  In
other words, $\poss(c)$ is the number of literals that are either
already satisfied or not valued by $P$, reduced by one (since true
clauses require at least one true literal).

If $S$ is a set of clauses, we will write $\poss_n(S,P)$ for the
subset of $c\in S$ for which $\poss(c,P)\leq n$.

In a similar way, we will define $\curr(c,P)$ to be
\[\curr(c,P) = |\set{l\in c \cap P}| - 1\]
We will write $\curr_n(S,P)$ for the subset of $c\in S$ for which
$\curr(c,P)\leq n$.
\label{d.poss}
\end{definition}
Informally, if $\poss(c,P)=0$, that means that any partial assignment
extending $P$ can make at most one literal in $c$ true; there is no
room for any ``extra'' literals to be true.  This might be because all
of the literals in $c$ are assigned values by $P$ and only one such
literal is true; it might be because there is a single unvalued
literal and all of the other literals are false.  If $\poss(c,P)<0$,
it means that the given partial assignment cannot be extended in a way
that will cause $c$ to be satisfied.  Thus we see that
$\poss_{-1}(S,P)$ is the set of clauses in $S$ that are falsified by
$P$.  Since $\curr$ gives the ``current'' excess in the number of
satisfied literals (as opposed to $\poss$, which gives the possible
excess), the set $\poss_0(S,P)\cap \curr_{-1}(S,P)$ is the set of
clauses that are not currently satisfied and have at most one unvalued
literal.  These are generally referred to as {\em unit\/} clauses.

We note in passing that \defn{poss} can easily be extended to deal
with \pb\ instead of Boolean clauses, although that extension will
not be our focus here.

\begin{definition}  An {\em annotated partial assignment\/} is an
ordered sequence
\[\langle (l_1,c_1),\dots,(l_n,c_n)\rangle\]
of distinct and consistent literals and clauses, where $c_i$ is the
{\em reason\/} for literal $l_i$ and either $c_i=\true$ (indicating
that $l_i$ was a branch point) or $c_i$ is a clause such that:
\begin{enumerate}
\item $l_i$ is a literal in $c_i$, and
\item $\poss(c_i,\langle l_1,\dots,l_{i-1}\rangle) = 0$
\end{enumerate}
 An annotated partial assignment will be called {\em sound\/} with
respect to a set of clauses $C$ if $C\models c_i$ for each reason
$c_i$.
\label{d.reason}
\end{definition}
 The reasons have the property that after the literals
$l_1,\dots,l_{i-1}$ are all included in the partial assignment, it is
possible to conclude $l_i$ directly from $c_i$, since there is no
other way for $c_i$ to be satisfied.

\begin{definition} Let $c_1$ and $c_2$ be clauses, each a set
of literals to be disjoined.  We will say that $c_1$ and $c_2$ {\em
resolve\/} if there is a unique literal $l$ such that $l\in c_1$ and
$\neg l\in c_2$.  If $c_1$ and $c_2$ resolve, their {\em resolvent},
to be denoted $\resolve(c_1,c_2)$, is the disjunction of the literals
in the set $c_1\cup c_2 - \set{l,\neg l}$.

If $r_1$ and $r_2$ are reasons, the result of resolving $r_1$ and
$r_2$ is defined to be:
\[\resolve(r_1,r_2)=\cases{r_2,& if $r_1=\true$;\cr
			r_1,& if $r_2=\true$;\cr \mbox{the
	conventional resolvent of $r_1$ and $r_2$},& otherwise.\cr}\]
\end{definition}

\begin{definition}  Let $C$ be a set of clauses and $P$ a partial 
assignment.  A {\em nogood for $P$\/} is any clause $c$ that is
entailed by $C$ but falsified by $P$.  A {\em nogood\/} is any clause
$c$ that is entailed by $C$.
\end{definition}

We are now in a position to present one of the basic building blocks
of \dpll\ or \rbl, the {\em \up} procedure.  This computes the
``obvious'' consequences of a partial assignment:

\begin{procedure}[\Up] To compute $\proc{Unit-Propagate}(C,P)$ for a
set $C$ of clauses and an annotated partial assignment $P$:\em
\begin{codebox}
\li \While $\poss_0(C,P)\cap\curr_{-1}(C,P) \neq \emptyset$
\li \Do \If $\poss_{-1}(C,P) \neq \emptyset$
\li         \Then $c\gets$ an element of $\poss_{-1}(C,P)$
\li		  $l_i\gets$ the literal in $c$ with the highest index in $P$
\li		  \Return $\langle\true,\resolve(c,c_i)\rangle$ \label{l.fail}
\li	    \Else $c\gets$ an element of $\poss_0(C,P)\cap\curr_{-1}(C,P)$
\li		  $l \gets$ the literal in $c$ unassigned by $P$
\li     	  $P \gets \langle P, (l,c)\rangle$
	    \End
	\End
\li \Return $\langle\false,P\rangle$
\end{codebox}
\label{p.upr}
\end{procedure}
The above procedure returns a pair of values.  The first indicates
whether a contradiction has been found.  If so, the second value is
the reason for the failure, a consequence of the clausal database $C$
that is falsified by the partial assignment $P$ (i.e., a nogood).  If
no contradiction is found, the second value is a suitably extended
partial assignment.  \prc{upr} has also been modified to work with
annotated partial assignments, and to annotate the new choices that
are made when $P$ is extended.

\begin{proposition} Suppose that $C$ is a \bs\ problem, and $P$ is a
sound annotated partial assignment.  Then:
\begin{enumerate}
\item If $\unit(P)=\langle\false,P'\rangle$, then $P'$ is a sound
extension of $P$, and
\item If $\unit(P) = \langle\true,c\rangle$, then $c$ is a nogood for $P$.
\end{enumerate}
\label{p.uprx}
\end{proposition}

\proof In the interests of maintaining the continuity of the
exposition, most proofs (including this one!) have been deferred to
the appendix.  Proofs or proof sketches will appear in the main text
only when they further the exposition in some way.\proofend

We can now describe relevance-bounded learning:

\begin{procedure} [Relevance-bounded reasoning, \rbl] Let $C$ be a \sat\
problem, and $D$ a set of learned nogoods, so that $C\models D$.  Let
$P$ be an annotated partial assignment, and $k$ a fixed relevance
bound.  To compute $\proc{rbl}(C,D,P)$:\em
\begin{codebox}
\li $\langle x,y\rangle \gets \proc{Unit-Propagate}(C\cup D,P)$\label{l.rbl-d}
\li \If $x=\true$\label{l.rbl-x}
\li  	\Then $c\gets y$
\li     \If $c$ is empty
\li	  \Then \Return \const{failure}
\li	  \Else remove successive elements from $P$ so that $c$ is 
			satisfiable and
\zi		\qquad $\poss(c,P)\leq k$ \label{l.rbl-a}
\li	        $D\gets \set c \cup \poss_k(D,P)$\label{l.rbl-b}
\li		     	\Return $\proc{rbl}(C,D,P)$
		  \End
\li \Else $P\gets y$\label{l.rbl-e}
\li   \If $P$ is a solution to $C$\label{l.rbl-done}
\li     \Then \Return $P$
\li	\Else $l\gets$ a literal not assigned a value by $P$\label{l.rblbranch}
\li	   \Return $\proc{rbl}(C,D,\langle P,(l,\true)\rangle)$\label{l.rbl-c}
	  \End
	\End
\end{codebox}
\label{p.rbl}
\end{procedure}

This procedure is fairly different from the original description of
\dpll, so let us go through it.

In general, variables are assigned values either via branching on
\lin{rbl-c}, or \up\ on lines \ref{l.rbl-d} and \ref{l.rbl-e}.  If
\up\ terminates without reaching a contradiction or finding a solution
(so that $x$ is $\false$ on \lin{rbl-x} and the test on \lin{rbl-done}
fails as well), then a branch variable is selected and assigned a
value, and the procedure recurs.

If the \up\ procedure ``fails'' and returns $\langle\true,c\rangle$
for a new nogood $c$, the new clause is learned by adding it to $D$,
and the search backtracks at least to the point where $c$ is
satisfiable.\footnote{As we remarked in \zapz, some systems such as
\zchaff~\cite{zchaff} backtrack further to the point where $c$ is
unit.}  Any learned clauses that have become irrelevant (in that their
$\poss$ value exceeds the irrelevance cutoff $k$) are removed.  Note
that we only remove {\em learned\/} irrelevant nogoods; we obviously
cannot remove clauses that were part of the original problem
specification.  It is for this reason that the sets $C$ and $D$ (of
original and learned clauses respectively) are maintained separately.

\prc{rbl} can fail only if a contradiction (an empty clause $c$) is
derived.  In all other cases, progress is made by augmenting the set
of clauses to include at least one new nogood that eliminates the
current partial assignment.  Instead of resetting the branch literal
$l$ to take the opposite value as in Davis et.al.'s original
description of their algorithm, a new clause is learned and added to
the problem.  This new clause causes either $l$ or some previous
variable to take a new value.

The above description is ambiguous about a variety of points.  We do
not specify how far to backtrack on \lin{rbl-a}, or the branch literal
to be chosen on \lin{rblbranch}.  We will not be concerned with these
choices; \zap\ takes the same approach that \zchaff\ does and the
implementation is straightforward.

\begin{theorem} \Rbl\ is sound and complete in that 
${\mbox \rbl}(C,\emptyset,\langle\rangle)$ will always return a
satisfying assignment if $C$ is satisfiable and will always report
failure if $C$ is unsatisfiable.  \Rbl\ also uses an amount of memory
polynomial in the size of $C$ (although exponential in the relevance
bound $k$).\label{t.rbl}\end{theorem}

As discussed at some length in \zapz, other authors have focused on
extending the language of \bs\ in ways that preserve the efficiency of
\rbl.  These extensions include the ability to deal with
quantification \cite{Ginsberg:qprop}, \pb\ or cardinality clauses
\cite{Barth:pseudo,Barth:01,Chandru:logic_book,Dixon:AIOR,Hooker:genres,OR:cut},
or parity clauses \cite{baumgartner:xor,Li:mod2}.

\section{Some Concepts from Group Theory}
\label{s.group-intro}

Relevance-bounded learning is only a part of the background that we
will need to describe \zap; we also need some basic ideas from group
theory.  There are many excellent references available on this topic
\cite[and others]{Rotman:groups}, and we can only give a brief account
here.  Our goal is not to present a terse sequence of definitions and
to then hollowly claim that this paper is self-contained; we would
rather provide insight regarding the goals and underlying philosophy
of group theory generally.  We will face a similar problem in the
final paper in this series, where we will draw heavily on results from
\cgt\ and will, once again, present a compact and hopefully helpful
overview of a broad area of mathematics.

\begin{definition} A {\em group\/} is a set $S$ equipped with an
associative binary operator $\circ$.  The operator $\circ$ has an
identity $1$, with $1\circ x = x\circ 1 = x$ for all $x\in S$, and an
inverse, so that for every $x\in S$ there is an $x^{-1}$ such that
$x\circ x^{-1} = x^{-1}\circ x = 1$.
\end{definition}

In other words, $\circ$ is a function $\circ:S\times S\rightarrow S$;
since $\circ$ is associative, we always have
\[(x\circ y)\circ z = x \circ (y\circ z)\]
The group operator $\circ$ is not required to be commutative; if it is
commutative, the group is called {\em Abelian}.

Typical examples of groups include $\mathbb{Z}$, the group of integers
with the operation being addition.  Similarly, $\mathbb{Q}$ and
$\mathbb{R}$ are the groups of rationals or reals under addition.  For
multiplication, zero needs to be excluded, since it has no inverse,
and we get the groups $\mathbb{Q}^*$ and $\mathbb{R}^*$.  Note that
$\mathbb{Z}^*$ is not a group, since $1/n$ is not an integer for most
integers $n$.

Other common groups include $\mathbb{Z}_n$ for any positive integer
$n$; this is the group of integers $\mod\ n$, where the group
operation is addition $\mod\ n$.  For a prime $p$, the set
$\mathbb{Z}^*_p$ of nonzero integers $\mod\ p$ does have a
multiplicative inverse, so that $\mathbb{Z}^*_p$ is a group under
multiplication.  The group $\mathbb{Z}_1$ contains the single element
0 and is the {\em trivial\/} group.  This group is often denoted by
{\bf 1}.

All of the groups we have described thus far are Abelian, but
non-Abelian groups are not hard to come by.  As an example, the set of
all $n\times n$ matrices with real entries and nonzero determinants is
a group under multiplication, since every matrix with a nonzero
determinant has an inverse.  This group is called the {\em general
linear group\/} and is denoted $GL(n)$.

Of particular interest to us will be the so-called {\em permutation
groups}:

\begin{definition}  Let $T$ be a set.  A {\em permutation\/} of $T$ is
a bijection $\omega:T\rightarrow T$ from $T$ to itself.
\end{definition}

\begin{proposition}  Let $T$ be a set.  Then the set of permutations of
$T$ is a group under the composition operator.
\end{proposition}

\proof This is simply a matter of validating the definition.
Functional composition is well known to be associative (although not
necessarily commutative), and the identity function from $T$ to itself
is the identity for the composition operator.  Since each permutation
is a bijection, permutations can be inverted to give the inverse
operator for the group.\proofend

The group of permutations on $T$ is called the {\em symmetry group of
$T$}, and is typically denoted $\Sym(T)$.  We will take the view that
the composition $f\circ g$ acts with $f$ first and $g$ second, so that
$(f\circ g)(x) = g(f(x))$ for any $x\in T$.  (Note the variable
order.)

Because permutation groups will be of such interest to us, it is
worthwhile to introduce some additional notation for dealing with them
in the case where $T\subseteq \mathbb Z$ is a subset of the integers.
In the special case where $T=\set{1,\dots,n}$, we will often
abbreviate $\Sym(T)$ to either $\Sym(n)$ or simply $S_n$.

Of course, we can get groups of permutations without including {\em
every\/} permutation on a particular set; the 2-element set consisting
of the identity permutation and the permutation that swaps two
specific elements of $T$ is closed under inversion and composition and
is therefore a group as well.  In general, we have:

\begin{definition} Let $(G,\circ)$ be a group.  Then a subset
$H\subseteq G$ is called a {\em subgroup\/} if $(H,\circ)$ is a group.
This is denoted $H\leq G$.  If the inclusion is proper, we write
$H<G$.
\end{definition}

A subgroup of a group $G$ is any subset of $G$ that includes the
identity and that is closed under composition and inversion.

If $G$ is a finite group, closure under composition suffices.  To
understand why, suppose that we have some subset $H\subseteq G$ that
is closed under composition, and that $x\in H$.  Now $x^2\in H$, and
$x^3\in H$, and so on.  Since $G$ is finite, we must eventually have
$x^m=x^n$ for some integers $m$ and $n$, where we assume $m>n$.  It
follows that $x^{m-n}=1$ so $x^{m-n-1}=x^{-1}$, so $H$ is closed under
inversion and therefore a subgroup.

\begin{proposition} Let $G$ be a group, and suppose that $H_1\leq G$
and $H_2\leq G$ are subgroups.  Then $H_1\cap H_2\leq G$ is a subgroup
of $G$ as well.\proofend
\label{p.intersect}
\end{proposition}

This should be clear, since $H_1\cap H_2$ must be closed under
inversion and composition if each of the component groups is.

\begin{definition}  Let $G$ be a group, and $S\subseteq G$ a subset.
Then there is a unique smallest subgroup of $G$ containing $S$, which
is denoted $\langle S \rangle$ and called the subgroup of $G$ {\em
generated\/} by $S$.  The {\em order\/} of an element $g\in G$ is
defined to be $|\langle g\rangle|$.
\end{definition}

The generated subgroup is unique because it can be formed by taking
the intersection of all subgroups containing $S$.  This intersection
is itself a subgroup by virtue of \prop{intersect}.  If $S=\emptyset$
or $S=\set{1}$, the trivial subgroup is generated, consisting of only
the identity element of $G$.  Thus the order of the identity element
is one.  For any element $g$, the order of $g$ is the least nonzero
exponent $m$ for which $g^m=1$.

We have already remarked that the two-element set $\set{1,(ab)}$ is a
group, where $1$ represents the trivial permutation and $(ab)$ is the
permutation that swaps $a$ and $b$.  It is easy to see that
$\set{1,(ab)}$ is the group generated by $(ab)$.  The order of $(ab)$
is two.

In a similar way, if $(abcd)$ is the permutation that maps $a$ to $b$,
$b$ to $c$, $c$ to $d$ and $d$ back to $a$, then the subgroup
generated by $(abcd)$ is
\[\set{1,(abcd),(ac)\circ (bd),(adcb)}\]
The third element simultaneously swaps $a$ and $c$, and swaps $b$ and
$d$.  The order of the permutation $(abcd)$ is four, and $(abcd)$ is
called a {\em 4-cycle}.  Both this subgroup and the previous subgroup
generated by $(ab)$ are Abelian, although the full permutation group
$\Sym(L)$ is not Abelian if $|L|>2$.  It is not hard to see that
$\langle\rho\rangle$ is Abelian for any specific permutation~$\rho$.

Slightly more interesting is the group generated by $(abcd)$ together
with $(ac)$.  This group has eight elements:
\begin{equation}
\set{1,(abcd),(ac)\circ (bd),(adcb),(ac),(ad)\circ (bc),(bd),(ab)\circ(cd)}
\label{e.square}
\end{equation}
The first four permutations don't ``use'' $(ac)$ and the second four
do.  Since $(abcd)\circ(ac) \neq (ac)\circ(abcd)$, this group is not
Abelian.

It is not hard to see that the group \eq{square} is in fact the group
of rigid motions of a square whose vertices are labeled $a$, $b$, $c$
and $d$.  The first permutation $(abcd)$ corresponds to a rotation of
the square by $90^{\circ}$ and the second $(ac)$, to a flip around the
$b$-$d$ diagonal.  The first four permutations in \eq{square} simply
rotate the square, while the second four use the flip as well; the
group is not Abelian because a flip followed by a $90^{\circ}$
clockwise rotation is different than the rotation followed by the
flip.  In a similar way, the six basic twists of Rubik's cube generate
a permutation group of size approximately $4.3\times 10^{19}$, giving
all accessible permutations of the faces.

In general, suppose that $f$ is a permutation on a set $S$ and $x\in
S$.  We can obviously consider the image of $x$ under $f$.  Rather
than denote this image by $f(x)$ as usual, it is customary to denote
it by $x^f$.  The reason for this ``inline'' notation is that we now
have
\[x^{fg} = (x^f)^g\]
which seems natural, as opposed to the unnatural
\[(fg)(x) = g(f(x))\]
as mentioned previously.  We have dropped the explicit composition
operator $\circ$ here.

Continuing, we can form the set of images $x^f$ where $f$ varies over
all elements of some permutation group $G$.  This is called the {\em
orbit\/} of $x$ under $G$:

\begin{definition} Let $G\leq \Sym(T)$ be a permutation group.  Then
for any $x\in T$, the {\em orbit of $x$ in $G$}, to be denoted by
$x^G$, is given by $x^G=\set{x^g|\mbox{$g\in G$}}$.
\end{definition}

Returning to the case of permutations on integers, suppose that $n$ is
an integer and $\omega$ a permutation.  We can consider
$\langle\omega\rangle$, the group of permutations generated by
$\omega$, which is the set of powers of $\omega$ until we eventually
have $\omega^m=1$ for $m$ the order of $\omega$.  The orbit of $n$
under $\langle\omega\rangle$ is the set $n^{\langle\omega\rangle} =
\set{n,n^{\omega},n^{\omega^2},\dots,n^{\omega^{m-1}}}$.

Now suppose that $n'$ is some other integer that appears in this
sequence, say $n' = n^{\omega^k}$.  Now $n'^{\omega} =
(n^{\omega^k})^w = n^{\omega^{k+1}}$, so that the images of $n'$ can
be ``read off'' from the sequence of images of $n$.  It therefore
makes sense to write this ``piece'' of the permutation as (for
example)
\begin{equation}
(1,3,4)
\label{e.cycle-example}
\end{equation}
indicating that 1 is mapped to 3, that 3 is mapped to 4, and that 4 is
mapped back to 1.

Of course, the 3-cycle \eq{cycle-example} doesn't tell us what happens
to integers that are not in $n^{\langle\omega\rangle}$; for them, we
need another cycle as in \eq{cycle-example}.  So if the permutation
$\omega$ swaps 2 and 5 in addition to mapping 1 to 3 and so on, we
might write
\begin{equation}
\omega = (1,3,4)(2,5)
\label{e.cycle-short}
\end{equation}
If 6 is not moved by $\omega$ (so that $6^\omega = 6$), we could write
\begin{equation}
\omega = (1,3,4)(2,5)(6)
\label{e.cycle-long}
\end{equation}
In general, we will not mention variables that are fixed by the
permutation, preferring \eq{cycle-short} to the longer
\eq{cycle-long}.  We can often omit the commas within the cycles, so
that we will continue to abbreviate $(a,b,c)$ as simply $(abc)$.  If
we need to indicate explicitly that two cycles are part of a single
permutation, we will introduce an extra set of parentheses, perhaps
rewriting \eq{cycle-short} as
\[\omega = ((1,3,4)(2,5))\]
Every permutation can be written as a product of disjoint cycles in
this way.

Finally, in composing permutations written in this fashion, we will
either drop the $\circ$ or replace it with $\cdot$, so that we have,
for example,
\[(abc)\cdot (abd) = (ad)(bc)\]
The point $a$ is moved to $b$ by the first cycle and then to $d$ by
the second.  The point $b$ is moved to $c$ by the first cycle and then
not changed by the second; $c$ is moved to $a$ and then on to $b$.
Finally, $d$ is not moved by the first cycle but is moved to $a$ by
the second.

Two other notions that we will need are that of closure and
stabilizer:

\begin{definition} Let $G\leq \Sym(T)$, and $S\subseteq T$.  By the
{$G$-closure of $S$}, to be denoted $S^G$, we will mean the set
\[S^G=\set{s^g|\mbox{$s\in S$ and $g\in G$}}\]
\label{d.closure}
\end{definition}

\begin{definition}  Given a group $G\leq \Sym(T)$ and $L\subseteq T$, 
the {\em pointwise stabilizer\/} of $L$, denoted $G_L$, is the
subgroup of all $g\in G$ such that $l^g = l$ for every $l\in L$.  The
{\em set stabilizer\/} of $L$, denoted $G_{\set L}$, is that subgroup
of all $g\in G$ such that $L^g=L$.
\label{d.stabilize}
\end{definition}

As an example, consider the group $G$ generated by the permutation
$\omega=(1,3,4)(2,5)$ that we considered above.  Since $\omega^2 =
(1,4,3)$ and $\omega^3 = (2,5)$, it is not too hard to see that
$G=\langle(1,4,3),(2,5)\rangle$ is the group generated by the 3-cycle
$(1,4,3)$ and the 2-cycle $(2,5)$.  The subgroup of $G$ that point
stabilizes the set $\set 2$ is thus $G_2 = \langle(1,4,3)\rangle$, and
$G_{2,5}$ is identical.  The subgroup of $G$ that {\em set\/}
stabilizes $\set{2,5}$ is $G_{\set{2,5}} = G$, however, since every
permutation in $G$ leaves the set $\set{2,5}$ intact.

\section{Axiom Structure as a Group}
\label{s.group}

While we will need the details of Procedures \ref{p.rbl} and
\ref{p.upr} in order to implement our ideas, the procedures themselves
inherit certain weaknesses of \dpll\ as originally described.  Two
weaknesses that we hope to address are:

\begin{enumerate}
\item The appearance of $\poss_0(C,P)\cap\curr_{-1}(C,P)$ in the inner
\up\ loop requires an examination of a significant subset of the
clausal database at each inference step, and
\item Both \dpll\ and \rbl\ are fundamentally resolution-based
methods; there are known problem classes that are exponentially
difficult for resolution-based methods but which are easy if the
language in use is extended to include either cardinality or parity
clauses.
\end{enumerate}

\subsection{Examples of Structure}
\label{s.structure}

Let us begin by examining examples where specialized techniques can
help to address these difficulties.

\subsubsection{Subsearch}
\label{s.qprop-structure}

As we have discussed elsewhere \cite{Ginsberg:zap1,Ginsberg:qprop},
the set of axioms that need to be investigated in the \dpll\ inner
loop often has structure that can be exploited to speed the
examination process.  If a ground axiomatization is replaced with a
lifted one, the search for axioms with specific syntactic properties
is NP-complete in the number of variables in the lifted axiom, and is
called {\em subsearch\/} for that reason.

In many cases, search techniques can be applied to the subsearch
problem.  As an example, suppose that we are looking for instances of
the lifted axiom
\begin{equation}
a(x,y) \vee b(y,z) \vee c(x,z)
\label{e.qprop}
\end{equation}
that are unit, so that $\poss(i,P)=0$ and $\curr(i,P)=-1$ for some
such instance $i$ and a unit propagation is possible as a result.

Our notation here is that of \qprop.  There is an implicit universal
quantification over $x$, $y$ and $z$, and each quantification is over
a domain of finite size.  We assume that all of the domains are of
size $d$, so \eq{qprop} corresponds to $d^3$ ground axioms.  If
$a(x,y)$ is true for all $x$ and $y$ (which we can surely conclude in
time $O(d^2)$), then we can conclude without further work that
\eq{qprop} has no unit instances, since every instance of \eq{qprop}
is already satisfied.  If $a(x,y)$ is true except for a single $(x,y)$
pair, then we need only examine the $d$ possible values of $z$ for
unit instances, reducing our total work from $d^3$ to $d^2+d$.

It will be useful in what follows to make this example still more
specific, so let us assume that $x$, $y$ and $z$ are all chosen from a
two element domain $\set{A,B}$.  The single lifted axiom~\eq{qprop}
now corresponds to the set of ground instances:
\begin{eqnarray*}
& a(A,A) \vee b(A,A) \vee c(A,A) & \\
& a(A,A) \vee b(A,B) \vee c(A,B) & \\
& a(A,B) \vee b(B,A) \vee c(A,A) & \\
& a(A,B) \vee b(B,B) \vee c(A,B) & \\
& a(B,A) \vee b(A,A) \vee c(B,A) & \\
& a(B,A) \vee b(A,B) \vee c(B,B) & \\
& a(B,B) \vee b(B,A) \vee c(B,A) & \\
& a(B,B) \vee b(B,B) \vee c(B,B) & 
\end{eqnarray*}

If we introduce ground literals $l_1,l_2,l_3,l_4$ for the instances of
$a(x,y)$ and so on, we get:
\begin{eqnarray}
& l_1 \vee l_5 \vee l_9 & \nonumber \\
& l_1 \vee l_6 \vee l_{10} & \nonumber \\
& l_2 \vee l_7 \vee l_9 & \nonumber \\
& l_2 \vee l_8 \vee l_{10} & \label{e.ex1} \\
& l_3 \vee l_5 \vee l_{11} & \nonumber \\
& l_3 \vee l_6 \vee l_{12} & \nonumber \\
& l_4 \vee l_7 \vee l_{11} & \nonumber \\
& l_4 \vee l_8 \vee l_{12} & \nonumber
\end{eqnarray}
at which point the structure implicit in \eq{qprop} has been obscured.
We will return to the details of this example shortly.

\subsubsection{Cardinality}
\label{s.card}

Structure is also present in the sets of axioms used to encode the
\php, which is known to be exponentially difficult for any
resolution-based method~\cite{Haken}.  As shown by a variety of
authors \cite{Cook:php,Dixon:AIOR}, the \php\ can be solved in
polynomial time if we extend our representation to include cardinality
axioms such as
\begin{equation}
x_1+\cdots+x_m \geq k
\label{e.card2}
\end{equation}
As shown in \zapz, the single axiom \eq{card2} is equivalent to $m
\choose {k-1}$ conventional disjunctions.

As in \secn{qprop-structure}, we will consider this example in detail.
Suppose that we have the clause
\begin{equation}
x_1+x_2+x_3+x_4+x_5 \geq 3
\label{e.card}
\end{equation}
saying that at least 3 of the $x_i$'s are true.  This is equivalent to
\begin{eqnarray}
 x_1 \vee x_2 \vee x_3 & & x_1 \vee x_4 \vee x_5  \nonumber \\
 x_1 \vee x_2 \vee x_4 & & x_2 \vee x_3 \vee x_4  \nonumber \\
 x_1 \vee x_2 \vee x_5 & & x_2 \vee x_3 \vee x_5  \label{e.ex2} \\
 x_1 \vee x_3 \vee x_4 & & x_2 \vee x_4 \vee x_5  \nonumber \\
 x_1 \vee x_3 \vee x_5 & & x_3 \vee x_4 \vee x_5  \nonumber 
\end{eqnarray}

\subsubsection{Parity Clauses}

Finally, we consider clauses that are most naturally expressed
using modular arithmetic or exclusive or's, such as
\begin{equation}
x_1 + \cdots + x_k \equiv 0\;(\mod\ 2)
\label{e.mod2-even}
\end{equation}
or
\begin{equation}
x_1 + \cdots + x_k \equiv 1\;(\mod\ 2)
\label{e.mod2}
\end{equation}
The parity of the sum of the $x_i$'s is specified as even in
\eq{mod2-even} or as odd in \eq{mod2}.

It is well known that axiom sets consisting of parity clauses in
isolation can be solved in polynomial time using Gaussian elimination,
but there are examples that are exponentially difficult for
resolution-based methods \cite{Tseitin:complexity}.  As in the other
examples we have discussed, single axioms such as \eq{mod2} reveal
structure that a straightforward Boolean axiomatization obscures.  In
this case, the single axiom \eq{mod2} with $k=3$ is equivalent to:
\begin{eqnarray}
& x_1 \vee x_2 \vee x_3 & \nonumber \\
& x_1 \vee \neg x_2 \vee \neg x_3 & \label{e.ex3} \\
& \neg x_1 \vee x_2 \vee \neg x_3 & \nonumber \\
& \neg x_1 \vee \neg x_2 \vee x_3 & \nonumber
\end{eqnarray}
  As the cardinality axiom \eq{card2} is equivalent to $m \choose
{k-1}$ disjunctions, a parity axiom of the form of \eq{mod2-even} or
\eq{mod2} is in general equivalent to $2^{k-1}$ Boolean disjunctions.

\subsection{Formalizing Structure}
\label{s.formalize}

Of course, the ground axiomatizations \eq{ex1}, \eq{ex2} and \eq{ex3}
are equivalent to the original descriptions given by \eq{qprop},
\eq{card2} and \eq{mod2}, so that any structure present in these
original descriptions is still there.  That structure has, however,
been obscured by the ground encodings.  Our goal in this section is to
begin the process of understanding the structure in a way that lets us
describe it in general terms.

As a start, note that each of the axiom sets consists of axioms of
equal length; it follows that the axioms can all be obtained from a
single one simply by permuting the literals in the theory.  In
\eq{ex1} and \eq{ex2}, literals are permuted with other literals of
the same sign; in \eq{ex3}, literals are permuted with their negated
versions.  But in every instance, a permutation suffices.

Thus, for example, the set of permutations needed to generate \eq{ex2}
from the first ground axiom alone is clearly just the set
\begin{equation}
\Omega = \Sym({\set{x_1,x_2,x_3,x_4,x_5}})
\label{e.ex2-sub}
\end{equation}
since these literals can be permuted arbitrarily to move from one
element of \eq{ex2} to another.  The set $\Omega$ in \eq{ex2-sub} is a
subgroup of the full permutation group $S_{2n}$ on $2n$ literals in
$n$ variables, since $\Omega$ is easily seen to be closed under
inversion and composition.

What about the example \eq{ex3} involving a parity clause?  Here
the set of permutations needed to generate the four axioms from the
first is given by:
\begin{eqnarray}
& (x_1,\neg x_1)(x_2,\neg x_2) & \\
& (x_1,\neg x_1)(x_3,\neg x_3) & \\
& (x_2,\neg x_2)(x_3,\neg x_3) &
\end{eqnarray}
Literals are now being exchanged with their negations, but this set,
too, is closed under the group inverse and composition operations.
Since each element is a composition of disjoint transpositions, each
element is its own inverse.  The composition of the first two elements
is the third.

The remaining example \eq{ex1} is a bit more subtle; perhaps this is
to be expected, since the axiomatization \eq{ex1} obscures the
underlying structure far more effectively than does either \eq{ex2} or
\eq{ex3}.

To understand this example, note that the set of axioms \eq{ex1} is
``generated'' by a set of transformations on the underlying variables.
In one transformation, we swap the values of $A$ and $B$ for $x$ while
leaving the values for $y$ and $z$ unchanged, corresponding to the
permutation
\[(a(A,A),a(B,A))(a(A,B),a(B,B))(c(A,A),c(B,A))(c(A,B),c(B,B))\]
We have included in a single permutation the induced changes to all of
the relevant ground literals.  (The relation $b$ doesn't appear
because $b$ does not have $x$ as an argument in~\eq{qprop}.)  In terms
of the literals in \eq{ex1}, this becomes
\[\omega_x = (l_1 l_3)(l_2 l_4)(l_9 l_{11})(l_{10} l_{12})\]
In a similar way, swapping the two values for $y$ corresponds to the
permutation
\[\omega_y = (l_1 l_2)(l_3 l_4)(l_5 l_7)(l_6 l_8)\]
and $z$ produces
\[\omega_z = (l_5 l_6)(l_7 l_8)(l_9 l_{10})(l_{11} l_{12})\]

Now consider $\Omega = \langle \omega_x, \omega_y, \omega_z\rangle$,
the subgroup of $\Sym(\set{l_1,\dots,l_{12}})$ that is generated by
$\omega_x$, $\omega_y$ and $\omega_z$.  Since the clauses in \eq{ex1}
can be obtained from any single clause by permuting the values of $x$,
$y$ and $z$, it is clear that the image of any single clause in the
set \eq{ex1} under $\Omega$ is exactly the complete set of clauses
\eq{ex1}.

As an example, operating on the first axiom in \eq{ex1} with
$\omega_x$ produces
\[l_3\vee l_5 \vee l_{11}\]
This is the fifth axiom, as it should be, since we have swapped
$a(A,A)$ with $a(B,A)$ and $c(A,A)$ with $c(B,A)$.

Alternatively, a straightforward calculation shows that
\[\omega_x \omega_y = 
  (l_1 l_4)(l_2 l_3)(l_5 l_7)(l_6 l_8)(l_9 l_{11})(l_{10} l_{12})\]
and maps the first axiom in \eq{ex2} to the next-to-last, the
second axiom to last, and so on.

It should be clear at this point what all of these examples have in
common.  In every case, the set of ground instances corresponding to a
single non-Boolean axiom can be generated from any {\em single\/}
ground instance by the elements of a subgroup of the group $S_{2n}$ of
permutations of the literals in the problem.

Provided that all of the clauses are the same length, there is
obviously some sub{\em set\/} (as opposed to sub{\em group}) of
$S_{2n}$ that can produce all of the clauses from a single one.  But
subgroups are highly structured objects; there are many fewer
subgroups of $S_{2n}$ than there are subsets.\footnote{In general,
$S_{2n}$ has $2^{(2n)!}$ subsets, of which only approximately
$2^{n^2/4}$ are subgroups~\cite{Pyber}.}  One would not expect, a
priori, that the particular sets of permutations arising in our
examples would all have the structure of subgroups.  The fact that
they do, that all of these particular subsets are subgroups even
though so few subsets are in general, is what leads to our general
belief that the structure of the subgroups captures and generalizes
the general idea of structure underlying our motivating examples.

In problems without structure, the subgroup property is absent.  An
instance of random 3-{\sc sat}, for example, can always be encoded
using a single 3-literal clause $c$ and then that set of permutations
needed to recover the entire problem from $c$ in isolation.  There is
no structure to the set of permutations because the original set of
clauses was itself unstructured.  In the examples we have been
considering, on the other hand, the structure is implicit in the
requirement that the set $\Omega$ used to produce the clauses be a
group.  As we will see, this group structure also has just the
computational properties needed if we are to lift \rbl\ and other \bs\
techniques to our broader setting.

Let us also point out the surprising fact that the subgroup idea
captures {\em all\/} of the structures discussed in \zapz.  It is not
surprising that the various structures used to reduce proof size all
have a similar flavor, or that the structure used to speed \up\ be
uniform.  But it strikes us as remarkable that these two types of
structure, used for such different purposes, are in fact instances of
a single framework.

This, then, is the technical insight on which \zap\ rests: Instead of
generalizing the language of \bs\ as seems required by the range of
examples we have considered, it suffices to annotate ground clauses
with the $\Omega$ needed to reproduce a larger axiom set.  Before we
formalize this, however, note that any ``reasonable'' permutation that
maps a literal $l_1$ to another literal $l_2$ should respect the
semantics of the axiomatization and map $\neg l_1$ to $\neg l_2$ as
well.

\begin{definition}  Given a set of $n$ variables, we will denote by
$W_n$ that subgroup of $S_{2n}$ consisting of permutations that map
the literal $\neg l_1$ to $\neg l_2$ whenever they map $l_1$ to
$l_2$.\label{d.wreath}
\end{definition}
Informally, an element of $W_n$ corresponds to a permutation of the
$n$ variables, together with a choice to flip some subset of them;
$W_n$ is therefore of size $|W_n|=2^n n!$.\footnote{We note in passing
that $W_n$ is the so-called wreath product of $S_2$ and $S_n$,
typically denoted $S_2 \wr S_n$.  The specific group $W_n$ is also
called the group of ``permutations and complementations'' by Harrison
\citeyear{Harrison}.}

We are now in a position to state:

\begin{definition} An {\em augmented clause\/} in an $n$-variable
\bs\ problem is a pair $(c,G)$ where $c$ is a Boolean clause and
$G\leq W_n$.  A ground clause $c'$ is an {\em instance\/} of an
augmented clause $(c,G)$ if there is some $g\in G$ such that $c'=c^g$.
The clause $c$ will be called the {\em base instance\/} of
$(c,G)$.\end{definition}

Our aim in the remainder of this paper is to show that augmented
clauses have the properties needed to justify the claims we made in
the introduction:
\begin{enumerate} \bf
\item They can be represented compactly,
\item They can be combined efficiently using a generalization of
resolution,
\item They generalize existing concepts such as quantification over
finite domains, cardinality, and parity clauses, together with
providing natural generalizations for proof techniques involving such
clauses,
\item \Rbl\ can be extended with little or no computational overhead
to manipulate augmented clauses instead of ground ones, and
\item Propagation can be computed efficiently in this generalized
setting.
\end{enumerate}
 The first four points will be discussed in this and the next three
sections of the paper.  The final point is presented in the next paper
in this series.

\subsection{Efficiency of Representation}
\label{s.efficiency}

For the first point, the fact that the augmentations $G$ can be
represented compactly is a consequence of $G$'s group structure.  In
the example surrounding the reconstruction of \eq{ex2} from
\eq{ex2-sub}, for example, the group in question is the full symmetry
group on $m$ elements, where $m$ is the number of variables in the
cardinality clause.  In the lifting example \eq{ex3}, we can describe
the group in terms of the generators $\omega_x$, $\omega_y$ and
$\omega_z$ instead of listing all eight elements that the group
contains.  In general, we have (recall that proofs appear in the
appendix):

\begin{proposition} Let $S$ be a set of ground clauses, and
$(c,G)$ an equivalent augmented clause, where $G$ is represented by
generators.  It is possible in polynomial time to find a set of
generators $\set{\omega_1,\dots,\omega_k}$ where $k\leq \log_2 |G|$
and $G=\langle
\omega_1,\dots,\omega_k\rangle$.\label{p.size}\end{proposition}

Since the size of the full permutation group $S_n$ is only $n!<n^n$
and a single generator takes at most $O(n)$ space, we have:

\begin{corollary} Any augmented clause in a theory containing $n$
literals can be expressed in $O(n^2 \log_2 n)$
space.\proofend\label{c.small}\end{corollary}
 This result can be strengthened using:

\begin{proposition}{\bf \cite{Jerrum:stabchain,Knuth:stabchain}} Let 
$G\leq S_n$.  It is possible to find in polynomial time a set of
generators for $G$ of size at most $O(n)$.\proofend
\label{p.small}
\end{proposition}
 This reduces the $O(n^2 \log_2 n)$ in the corollary to simply
$O(n^2)$.\footnote{Although the methods used are nonconstructive,
Babai~\citeyear{Babai:bound} showed that the length of an increasing
sequence of subgroups of $S_n$ is at most $\lfloor\frac{3n}2\rfloor -
2$; this imposes the same bound on the number of generators needed
(compare the proof of \prop{size}).  Using other methods, McGiver and
Neumann stated \citeyear{McIver:bound} that for $n\neq 3$, there is
always a generating set of size at most $\lfloor \frac n2 \rfloor$.}

Before proceeding, let us make a remark regarding computational
complexity.  All of the group-theoretic constructs of interest to us
can be computed in time polynomial in the group size; basically one
simply enumerates the group and evaluates the construction (generate
and test, as it were).  What is interesting is the collection of group
constructions that can be computed in time polynomial in the number of
{\em generators\/} of the group and the number of variables in the
problem.  Given \prop{small}, the time is thus polynomial in the
number of variables in the problem.

Note that the size of the group $G$ can be vastly greater than the
number of instances of any particular augmented clause $(c,G)$.  As an
example, for the cardinality clause
\begin{equation}
x_1+\cdots+x_m \geq k
\label{e.card4}
\end{equation}
the associated symmetry group $\Sym\set{x_1,\dots,x_m}$ acts on an
instance such as
\begin{equation}
x_1\vee\cdots\vee x_{m-k+1}
\label{e.card3}
\end{equation}
to reproduce the full Boolean axiomatization.  But each such instance
corresponds to \mbox{$(m-k+1)!$} distinct group elements as the
variables within the clause \eq{card3} are permuted.

In this particular case, the symmetry group $\Sym\set{x_1,\dots,x_m}$
can in fact be generated by the two permutations $(x_1,x_2)$ and
$(x_2,x_3,\dots,x_m)$.

\begin{definition}  Two augmented clauses $(c_1,G_1)$ and $(c_2,G_2)$
will be called {\em equivalent\/} if they have identical sets of
instances.  This will be denoted $(c_1,G_1) \equiv
(c_2,G_2)$.\end{definition}

\begin{proposition}  Let $(c,G)$ be an augmented clause.  Then if
$c'$ is any instance of $(c,G)$, $(c,G)\equiv
(c',G)$.\label{p.rewrite}\end{proposition}

We also have:

\begin{proposition}  Let $(c,G)$ be an augmented clause with $d$
distinct instances.  Then there is a subgroup $H\leq G$ that can be
described using $O(\log_2(d))$ generators such that $(c,H)\equiv
(c,G)$.  Furthermore, given $d$ and generators for $G$, there is a
Monte Carlo polynomial-time algorithm for constructing the generators
of such an $H$.\footnote{A Monte Carlo algorithm is one that is not
deterministic but that can be made to work with arbitrarily high
specified probability without changing its overall complexity
\cite{Seress}.}
\label{p.rsize}
\end{proposition}

\prop{small} is the first of the results promised in the introduction:
If $d$ Boolean axioms involving $n$ variables can be captured as
instances of an augmented clause, that augmented clause can be
represented using $O(n)$ generators; \prop{rsize} guarantees that
$O(\log_2 d)$ generators suffice as well.

In the specific instances that we have discussed, the representational
efficiencies are greater still:
\begin{center}
\begin{tabular}{c|c|c|c}
{\bf clause} & {\bf Boolean} && {\bf total} \\
{\bf type} & {\bf axioms} & {\bf generators} & {\bf size} \\
\hline
cardinality & $m \choose {k-1}$ & 2 & $m+1$ \\
parity & $2^{k-1}$ & 3 & $k+5$ \\
\qprop & $d^v$ & $2v$ & $v(d+1)$
\end{tabular}
\end{center}

Each row gives the number of Boolean axioms or generators needed to
represent a clause of the given type, along with the total size of
those generators.  For the cardinality clause \eq{card4}, the complete
symmetry group over $m$ variables can be expressed using exactly two
generators, one of size 2 and the other of size $m-1$.\footnote{As
noted earlier, $S_n$ is generated by the transposition $(1,2)$ and the
$n-1$-cycle $(2,3,\dots,n)$.}  The number of Boolean axioms is $m
\choose {k-1}$ as explained in \secn{card}.

For the parity clause
\[x_1 + \cdots + x_k \equiv m\;(\mod\ 2)\] 
the number of Boolean axioms is the same as the number of ways to
select an even number of the $x_i$'s, which is half of all of the
subsets of $\set{x_1,\dots,x_k}$.  (Remove $x_1$ from the set; now
{\em any\/} subset of the remaining $x_i$ can be made of even parity
by including $x_1$ or not as appropriate.)  The parity groups $F_k$
can be captured by $k-1$ generators of the form $(x_1,\neg
x_1),(x_i,\neg x_i)$ as $i=2,\dots,k$ (total size $4(k-1)$);
alternatively, one can combine the single generator $(x_1,\neg
x_1)(x_2,\neg x_2)$ with the full symmetry group on $x_1,\dots,x_k$ to
describe a parity clause using exactly three generators (total size
$4+2+k-1$).

Finally, a \qprop\ clause involving $v$ variables, each with a domain
of size $d$, corresponds to a set of $d^v$ individual domain axioms.
As we saw in \secn{formalize} and will formalize in \secn{qprop}, the
associated group can be described using symmetry groups over the
domains of each quantified variable; there are $v$ such groups and two
generators (of size 2 and $d-1$) are required for
each.\footnote{Depending on the sizes, the number of generators needed
for a product of symmetry groups can be reduced in many cases,
although the total size is unchanged.}

Note that the total sizes are virtually optimal in all of these cases.
For cardinality and parity clauses, it is surely essential to
enumerate the variables in question (size $m$ and $k$ respectively).
For \qprop\ clauses, simply enumerating the domains of quantification
takes space $vd$.

\section{Resolution}
\label{s.resolution}

We now turn to the question of basing derivations on augmented clauses
instead of ground ones.  We begin with a few preliminaries:

\begin{proposition} For ground clauses $c_1$ and $c_2$ and a permutation
$\omega \in W_n$, 
\[\resolve(\omega(c_1),\omega(c_2)) = \omega(\resolve(c_1,c_2))\]
\label{p.resolve-homo}
\end{proposition}

\begin{definition} If $C$ is a set of augmented clauses, we will
say that $C$ {\em entails\/} an augmented clause $(c,G)$, writing
$C\models (c,G)$, if every instance of $(c,G)$ is entailed by the set
of instances of the augmented clauses in $C$.\end{definition}

We are now in a position to consider lifting the idea of resolution to
our setting, but let us first discuss the overall intent of this
lifting.  What we would like to do is to think of an augmented clause
as having force similar to all of its instances; as a result, when we
resolve two augmented clauses $(c_1,G_1)$ and $(c_2,G_2)$, we would
like to obtain as the (augmented) resolvent the set of all resolutions
that are sanctioned by resolving an instance of $(c_1,G_1)$ with one
of $(c_2,G_2)$.  Unfortunately, we have:

\begin{proposition} There are augmented clauses $c_1$ and $c_2$ such
that the set $S$ of resolvents of instances of the two clauses does
not correspond to any single augmented clause $(c,G)$.
\label{p.no-resolve}
\end{proposition}

Given that we cannot capture {\em exactly\/} the set of possible
resolvents of two augmented clauses, what {\em can\/} we do?  If
$(c,G)$ is an ``augmented resolvent'' of $(c_1,G_1)$ and $(c_2,G_2)$,
we might expect $(c,G)$ to have the following properties:

\begin{enumerate}
\item It should be {\em sound}, in that $(c_1,G_1) \wedge (c_2,G_2)
\models (c,G)$.\label{sound} This says that every instance of $(c,G)$
is indeed sanctioned by resolving an instance of $(c_1,G_1)$ with an
instance of $(c_2,G_2)$.
\item It should be {\em complete}, in that $\resolve(c_1,c_2)$ is an
instance of $(c,G)$.  We may not be able to capture every possible
resolvent in the augmented clause $(c,G)$, but we should surely
capture the base case that is obtained by resolving the base instance
$c_1$ directly against the base instance $c_2$.\label{complete}
\item It should be {\em monotonic}, in that if $G_1\leq H_1$ and
$G_2\leq H_2$, then $(c,G)$ is also a resolvent of $(c_1,H_1)$ and
$(c_2,H_2)$.\label{monotonic} As the clauses being resolved become
stronger, the resolvent should become stronger as well.
\item It should be {\em polynomial}, in that it is possible to confirm
that $(c,G)$ is a resolvent of $(c_1,G_1)$ and $(c_2,G_2)$
in polynomial time.\label{polynomial}
\item It should be {\em stable}, in that if $c_1^G=c_2^G$, then
$(\resolve(c_1,c_2),G)$ is a resolvent of $(c_1,G)$ and
$(c_2,G)$.\label{stable} Roughly speaking, this says that if the
groups in the two input clauses are the same, then the augmented
resolvent can be obtained by resolving the base instances $c_1$ and
$c_2$ and then operating with the same group.
\item It should be {\em strong}, in that if no element of $c_1^{G_1}$
is moved by $G_2$ and similarly no element of $c_2^{G_2}$ is moved by
$G_1$, then $(\resolve(c_1,c_2),\langle G_1,G_2\rangle)$ is a
resolvent of $(c_1,G_1)$ and $(c_2,G_2)$.  This says that if the group
actions are distinct in that $G_1$ acts on $c_1$ and leaves $c_2$
completely alone and vice versa, then we should be able to get the
complete group of resolvents in our answer.  This group corresponds to
be base resolvent $\resolve(c_1,c_2)$ acted on by the group generated
by $G_1$ and $G_2$.
\label{aggressive}
\end{enumerate}

\begin{definition} A definition of augmented resolution will be
called {\em satisfactory\/} if it satisfies the above conditions.
\label{d.satisfactory}
\end{definition}

Note that we do {\em not\/} require that the definition of augmented
resolution be unique.  Our goal is to define conditions under which
$(c,G)$ is {\em an\/} augmented resolvent of $(c_1,G_1)$ and
$(c_2,G_2)$, as opposed to ``the'' augmented resolvent of $(c_1,G_1)$
and $(c_2,G_2)$.  To the best of our knowledge (and as suggested by
\prop{no-resolve}), there is no satisfactory definition of augmented
resolution that defines the resolvent of two augmented clauses
uniquely.

As we work toward a satisfactory definition of augmented resolution,
let us consider some examples to help understand what the basic issues
are.  Consider, for example, resolving the two clauses
\[(a\vee b,\langle (bc)\rangle)\]
which has instances $a\vee b$ and $a\vee c$ and
\[(\neg a \vee d,\langle \rangle)\]
which has the single instance $\neg a \vee d$.  We will write these
somewhat more compactly as
\begin{equation}
(a\vee b,(bc))
\label{e.augment1}
\end{equation}
and
\begin{equation}
(\neg a \vee d,{\bf 1})
\label{e.augment2}
\end{equation}
respectively.

Resolving the clauses individually, we see that we should be able to
derive the pair of clauses $b\vee d$ and $c\vee d$; in other words,
the augmented clause
\begin{equation}
(b\vee d,(bc))
\label{e.augment3}
\end{equation}
It certainly seems as if it should be possible to capture this in our
setting, since the base instance of \eq{augment3} is just the
resolvent of the base instances of \eq{augment1} and
\eq{augment2}.\footnote{Indeed, condition (\ref{aggressive}) requires
that $b\vee d$ be an instance of some augmented resolvent, since the
groups act independently in this case.}  Where does the group
generated by $(bc)$ come from?

To answer this, we begin by introducing some additional notation.

\begin{definition}  Let $\omega$ be a permutation and $S$ a
set.  Then by $\omega|_S$ we will denote the result of restricting the
permutation to the given set.
\end{definition}
 Note that $\omega|_S$ will be a permutation on $S$ if and only if
$S^{\omega}= S$, so that $S$ is fixed by $\omega$.

\begin{definition}  For $K_1,\dots,K_n\subseteq L$ and $G_1,\dots,G_n
\leq \Sym(L)$, we will say that a permutation $\omega\in \Sym(L)$ is
an {\em extension of $\set{G_1,\dots,G_n}$ for
$\set{K_1,\dots,K_n}$\/} if there are $g_i\in G_i$ such that for all
$i$, $\omega|_{K_i} = g_i|_{K_i}$.  We will denote the set of such
extensions by $\ext(K_i,G_i)$.
\label{d.extension}
\end{definition}
 The definition says that any particular extension $x\in\ext(K_i,G_i)$
must simultaneously extend elements of all of the individual groups
$G_i$, when those groups act on the various subsets $K_i$.

As an example, suppose that $K_1 = \set{a,b}$ and $K_2 = \set{\neg
a,e}$, with $G_1=\Sym\set{b,c,d}$ and $G_2=\langle(ed)\rangle$.  A
permutation is an extension of the $G_i$ for $K_i$ if and only if,
when restricted to $\set{a,b}$ it is a member of $\Sym(b,c,d)$ and,
when restricted to $\set{a,e}$ it is a member of $\langle(ed)\rangle$.
In other words, $b$ can be mapped to $b$, $c$ or $d$, and $e$ can be
mapped to $d$ if desired.  The set of extensions is thus
\begin{equation}
\set{(),(bc),(bd),(bcd),(bdc),(cd),(ed),(edc),(bc)(de)}
\label{e.nongroup}
\end{equation}
Note that this set is not a group because it is not closed under the
group operations; $(edc)$ is permitted ($e$ is mapped to $d$ and we
don't care where $d$ and $c$ go), but $(edc)^2 = (ecd)$ is not.

Considered in the context of resolution, suppose that we are trying to
resolve augmented clauses $(c_1,G_1)$ and $(c_2,G_2)$.  At some level,
any result $(\resolve(c_1,c_2),G)$ for which $G\subseteq
\ext(c_i,G_i)$ should be a legal resolvent of the original clauses,
since each instance is sanctioned by resolving instances of the
originals.\footnote{We can't write $G\leq \ext(c_i,G_i)$ because
$\ext(c_i,G_i)$ may not be a group.}  We can't define the resolvent to
be $(\resolve(c_1,c_2),\ext(c_i,G_i))$ because, as we have seen from
our example, neither $\ext(c_i,G_i)$ nor $\ext(c_i,G_i)\cap W_n$ need
be a group.  (We also know this from \prop{no-resolve}; there may be
no single group that captures all of the possible resolvents.)  But we
can't simply require that the augmented resolvent $(c,G)$ have
$G\subseteq \ext(c_i,G_i)$, because there is no obvious polynomial
test for inclusion of a group in a set.\footnote{It is possible to
test in polynomial time if $G\leq H$, since we can simply test each
generator of $G$ for membership in $H$.  But if $H$ is not closed
under the group operation, the fact that the generators are all in $H$
is not sufficient to conclude that $G\subseteq H$.}

To overcome these difficulties, we need a version of \defn{extension}
that produces a {\em group\/} of extensions, as opposed to just a set:

\begin{definition}  For $K_1,\dots,K_n\subseteq L$ and $G_1,\dots,G_n
\leq \Sym(L)$, we will say that a permutation $\omega\in \Sym(L)$ is a
{\em stable extension of $\set{G_1,\dots,G_n}$ for
$\set{K_1,\dots,K_n}$\/} if there are $g_i\in G_i$ such that for all
$i$, $\omega|_{K_i^{G_i}} = g_i|_{K_i^{G_i}}$.  We will denote the set
of stable extensions of $\set{G_1,\dots,G_n}$ for
$\set{K_1,\dots,K_n}$ by $\sext(K_i,G_i)$.
\label{d.stable}
\end{definition}
 This definition is modified from \defn{extension} only in that the
restriction of $\omega$ is not just to the original sets $K_i$ for
each $i$, but to $K_i^{G_i}$, the $G_i$-closure of $K_i$ (recall
\defn{closure}).

In our example where $K_1 = \set{a,b}$ and $K_2 = \set{\neg a,e}$,
with $G_1=\Sym\set{b,c,d}$ and $G_2=\langle(ed)\rangle$, a stable
extension must be a member of $\Sym(b,c,d)$ when restricted to
$\set{a,b,c,d}$ (the $G_1$-closure of $K_1$), and must be a member of
$\langle(ed)\rangle$ when restricted to $\set{d,e}$.  This means that
we {\em do\/} care where a candidate permutation maps $c$ and $d$, so
that the set of stable extensions, instead of \eq{nongroup}, is
instead simply $\set{(),(bc)} = \langle(bc)\rangle$.  The fact that
$d$ has to be mapped to $b$, $c$, or $d$ by virtue of $G_1$ and has to
be mapped to either $d$ or $e$ by virtue of $G_2$ means that $d$ has
to be fixed by any permutation in $\sext(K_i,G_i)$, which is why the
resulting set of stable extensions is so small.

In general, we have:

\begin{proposition} $\sext(K_i,G_i)\leq \Sym(L)$.\label{p.stable}
\end{proposition}
 In other words, $\sext(K_i,G_i)$ is a subgroup of $\Sym(L)$.

At this point, we still need to deal with the monotonicity condition
(\ref{monotonic}) of \defn{satisfactory}.  After all, if we have
\[(c,G) \models (c',G')\]
we should also have
\[\resolve((c,G),(d,H)) \models \resolve((c',G'),(d,H))\]
To see why this is an issue, suppose that we are resolving
\begin{equation}
(a\vee b,\Sym\set{b,c,d})
\label{e.mon1}
\end{equation}
 with
\begin{equation}
(\neg a\vee e,{(ed)})
\label{e.mon2}
\end{equation}
 Because the groups both act on $d$, we have already seen that if we
take the group of stable extensions as the group in the resolvent, we
will conclude $(b\vee e,{(bc)})$.  But if we replace \eq{mon2} with
$(\neg a\vee e,{\bf 1})$ before resolving, the result is the stronger
$(b\vee e,\Sym\set{b,c,d})$.  If we replace \eq{mon1} with $(a\vee
b,{(bc)})$, the result is the different but also stronger $(b\vee
e,\grp{(bc),(de)})$

The monotonicity considerations suggest:

\begin{definition}  Suppose that $(c_1,G_1)$ and $(c_2,G_2)$ are
augmented clauses where $c_1$ and $c_2$ resolve in the conventional
sense.  Then a {\em resolvent\/} of $(c_1,G_1)$ and $(c_2,G_2)$ is any
augmented clause of the form $(\resolve(c_1,c_2),G)$ where $G\leq
\sext(c_i,H_i)\cap W_n$ for some $H_i\leq G_i$ for $i=1,2$.  The {\em
canonical resolvent\/} of $(c_1,G_1)$ and $(c_2,G_2)$, to be denoted
by $\resolve((c_1,G_1),(c_2,G_2))$, is the augmented clause
$(\resolve(c_1,c_2),\sext(c_i,G_i) \cap W_n)$.
\label{d.resolution}
\end{definition}

\begin{proposition} \defn{resolution} of (noncanonical) resolution is
satisfactory.  The definition of canonical resolution satisfies all of
the conditions of \defn{satisfactory} except for monotonicity.
\label{p.resolution}
\end{proposition}

Before proceeding, let us consider the example that preceded
\defn{resolution} in a bit more detail.  There, we were looking for
augmented resolvents of $(a\vee b,\Sym\set{b,c,d})$ from \eq{mon1} and
$(\neg a\vee e,{(ed)})$ from \eq{mon2}.

To find such a resolvent, we begin by selecting $H_1\leq
G_1=\Sym\set{b,c,d}$ and $H_2\leq G_2=\langle(ed)\rangle$.  We then
need to use \defn{stable} to compute the group of stable extensions of
$(c_1,H_1)$ and $(c_2,H_2)$.

If we take $H_1$ and $H_2$ to be the trivial group $\bf 1$, then the
group of stable extensions is also trivial, so we see that
\[(\resolve(a\vee b,\neg a\vee e),{\bf 1}) = (b\vee e,{\bf 1})\]
is a resolvent of \eq{mon1} and \eq{mon2}.  Other choices for $H_1$
and $H_2$ are more interesting.

If we take $H_1={\bf 1}$ and $H_2=G_2$, the stable extensions leave
the first clause fixed but can move the image of the second consistent
with $G_2$.  This produces the augmented resolvent $(b\vee e,(de))$.

If, on the other hand, we take $H_1=G_1$ and $H_2={\bf 1}$, we have to
leave $e$ fixed but can exchange $b$, $c$ and $d$ freely, and we get
$(b\vee e,\Sym\set{b,c,d})$ as the resolvent.

If $H_1=G_1$ and $H_2=G_2$, we have already computed the group of
stable extensions in earlier discussions of this example; the
augmented resolvent is $(b\vee e,(bc))$, which is weaker than the
resolvent of the previous paragraph.  And finally, if we take
$H_1=\langle(bc)\rangle$ and $H_2=G_2$, we can exchange $b$ and $c$ or
independently exchange $d$ and $e$ so that we get the augmented
resolvent $(b\vee e,\grp{(bc),(de)})$.  These choices have already
been mentioned in the discussion of monotonicity that preceded
\defn{resolution}.

There is a variety of additional remarks to be made about
\defn{resolution}.  First, {\em canonical\/} resolution lacks the
monotonicity property, as shown by our earlier example.  In addition,
the resolvent of two augmented clauses can obviously depend on the
choice of the representative elements in addition to the choice of
subgroup of $\sext(c_i,G_i)$.  Thus, if we resolve
\begin{equation}
(l_1,(l_1l_2))
\label{e.instance-a}
\end{equation}
with
\begin{equation}
(\neg l_1,{\bf 1})
\label{e.instance-b}
\end{equation}
we get a contradiction.  But if we rewrite \eq{instance-a} so that we
are attempting to resolve \eq{instance-b} with
\[(l_2,(l_1l_2))\]
no resolution is possible at all.

To address this in a version of \rbl\ that has been lifted to our more
general setting, we need to ensure that if we are trying to resolve
$(c_1,G_1)$ and $(c_2,G_2)$, the base instances $c_1$ and $c_2$
themselves resolve.  As we will see, this can be achieved by
maintaining ground reasons for each literal in the annotated partial
assignment.  These ground clauses will always resolve when a
contradiction is found and the search needs to backtrack.

We should also point out that there are computational issues involved
in the evaluation of $\sext(c_i,G_i)$.  If the component groups $G_1$
and $G_2$ are described by listing their elements, an incremental
construction is possible where generators are gradually added until it
is impossible to extend the group further without violating
\defn{resolution}.  But if $G_1$ and $G_2$ are described only in terms
of their generators, as suggested by the results in \secn{efficiency},
computing $\sext(c_i,G_i)$ involves the following computational
subtasks \cite{Ginsberg:zap3} (recall
\defn{stabilize}):\footnote{There is an additional requirement that we
be able to compute $\sext(c_i,G_i)\cap W_n$ from $\sext(c_i,G_i)$.
This is not an issue in practice because we work with an overall
representation in which all groups are represented by their
intersections with $W_n$.  Thus if $g$ is included as a generator for
a group $G$, we automatically include in the generators for $G$ the
``dual'' permutation to $g$ where every literal has had its sign
flipped.}
\begin{enumerate}
\item Given a group $G$ and set $C$, find $G_{\set C}$.
\item Given a group $G$ and set $C$, find $G_C$.
\item Given two groups $G_1$ and $G_2$ described in terms of
generators, find a set of generators for $G_1\cap G_2$.
\item Given $G$ and $C$, let $\omega \in G_{\set C}$.  Now
$\omega|_C$, the restriction of $\omega$ to $C$, makes sense because
$C^{\omega} = C$.  Given a $\rho$ that is such a restriction, find an
element $\rho'\in G$ such that $\rho'|_C = \rho$.
\end{enumerate}

We will have a great deal more to say about these issues in the paper
describing the \zap\ implementation.  At this point, we remark merely
that time complexity is known to be polynomial only for the second and
fourth of the above problems; the other two are not known to be in
polynomial time.  However, \cgt\ systems incorporate procedures that
rarely exhibit super-polynomial behavior even though one can construct
examples that force them to take exponential time (as usual, in terms
of the number of generators of the groups, not their absolute size).

In the introduction, we claimed that the result of resolution was
unique using reasons and that \zap's fundamental inference step was
both in NP with respect to the \zap\ representation and of low-order
polynomial complexity in practice.  The use of reasons breaks the
ambiguity surrounding \eq{instance-a} and \eq{instance-b}, and the
remarks regarding complexity correspond to the computational
observations just made.

\section{Examples and Proof Complexity}
\label{s.example}

Let us now turn to the examples that we have discussed previously:
first-order axioms that are quantified over finite domains, along with
the standard examples from proof complexity, including \php s, clique
coloring problems and parity clauses.  For the first, we will see
that our ideas generalize conventional notions of quantification while
providing additional representational flexibility in some cases.  For
the other examples, we will present a ground axiomatization, recast it
using augmented clauses, and then give a polynomially sized derivation
of unsatisfiability using augmented resolution.  

\subsection{Lifted Clauses and QPROP}
\label{s.qprop}

To deal with lifted clauses, suppose that we have a quantified
clause such as
\begin{equation}
\forall xyz.a(x,y)\vee b(y,z) \vee c(z)
\label{e.lifted}
\end{equation}
Suppose that the domain of $x$ is $X$, that of $y$ is $Y$, and that of
$z$ is $Z$.  Thus a grounding of the clause \eq{lifted} involves
working with a map that takes three elements $x\in X$, $y\in Y$ and
$z\in Z$ and produces the ground atoms corresponding to $a(x,y)$,
$b(y,z)$ and $c(z)$.  In other words, if $V$ is the set of variables
in our problem, there are injections
\begin{eqnarray*}
a&:& X\times Y \rightarrow V \\
b&:& Y\times Z \rightarrow V \\
c&:& Z \rightarrow V 
\end{eqnarray*}
 where the images of $a$, $b$ and $c$ are disjoint and each is an
injection because distinct relation instances must be mapped to distinct
ground atoms.

Now given a permutation $\omega$ of the elements of $X$, we can define
a permutation $\rho_X(\omega)$ on $V$ given by:
\[\rho_X(\omega)(v) = \cases{a(\omega(x),y),& if $v=a(x,y)$; \cr
		       v; & otherwise.\cr}\]
 In other words, there is a mapping $\rho_X$ from the set of permutations
on $X$ to the set of permutations on $V$:
\[\rho_X:\Sym(X)\rightarrow \Sym(V)\]

\begin{definition} Let $G$ and $H$ be groups and $f:G\rightarrow H$
a function between them.  $f$ will be called a {\em homomorphism\/} if
it respects the group operation in that $f(g_1 g_2) = f(g_1)
f(g_2)$.\end{definition}

It should be clear that:

\begin{proposition} $\rho_X:\Sym(X)\rightarrow \Sym(V)$ is an injection 
and a homomorphism.\proofend\end{proposition}

\noindent In other words, $\rho_X$ makes a ``copy'' of $\Sym(X)$
inside of $\Sym(V)$ corresponding to permuting the elements of $x$'s
domain $X$.

In a similar way, we can define homomorphisms $\rho_Y$ and
$\rho_Z$ given by
\[\rho_Y(\omega)(v) = \cases{a(x,\omega(y)),& if $v=a(x,y)$; \cr
		       b(\omega(y),z),& if $v=b(y,z)$; \cr
		       v; & otherwise.\cr}\]
and
\[\rho_Z(\omega)(v) = \cases{b(y,\omega(z)),& if $v=b(y,z)$; \cr
		       c(\omega(z)),& if $v=c(z)$; \cr
		       v; & otherwise.\cr}\]

Now consider the subgroup of $\Sym(V)$ generated by the three images
$\rho_X(\Sym(X))$, $\rho_Y(\Sym(Y))$ and $\rho_Z(\Sym(Z))$.  It is
clear that the three images commute with one another, and that their
intersection is only the trivial permutation.  This means that
$\rho_X$, $\rho_Y$ and $\rho_Z$ collectively inject the product
$\Sym(X)\times \Sym(Y)\times \Sym(Z)$ into $\Sym(V)$; we will denote
this by
\[\rho_{XYZ}:\Sym(X)\times \Sym(Y)\times \Sym(Z)\rightarrow \Sym(V)\]
 and it should be clear that the original quantified axiom \eq{lifted}
is equivalent to the augmented axiom 
\[(a(A,B)\vee b(B,C) \vee c(C),\rho_{XYZ}(\Sym(X)\times \Sym(Y)\times \Sym(Z)))\]
 where $A$, $B$ and $C$ are any (not necessarily distinct) elements of
$X$, $Y$ and $Z$, respectively.  The quantification is exactly
captured by the augmentation.

The interesting thing is what happens to resolution in this setting:

\begin{proposition} Let $p$ and $q$ be quantified clauses such that
there is a term $t_p$ in $p$ and $\neg t_q$ in $q$ where $t_p$ and
$t_q$ have common instances.  Suppose also that $(p_g,P)$ is an
augmented clause equivalent to $p$ and $(q_g,Q)$ is an augmented
clause equivalent to $q$, where $p_g$ and $q_g$ resolve.  Then if no
terms in $p$ and $q$ except for $t_p$ and $t_q$ have common instances,
the result of resolving $p$ and $q$ in the conventional lifted sense
is equivalent to
$\resolve((p_g,P),(q_g,Q))$.\label{p.qprop}\end{proposition}

Here is an example.  Suppose that $p$ is
\begin{equation}
a(A,x) \vee b(C,y,z) \vee c(x,y,z)
\label{e.lift1}
\end{equation}
and $q$ is
\begin{equation}
a(B,x) \vee \neg b(x,D,z)
\label{e.lift2}
\end{equation}
 so that the most general unifier of the two appearances of $b$ binds
$x$ to $C$ in \eq{lift2} and $y$ to $D$ in \eq{lift1} to produce
\begin{equation}
a(A,x) \vee c(x,D,z) \vee a(B,C)
\label{e.liftr}
\end{equation}

In the version using augmented clauses, it is clear that if we select
ground instances $p_g$ of \eq{lift2} and $q_g$ of \eq{lift1} that
resolve, the resolvent will be a ground instance of \eq{liftr}; the
interesting part is the group.  For this, note simply that the image
of $p_g$ is the entire embedding of $\Sym(X)\times
\Sym(Y)\times\Sym(Z)$ into $\Sym(L)$ corresponding to the lifted axiom
\eq{lift1}, and the image of $q_g$ is similarly the embedded image of
$\Sym(X)\times \Sym(Z)$ corresponding to \eq{lift2}.

The group of stable extensions of the two embeddings corresponds to
any bindings for the variables in \eq{lift1} and \eq{lift2} that can
be extended to a permutation of all of the variables in question; in
other words, to bindings that (a) are consistent in that common ground
literals in the two expressions are mapped to the same ground literal
by both sets of bindings, and (b) are disjoint in that we do not
attempt to map two quantified literals to the same ground instance.
This latter condition is guaranteed by the conditions of the
proposition, which require that the non-resolving literals have no
common ground instances.  In this particular example, if we choose the
instances
\[a(A,\alpha) \vee b(C,D,\beta) \vee c(\alpha,D,\beta)\]
for \eq{lift1} and 
\[a(B,C) \vee \neg b(C,D,\beta)\]
for \eq{lift2}, the resulting augmented clause is
\begin{equation}
(a(A,\alpha) \vee c(\alpha,D,\beta) \vee a(B,C),G)
\label{e.lift3}
\end{equation}
where $G$ is the group mapping $\Sym(X)\times\Sym(Z)$ into $\Sym(L)$
so that \eq{lift3} corresponds to the quantified clause \eq{liftr}.

The condition requiring lack of commonality of ground instances is
necessary; consider resolving
\[a(x) \vee b\]
with
\[a(y) \vee \neg b\]

In the quantified case, we get
\begin{equation}
\forall xy.a(x)\vee a(y)
\label{e.liftsame}
\end{equation}
 In the augmented case, it is not hard to see that if we resolve
$(a(A)\vee b,G)$ with $(a(A)\vee \neg b,G)$ we get
\[(a(A),G)\]
corresponding to 
\begin{equation}
\forall x.a(x)
\label{e.augmentedsame}
\end{equation}
while if we choose to resolve $(a(A)\vee b,G)$ with $(a(B)\vee \neg
b,G)$, we get instead
\[\forall x\neq y.a(x) \vee a(y)\]

It is not clear which of these representations is superior.  The
conventional \eq{liftsame} is more compact, but obscures the fact that
the stronger \eq{augmentedsame} is entailed as well.  This particular
example is simple, but other examples involving longer clauses and
some residual unbound variables can be more complex.

\subsection{Proof Complexity}

We conclude this section with a demonstration that \zap\ can produce
polynomial proofs of the problem instances appearing in the original
table of the introduction.

\subsubsection{Pigeonhole Problems}

Of the examples known to be exponentially difficult for conventional
resolution-based systems, \php s are in many ways the simplest.  As
usual, we will denote by $p_{ij}$ the fact that pigeon $i$ (of $n+1$)
is in hole $j$ of $n$, so that there are $n^2+n$ variables in the
problem.  We denote by $G$ the subgroup of $W_{n^2+n}$ that allows
arbitrary exchanges of the $n+1$ pigeons or the $n$ holes, so that $G$
is isomorphic to $S_{n+1}\times S_n$.  This particular example is
straightforward because there is a single global group that we will be
able to use throughout the analysis.

Our axiomatization is now:
\begin{equation}
(\neg p_{11} \vee \neg p_{21},G)
\label{e.pig1}
\end{equation}
saying that no two pigeons can be in the same hole, and
\begin{equation}
(p_{11}\vee\cdots \vee p_{1n},G)
\label{e.pig2}
\end{equation}
saying that the first (and thus every) pigeon has to be in some hole.

\begin{proposition} There is an augmented resolution proof of polynomial
size of the mutual unsatisfiability of \eq{pig1} and
\eq{pig2}.\label{p.php}\end{proposition}

\proof This is a consequence of the stronger \prop{php2} below, but we
also present an independent proof in the appendix.  The ideas in the
proof are needed in the analysis of the clique-coloring problem.
\proofend

\begin{proposition} Any implementation of \prc{rbl} that branches on
positive literals in unsatisfied clauses on \lin{rblbranch} will
produce a proof of polynomial size of the mutual unsatisfiability of
\eq{pig1} and \eq{pig2}, independent of specific branching choices
made.\label{p.php2}
\end{proposition}
 This strikes us as a remarkable result: Not only is it possible to
find a proof of polynomial length in the augmented framework, but in
the presence of \up, it is difficult not to!

A careful proof of this result is in the appendix, but it will be
useful to examine in detail how a prover might proceed in a small
(four pigeon, three hole) example.

We begin by branching on (say) $p_{11}$, saying that pigeon one is in
hole one.  Now \up\ allows us to conclude immediately that no other
pigeon is in hole one, so our annotated partial assignment is:
\[\begin{array}{c|c}
\mbox{literal} & \mbox{reason} \\
\hline
p_{11} & \true \\
\neg p_{21} & \neg p_{11} \vee \neg p_{21} \\
\neg p_{31} & \neg p_{11} \vee \neg p_{31} \\
\neg p_{41} & \neg p_{11} \vee \neg p_{41}
  \end{array}
\]

Now we try putting pigeon two in hole two,\footnote{We cannot conclude
that pigeon two is in hole two ``by symmetry'' from the existing
choice that pigeon one is in hole one, of course.  The symmetry group
can only be applied to the original clauses and to derived nogoods,
not to branch choices.  Alternatively, the branch choice corresponds
to the augmented clause $(p_{11},\bf 1)$ and not $(p_{11},G)$.} and
extend the above partial assignment with:
\[\begin{array}{c|c}
\mbox{literal} & \mbox{reason} \\
\hline
p_{22} & \true \\
\neg p_{12} & \neg p_{22} \vee \neg p_{12} \\
\neg p_{32} & \neg p_{22} \vee \neg p_{32} \\
\neg p_{42} & \neg p_{22} \vee \neg p_{42}
  \end{array}
\]

At this point, however, we are forced to put pigeons three and four in 
hole three, which leads to a contradiction $\bot$:
\[\begin{array}{c|c}
\mbox{literal} & \mbox{reason} \\
\hline
p_{33} & p_{31}\vee p_{32} \vee p_{33} \\
p_{43} & p_{41}\vee p_{42} \vee p_{43} \\
\bot & \neg p_{33} \vee \neg p_{43}
  \end{array}
\]

Resolving the last two reasons produces $\neg p_{33} \vee p_{41}\vee
p_{42}$, which we can resolve with the reason for $p_{33}$ to get
$p_{41}\vee p_{42} \vee p_{31}\vee p_{32}$.  Continuing to backtrack
produces $p_{41}\vee \neg p_{22} \vee p_{31}$.

Operating on the clause $p_{41}\vee \neg p_{22} \vee p_{31}$ with the
usual symmetry group (swapping hole 2 and hole 3) produces $p_{41}\vee
\neg p_{23} \vee p_{31}$, and now there is nowhere for pigeon two to
go.  We resolve these two clauses with $p_{21}\vee p_{22} \vee p_{23}$
to get $p_{41}\vee p_{31} \vee p_{21}$, and thus $\neg p_{11}$.  This
implies $\neg p_{ij}$ for all $i$ and $j$ under the usual symmetry,
and we conclude that the original axiomatization was unsatisfiable.

\subsubsection{Clique Coloring Problems}

The \php\ is difficult for resolution but easy for many other proof
systems; clique coloring problems are difficult for both resolution
and other approaches such as \pb\ axiomatizations \cite{clique}.

Clique coloring problems are derivatives of \php s where the exact
nature of the \php\ is obscured.  Somewhat more specifically, they say
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.

To formalize this, we will use $e_{ij}$ to describe the graph,
$c_{ij}$ to describe the coloring of the graph, and $q_{ij}$ to
describe the embedding of the clique into the graph.  The graph has
$m$ nodes, the clique is of size $n+1$, and there are $n$ colors
available.  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.  As in the
\php s, there is a global symmetry in this problem in that any two
nodes, clique elements or colors can be swapped.

\begin{proposition} There is an augmented resolution proof of polynomial
size of the unsatisfiability of
\eq{okcolor}--\eq{okmap}.\label{p.clique}\end{proposition}

The proof in the appendix presents a \zap\ proof of size $O(m^2n^2)$
for clique-coloring problems, where $m$ is the size of the graph and
$n$ is the size of the clique.  The \zap\ implementation produces
shorter proofs, of size $O((m+n)^2)$ \cite{Ginsberg:zap3}.  While
short, these proofs involve the derivation and manipulation of subtle
clauses and are too complex for us to understand.\footnote{It is not
clear whether one should conclude from this something good about \zap,
or something bad about the authors.  Perhaps both.}

Before we move on to parity clauses, note that the approach we are
proposing is properly stronger than one based on "symmetry-breaking"
axioms \cite{Ginsberg:symmetry} or the approaches taken by
Krishnamurthy \citeyear{Krish:symmetry} or Szeider
\citeyear{Szeider:symmetry}.  In the symmetry-breaking approach, the
original axiom set is modified so that as soon as a single symmetric
instance is falsified, so are all of that instance's symmetric
variants.  Both we and the other authors
\cite{Krish:symmetry,Szeider:symmetry} achieve a similar effect by
attaching a symmetry to the conclusion; either way, all symmetric
instances are removed as soon as it is possible to disprove any.
Unlike all of these other authors, however, an approach based on
augmented clauses is capable of exploiting local symmetries present in
a subset of the entire axiom set.  The other authors require the
presence of a global symmetry across the entire structure of the
problem.

\subsubsection{Parity Clauses}

Rather than discuss a specific example here, we show that determining
the satisfiability of any set of parity clauses is in $P$ for
augmented resolution.  The proof of this is modeled on a proof that
satisfiability of parity clauses is in $P$:

\begin{lemma} Let $C$ be a theory consisting entirely of parity
clauses.  Then determining whether or not $C$ is satisfiable is in
$P$.\label{l.mod2-easy}
\end{lemma} 
 As discussed in the introduction, the proof is basically a Gaussian
reduction argument.

\begin{definition}  Let $S$ be a subset of a set of $n$ variables.  We
will say that a permutation $\omega$ {\em flips\/} a variable $v$ if
$\omega(v) = \neg v$, and will denote by $F_S$ that subset of $W_n$
consisting of all permutations that leave the variable order unchanged
and flip an even number of variables in $S$.\end{definition}

\begin{lemma} $F_S \leq W_n$.\label{l.flip-ok}\end{lemma}

We now have the following:

\begin{lemma} Let $S =\set{x_1,\dots,x_k}$ be a subset of a set of
$n$ variables.  Then the parity clause
\[\sum x_i \equiv 1\]
is equivalent to the augmented clause
\[(x_1 \vee \cdots \vee x_k,F_S)\]
The parity clause
\[\sum x_i \equiv 0\]
is equivalent to the augmented clause
\[(\neg x_1 \vee x_2 \vee \cdots \vee x_k,F_S)\]
\label{l.mod2-rep}\end{lemma}

We can finally show:

\begin{proposition} Let $C$ be a theory consisting entirely of parity
clauses.  Then determining whether or not $C$ is satisfiable is in
$P$ for augmented resolution.
\label{p.mod2}
\end{proposition}

We note in passing that the construction in this section fails in the
case of modularity clauses with a base other than 2.  One of the
(many) problems is that the set of permutations that flip a set of
variables of size congruent to $m$ (mod $n$) is not a group unless
$m=0$ and $n<3$.  We need $m=0$ for the identity to be included, and
since both
\[(x_1,\neg x_1)\cdots(x_n,\neg x_n)\]
and 
\[(x_2,\neg x_2)\cdots(x_{n+1},\neg x_{n+1})\]
 are included, it follows that 
\[(x_1,\neg x_1)(x_{n+1},\neg x_{n+1})\]
 must be included, so that $n=1$ or $n=2$.

It is not clear whether this is coincidence, or whether there is a
deep connection between the fact that mod 2 clauses can be
expressed compactly using augmented clauses and are also solvable in
polynomial time.

\section{Theoretical and Procedural Description}
\label{s.describe}

In addition to resolution, an examination of Procedures \ref{p.rbl}
and \ref{p.upr} shows that we need to be able to eliminate nogoods
when they are irrelevant and to identify instances of augmented
clauses that are unit.  Let us now discuss each of these issues.

The problems around irrelevance are easier to deal with.  In the
ground case, we remove clauses when they are no longer relevant; in
the augmented version, we remove clauses that no longer possess
relevant instances.  We will defer until the final paper in this
series discussion of a procedure for determining whether $(c,G)$ has a
relevant instance.

We will also defer discussion of a specific procedure for computing
$\unit(P)$, but do include a few theoretical comments at this point.
In \up, we have a partial assignment $P$ and need to determine which
instances of axioms in $C$ are unit.  To do this, suppose that we
denote by $S(P)$ the set of \underline{S}atisfied literals in the
theory, and by $U(P)$ the set of \underline{U}nvalued literals.  Now
for a particular augmented clause $(c,G)$, we are looking for those
$g\in G$ such that $c^g\cap S(P) = \emptyset$ and $|c^g\cap
U(P)|\leq 1$.  The first condition says that $c^g$ has no satisfied
literals; the second, that it has at most one unvalued literal.

\begin{procedure}[\Up] To compute $\proc{Unit-Propagate}(C,P)$ for a
set $C$ of augmented clauses and an annotated partial assignment $P =
\langle(l_1,c_1),\dots,(l_n,c_n)\rangle$: \em
\begin{codebox}
\li \While there is a $(c,G)\in C$ and $g\in G$ with $c^g\cap
S(P) = \emptyset$ and $|c^g\cap U(P)|\leq 1$ \label{l.ddag}
\li   \Do \If $c^g\cap U(P) = \emptyset$
\li          \Then $l_i \gets$ the literal in $c^g$ with the highest
		 index in $P$
\li	     \Return $\langle \true,\resolve((c,G),c_i)\rangle$  \label{l.dag}
\li	    \Else $l\gets$ the literal in $c^g$ unassigned by $P$
\li		  add $(l,(c^g,G))$ to $P$
	  \End
     \End
\li \Return $\langle\false,P\rangle$
 \end{codebox}
\label{p.upg}
\end{procedure}
 Note that the addition made to $P$ when adding a new literal includes
both $c^g$, the instance of the clause that led to the propagation,
and the augmenting group as usual.  We can use $(c^g,G)$ as the
augmented clause by virtue of \prop{rewrite}.

Finally, the augmented version of \prc{rbl} is:

\begin{procedure}[Relevance-bounded reasoning, \rbl] Let $C$ be a \sat\
problem, and $D$ a set of learned nogoods.  Let $P$ be an annotated
partial assignment, and $k$ a fixed relevance bound.  To compute
$\proc{rbl}(C,D,P)$:\em
\begin{codebox}
\li $\langle x,y\rangle \gets \proc{Unit-Propagate}(C\cup D,P)$
\li  \If $x=\true$
\li    \Then $(c,G)\gets y$ \label{l.unit}
\li  \If $c$ is empty
\li    \Then \Return \const{failure}
\li    \Else remove successive elements from $P$ so that $c$ is unit
	\label{l.backtrackz}
\li	 $D\gets D\cup \set c$
\li	 remove from $D$ all augmented clauses without $k$-relevant instances
  \label{l.relevant}
\li   \Return $\proc{\rbl}(C,D,P)$
      \End
\li   \Else $P\gets y$
\li	\If $P$ is a solution to $C$
\li	  \Then \Return $P$
\li	\Else $l\gets$ a literal not assigned a value by $P$
\li	\Return $\proc{rbl}(C,\langle P,(l,\true)\rangle)$
      \End
    \End
\end{codebox}
\label{p.rblg}
\end{procedure}

Examining these two procedures, we see that we need to provide
implementations of the following:

\begin{enumerate}
\item A routine that computes the group of stable extensions appearing
in the definition of augmented resolution, needed by line \ref{l.dag}
in the unit propagation procedure \ref{p.upg}.
\item A routine that finds instances of $(c,G)$ for which $c^g\cap
S=\emptyset$ and $|c^g \cap U|\leq 1$ for disjoint $S$ and $U$,
needed by line \ref{l.ddag} in the unit propagation procedure
\ref{p.upg}.
\item A routine that determines whether $(c,G)$ has an instance for
which $\poss(c^g,P) \leq k$ for some fixed $k$, as needed by
\lin{relevant} of \prc{rblg}.
\end{enumerate}

All of these problems are known to be NP-complete, although we remind
the reader that we continue to measure complexity in terms of the size
of the domain and the number of generators of any particular group;
the number of generators is logarithmic in the number of instances of
any particular augmented clause.  It is also the case that the
practical complexity of solving these problems appears to be low-order
polynomial.

Our focus in the final paper in this series will be on the development
of efficient procedures that achieve the above goals, their
incorporation into a \zchaff-like prover, and an evaluation of the
performance of the resulting system.

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

Our aim in this paper has been to give a theoretical description of a
generalized representation scheme for satisfiability problems.  The
basic building block of the approach is an ``augmented clause,'' a
pair $(c,G)$ consisting of a ground clause $c$ and a group $G$ of
permutations on the literals in the theory; the intention is that the
augmented clause is equivalent to the conjunction of the results of
operating on $c$ with elements of $G$.  We argued that the structure
present in the requirement that $G$ be a group provides a
generalization of a wide range of existing notions, from
quantification over finite domains to parity clauses.

We went on to show that resolution could be extended to deal with
augmented clauses, and gave a generalization of relevance-bounded
learning in this setting (Procedures \ref{p.upg} and \ref{p.rblg}).
We also showed that the resulting proof system generalized first-order
techniques when applied to finite domains of quantification, and could
produce polynomially sized proofs of the \php, clique coloring
problems, Tseitin's graph coloring problems, and parity clauses in
general.

Finally, we described the specific group-theoretic problems that need
to be addressed in implementing our ideas.  As discussed in the
previous section, they are:
\begin{enumerate}
\item Implementing the group operation associated with the
generalization of resolution,
\item Finding unit instances of an augmented clause, and
\item Determining whether an augmented clause has relevant
instances.
\end{enumerate}
 We will return to these issues in the final paper in this series
\cite{Ginsberg:zap3}, which describes an implementation of our ideas
and its computational performance.

\section*{Acknowledgments}

We would like to thank the members of {\sc cirl}, the technical staff
of On Time Systems, Paul Beame of the University of Washington, and
David Hofer of the CIS department at the University of Oregon for
their assistance with the ideas in this series of papers.  We also
thank the anonymous reviewers for their comments, which improved the
exposition greatly.

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, the National Science Foundation ({\sc nsf})
under grant number CCR9820945, 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.

\appendix

\section{Proofs}

\begin{oldproposition}{\ref{p.uprx}}  Suppose that $C$ is a \bs\
problem, and $P$ is a sound annotated partial assignment.  Then:
\begin{enumerate}
\item If $\unit(P)=\langle\false,P'\rangle$, then $P'$ is a sound
extension of $P$, and
\item If $\unit(P) = \langle\true,c\rangle$, then $c$ is a nogood for $P$.
\end{enumerate}
\end{oldproposition}

\proof In the first case, we need to show that any extension of $P$ in
the procedure leaves $P$ a sound partial assignment.  In other words,
when we add $(l,c)$ to $P$, we must show that:
\begin{enumerate}
\item $C\models c$,
\item $l$ appears in $c$, and
\item Every other literal in $c$ is false by virtue of an assignment in $P$.
\end{enumerate}

For (1), note that $c\in C$.  For (2), $l$ is explicitly set to a
literal in $c$.  And for (3), since $c\in \poss_0(C,P)$, every other
literal in $c$ must be set false by $P$.

In the second case in the proposition, $C\models c$ because $c$ is the
result of resolving a clause in $C$ with some reason $c_i$, which is
entailed by $C$ by virtue of the soundness of $P$.  To see that $c$ is
falsified by $P$, note that the clause in $\poss_{-1}(C,P)$ is surely
falsified by $P$, and that every literal in the reason $c_i$ for $l_i$
is also falsified except for $l_i$ itself.  It follows that the result
of resolving these two clauses will also be falsified by the
assignments in $P$.\proofend

\begin{oldtheorem}{\ref{t.rbl}} \Rbl\ is sound and complete in that 
it will always return a solution to a satisfiable theory $C$ and
always report failure if $C$ is unsatisfiable.  \Rbl\ also uses an
amount of memory polynomial in the size of $C$ (although exponential
in the relevance bound $k$).\end{oldtheorem}

\proof Soundness is immediate.  For completeness, note that every
nogood learned eliminates an additional portion of the search space, 
and the backtrack is constrained to not go so far that the newly
learned nogood is itself removed as irrelevant.

For the last claim, we extend \defn{reason} somewhat, defining a {\em
reason} for a literal $l$ to be any learned clause involving $l$ where
$l$ was the most recently valued literal at the point that the clause
was learned.  We will now show that for any literal $l$, there are
never more than $(2n)^k$ reasons for $l$, where $n$ is the number of
variables in the problem.

To see this, let $R$ be the set of reasons for $l$ at some point.  Let
$r$ be any reason in this set; between the time that $r\in R$ was
learned and the current point, at most $k$ literals in $r$ could have
been unassigned by the then-current partial assignment.  It follows
that there is some fixed partial assignment $P'$ that holds throughout
the ``life'' of each $r\in R$ and such that each $r$ has at most $k$
literals unassigned values by $P'$.  Let $S$ be the set of literals
assigned values by $P'$.

Given a reason $r_i\in R$, we will view $r_i$ simply as the set of
literals that it contains, so that $r_i - S$ is the set of literals
appearing in $r_i$ but outside of the stable partial assignment $P'$.
Now if $r_j$ was learned before $r_i$, some literal $l_i\in r_i-S$
must not be in $r_j-S$; otherwise, $r_j$ together with the stable
partial assignment $P'$ would have precluded the set of variable
assignments that led to the conclusion $r_i$.  In other words, $r_i
-S$ is unique for each reason in the set $R$.

But we also know that $|r_i-S|\leq k$, so that each reason corresponds
to choosing at most $k$ literals from the complement of $S$.  If there
are $n$ variables in the problem, there are most $2n$ literals in this
set, so that the number of reasons is bounded by $(2n)^k$.  It follows
that the total number of reasons learned is bounded by $(2n)^{k+1}$,
and the conclusion follows.\proofend

\begin{theorem}[Lagrange] If $G$ is a finite group and $S\leq G$, then
$|S|$ divides $|G|$.\proofend\label{t.lagrange}\end{theorem}

\begin{oldproposition}{\ref{p.size}} Let $S$ be a set of ground clauses, and
$(c,G)$ an equivalent augmented clause, where $G$ is represented by
generators.  It is possible in polynomial time to find a set of
generators $\set{\omega_1,\dots,\omega_k}$ where $k\leq \log_2 |G|$
and $G=\langle \omega_1,\dots,\omega_k\rangle$.\end{oldproposition}

\proof Even the simplest approach suffices.  If $G=\langle
g_i\rangle$, checking to see if $g_i\in \langle
\omega_1,\dots,\omega_j\rangle$ for each generator $g_i$ can be
performed in polynomial time using a well-known method of Sims
\cite{Ginsberg:zap3,Luks:group,Seress}; if $g_i$ is already in the
generated set we do nothing and otherwise we add it as a new
generator.  By virtue of Lagrange's theorem, a subgroup can never be
larger than half the size of a group that properly contains it, so
adding a new generator to the set of $\omega_i$'s always at least
doubles the size of the generated set.  It follows that the number of
generators needed can never exceed $\log_2 |G|$.\proofend

\begin{oldproposition}{\ref{p.rewrite}} Let $(c,G)$ be an augmented
clause.  Then if $c'$ is any instance of $(c,G)$, $(c,G)\equiv
(c',G)$.\end{oldproposition}

\proof Since $c'$ is an instance of $(c,G)$, we must have $c'=c^g$ for
some $g\in G$.  Thus the instances of $(c',G)$ are clauses of the form
$c'^{g'} = c^{gg'}$.  But $c^{gg'} = c^{g''}$ for $g'' = gg'\in G$.
Similarly, an instance of $(c,G)$ is a clause of the form $c^{g'} =
c'^{g^{-1}g'} = c'^{g''}$.\proofend

\begin{definition}  Let $G\leq \Sym(S)$.  We will say that $G$ acts
{\em transitively\/} on $S$ if, for any $x,y\in S$, there is a $g\in
G$ with $x^g = y$.
\end{definition}

\begin{oldproposition}{\ref{p.rsize}}  Let $(c,G)$ be an augmented
clause with $d$ distinct instances.  Then there is a subgroup $H\leq
G$ that can be described using $O(\log_2(d))$ generators such that
$(c,H)\equiv (c,G)$.  Furthermore, given $d$ and generators for $G$,
there is a Monte Carlo polynomial-time algorithm for constructing the
generators of such an $H$.
\end{oldproposition}

\proof The basic ideas in the proof follow methods introduced by
Babai, Luks and Seress~\citeyear{Babai:perm}.  The proof of this
particular result is a bit more involved than the others in this
paper, and following it is likely to require an existing familiarity
with group theory.

Let $D$ be the set of instances of $(c,G)$, so that $G$ acts
transitively on $D$.  Now consider a sequence $g_1,g_2, \ldots $ of
uniformly distributed random elements of $G$ and, for each $r\ge 0$,
let $H_r = \langle g_1,g_2,\ldots, g_r\rangle$ (in particular, $H_0
=\langle \emptyset \rangle = {\bf 1}$).  Suppose that $H_{r-1}$ does
not act transitively on $D$ and let $K$ be any orbit of $H_{r-1}$ in
$D$.  Since $G_{\{K\}}$ is a proper subgroup of $G$, Lagrange's
theorem implies that the probability that $g_r\in G_{\{K\}}$ is $\le
\frac 12$.  Hence, the probability that $H_r$ enlarges this $K$ is
$\ge \frac 12$.  On average then, at least $\frac 12$ of the orbits
will be enlarged in passing from $H_{r-1}$ to $H_r$.  Since the orbits
partition the entire set $D$, an orbit can only be enlarged if it is
merged with one or more other orbits.  Thus the fact that at least
half of the orbits are enlarged implies that the total number of such
orbits is reduced by at least $\frac 14$.  Thus for each $r$, the
expected number of orbits of $H_r$ in $D$ is $\le d (3/4)^r$.  As a
consequence, with high probability, there exists $r=O(\log_2 d)$ such
that $H_r$ acts transitively on $D$.  (The probability of failure can
be kept below $\epsilon$ for any fixed $\epsilon >0$.)

An implementation of the algorithm implicit in this proof requires the
ability to select uniformly distributed random elements of $G$.  These
are available at a cost $O(v^2)$ per element, given the standard data
structures for permutation group computation
\cite{Seress}.\footnote{The reason that we only have a Monte Carlo
method is that there is no known deterministic polynomial time test
for testing whether $H\le G$ acts transitively on $D$; note that $D$
may be exponential in the number of variables in the problem.

Note also that the algorithm explicitly requires that we know $d$ in
advance.  This is necessary since the quantity is not known to be
computable in polynomial time.  However, there are methods for
computing $d$ that seem to be efficient in practice.}\proofend

\begin{oldproposition}{\ref{p.resolve-homo}} For ground clauses
$c_1$ and $c_2$ and a permutation $\omega \in W_n$,
\[\resolve(\omega(c_1),\omega(c_2)) = \omega(\resolve(c_1,c_2))\]
\end{oldproposition}

\proof Suppose that the literal being resolved on is $l$, so that if
we think of $c_1$ and $c_2$ as being represented simply by the
literals they contain, the resolvent corresponds to
\[c_1 \cup c_2 - \set{l,\neg l}\]
Permuting with $\omega$ gives us
\begin{equation}
\omega(c_1) \cup \omega(c_2) - \set{\omega(l),\omega(\neg l)} =
\omega(c_1) \cup \omega(c_2) - \set{\omega(l),\neg\omega(l)}
\label{e.resolve-ok}
\end{equation}
where the equality is a consequence of the fact that the permutation
in question is a member of $W_n$ instead of simply $S_{2n}$.  The
right hand side of \eq{resolve-ok} is simply
$\resolve(\omega(c_1),\omega(c_2))$.\proofend

\begin{oldproposition}{\ref{p.no-resolve}} There are augmented 
clauses $c_1$ and $c_2$ such that the set $S$ of resolvents of
instances of the two clauses does not correspond to any single
augmented clause $(c,G)$.
\end{oldproposition}

\proof Consider resolving the augmented clause
\[c_1 = (a\vee b,(bc))\]
with the two instances $a\vee b$ and $a\vee c$, with the augmented
clause
\[c_2 = (\neg a \vee d,(dc))\]
 corresponding to $\neg a \vee d$ and $\neg a \vee c$.  The ground
clauses that can be obtained by resolving instances of $c_1$ and of
$c_2$ are $b\vee d$, $b\vee c$, $c\vee b$, and $c$.  Since these
clauses are not of uniform length, they are not instances of a single
augmented clause.\proofend

\begin{oldproposition}{\ref{p.stable}} $\sext(K_i,G_i)\leq \Sym(L)$.
\end{oldproposition}

\proof Suppose we have $\omega_1,\omega_2 \in \sext(K_i,G_i)$.  Now
for some fixed $i$ and $g_1 \in G_i$, $\omega_1|_{K_i^{G_i}} =
g_1|_{K_i^{G_i}}$ and similarly for $\omega_2$ and some $g_2$.  But
now for any $x\in K_i^{G_i}$,
\begin{eqnarray*}
x^{\omega_1\omega_2} & = & x^{g_1\omega_2} \\
& = & x^{g_1  g_2} 
\end{eqnarray*}
 so that $\omega_1\omega_2\in \sext(K_i,G_i)$.  The first equality
holds by virtue of the definition of a stable extension, and the
second holds because $x^{g_1}$ is necessarily in the $G_i$-closure of
$K_i$.  Inversion is similar.\proofend

\begin{olddefinition}{\ref{d.satisfactory}} A definition of augmented
resolution will be called {\em satisfactory\/} if any resolvent
$(c,G)$ of $(c_1,G_1)$ and $(c_2,G_2)$ satisfies the following
conditions:
\begin{enumerate}
\item It is {\em sound}, in that $(c_1,G_1) \wedge (c_2,G_2)
\models (c,G)$.
\item It is {\em complete}, in that $\resolve(c_1,c_2)$ is an
instance of $(c,G)$.
\item It is {\em monotonic}, in that if $G_1\leq H_1$ and
$G_2\leq H_2$, then $(c,G)$ is also a resolvent of $(c_1,H_1)$ and
$(c_2,H_2)$.
\item It is {\em polynomial}, in that it is possible to confirm
that $(c,G)$ is a resolvent of $(c_1,G_1)$ and $(c_2,G_2)$
in polynomial time.
\item It is {\em stable}, in that if $c_1^G=c_2^G$, then
$(\resolve(c_1,c_2),G)$ is a resolvent of $(c_1,G)$ and $(c_2,G)$
\item It is {\em strong}, in that if no element of $c_1^{G_1}$ is
moved by $G_2$ and similarly no element of $c_2^{G_2}$ is moved by
$G_1$, then $(\resolve(c_1,c_2),\langle G_1,G_2\rangle)$ is a
resolvent of $(c_1,G_1)$ and $(c_2,G_2)$.
\end{enumerate}
\end{olddefinition}

\begin{oldproposition}{\ref{p.resolution}} \defn{resolution} of
(noncanonical) resolution is satisfactory.  The definition of
canonical resolution satisfies all of the conditions of
\defn{satisfactory} except for monotonicity.
\end{oldproposition}

\proof We deal with the conditions of the definition one at a time.

\paragraph{1. Soundness} Any instance of $(c,G)$ must be of the form
\[\omega(\resolve(c_1,c_2)))\]
for some $\omega$ that simultaneously extends $G_1$ acting on $c_1$
and $G_2$ acting on $c_2$.  But by \prop{resolve-homo}, this is just
\[\resolve(\omega(c_1),\omega(c_2))\]
The first of these clauses is an instance of $(c_1,G_1)$, and the
second is an instance of $(c_2,G_2)$, so the proposition follows from
the soundness of resolution.

\paragraph{2. Completeness}  $\resolve(c_1,c_2)$ is an instance of
$(c,G)$ because $c=\resolve(c_1,c_2)$ and $1\in G$.

\paragraph{3. Monotonicity} If $(c,G)$ is a resolvent of $(c_1,H_1)$
and $(c_2,H_2)$, then $G=\sext(c_i,K_i)$ where $K_i\leq H_i$.  But
since $H_i\leq G_i$, it follows that $K_i\leq G_i$ and $(c,G)$ is a
resolvent of $(c_1,G_1)$ and $(c_2,G_2)$ as well.

\paragraph{4. Polytime checking} We assume that we are provided with the
intermediate groups $H_1$ and $H_2$, so that we must simply check that
$G\leq \sext(c_i,H_i)$.  Since $\sext(c_i,H_i)$ is a group by virtue
of \prop{stable}, it suffices to check that each generator of $G$ is
in $\sext(c_i,H_i)$.  But this is straightforward.  Given a generator
$g$, we need simply check that restricting $g$ to $c_i^{G_i}$, the
image of $c_i$ under $G_i$, produces a permutation that is the
restriction of an element of $G_i$.  As we remarked in proving
\prop{size}, this test is known to be in P.

\paragraph{5. Stability} It is clear that $(\resolve(c_1,c_2),G)$ is
a resolvent of $(c_1,G)$ and $(c_2,G)$, since every element of $G$ 
is clearly a stable extension of $(c_1,G)$ and $(c_2,G)$.

We need the additional condition that $c_1^G=c_2^G$ to show that
$(\resolve(c_1,c_2),G)$ is the {\em canonical\/} resolvent; there is
no explicit requirement that the group of stable extensions of
$(c_1,G)$ and $(c_2,G)$ be a subgroup of $G$.  But if $c_1^G=c_2^G$,
the stable extensions must agree with elements of $G$ on
$c_1^G=c_2^G$, and hence must agree with elements of $G$ on $c_1$ and
$c_2$ themselves, and therefore on $\resolve(c_1,c_2)$ as well.  Thus
the canonical resolvent is equivalent to $(\resolve(c_1,c_2),G)$.

\paragraph{6. Strength} It is clear that the group of stable extensions
can never be bigger than $\langle G_1,G_2\rangle$, since every
permutation that either agrees with $c_1$ on $G_1$ and with $c_2$ on
$G_2$ is contained in this group.  But if $g=\prod g_i$ is an element
of $\langle G_1,G_2\rangle$, with $g_i\in G_1$ for $i$ odd and $g_i\in
G_2$ for $i$ even, then $c_1^g = c_1^{(\prod_{i \rm{\ odd}} g_i)} =
c_1^{g'}$ for $g' = \prod_{i \rm{\ odd}} g_i \in G_1$.  The
$(c_2,G_2)$ case is similar, so $(\resolve(c_1,c_2),\langle
G_1,G_2\rangle)$ is the canonical resolvent of $(c_1,G)$ and
$(c_2,G)$.  \proofend

\begin{oldproposition}{\ref{p.qprop}} Let $p$ and $q$ be quantified
clauses such that there is a term $t_p$ in $p$ and $\neg t_q$ in $q$
where $t_p$ and $t_q$ have common instances.  Suppose also that
$(p_g,P)$ is an augmented clause equivalent to $p$ and $(q_g,Q)$ is an
augmented clause equivalent to $q$, where $p_g$ and $q_g$ resolve.
Then if no terms in $p$ and $q$ except for $t_p$ and $t_q$ have common
instances , the result of resolving $p$ and $q$ in the conventional
lifted sense is equivalent to $\resolve((p_g,P),(q_g,Q))$.
\end{oldproposition}

\proof The proof is already contained in the discussion surrounding
the example in the main text.  The base instance of the augmented
resolvent is clearly an instance of the quantified resolution; for the
group, we have already remarked that the group of stable extensions of
the two embeddings corresponds simply to any bindings for the
variables in the resolvents that can be extended to a permutation of
all of the variables in question.  This means that the bindings must
be consistent with regard to the values selected for shared terms, and
no two distinct quantified literals are mapped to identical ground
atoms.  The latter condition follows from the assumption that the
non-resolving literals have no common ground instances.\proofend

\begin{oldproposition}{\ref{p.php}} There is an augmented resolution 
proof of polynomial size of the mutual unsatisfiability of \eq{pig1}
and \eq{pig2}.\end{oldproposition}

\proof We begin by explaining how the proof goes generally, and only
subsequently provide the details.  From the fact that the first pigeon
has to be in one of the $n$ holes, we can conclude that one of the
first two pigeons must be in one of the last $n-1$ holes (since these
first two pigeons can't both be in the first hole).  Now one of the
first three pigeons must be in one of the last $n-2$ holes, and so on
until we conclude that one of the first $n$ pigeons must be in the
last hole.  Similarly, one of the first $n$ pigeons must be in each
hole, leaving no hole for the final pigeon.

To formalize this, we will write $A_k$ for the fact that one of the
first $k$ pigeons must be in one of the last $n+1-k$ holes:
\[A_k \equiv \bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k\leq j \leq n}} p_{ij}\]
 Our basic strategy for the proof will be to show that if we denote
the original axioms \eq{pig1} and \eq{pig2} by $PHP$:\footnote{Our
notation here is vaguely similar to that used by Krishnamurthy
\citeyear{Krish:symmetry}, although the both problem being solved and
the techniques used are different.}
\begin{enumerate}
\item $PHP \vdash A_1$,
\item $PHP \wedge A_k \vdash A_{k+1}$,
\item $PHP \wedge A_n \vdash \bot$, where $\bot$ denotes a contradiction.
\end{enumerate}
 In addition, since the same group $G$ appears throughout the original
axiomatization, we will drop it from the derivation, but will feel
free to resolve against $c^g$ for any $g\in G$ and derived conclusion
$c$.

For the first claim, note that $A_1$ is given by
\[\bigvee_{1\leq j \leq n} p_{1j}\]
 which is an instance of \eq{pig2}.

For the second, we have $A_k$, which is
\[ \bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k\leq j \leq n}} p_{ij}\]
and we need to remove all of the variables $p_{jk}$ that refer to the
$k$th hole.  To do this, we resolve the above clause with each of
\[\begin{array}{rcl}
\neg p_{1k} & \vee & \neg p_{k+1,k} \\
\neg p_{2k} & \vee & \neg p_{k+1,k} \\
& \vdots & \\
\neg p_{kk} & \vee & \neg p_{k+1,k} 
 \end{array}\]
 to get
\[\neg p_{k+1,k} \vee \bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k+1\leq j \leq n}} p_{ij}\]

Now note that the only holes mentioned in the disjunction on the right
of the above expression are the $k+1$st and higher, so that we can
apply the group $G$ to conclude
\[\neg p_{k+1,m} \vee \bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k+1\leq j \leq n}} p_{ij}\]
 for any $1\leq m \leq k$.  Now if we resolve each of these with the
instance of \eq{pig2} given by
\[p_{k+1,1} \vee \cdots \vee p_{k+1,n}\]
 we get
\[\bigvee_{k+1\leq j \leq n} p_{k+1,j} \vee \bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k+1\leq j \leq n}} p_{ij}\]
 which is to say
\[\bigvee_{\stackrel{1\leq i \leq k+1}{\scriptscriptstyle k+1\leq j \leq n}} p_{ij}\]
 or $A_{k+1}$.

Finally, we need to derive a contradiction from $A_n$, which is to say
\[\bigvee_{1\leq i \leq n} p_{in}\]
 Resolving with each of 
\[\begin{array}{rcl}
\neg p_{1n} & \vee & \neg p_{n+1,n} \\
\neg p_{2n} & \vee & \neg p_{n+1,n} \\
& \vdots & \\
\neg p_{nn} & \vee & \neg p_{n+1,n} 
\end{array}\]
 now gives $\neg p_{n+1,n}$, and we can thus conclude $\neg p_{ij}$
for any $i$ and $j$ by acting with the group $G$.  Resolving into any
instance of \eq{pig2} now gives the desired contradiction.\proofend

\begin{lemma}
Assuming that we only branch on positive literals in unsatisfied
clauses, let $p_{jk}$ be any of the first $n-2$ branch decisions in
solving the \php.  The set of unit propagations that result from this
branch decision is exactly the set $S_k = \set{\neg p_{ik} | i \neq
j}$.
\label{l.up}
\end{lemma}

\proof We prove this by induction on the number of branch decisions.
For the base case, we take $n \geq 3$ and consider the first branch
decision $p_{jk}$.  For each $\neg{p}_{ik} \in S_k$ there is an
instance of \eq{pig2} of the form $\neg{p}_{jk} \vee \neg{p}_{ik}$
that causes the unit propagation $\neg{p}_{ik}$.  No other instances
of \eq{pig2} contain literals that refer to hole $k$, so \eq{pig2}
produces no further unit propagations.  Each instance of \eq{pig1} has
a total of $n$ literals with at most one literal that refers hole $k$.
Because $n \geq 3$, each instance must have at least two unvalued
literals and therefore does not generate a unit propagation.
 
For the inductive case, we assume that \lem{up} holds for the first
$m$ branches with $m < n-2$.  Under this assumption, each branch
decision $p_{jk}$ and its subsequent unit propagations value exactly
the variables involving hole $k$.  We can therefore make the same
argument as we did in the base case.  Let $p_{jk}$ be the $m+1^{st}$
branch decision.  Clause \eq{pig2} produces exactly the set $S_k =
\set{\neg{p}_{ik} | i \neq j}$ via \up, and because $m + 1 \leq n-2$,
each instance of \eq{pig1} has at least two unvalued literals and
therefore does not generate any unit propagations.

The key observation is that each branch decision and its subsequent
unit propagations value all the variables (and only the variables)
that refer to a particular hole.\proofend

\begin{lemma}
Let $P= \set{ l_1,l_2, \dots , l_m}$ be a partial assignment obtained
in solving the \php, where every branch decision is on a positive
literal in an unsatisfied clause.  For every branch decision $l_i$ in
$P$, the subproblem below the open branch
$\set{l_1,l_2,\dots,l_{i-1},\neg{l}_i}$ can be solved by unit
propagation.
\label{l.closebranch}
\end{lemma} 

\proof Assume we are about to begin exploring the subproblem below 
\[P = \set{ l_1,l_2, \dots , l_i, \neg{p}_{jk} }\]
 for some branch variable $p_{jk}$.  The subproblem below $P = \set{
l_1,l_2, \dots , l_i, p_{jk} }$ has already been explored, found to be
unsatisfiable, and we've generated a nogood defining the reason for
the failure.  This nogood will be an augmented clause of the form
\begin{equation}
(a_1 \vee \cdots \vee a_m \vee \neg{p}_{jk},G) \label{e.nogood}
\end{equation}
The $a_i$ are unsatisfied under $P = \set{ l_1,l_2,\dots,l_i }$, and
$G$ is the global symmetry group for the problem.

But now recall that by virtue of \lem{up}, each of our original branch
decisions together with its subsequent unit propagations valued all of
the variables that referred to one particular hole and no more.
Consider the set of all holes referred to by the partial assignment
$\set{l_1,l_2,\dots,l_i}$.  We will call this set $H$.

When we branched on $p_{jk}$, pigeon $j$ had not yet been assigned to
a hole.  This follows from our assumption that we branch only on
positive literals in unsatisfied clauses.  Thus for all $h \in H$,
$\neg{p}_{jh} \in P$; in other words, pigeon $j$ was excluded from all
of the holes in $H$ prior to our decision to place it in hole $k$.
The derived nogood \eq{nogood} asserts that pigeon $j$ cannot go in
hole $k$ either.

But as in the small example worked in the main text, the nogood
\eq{nogood} represents more than a single clause.  It represents the
set of clauses that can be generated by applying permutations in $G$
to $a_1 \vee \cdots \vee a_m \vee \neg{p}_{jk}$.  If we apply a
permutation that swaps hole $k$ with any hole $g \not \in H$, the
literals $a_1, \dots, a_m$ will be unchanged and will remain
unsatisfied under $P = \set{ l_1,l_2,\dots,l_i }$.  So the clause
\begin{equation}
a_1 \vee \cdots \vee a_m \vee \neg{p}_{jg}
\label{e.stillbad}
\end{equation}
is also an instance of \eq{nogood} for any $g \not \in H$, and
\eq{stillbad} is also unit under the partial assignment $P$.  The
nogood \eq{nogood} thus generates a series of unit propagations
indicating that pigeon $j$ cannot be in any hole not in $H$.  Since
the holes in $H$ are already known to be excluded, there is no hole
available for pigeon $j$.  A contradiction occurs and the subproblem
below $P = \set{ l_1,l_2, \dots , l_i, \neg{p}_{jk} }$ is
closed.\proofend

\begin{oldproposition}{\ref{p.php2}} Any implementation of \prc{rbl}
that branches on positive literals in unsatisfied clauses on
\lin{rblbranch} will produce a proof of polynomial size of the mutual
unsatisfiability of \eq{pig1} and \eq{pig2}, independent of specific
branching choices made.
\end{oldproposition}

\proof Note first that any \rbl\ search tree has size polynomial in
the number of branch decisions, since the number of variable
assignments that can result from \up\ is bounded by the number of
variables.  To show that the search tree has size polynomial in the
number of pigeons $n$, it thus suffices to show that the number of
branch decisions is polynomial in $n$.  We will show that under the
given branch heuristic, the number of branch decisions is $n-1$
specifically.

To do this, we first descend into the tree through branching and
propagation until a contradiction is reached, and describe the partial
assignment that is created and show how a contradiction is drawn.  We
then show the backtracking process, proving that the empty clause can
be derived in a single backtrack.  More specifically, we show that
every open branch of the search tree can be closed through propagation
alone.  No further branch decisions are needed.

\lem{up} deals with the first $n-2$ branch decisions.  What about the
$n-1^{st}$ decision?  If this branch decision is $p_{jk}$, we again
generate the set of unit propagations $S_k = \set{\neg{p}_{ik} | i
\neq j}$.  This time we will generate some additional unit
propagations.  Since we have assigned $n-1$ of the pigeons each to a
unique hole, there is only one empty hole remaining.  If this is hole
$h$, the two remaining pigeons (say pigeons $a$ and $b$) are both
forced into hole $h$, while only one can occupy it.  This leads to the
expected contradiction.  But now \lem{closebranch} shows that no
further branches are necessary, so that the total number of branches
is $n-1$, and the \rbl\ search tree is polynomially sized.\proofend

\begin{oldproposition}{\ref{p.clique}} There is an augmented resolution 
proof of polynomial size of the unsatisfiability of
\eq{okcolor}--\eq{okmap}.\end{oldproposition}

\proof The proof proceeds similarly to the proof of \prop{php},
although the details are far more intricate.  As before, we will work
with ground axioms only and will suppress the augmentation by the
global symmetry group.

The analog to $p_{ij}$ is that the $i$th node of the clique gets the
$j$th color, or
\[(q_{i1}\wedge c_{1j}) \vee \cdots \vee (q_{im}\wedge c_{mj})\]
which we will manipulate in this form although it's clearly not {\sc
cnf}.

Now $A_1$, the statement that the first pigeon is in some hole, or
that the first node of the clique gets some color, is
\[[q_{11}\wedge(c_{11}\vee\cdots\vee c_{1n})] \vee \cdots 
\vee [q_{1m}\wedge(c_{m1}\vee\cdots\vee c_{mn})]\]

The expression for $A_k$, which was 
\begin{equation}
\bigvee_{\stackrel{1\leq i \leq k}{\scriptscriptstyle k\leq j \leq n}} p_{ij}
\label{e.biga}
\end{equation}
similarly becomes
\begin{equation}
[(q_{11}\vee\cdots\vee q_{k1})\wedge(c_{1k}\vee\cdots\vee c_{1n})] \vee \cdots 
\vee [(q_{1m}\vee\cdots\vee q_{km})\wedge(c_{mk}\vee\cdots\vee
c_{mn})]
\label{e.biga2}
\end{equation} saying that for some $i$ and $j$ as in \eq{biga},
there is an index $h$ such that $q_{ih}\wedge c_{hj}$; $h$ is the
index of the graph node to which a clique element of a suitable color
gets mapped.

In order to work with the expressions \eq{biga2}, we do need to
convert them into {\sc cnf}.  Distributing the $\wedge$ and $\vee$ in
\eq{biga2} will produce a list of conjuncts, each of the form
\begin{equation}
B_1\vee\cdots \vee B_m
\label{e.bigb}
\end{equation}
where each $B_i$ is of the form either $q_{1i}\vee\cdots\vee q_{ki}$
or $c_{ik}\vee\cdots\vee c_{in}$.  There are $2^m$ possible expressions
of the form \eq{bigb}.

Each of these $2^m$ expressions, however, is an instance of the result
of acting with the global group $G$ on one of the following:
\begin{equation}
\begin{array}{ccccccc}
(c_{1k}\vee\cdots\vee c_{1n}) & \vee & (c_{2k}\vee\cdots\vee c_{2n}) & \vee & \cdots & \vee & (c_{mk}\vee\cdots\vee c_{mn}) \\
(q_{11}\vee\cdots\vee q_{k1}) & \vee & (c_{2k}\vee\cdots\vee c_{2n}) & \vee & \cdots & \vee & (c_{mk}\vee\cdots\vee c_{mn}) \\
&&&&\vdots && \\
(q_{11}\vee\cdots\vee q_{k1}) & \vee & (q_{12}\vee\cdots\vee q_{k2}) & \vee & \cdots & \vee & (q_{1m}\vee\cdots\vee q_{km}) 
\end{array}
\label{e.biga3}
\end{equation}
We will view these as all instances of a general construct indexed by
$h$, with $h$ giving the number of initial clauses based on the $q$'s
instead of the $c$'s.  So the first row corresponds to $h=0$, the
second to $h=1$ and so on, with the last row corresponding to $h=m$.
It follows from this that $A_k$ is effectively
\begin{equation}
\bigwedge_{0\leq h\leq m} \left(\bigvee_{\stackrel{1\leq i\leq k}{\scriptscriptstyle 1\leq j\leq h}} q_{ij} \vee \bigvee_{\stackrel{h+1\leq i\leq m}{\scriptscriptstyle k\leq j\leq n}} c_{ij}\right)
\label{e.biga5}
\end{equation}

It is important to realize that we haven't actually started to prove
anything yet; we're just setting up the machinery needed to duplicate
the proof of \prop{php}.  The only remaining piece is the analog in
this framework of the axiom $\neg p_{ij} \vee \neg p_{kj}$, saying
that each hole can only contain one pigeon.  That is
\begin{equation}
\neg q_{ih} \vee \neg c_{hj} \vee \neg q_{kg} \vee \neg c_{gj}
\label{e.clique2}
\end{equation}
saying that if node $i$ of the clique is mapped to node $h$ of the
graph, and $k$ is mapped to $g$, then $g$ and $h$ cannot both get the
same color.

If $g\neq h$, we can derive \eq{clique2} by resolving \eq{okcolor} and
\eq{okmap}.  If $g=h$, then \eq{clique2} becomes $\neg q_{ih} \vee
\neg c_{hj} \vee \neg q_{kh}$ and is clearly a weakening of \eq{map}.
Thus $\neg p_{ij} \vee \neg p_{kj}$ becomes the pair of clauses
\begin{eqnarray*}
& \neg q_{ih} \vee \neg c_{hj} \vee \neg q_{kg} \vee \neg c_{gj} & \\
& \neg q_{ih} \vee \neg q_{kh}
\end{eqnarray*}
 both of which can be derived in polynomial time and are, as usual,
acted on by the group $G$.  We are finally ready to proceed with the
main proof.

For the base step, we must derive $A_1$, or the conjunction of
\[\bigvee_{\stackrel{1\leq i\leq 1}{\scriptscriptstyle 1\leq j\leq h}} q_{ij} \vee \bigvee_{\stackrel{h+1\leq i\leq m}{\scriptscriptstyle 1\leq j\leq n}} c_{ij}\]
which is to say
\[\begin{array}{ccccccc}
(c_{11}\vee\cdots\vee c_{1n}) & \vee & (c_{21}\vee\cdots\vee c_{2n}) & \vee & \cdots & \vee & (c_{m1}\vee\cdots\vee c_{mn}) \\
q_{11} & \vee & (c_{21}\vee\cdots\vee c_{2n}) & \vee & \cdots & \vee & (c_{m1}\vee\cdots\vee c_{mn}) \\
&&&&\vdots && \\
q_{11} & \vee & q_{12} & \vee & \cdots & \vee & q_{1m} 
\end{array}\]
 Except for the last row, each of these is obviously a weakening of
\eq{color} saying that every node in the graph gets a color.  The
final row is equivalent to \eq{clique} saying that each element of the
clique gets a node in the graph.

For the inductive step, we must show that $A_k\vdash A_{k+1}$.  Some
simplifying notation will help, so we introduce
\[C_{ij..k} \equiv (c_{ij} \vee \cdots\vee c_{ik})\]
and
\[Q_{i..jk} \equiv (q_{ik} \vee\cdots\vee q_{jk})\]

Now $A_k$ as in \eq{biga3} is actually
\begin{equation}
\begin{array}{ccccccc}
C_{1k..n} & \vee & C_{2k..n} & \vee & \cdots & \vee & C_{mk..n} \\
Q_{1..k1} & \vee & C_{2k..n} & \vee & \cdots & \vee & C_{mk..n} \\
&&&&\vdots && \\
Q_{1..k1} & \vee & Q_{1..k2} & \vee & \cdots & \vee & Q_{1..km} 
\end{array}
\label{e.biga4}
\end{equation}
 Following the pigeonhole proof, we need to reduce the number of holes
(i.e., colors) by one and increase the number of pigeons (i.e., clique
elements) by one.  For the first step, we need to resolve away the
appearances of $c_{ik}$ from \eq{biga4}.  We claim that from \eq{biga4}
it is possible to derive
\begin{equation}
\begin{array}{ccccccccccc}
C_{1,k+1..n} & \vee & C_{2,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m} & \vee & \neg c_{mk} \\
Q_{1..k1} & \vee & C_{2,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m} & \vee & \neg c_{mk}\\
&&&&\vdots &&& \\
Q_{1..k1} & \vee & Q_{1..k2} & \vee & \cdots & \vee & Q_{1..km} & \vee & \neg q_{k+1,m} & \vee & \neg c_{mk}
\end{array}
\label{e.biga6}
\end{equation}
 We show this by working from the bottom of the arrays ($h=m$ in the
description \eq{biga5}) to the top ($h=0)$.  For the last row, the
expression in \eq{biga6} is clearly a weakening of the final row in
\eq{biga4}.

Suppose that we have done $h=i$ and are now considering $h=i-1$
corresponding to the derivation of the disjunction
\[Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{i,k+1..n}\vee\cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee \neg c_{mk}\]
from
\begin{equation}
Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{ik..n}\vee\cdots \vee C_{mk..n}
\label{e.biga7}
\end{equation}

Now recall that $C_{jk..n}$ is
\[c_{jk} \vee \cdots \vee c_{jn}\]
and we want to remove the $c_{jk}$ term by resolving with
\eq{clique2}, adding literals of the form $\neg q_{k+1,m}\vee \neg
c_{mk}$.  The instance of \eq{clique2} that we use is
\[\neg q_{k+1,m} \vee \neg c_{mk} \vee \neg q_{lj} \vee \neg c_{jk}\]
and the resolvent is
\[C_{j,k+1..n} \vee \neg q_{k+1,m} \vee \neg c_{mk} \vee \neg q_{lj}\]
The result of resolving into \eq{biga7} is therefore
{\small\begin{equation}
Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{ik..n}\vee \cdots \vee C_{j-1,k..n}\vee C_{j,k+1..n} \vee C_{j+1,k..n} \vee \cdots\vee C_{mk..n} \vee \neg q_{k+1,m} \vee \neg c_{mk} \vee \neg q_{lj}
\label{e.biga8}
\end{equation}}
for any $l$ and $i\leq j \leq m$.

Now we have already done $h=i$, which means that we have derived
\[Q_{1..k1}\vee\cdots\vee Q_{1..ki} \vee C_{i+1,k+1..n}\vee \cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee \neg c_{mk}\]
Operating on this with the usual group allows us to exchange the $q$
and $c$ variables arbitrarily, so it matters not that the first $i$
terms involve the $q$ variables and the last $m-i$ involve the $c$
variables, but only that the {\em number\/} of terms involving $q$ and
$c$ variables are $i$ and $m-i$ respectively.  Thus we have also
derived
{\small \begin{equation}
Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{i,k+1..n}\vee \cdots \vee C_{j-1,k+1..n}\vee Q_{1..kj} \vee C_{j+1,k+1..n} \vee \cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee \neg c_{mk}
\label{e.biga8b}
\end{equation}}
(where we have essentially swapped node $i$ and node $j$ in
\eq{biga8}).  By taking $l=1,\dots,k$ in \eq{biga8}, we can resolve
\eq{biga8b} with \eq{biga8} to eliminate both the trailing $\neg
q_{lj}$ in \eq{biga8} and the $Q_{1..kj}$ term above.  Since the
literals in $C_{h,k+1..n}$ are a subset of those in $C_{hk..n}$, we
get
\[Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{ik..n}\vee \cdots \vee C_{j-1,k..n}\vee C_{j,k+1..n} \vee C_{j+1,k..n} \vee \cdots\vee C_{mk..n} \vee \neg q_{k+1,m} \vee \neg c_{mk}\]
 We can continue in this fashion, gradually raising the second index of each 
$C$ term from $k$ to $k+1$, to finally obtain
\begin{equation}
Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee C_{i,k+1..n}\vee \cdots\vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee \neg c_{mk}
\label{e.biga9}
\end{equation}
as in \eq{biga6}.

The hard part is now done; we have exploited the symmetry over the
nodes and it remains to use the symmetry over the colors.  In the
derivation of \eq{biga9}, the color $k$ in the final $\neg c_{mk}$ is
obviously irrelevant provided that it is chosen from the set
$1,\dots,k$; higher numbered colors (but only higher numbered colors)
already appear in the $C_{j,k+1..n}$.  So we have actually derived
\[\begin{array}{ccccccccccccccc}
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m} & \vee & \neg c_{mk} \\
&&&&&&&&&&&&&& \vdots \\
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m} & \vee & \neg c_{m2} \\
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m} & \vee & \neg c_{m1}
  \end{array}\]
 and when we resolve all of these with the domain axiom \eq{color}
\[c_{m1}\vee c_{m2} \vee \cdots \vee c_{mn}\]
 we get
\[Q_{1..k1} \vee \cdots \vee Q_{1..k,i-1} \vee C_{i,k+1..n} \vee \cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee c_{m,k+1} \vee \cdots \vee c_{mn}\]
 which is to say
\[Q_{1..k1} \vee \cdots \vee Q_{1..k,i-1} \vee C_{i,k+1..n} \vee \cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m} \vee C_{m,k+1..n}\]
 or
\[Q_{1..k1} \vee \cdots \vee Q_{1..k,i-1} \vee C_{i,k+1..n} \vee \cdots \vee C_{m,k+1..n} \vee \neg q_{k+1,m}\]

Now the $m$ subscript in the final $q$ variable is also of no import, 
provided that it remains at least $i$.  We can therefore resolve
\[\begin{array}{ccccccccccccc}
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,i} \\
&&&&&&&&&&&& \vdots \\
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m-1} \\
Q_{1..k1} & \vee & \cdots & \vee & Q_{1..k,i-1} & \vee & C_{i,k+1..n} & \vee & \cdots & \vee & C_{m,k+1..n} & \vee & \neg q_{k+1,m}
  \end{array}\]
 with the domain axiom \eq{clique}
\[q_{k+1,1}\vee\cdots\vee q_{k+1,m}\]
 to get
\[Q_{1..k1} \vee \cdots \vee Q_{1..k,i-1} \vee C_{i,k+1..n} \vee \cdots \vee C_{m,k+1..n} \vee q_{k+1,1} \vee \cdots \vee q_{k+1,i-1}\]
 which is to say
\[Q_{1..k+1,1} \vee \cdots \vee Q_{1..k+1,i-1} \vee C_{i,k+1..n} \vee \cdots \vee C_{m,k+1..n}\]
 This is $A_{k+1}$ as desired.

It remains to show that we can derive a contradiction from $A_n$.  If
we continue with the above procedure in an attempt to ``derive''
$A_{n+1}$, when we derive an instance of \eq{biga9}, the $C$ terms
will simply vanish because $k+1>n$.  We end up concluding
\[Q_{1..k1}\vee\cdots\vee Q_{1..k,i-1} \vee \neg q_{k+1,m} \vee \neg c_{mk}\]
and the $i=0$ instance is simply
\[ \neg q_{k+1,m} \vee \neg c_{mk}\]

All of the indices here are subject to the usual
symmetry, so we know
\[\begin{array}{ccc}
\neg q_{ji}& \vee & \neg c_{i1} \\
\neg q_{ji}& \vee & \neg c_{i2} \\
&\vdots\\
\neg q_{ji}& \vee & \neg c_{in}
\end{array}\]
 which we resolve with $c_{i1}\vee \cdots \vee c_{in}$ to get $\neg
q_{ji}$.  We can resolve instances of this with $q_{m1}\vee\cdots \vee
q_{mn}$ to finally get the desired contradiction.\proofend

\begin{oldlemma}{\ref{l.mod2-easy}} Let $C$ be a theory consisting 
entirely of parity clauses.  Then determining whether or not $C$
is satisfiable is in $P$.\end{oldlemma}

\proof The proof is essentially a Gaussian reduction argument, and
proceeds by induction on $n$, the number of variables in $C$.  If
$n=0$, the result is immediate.  So suppose that $C$ contains $n+1$
variables, and let one clause containing $x_1$ be
\[x_1 + \sum_{x\in S} x \equiv k\]
where $k=0$ or $k=1$.  This is obviously equivalent to
\[x_1 \equiv  \sum_{x\in S} x + k\]
which we can now use to eliminate $x_1$ from every other axiom in $C$
in which it appears.  Since the resulting theory can be tested for
satisfiability in polynomial time, the result follows.\proofend

\begin{lemma} Suppose that we have two axioms given by
\begin{equation}
x_1 +  \sum_{x\in S} x +  \sum_{x\in T_1} x \equiv k_1
\label{e.mod2-a}
\end{equation}
and 
\begin{equation}
x_1 +  \sum_{x\in S} x +  \sum_{x\in T_2} x \equiv k_2
\label{e.mod2-b}
\end{equation}
where the sets $S$, $T_1$ and $T_2$ are all disjoint.  Then it
follows that
\begin{equation}
 \sum_{x\in T_1} x +  \sum_{x\in T_2} x \equiv k_1 + k_2
\label{e.mod2-c}
\end{equation}
and furthermore, any proof system that can derive this in polynomial
time can also determine the satisfiability of sets of parity
clauses in polynomial time.\label{l.mod2}\end{lemma}

\proof Adding \eq{mod2-a} and \eq{mod2-b} produces \eq{mod2-c}.  That
this is sufficient to solve sets of parity clauses in polynomial
time is shown in the proof of \lem{mod2-easy}.\proofend

\begin{oldlemma}{\ref{l.flip-ok}} $F_S \leq W_n$.\end{oldlemma}

\proof $F_S$ is closed under inversion, since every element in $F_S$
is its own inverse.  To see that it is closed under composition as
well, suppose that $f_1$ flips the variables in a set $S_1$ and $f_2$
flips the variables in a set $S_2$.  Then $f_1 f_2$ flips the
variables in $S_{12} = S_1 \cup S_2 - (S_1 \cap S_2)$.  But now
\begin{eqnarray*}
|S_{12}| & = & |S_1 \cup S_2 - (S_1 \cap S_2)| \\
& = & |S_1 \cup S_2| - |S_1 \cap S_2| \\
& = & |S_1| + |S_2| - |S_1 \cap S_2| - |S_1 \cap S_2| \\
& = & |S_1| + |S_2| - 2 \cdot |S_1 \cap S_2|
\end{eqnarray*}
and is therefore even, so $f_1 f_2\in F_S$.\proofend

\begin{oldlemma}{\ref{l.mod2-rep}} Let $S =\set{x_1,\dots,x_k}$ be a 
subset of a set of $n$ variables.  Then the parity clause
\begin{equation}
\sum_{i=1}^k x_i \equiv 1
\label{e.mod2-rep-a}
\end{equation}
is equivalent to the augmented clause
\begin{equation}
(x_1 \vee \cdots \vee x_k,F_S)
\label{e.mod2-rep-b}
\end{equation}
The parity clause
\[\sum_{i=1}^k x_i \equiv 0\]
is equivalent to the augmented clause
\[(\neg x_1 \vee x_2 \vee \cdots \vee x_k,F_S)\]
\end{oldlemma}

\proof To see that \eq{mod2-rep-a} implies \eq{mod2-rep-b}, note that
\eq{mod2-rep-a} certainly implies $x_1 \vee \cdots \vee x_k$.  But the
result of operating on the disjunction with any element of $F_S$ flips
an even number of elements in it, so \eq{mod2-rep-b} follows.

For the converse, suppose that \eq{mod2-rep-a} fails, so that an even
number of the $x_i$'s are true.  The disjunction that flips exactly
those $x_i$'s that are true will obviously have no satisfied literals,
but will have flipped an even number of elements of $S$ so that some
instance of the augmented clause \eq{mod2-rep-b} is unsatisfied.

The second equivalence clearly follows from the first; replace $x_1$
with $\neg x_1$.\proofend

\begin{oldproposition}{\ref{p.mod2}} Let $C$ be a theory consisting 
entirely of parity clauses.  Then determining whether or not $C$
is satisfiable is in $P$ for augmented resolution.
\end{oldproposition}

\proof We need to show that the conditions of \lem{mod2} are met.  We
can assume without loss of generality that $k_1=1$ and $k_2=0$ in the
conditions of the lemma; other cases involve simply flipping the sign
of one of the variables involved.

In light of \lem{mod2-rep}, we have the two augmented axioms
\[(x_1 \vee \bigvee_{x\in S} x \vee \bigvee_{x\in T_1} x,F_{x_1\cup S\cup T_1})\]
and
\[(\neg x_1 \vee \bigvee_{x\in S} x \vee \bigvee_{x\in T_2} x,F_{x_1\cup S\cup T_2})\]
 where $S$, $T_1$, and $T_2$ are all disjoint.  The clause obtained in
the resolution is clearly
\[ \bigvee_{x\in S\cup T_1 \cup T_2} x\]
 but what is the group involved?

The elements of the group are the stable extensions of group elements
from $F_{x_1\cup S\cup T_1}$ and $F_{x_1\cup S\cup T_2}$; in other
words, any permutation that leaves the variables unchanged and
simultaneously flips an even number of elements of $x_1\cup S\cup T_1$
and of $x_1\cup S\cup T_2$.  We claim that these are exactly those
elements that flip any subset of $S$ and an even number of elements of
$T_1 \cup T_2$.

We first show that any stable extension $g$ flips an even number of
elements of $T_1 \cup T_2$ (along with some arbitrary subset of $S$).
If $g$ flips an odd number of elements of $T_1 \cup T_2$, then it must
flip an odd number of elements of one (say $T_1$) and an even number
of elements of the other.  Now if the parity of the number of flipped
elements of $x_1\cup S$ is even, the total number flipped in $x_1\cup
S\cup T_1$ will be odd, so that $g$ does not match an element of
$F_{x_1\cup S\cup T_1}$ and is therefore not an extension.  If the
parity of the number of flipped elements of $x_1\cup S$ is odd, the
number flipped in $x_1\cup S\cup T_2$ will be odd.

To see that any $g$ flipping an even number of elements of $T_1\cup
T_2$ corresponds to a stable extension, we note simply that by
flipping $x_1$ or not, we can ensure that $g$ flips an even number of
elements in each relevant subset.  Since $g$ flips an even number of
elements in $T_1\cup T_2$, it flips subsets of $T_1$ and of $T_2$ that
have the same parity.  So if it flips an even number of elements of
$S\cup T_1$, it also flips an even number of elements of $S\cup T_2$
and we leave $x_1$ unflipped.  If $g$ flips an odd number of elements
of $S\cup T_1$ and of $S\cup T_2$, we flip $x_1$.  Either way, there
are corresponding elements of $F_{x_1\cup S\cup T_1}$ and $F_{x_1\cup
S\cup T_2}$.

Now suppose that we denote by $K_S$ the group that flips an arbitrary
subset of $S$.  We have shown that the result of the resolution is
\begin{equation}
\left(\bigvee_{x\in S\cup T_1 \cup T_2} x,K_S \times F_{T_1\cup T_2}\right)
\label{e.mod2a}
\end{equation}
 Note that the resolution step itself is polytime, since we have given
the result explicitly in~\eq{mod2a}.\footnote{In general, augmented
resolution is not known to be polynomial in the number of generators
of the groups in question.  But it is polynomial for groups of
restricted form being considered here.}

Next, we claim that \eq{mod2a} implies
\begin{equation}
\left(\bigvee_{x\in T_1 \cup T_2} x,K_S \times F_{T_1\cup T_2}\right)
\label{e.mod2b}
\end{equation}
 where we have removed the elements of $S$ from the disjunction.

We prove this by induction on the size of $S$.  If $S=\emptyset$,
the result is immediate.  Otherwise, if $a\in S$ for some specific
$a$, two instances of \eq{mod2a} are
\[\left(a \vee \bigvee_{x\in S-\set a\cup T_1 \cup T_2} x,K_S \times F_{T_1\cup T_2}\right)\]
and
\[\left(\neg a \vee \bigvee_{x\in S-\set a\cup T_1 \cup T_2} x,K_S \times F_{T_1\cup T_2}\right)\]
  which we can resolve using the stability property (\ref{stable}) of
\defn{satisfactory} to conclude
\[\left(\bigvee_{x\in S-\set a\cup T_1 \cup T_2} x,K_S \times F_{T_1\cup T_2}\right)\]
so that \eq{mod2b} now follows by the inductive hypothesis.

At this point, however, note that the variables in $S$ do not appear
in the clause in \eq{mod2b}, so that we can drop $K_S$ from the group
in the conclusion without affecting it in any way.  Thus we have
concluded
\begin{equation}
\left(\bigvee_{x\in T_1 \cup T_2} x,F_{T_1\cup T_2}\right)
\label{e.mod2c}
\end{equation}

Applying \lem{mod2-rep} once again, we see that \eq{mod2c} is
equivalent to
\[\sum_{x\in T_1} x +  \sum_{x\in T_2} x \equiv 1\]
as needed by \lem{mod2}.  The proof is complete.\proofend

\bibliography{bib}
\bibliographystyle{theapa}

\end{document}
