Understanding the Power of Clause Learning

1 Introduction

In recent years the task of deciding whether a CNF propo­ sitional logic formula is satisfiable has gone from a problem of theoretical interest to a practical approach for solvmg real­ world problems. SAT procedures are now a standard tool for hardware verification, including verification of super-scalar processors [Velev and Bryant, 2001; Biere eta/., 1999]. O~en problems in group theory have been encoded and so!ve~ usmg satisfiability [Zhang and Hsiang, 1994]. Other applicatiOns of SAT include circuit diagnosis and experiment design [Konuk and Larrabee, 1993; Gomes et al., 1998b].

The most surprising aspect of such relatively recent practi­ cal progress is that the best complete satisfiability testi?g al­ gorithms remain variants of the DPLL procedure [Davi.s and Putnam, 1960; Davis et al., 1962] for backtrack search m the space of partial truth assignments. The main improvements to DPLL have been better branch selection heuristics (e.g., [Li and Anbulagan, 1997]), and extensions such as random­ ized restarts [Gomes et al., 1998a] and clause learning. One can argue that clause learning has been the most significant of these in scaling DPLL to realistic problems.

Clause learning grew out of work in AI on explanation­ based learning (EBL), which sought to improve the performance of backtrack search algorithms by generating expla­ nations for failure (backtrack) points, and then adding the explanations as new constraints on the original problem [de Kleer and Williams, 1987; Stallman and Sussman, 1977; Genesereth, 1984; Davis, 1984]. For general constraint sat­ isfaction problems the explanations are called "conflicts" or "no goods"; in the case of Boolean CNF satisfiability, the technique becomes clause learning. A series of . re­ searchers [Bayardo Jr. and Schrag, 1997; Marques-Silva and Sakallah, 1996; Zhang, 1997; Moskewicz eta!., 2001; Zhang et al., 2001] showed that clause learning can be ef­ ficiently implemented and used to solve hard problems that cannot be approached by any other technique.

· Research supported by NSF Grant ITR-0219468

Despite its importance there has been little work on for~al properties of clause learning, with the goal of understanding its fundamental strengths and limitations. A likely reason for such inattention is that clause learning is a rather complex rule of inference - in fact, as we describe below, a complex family of rules of inference. A contribution of this ~aper is that we provide a precise specification of clause learmng.

Another problem in characterizing clause learning is defin­ ing a formal notion of the strength or power of a reason­ ing method. This paper uses the no.tion of proof complex­ ity [Cook and Reckhow, 1977], which compares mference systems in terms of the sizes of the shortest proofs they sanc­ tion. A family of formulas C provides an exponential sep­ aration between systems sl and s2 if the shortest proofs of formulas inc in system sl are exponentially smaller than the corresponding shortest proofs in S2. From this basic proposi­ tional proof complexity point of view, only families of unsat­ isfiable formulas are of interest, because only proofs ofunsat­ isfiability can be large; minimum proofs of satisfiability are linear in the number of variables of the formula. Neverthe­ less, Achlioptas et al [2001] have shown how negative proof complexity results for unsatisfiable formulas can be us.ed to derive time lower bounds for specific inference algonthms running on satisfiable formulas as well.

Proof complexity does not capture everything we int~­ itively mean by the power of a reasoning system, because 11 says nothing about how difficult it is to find shortest proofs. However, it is a good notion with which to begin our anal­ ysis, because the size of proofs provides a lower-bound on the running time of any implementation of the system. In the systems we consider, a branching function, which determines which variable to split upon or which pair of clauses to re­ solve, guides the search. A negative proof complexity result for a system tells us that a family of formulas is intractable even with a perfect branching function; likewise, a positive result gives us hope of finding a branching function.

A basic result in proof complexity is that general resolution is exponentially stronger than the DPLL procedure [Bonet et a!., 2000; Ben-Sasson et al., 2000]. This is because the trace of DPLL running on an unsatisfiable formula can be con­ verted to a tree-like resolution proof of the same size, and tree-like proofs must sometimes be exponentially larger than the DAG-like proofs generated by general resolution. Al­ though resolution can yield shorter proofs, in practice DPLL is better because it provides a more efficient way to search for proofs. The weakness of the tree-resolution proofs that DPLL finds is that they do not reuse derived clauses. The conflict clauses found when DPLL is augmented by clause learning correspond to reuse of derived clauses in the associated res­ olution proofs and thus to more general forms of resolution proofs. An intuition behind the results in this paper is that the addition of clause learning moves DPLL closer to general resolution while retaining its practical efficiency.

It has been previously observed that clause learning can be viewed as adding resolvents to a tree-like proof [Marques­ Silva, 1998]. However, this paper provides the first mathe­ matical proof that clause learning is exponentially stronger than tree-like resolution. Further, we provide a family of for­ mulas that exponentially separates clause learning from reg­ ular resolution, a system that is known to be intermediate in strength between general and tree resolution. The proof uses a new clause learning scheme called FirstNewCut that we in­ troduce. We also show that combining clause learning with restarts is as strong as general resolution.

Although this paper focuses on basic proof complexity, we briefly indicate how the understanding we gain through this kind of analysis may lead to practical applications. For exam­ ple, our proofs describe an improvement to the clause learn­ ing rules previously suggested in the literature, and suggest an approach to leveraging the structure of a problem encoded as a CNF formula in order to create a branching heuristic that takes the greatest advantage of clause learning. As an ex­ ample, we apply these ideas to certain natural satisfiable and unsatisfiable formulas where we obtain significant speed-ups over existing methods.

2 Preliminaries

A CNF formula F is an AND (A) of clauses, where each clause is an OR (V) of literals, and a literal is a variable or its negation ( ·). It is natural to think ofF as a set of clauses and each clause as a set of literals. A clause that is a subset of another is called its subclause.

Let p be a partial assignment to the variables of F. The restricted formula Flp is obtained from F by replacing vari­ ables in p with their assigned values. F is said to be simplified if all clauses with at least one TRUE literal are deleted, all oc­ currences of FALSE literals are removed from clauses, and the resulting formula, if different, is simplified recursively.

2.1 The DPLL Procedure

The basic idea of the Davis-Putnam-Logemann-Loveland (DPLL) procedure [Davis and Putnam, 1960; Davis et a!., 1962] for testing satisfiability of CNF formulas is to branch on variables, setting them to TRUE or FALSE, until either an initial clause is violated (i.e. has all literals set to FALSE) or all variables have been set. In the former case, we backtrack to the last branching decision whose other branch has not been tried yet, reverse the decision, and proceed recursively. In the latter, we terminate with a satisfying assignment. If all pos­ sible branches have been unsuccessfully tried, the formul a is declared unsatisfiable. To increase efficiency, pure liter­ als (those whose negation does not appear) and unit clauses (those with only one unset literal) are immediately set to true.

Definition 1. A branching sequence for a CNF formula F is a sequence a = (11 , 12 , .. . , lk) ofliterals ofF, possibly with repetitions. DPLL on F branches according to a if it always picks the next variable v to branch on in the literal order given by a, skips it ifv is currently assigned a value, and branches further by setting the chosen literal to FALSE otherwise.

In this paper, we will use the term DPLL to denote the ba­ sic branching and backtracking procedure described above. It will, for instance, not include extensions such as learning con­ flict clauses or restarting, but will allow intelligent branching heuristics. Note that this is in contrast with the occasional use of the term DPLL to encompass practically all branching and backtracking approaches, including those involving learning.

2.2 Resolution

Resolution is a simple proof system that can be used to prove unsatisfiability of CNF formulas. The resolution rule states that given clauses (A V x) and (BV · x), we can derive clause (A V B) by resolving on x. A resolution derivation of C from a CNF formula F is a sequence 1r = ( C1, C2, . .. , Cs := C) where each clause Ci is either a clause ofF (an initial clause) or derived by applying the resolution rule to cj and Ck, j, k < i (a derived clause). The size of 7f iss, the number of clauses occurring in it. We will assume that each Cj =I= C in 7f is used to derive at least one other clause ci, i > j. Any derivation of the empty clause A from F, also called a refutation or proof ofF, shows that F is unsatisfiable.

Despite its simplicity, resolution is not efficiently imple­ mentable due to the difficulty of finding good choices of clauses to resolve; natural choices typically yield huge stor­ age requirements. Various restrictions on the structure of res­ olution proofs lead to less powerful but easier to implement variants such as tree-like, regular, linear and positive resolu­ tion. Tree-like resolution uses non-empty derived clauses ex­ actly once in the proof and is equivalent to an optimal DPLL procedure. Regular resolution allows any variable to be re­ solved upon at most once along any "path" in the proof from an initial clause to A. Both these variants are sound and com­ plete but differ in efficiency - regular resolution is known to be exponentially stronger than tree-like [Bonet et al., 2000; Ben-Sasson et al., 2000], and general resolution is exponen­ tially stronger than regular [Aiekhnovich et al., 2002].

Definition 2. A resolution derivation (C1, C2, ... , Ck) is trivial iff all variables resolved upon are distinct and each ci' i ;::: 3, is either an initial clause or is derived by resolving ci - 1 with an initial clause.

A trivial derivation is tree-like as well as regular. More­ over, the condition that each derived clause ci use ci -1 in its derivation makes it linear. As we will see, trivial derivations correspond to conflicts in clause learning algorithms.

3 Clause Learning

Clause learning proceeds by following the normal branching process of DPLL until there is a "conflict" after unit propaga­ tion. Jfthis conflict occurs without any branches, the formula is declared unsatisfiable. Otherwise, the "conflict graph" is analyzed and the "cause" of the conflict is learned in the form of a "conflict clause." We now backtrack and continue as in ordinary DPLL, treating the learned clause just like initial ones. A clause is said to be known at a stage if it is either an initial clause or has already been learned. The learning process is expected to save us from redoing the same compu­ tation when we later have an assignment that causes conflict due in part to the same reason.

If a given CNF formula F is unsatisfiable, clause learn­ ing terminates with a conflict without any branches. Since all clauses used in this conflict themselves follow directly or indirectly from F, this failure of clause learning in finding a satisfying assignment constitutes a logical proof of unsatisfi­ ability of F. Our bounds compare the size of such a proof with the size of a (possibly restricted) resolution proof of un­ satisfiability of F.

Variations of such conflict driven learning [Bayardo Jr. and Schrag, 1997; Marques-Silva and Sakallah, 1996; Zhang, 1997; Moskewicz et a/., 200 I ; Zhang et a/., 200 I] include different ways of choosing the clause to learn and possibly allowing multiple clauses to be learned from a single con­ flict. Although many such algorithms have been proposed and demonstrated to be empirically successful, a theoretical discussion of the underlying concepts and structures needed for our bounds is lacking. The rest of this section focuses on this formal framework.

Definition 3. A clause learning proof 1r of an unsatisfiable CNF formula F under schemeS and induced by branching sequence (j is the result of applying DPLL with unit propa­ gation on F, branching according to (j, and using schemeS to learn conflict clauses such that at the end of this process, there is a conflict without any branches. The size of the proof, size(1r), is l(jl.

All clause learning algorithms discussed in this paper are based on unit propagation, which is the process of repeat­ edly applying the unit clause rule followed by formula sim­ plification until no clause with exactly one unassigned literal remains. In this context, it is convenient to work with resid­ ual formulas at different stages of DPLL. Let p be the partial assignment at some stage of DPLL on formula F. The resid­ ual formula at this stage is obtained by simplifying Flp and applying unit propagation.

When using unit propagation, variables assigned values through the actual branching process are called decision vari­ ables and those assigned values as a result of unit propagation are called implied variables. Decision and implied literals are analogously defined. Upon backtracking, the last deci­ sion variable no longer remains a decision variable and might instead become an implied variable depending on the clauses learned so far. The decision level of a decision variable x is one more than the number of current decision variables at the time of branching on x . The decision level of an implied variable is the maximum of the decision levels of decision variables used to imply it. The decision level at any step of the underlying DPLL procedure is the maximum of the deci­ sion levels of all current decision variables.

3.1 Implication Graph and Conflicts

Unit propagation can be naturally associated with an impli­ cation graph that captures all possible ways of deriving all implied literals from decision literals.

Definition 4. The implication graph G at a given stage of DPLL is a directed acyclic graph with edges labeled with sets of clauses. It is constructed as follows:

• I . Create a node for each decision literal, labeled with that literal. These will be the indegree zero root nodes of G.
• While there exists a known clause C = (l1 V .. . lk V l) such that ·h, ... , --,[k label nodes in G,
• (a) Add a node labeled l if not already present in G.
• (b) Add edges ( li , l), 1 ::; i ::; k, if not already present.
• (c) Add C to the label set of these edges. These edges are thought of as grouped together and associated with clause C.
• Add to G a special node A. For any variable x which occurs both positively and negatively in G, add directed edges from x and · x to A.

Since all node labels in G are distinct, we identify nodes with the literals labeling them. Any variable x occurring both positively and negatively in G is a conflict variable, and x as well as ·X are conflict literals. G contains a conflict if it has at least one conflict variable. DPLL at a given stage has a conflict if the implication graph at that stage contains a con­ flict. A conflict can equivalently be thought of as occurring when the residual formula contains the empty clause A.

By definition, an implication graph may contain many con­ flict variables and several ways of deriving any single literal. To better understand and analyze a conflict, we work with a sub graph, called the conflict graph (see Figure 1 ), that cap· tures only one among possibly many ways of reaching a con· flict from the decision variables. The choice of the conflict graph is part of the strategy of the solver. It can also be thought of as giving power to clause learning by adding non­ determinism.

Definition 5. A conflict graph H is any subgraph of an im­ plication graph with the following properties:

1. H contains A and exactly one conflict variable.
2. All nodes in H have a path to A.
3. Every node l in H other than A either corre­ sponds to a decision literal or has precisely the nodes ·l1 , ·l2, ... , ,zk as predecessors where (l1 V l2 V ... V lk V l) is a known clause.

Consider the implication graph at a stage where there is a conflict and fix a conflict graph contained in that implication graph. Pick any cut in the conflict graph that has all decision variables on one side, called the reason side, and A as well as at least one conflict literal on the other side, called the con­ flict side. All nodes on the reason side that have at least one edge going to the conflict side form a cause of the conflict. The negations of the corresponding literals forms the conflict clause associated with this cut.

Proposition 1. Every conflict clause corresponds to a cut in a conflict graph that separates decision variables from A and a conflict literal.

Proof Let S denote the set containing the negations of the literals of a given conflict clause C and pred( S) be the set of all predecessors of these literals in the underlying implication graph. LetT denote the set containing all literals obtained by unit propagation after setting literals in S to TRUE. Since C is a conflict clause, T must contain a conflict literal. Consider the subgraph Gs,r of the implication graph induced by A and the literals in S U pred(S) U T, but having no edges going from pred(S) toT. Fix any conflict graph that is a subgraph of G s,T· The cut in this conflict graph with T as the conflict side has C as the conflict clause. 0

Proposition 2. If there is a trivial resolution derivation of a clause C from a set of clauses F, then setting all literals of C to FALSE leads to a conflict.

Proof Let 1r = (C1, C2, ... , Ck =:C) be a trivial resolution derivation of C from F. Assume without loss of generality that clauses in 1r are ordered so that all initial clauses pre­ cede any derived clause. We give a proof by induction on the number of derived clauses in 1r.

For the base case, 1r does not have any derived clauses. Consequently, Ck E F. Let Ck = (h V l2 V ... V lq) and p be the partial assignment that sets allli, 1 ::; i::; q, to FALSE. Unit propagation using clause Ck with li, 1 ::; i ::; q- 1, set to FALSE derives the literallq. Since ·lq is a decision literal of p, lq serves as a conflict variable and we have a conflict.

When 1r does have derived clauses, Ck, by triviality of 1r, must be derived by resolving Ck_1 with a clause in F. As­ sume without loss of generality that Ck-1 = (A V x) and the clause from Fused in this resolution step is (B V ·x), where both A and B are subclauses of Ck. p falsifies all lit­ erals of B, implying x =FALSE by unit propagation. This in turn results in falsifying all literals of Ck-1 because all liter­ als of A are also set to FALSE by p. Now (C1, ... , Ck_I) is a trivial resolution derivation of Ck-1 from F with one less derived clause than 1r, and all literals of Ck-1 are falsified. By induction, this must lead to a conflict. 0

Proposition 3. Any conflict clause can be derived from known clauses using a trivial resolution derivation.

Proof In the light of Proposition 1, asswne that we have a conflict clause associated with a cut a in a fixed conflict graph. Let Vcon fli ct (a) denote the set of variables on the conflict side of a, but including the conflict variable only if it occurs both positively and negatively on the conflict side.

We will prove by induction on IVconflict(a)i the stronger statement that the conflict clause associated with a cut a has a trivial derivation resolving precisely on the variables in Vconflict(a).

For the base case, Vconflict(a) = ¢ and the conflict side contains only A and a conflict literal, say x. The cause asso­ ciated with this cut consists of node -.x that has an edge to A, and nodes ·h, --.[2, . .. , -.lk corresponding to a known clause Cx = (l1 V l2 V ... V lk V x) that each have an edge to x . The conflict clause for this cut is simply the known clause Cx itself, having a length zero trivial derivation.

When Vconflict(a) "/=¢,pick a node yon the conflict side all whose predecessors are on the reason side. Let the conflict clause be C = (l1 V l2 V ... V lp) and assume without loss of generality that the predecessors of y are ·11, ·l2, .. . , -.lk for some k ::; p. By definition of unit propagation, Cy = (h Vl2 V . .. V lk Vy) must be a known clause. Obtain a new cut a' from a by pulling node y to the reason side. The new associated conflict clause must be of the form C' = ( -.y V D), where Dis a subclause of C. Now Vconflict(a') C Vcon fli ct (a). Consequently, by induction, C' must have a trivial resolu­ tion derivation from known clauses resolving precisely upon the variables in Vcon fli ct (a'). Recall that no variable occurs twice in a conflict graph except the conflict variable. Hence Vcon fli ct (a') has exactly all variables of Vconflict (a) except y. Using this trivial derivation of C' and finally resolving C' with the known clause Cy on variable y gives us a triv­ ial derivation of C from known clauses. This completes the inductive step. 0

3.2 Different Learning Schemes

Different cuts separating decision variables from A and a con­ flict literal correspond to different learning schemes (see Fig­ ure 1. One can also create learning schemes based on cuts not involving conflict literals at all [Zhang et a/., 2001 ], but their effectiveness is not clear. These will not be considered here.

It is insightful to think of the non-deterministic scheme as the most general learning scheme. Here we pick the cut non­ deterministically, choosing, whenever possible, one whose associated clause is not already known. Since we can re­ peatedly branch on the same last variable, non-deterministic learning subsumes learning multiple clauses from a single conflict as long as the sets of nodes on the reason side of the corresponding cuts form a (set-wise) decreasing sequence. For simplicity, we will asswne that only one clause is learned from any conflict.

In practice, however, we employ deterministic schemes. The decision scheme [Zhang eta/., 2001], for example, uses the cut whose reason side comprises all decision variables. rel- sat [Bayardo Jr. and Schrag, 1997] uses the cut whose conflict side consists of all implied variables at the current de­ cision level. This scheme allows the conflict clause to have exactly one variable from the current decision level, causing an automatic flip in its assignment upon backtracking.

This nice flipping property holds in general for all unique implication points (UIPs) [Marques-Silva and Sakallah, 1996]. A UIP of an implication graph is a node at the current decision level d such that any path from the decision vari­ able at level d to the conflict variable as well as its negation must go through it. Intuitively, it is a single reason at level d that causes the conflict. Whereas re 1- sat uses the de­ cision variable as the obvious UIP, GRASP [Marques-Silva and Sakallah, 1996] and zChaff [Moskewicz eta!., 2001] use FirstUIP, the one that is "closest" to the conflict variable. GRASP also learns multiple clauses when faced with a con­ flict. This makes it typically require fewer branching steps but possibly slower because of the time lost in learning and unit propagation.

The concept of UIP can be generalized to decision levels other than the current one. The I UJP scheme corresponds to learning the FirstUIP clause of the current decision level, the 2UIP scheme to learning the FirstUIP clauses of both the current level and the one before, and so on. Zhang eta! [200 1] present a comparison of all these and other learning schemes and conclude that I UIP is quite robust and outperforms all other schemes they consider on most of the benchmarks.

The FirstNewCut Scheme

We propose a new learning scheme called FirstNewCut whose ease of analysis helps us demonstrate the power of clause learning. We would like to point out that we use this scheme here only to prove our theoretical bounds. Its effec­ tiveness on other formulas has not been studied yet.

The key idea behind FirstNewCut is to make the con­ flict clause as relevant to the current conflict as possible by choosing a cut close to the conflict literals. This is what the FirstUIP scheme also tries to achieve in a slightly different manner. For the following definitions, fix a cut in a conflict graph and let S be the set of nodes on the reason side that have an edge to some node on the conflict side (S is the rea­ son side frontier of the cut). Let Cs be the conflict clause associated with this cut.

Definition 6. Minimization of conflict clause C s is the pro­ cess of repeatedly identifying, if one exists, a node v E S, all of whose predecessors are also in S, moving it to the conflict side, and removing it from S.

Definition 7. FirstNewCut scheme: Start with a cut whose conflict side consists of A and a conflict literal. If necessary, repeat the following until the associated conflict clause, af­ ter minimization, is not already known: pick a node on the conflict side, pull all its predecessors except those that cor­ respond to decision variables into the conflict side. Finally, learn the resulting new minimized conflict clause.

This scheme starts with the cut that is closest to the con­ flict literals and iteratively moves it back toward the decision variables until a new associated conflict clause is found. This backward search always halts because the cut with all deci­ sion variables on the reason side is certainly a new cut. Note that there are potentially several ways of choosing a literal to move the cut back, leading to different conflict clauses. The FirstNewCut scheme, by definition, always learns a clause not already known. This motivates the following:

Definition 8. A clause learning scheme is non-redundant if on a conflict, it always learns a clause not already known.

3.3 Fast Backtracking and Restarts

Most clause learning algorithms use fast backtracking where one uses the conflict graph to backtrack not only the last branching decision but also all other recent decisions that did not contribute to the conflict [Stallman and Sussman, 1977]. This adds power to clause learning because the current con­ flict might use clauses learned earlier as a result of branching on the apparently redundant variables. Hence, fast backtrack­ ing in general cannot be replaced by a "good" branching se­ quence that does not produce redundant branches. For the same reason, fast backtracking cannot either be replaced by simply learning the decision scheme clause. However, there­ sults we present in this paper are independent of whether or not fast backtracking is used.

Restarts allow clause learning algorithms to arbitrarily restart their branching process. All clauses learned so far are however retained and now treated as additional initial clauses [Baptista and Silva, 2000]. As we will show, un­ limited restarts can make clause learning very powerful at the cost of adding non-determinism. Unless otherwise stated, clause learning proofs will be assumed to allow no restarts.

4 Clause Learning and General Resolution

Lemma 1. Let F be a CNF formula over n variables. If F has a general resolution proof of size s, then it also has a clause learning proof of size at most ns using any non­ redundant learning scheme and at most s restarts.

Proof Let 1r = ( C1 , C2, ... , Cs = A) be a general resolu­ tion proof of F where each Ci is either an initial clause or derived by resolving two clauses cj and ck. j, k < i, occur­ ring earlier in 1r. If 1r contains a derived clause Ci whose strict subclause c: can be derived by resolving two previously oc­ curring clauses, then we can replace ci with c:, do trivial simplifications on further derivations that used ci and obtain another proof 7T 1 ofF of size at most s. Doing this repeat­ edly will remove all such redundant clauses and leave us with a simplified proof no larger in size. Hence we will assume without loss of generality that 1r has no such clause.

A clause learning proof ofF can be constructed by choos­ ing derived clauses of 1r in order, learning each of them, and restarting. Suppose every clause Ci, i < p, is already known and we are at decision level zero. This is trivially true when C1 , ... , Cp-l are initial clauses. If p = s, there are two known clauses x and ·X whose resolution generates Cs = A. In this case we have a conflict from the known clauses at de­ cision level zero and our clause learning proof is complete.

Otherwise, let Cp = (h V 12 V ... V 1k) and assume without loss of generality that Cp is derived by resolving two known clauses (A V x ) and (B V ·x), where both A and B are subclauses of Cp. Our clause learning proof will choose to branch on and set all of 11, 12, . .. , 1k to FALSE. This will fal­ sify both A and B and thus imply both x and ·X after unit propagation, resulting in a conflict. It is easy to see that the only new clause that can be learned from this conflict is Cp. Accordingly, we will use any non-redundant learning scheme, learn Cp and restart to get back to decision level zero. Due to the non-redundancy of Cp assumed earlier in the proof, there is no premature conflict until all of 11, 12 , .·. , 1k have been branched upon. This makes sure that our clause learn­ ing proof proceeds as described above and we learn precisely the clause Cp.

We learn at most s clauses and each learning stage requires branching on at most n variables and exactly one restart. This gives the desired bounds on the size of the constructed clause learning proof and the number of restarts it uses. D

Lemma 2. Let F be a CNF formula over n variables. If F has a clause learning proof of size s using any learning scheme and any number of restarts, then F also has a general resolution proof of size at most ns.

Proof Given a clause learning proof 71' of F, a resolution proof can be constructed by sequentially deriving all clauses that 71' learns, which includes the empty clause A. From Proposition 3, all these derivations are trivial and hence re­ quire at most n steps each. Consequently, the size of the re­ sulting clause learning proof is at most ns. Note that since we derive clauses of 71' individually, restarts in 71' do not change the construction. D

Combining Lemmas 1 and 2, we immediately get

Theorem 1. Clause learning with any non-redundant scheme and unlimited restarts is equivalent to general resolution.

Note that this theorem strengthens the result from [Baptista and Silva, 2000] that clause learning together with restarts is complete. Our theorem makes the stronger claim that clause learning with restarts can find proofs that are as short as those of general resolution.

5 Clause Learning and Regular Resolution

Here we prove that clause learning even without restarts is exponentially stronger than regular resolution on some for­ mulas. We do this by first introducing a way of extending any CNF formula based on a given resolution proof of it. We then show that if a formula exponentially separates general res­ olution from regular resolution, its extension exponentially separates clause learning from regular resolution. Finally, we cite specific formulas called �T~ that satisfy this property.

5.1 The Proof Trace Extension

Definition 9. Let F be a CNF formula and 71' be a resolution refutation of it whose last step resolves v with ·V. Let S = 71' \ (F U { ·v, A}). The proof trace extension PT(F, 7r) ofF is a CNF formula over variables ofF and new trace variables tc for clauses C E S. The clauses of PT(F, 7r) are all initial clauses ofF together with a trace clause ( ·x V tc) for each clause C E Sand each literal x E C.

We first show that if a formula has a short general reso­ lution refutation, then the corresponding proof trace exten­ sion has a short clause learning proof. Intuitively, the new trace variables allow us to handle every resolution step of the original proof individually, effectively letting us restart after learning each derived clause.

Lemma 3. Let F be any CNF formula and 71' be a resolution refutation of it. Then PT( F, 71') has a clause learning proof of size less than size( 71') using the FirstNewCut scheme and no restarts.

Proof Let v be the variable resolved upon in the last step of the resolution proof 71' and S = 71' \ (F U { ·v, A}) . Let (C1, C2 , ... , Ck = v) be the subsequence of 71' that has pre­ cisely the clauses in S. Assume without loss of generality as in the proof of Lemma 1 that 71' does not contain a de­ rived clause ci whose strict subclause c: can be derived by resolving two previously occurring clauses. We claim that the branching sequence ( tc,, tc 2 , ··· , tc.) induces a clause learning proof ofF using the FirstNewCut scheme.

Suppose cl = (xl v X2 v 0 0 0 v Xt) and assume without loss of generality that it was derived by resolving two previ­ ous clauses (A V y) and (B V ·y), where both A and Bare subclauses ofC1. The first branch tc, =FALSE followed by unit propagation results in implied literals ·x1, · x2 , . .. , ·Xt using trace clauses ( ·Xi V tc, ). Further unit propagation us­ ing A and B implies y as well as ·y and we have a con­ flict. The cut in the conflict graph containing y and 'Y on the conflict side and everything else on the reason side makes us learn C1 as the FirstNewCut conflict clause. We now backtrack the branch on tc, and continue. Subsequent branches on tc 2 , tc 3 , . ·· , tc. similarly make us learn clauses c2, c3, ... , ck.

We have now learned (or have as initial clauses) the clause v as well as the two clauses used to derive ·v in 71'. These gen­ erate A in the residual formula, leading to a conflict without any branches and finishing the clause learning proof. Note that the maximum decision level in this proof is 1. D

Lemma 4. Let F be a CNF formula over n variables that has a polynomial (in n) size general resolution proof 71' but requires exponential size regular resolution proofs. Then PT( F, 71') has a polynomial size clause learning proof using the FirstNewCut scheme and no restarts, but requires expo­ nential size regular resolution proofs.

Proof Lemma 3 immediately implies that PT(F, 7r) has a polynomial size FirstNewCut clause learning proof.

For the other part, we use a simple reduction argument. Suppose PT(F, 7r) has a regular resolution refutation 71' 1 of size s. Consider the restriction p that sets every trace vari­ able of this formula to TRUE. p keeps original clauses ofF intact and trivially satisfies all trace clauses, thereby reduc­ ing the initial clauses of PT(F, 7r) to precisely F. Recall that regularity of resolution proofs is preserved under arbi­ trary restrictions. Consequently, applying p to 71' 1 gives us a regular resolution refutation ofF of size at most s. By the assumption in the Lemma, s must be exponential in n. Note that PT(F, 1r) itself is of size polynomial in n because of our choice of 1r. Hence s is also exponential in the size of PT(F, 1r) itself. D

5.2 The �T~ Formulas

We use the proof trace extension of an explicit family of un­ satisfiable CNF formulas called �T~ to obtain an exponen­ tial separation between regular resolution and clause learning. Note that in place of �T~, we could also have used any other formulas satisfying the conditions on F in Lemma 4, such as the modified pebbling formulas of Alekhnovich eta! [2002].

The �T~ formulas are based on the ordering principle that any partial linear ordering on the set { 1, 2, .. . , n} must have a maximal element. The original formulas, called GTn, were first considered by Krishnamurthy [ 1985] and later used by Bonet and Galesi [1999] to show the optimality of the size-width relationship of resolution proofs. Recently, Alekhnovich et a! [2002] used �T~ to show an exponential separation between general and regular resolution. We refer the reader to this paper for exact specification of the �T~ for­ mulas. For our bound, we only need the following result:

Lemma 5 (IAiekhnovich eta/., 2002)). �T~ has a polyno­ mial size general resolution refutation but requires exponen­ tial size regular resolution proofs.

Let 1fGT' be the polynomial size resolution refutation of �T~ described in [Alekhnovich eta!., 2002]. It follows from Lemmas 4 and 5 that PT( �T~, 7f GT') has a polynomial size clause learning proof using the FirstNewCut scheme but re­ quires exponential size regular resolution proofs. Hence,

Theorem 2. There exist CNF formulas on which clause learning using the FirstNewCut scheme and no restarts pro­ vides exponentially smaller proofs than regular resolution.

6 Experimental Results

Table 1 reports the performance of variants of zChaff on grid pebbling formulas. We conducted experiments on a 1600 MHz Linux machine with memory limit set to 512MB. Base code of zChaf f was extended to allow a (partial) branching sequence to be specified as part of the input. We used the more popular 1 UIP learning scheme of zChaff instead of FirstNewCut because for these formulas, both schemes pro­ vide small proofs.

Pebbling formulas based on pebbling graphs are known to be hard for tree-like resolution but easy for regular resolu­ tion [Ben-Sasson and Wigderson, 1999]. We refer the reader to this paper for exact specification of the formulas. For our experiments, we worked with a uniform, grid like version, where every non-leaf node has precisely two predecessors. For a k layer graph, the corresponding formula has O(k 2 ) variables and clauses. These formulas are minimally unsatis­ fiable. We also used a satisfiable version obtained by delet­ ing a randomly chosen clause. The branching sequence was generated based on depth first traversal of the underlying peb­ bling graph. Results are reported for zChaff with no learn­ ing or specified branching sequence (DPLL), with specified branching sequence only, with clause learning only (original zChaff), and both.

Table 1: zChaff on pebbling formulas. t denotes out of memory

7 Discussion and Open Problems

This paper has begun the task of formally understanding the power of clause learning from a proof complexity perspec­ tive. We have seen that clause learning can be more powerful than even regular resolution, and that learning with restarts yields general resolution.

In practice, a solver must employ good branching heuris­ tics as well as implement a powerful proof system. Our result that modified pebbling formulas have small clause learning proofs depends critically upon the solver choosing a branch­ ing sequence that solves the formula in "bottom up" fashion, so that the learned clauses have maximal reuse. As we de­ scribe in a subsequent paper [Sabharwal et a!., 2003], this branching sequence can be efficiently generated by a combi­ nation ofbreadth-first and depth-first traversals of the original pebbling graph even for more general classes of pebbling for­ mulas. As shown in Table 1, one needs both clause learning as well as a good branching sequence to efficiently solve large problem instances.

Of course, pebbling graphs, which correspond to problems involving precedence of tasks, represent a narrow domain of applicability. However, logic encodings of many kinds of real-world problems, such as planning graphs [Kautz and Selman, 1996], exhibit layered structure not unlike pebbling graphs. An important direction of our current research is to generate branching sequences that allow clause learning to work well on the general classes of structures that arise in encodings of particular problem domains.

Different learning schemes are likely to vary in their effec­ tiveness when used on formulas from different domains. We introduced FirstNewCut as a new scheme and used it in this paper to derive our theoretical results. How well it performs on encodings of real-world problems is still open. It would be interesting to know if there is a class of practical problems on which FirstNewCut works better than other schemes.

This paper inspires but leaves open several interesting questions of proof complexity. We have shown that with arbitrary restarts, clause learning is as powerful as general resolution. However, judging when to restart and deciding what branching sequence to use after restarting adds more non-determinism to the process, making it harder for prac­ tical implementations. Can clause learning with no or lim­ ited restarts also simulate general resolution efficiently? We showed that there are formulas on which clause learning is much more efficient than regular resolution. In general, can every small regular refutation be converted into a small clause learning proof? Or are regular resolution and clause learning incomparable?