Limits of CDCL Learning via Merge Resolution
Marc Vinyals #University of Auckland, New Zealand

Chunxiao Li #University of Waterloo, Canada

Noah Fleming #Memorial University of Newfoundland, Canada

Antonina Kolokolova #Memorial University of Newfoundland, Canada

Vijay Ganesh #University of Waterloo, Canada

Abstract
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showedthat CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous
work does not address the tightness of the simulation, i.e., the question of how large this overhead
needs to be. In this paper, we address this question by focusing on an important property of proofs
generated by CDCL solvers that employ standard learning schemes, namely that the derivation ofa learned clause has at least one inference where a literal appears in both premises (aka, a merge
literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most alinear overhead, but there also exist formulas where such overhead is necessary or, more precisely,that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.
2012 ACM Subject Classification Theory of computation → Proof complexity; Theory of computation → Constraint and logic programming
Keywords and phrases proof complexity, resolution, merge resolution, CDCL, learning scheme
Digital Object Identifier 10.4230/LIPIcs.SAT.2023.27
Related Version Full Version: https://arxiv.org/abs/2304.09422
Acknowledgements The authors are grateful to Yuval Filmus and a long list of participants inthe program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theoryof Computing for numerous discussions. We also thank the SAT 2023 reviewers for their helpful
suggestions. This work was done in part while the authors were visiting the Simons Institute for the
Theory of Computing.

1

Introduction

Over the last two decades, CDCL SAT solvers have had a dramatic impact on many areas ofsoftware engineering [10], security [13, 28], and AI [7]. This is due to their ability to solve
very large real-world formulas that contain upwards of millions of variables and clauses [17].
Both theorists and practitioners have expended considerable effort in understanding the
CDCL algorithm and the reasons for its unreasonable effectiveness in the context of practicalapplications. While considerable progress has been made, many questions remain unanswered.
Perhaps the most successful set of tools for understanding the CDCL algorithm come fromproof complexity, and a highly influential result is the one that shows that idealized modelsof CDCL can polynomially simulate the resolution proof system, proved independently by
Atserias, Fichte, and Thurley [2], and Pipatsrisawat and Darwiche [23], building on initial
results by Beame et al. [5] and Hertel et al. [15]. (See also a recent alternative proof by© Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh;licensed under Creative Commons License CC-BY 4.0
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023).
Editors: Meena Mahajan and Friedrich Slivovsky; Article No. 27; pp. 27:1–27:19
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

27:2

Limits of CDCL Learning via Merge Resolution

Beyersdorff and Böhm [6].) Such simulation results are very useful because they reassure us
that whenever a formula has a short resolution proof then CDCL with the right choice ofheuristics can reproduce it.
Recent models make assumptions that are closer to real solvers, but pay for that with apolynomial overhead in the simulation. A series of papers have focused on understanding
which of the assumptions are needed for these simulations to hold, often using and/or introducing refinements of resolution along the way. For instance, the question of whether restarts
are needed, while still open, has been investigated at length, and the pool resolution [26]and RTL [9] proof systems were devised to capture proofs produced by CDCL solvers that
do not restart. The importance of decision heuristics has also been explored recently, withresults showing that neither static [21] nor VSIDS-like [27] ordering of variables are enoughto simulate resolution in full generality (unless VSIDS scores are periodically erased [16]).
In the case of static ordering, the (semi-)ordered resolution proof system [21] was used toreason about such variants of CDCL solvers.
But even if we stay within the idealized model, it is not clear how efficient CDCL is in
simulating resolution. The analysis of Pipatsrisawat and Darwiche gives an O(n4 ) overhead—that is, if a formula over n variables has a resolution refutation of length L, then a CDCL
proof with no more than O(n4 L) steps exists. Beyersdorff and Böhm [6] improved theoverhead to O(n3 ), but we do not know what the optimal is. Furthermore, to the best of
our knowledge, prior to our paper, we did not even know if the overhead can be avoided
altogether.

1.1

Learning Schemes in CDCL and Connection with Merges

A common feature of CDCL solvers is the use of 1-empowering learning schemes [22, 2]: thatis, they only learn clauses which enable unit propagations that were not possible before. An
example of 1-empowering learning scheme is the popular First Unique Implication Point(1UIP) learning scheme [18]. To model this behavior we build upon a connection between
1-empowerment, and merges [1], i.e., resolution steps involving clauses with shared literals.
Nearly every CDCL solver nowadays uses the 1UIP learning scheme, where conflict
analysis starts with a clause falsified by the current state of the solver and sequentiallyresolves it with clauses responsible for unit propagations leading to the conflict, until theclause becomes asserting, i.e., unit immediately upon backjumping.
Descriptions of early implementations of CDCL solvers [18, 20] already remark on theimportance of learning an asserting clause, since that nudges the solver towards another partof the search space, and consequently early alternative learning schemes explored learning
many kinds of asserting clauses. First observe that conflict analysis can be extended to
produce other asserting clauses that appear after the 1UIP during conflict analysis such as
intermediate UIPs and the last UIP [4]. The early solver GRASP can even learn multiple
UIP clauses from a single conflict. While there is empirical evidence that it is often best
to stop conflict analysis at the 1UIP [29], recent work has identified conditions where it isadvantageous to continue past it [14] (see also the discussion of learning schemes therein).
Ryan [24, §2.5] also observed empirically that clause quality is negatively correlated withthe length of the conflict analysis derivation and considered the opposite approach, thatis, learning clauses that appear before the 1UIP during conflict analysis in addition to the
1UIP. This approach is claimed to be useful for some empirical benchmarks but, like any
scheme that learns multiple clauses, slows down Boolean constraint propagation (BCP) in
comparison to a scheme that learns just the 1UIP.
Later works provide a more theoretically oriented approach to understanding the strengthM. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:3

of 1UIP and to learning clauses that appear before the 1UIP [12, 22]. In particular, andhighly relevant for our discussion, Pipatsrisawat and Darwiche identified 1-empowerment
as a fundamental property of asserting clauses. Furthermore they identified a connection
between 1-empowering clauses and merges, and used the simplicity of checking for merges as
an approximation for 1-empowerment.
An orthogonal approach is to extend the 1UIP derivation by resolving it with clauses
other than those that would usually be used during conflict analysis [3]. A prominent example
is clause minimization [25], where literals are eliminated from the 1UIP clause by resolving itwith the appropriate input clauses, independently of their role in the conflict, so the resultant
clause that is actually learned is a shorter and therefore stronger version of the 1UIP.
Furthermore, a relation between merges and unit-resolution completeness has also been
observed in the context of knowledge compilation [11]. Finally, the amount of merges directly
inferable from a formula (i.e., in a single resolution step) has been proposed, under thename of mergeability, as a measure to help explain the hardness of a formula based on bothcontrolled experiments as well as analysis of real-world instances [30].
To summarize, merges are relevant in the context of CDCL learning schemes for thefollowing reason: all practical CDCL learning schemes either produce a 1-empowering clauseor extend one, and since 1-empowering clauses always contain a merge in its derivation,
we have that all practical learning schemes produce a clause that contains a merge in its
derivation, which is exactly the property imposed by the proof systems we introduce below.

1.2

Our Contributions

As mentioned earlier, we build upon a connection between 1-empowerment and merges [22, 2],
and introduce a DAG-like version of Andrews’ merge resolution which includes CDCL withan arbitrary 1-empowering learning scheme. This is because for any 1-empowering clause,
at least one step in its resolution derivation must resolve two clauses that share a common
literal: a merge step in the sense of Andrews [1]. This is precisely the condition that ourmerge resolution proof system enforces. Clause minimization procedures, as long as they areapplied on top of 1-empowering clauses, are also modelled by merge resolution.
We prove that, on the one hand, merge resolution is able to simulate resolution only witha linear overhead. On the other hand, we show a quadratic separation between resolution
and merge resolution, that is there exist formulas with resolution proofs of linear length that
require merge resolution proofs of quadratic length. The practical consequence of this pair ofresults is that CDCL may be polynomially worse than resolution because of the properties ofa standard learning scheme, but the blow-up due to these properties is not more than linear.
We also consider weaker proof systems, all of which contain 1UIP (and do so with finer
granularity), but not necessarily other asserting learning schemes. A technical point ofinterest is that we work with proof systems that are provably not closed under restrictions,which is unusual in proof complexity. This fact forces our proof to exploit syntactic propertiesof the proof system, as opposed to relying on more convenient semantic properties.

2

Preliminaries

A literal is either a variable x1 = x or its negation x0 = x. A clause is a disjunction of literals,
and a CNF formula is a conjunction of clauses. The support of a clause or vars(C) is the setof variables it contains. A resolution derivation from a formula F is a sequence of clauses
η = C1 , . . . , CL such that Ci is either an axiom in F or it is the conclusion of applying the

S AT 2 0 2 3

27:4

Limits of CDCL Learning via Merge Resolution

resolution rule
Res(A ∨ x, B ∨ x, x) = Res(A ∨ x, B ∨ x) = A ∨ B
on two premises Cj , Ck with j, k < i. The unique variable x that appears with opposite
signs in the premises of a resolution inference is called the pivot. If furthermore there
is a literal common to A and B the resolvent is called a merge. If instead of being theresult of a syntactic inference we allow Ci to be any clause semantically implied by Cj
and Ck , even if Cj and Ck might not be resolvable, then we say η is a semantic resolution
derivation. A derivation is a refutation if its last clause is the empty clause ⊥. We denoteη[a, b] = {Ci ∈ η | i ∈ [a, b]}.
We assume that every clause in a derivation is annotated with the premises it is obtained
from, which allows us to treat the proof as a DAG where vertices are clauses and edges pointfrom premises to conclusions. When this DAG is a tree we call a derivation tree-like, andwhen it is a centipede (i.e., a maximally unbalanced tree) we call it input.
A derivation is unit if in every inference at least one of the premises is a unit clauseconsisting of a single literal. Since neither input nor unit resolution are complete proof
systems, we write F ⊢i C (respectively F ⊢1 C) to indicate that there exists an input (resp.
unit) resolution derivation of C from F .
A clause C syntactically depends on an axiom A with respect to a derivation η if there isa path from A to C in the DAG representation of η. This does not imply that A is required
to derive C, since a different derivation might not use A.
A restriction—or more formally a variable substitution, since we allow mapping variables
to other variables—is a mapping ρ : X → X ∪ {0, 1}, successively extended to literals, clauses,
formulas, and derivations, simplifying where needed. We write ρ(x) = ∗ as a shorthand forρ(x) = x. It is well-known that if η is a resolution derivation from F and ρ is a restriction,then η↾ρ is a semantic resolution derivation from F ↾ρ .
It is convenient to leave satisfied clauses in place in a derivation that is the result ofapplying a restriction to another derivation so that we can use the same indices to refer
to both derivations. To do that we use the symbol 1 and treat it as a clause that always
evaluates to true, is not supported on any set, does not depend on any clause, and cannot be
syntactically resolved with any clause.
A semantic derivation can be turned into a syntactic derivation by ignoring unnecessary
clauses. Formally, if η is a semantic resolution derivation, we define its syntactic equivalents(η) as the syntactic resolution derivation obtained by replacing each clause of C ∈ η bya clause s(C) as follows. If C is an axiom then s(C) = C. Otherwise let A and B be theparents of C. If s(A) ⊨ C we set s(C) = s(A), analogously with s(B). Otherwise we sets(C) = Res(s(A), s(B)). It is not hard to see that for each Ci ∈ η, s(Ci ) ⊨ Ci .

2.1

CDCL

We need to define a few standard concepts from CDCL proofs. An in-depth treatment canbe found in the Handbook of Satisfiability [8]. Let F be a CNF formula, to which we refer asa clause database. A trail τ is a sequence of tuples (xji = b, Ci ) where Ci is either a clausein F or the special symbol d representing a decision. We denote by α<i the assignment{xji = b | i′ < i}. A trail is valid with respect to F if for every position i that is not adecision we have that Ci ↾α<i = xbji , in which case we say that Ci propagates xbji , and if forevery decision i there is no clause C ∈ F such that C↾α<i = xb .
We denote by dl(i) = dl(i − 1) + JCi = dK the decision level at position i, that is thenumber of decisions up to i. Here JCi = dK is the indicator of the event that the ith variable

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:5

on the trail was set by a decision. We mark the position of the last decision in a trail by i∗ .
A clause C is asserting if it is unit at the last decision in the trail, that is C↾α<i∗ = xb .
It is 1-empowering if C is implied by F and can lead to new unit propagations after being
added to F , that is if there exists a literal ℓ ∈ C such that for some A ∈ {⊥, ℓ}, it holds thatF ∧ C \ ℓ ⊬1 A. If a clause is not 1-empowering then we say it is absorbed by F .
Given a clause D|τ | falsified by a trail τ , the conflict derivation is an input derivation
D|τ | , D|τ |−1 , . . . , Dk where Di−1 = Res(Di , Ci , xji ) if Ci =
̸ d and xji ∈ Di , and Di−1 = Di
otherwise. The first (i.e., with the largest index) asserting clause in the derivation is called
the 1UIP. Note that Di∗ is always asserting (because Di∗ is falsified by α≤i∗ but not byα<i∗ ), therefore we can assume that the 1UIP always has index at least i∗ .
We call a sequence of input derivations input-structured if the last clause of each derivation
can be used as an axiom in successive derivations. The last clause of each but the lastderivation is called a lemma. A CDCL derivation is an input-structured sequence of conflictderivations, where learned clauses are lemmas. This definition is similar to that of Resolution
Trees with Input Lemmas [9], with the difference that the sequence only needs to be ordered,without imposing any further tree-structure on the global proof.
The following Lemmas highlight the practical relevance of merges by relating them to
1UIP, asserting, and 1-empowering clauses.
▶ Lemma 1 ([22, Proposition 2]). If a clause is asserting, then it is 1-empowering.1▶ Lemma 2 ([2, Lemma 8]). If A ∨ x and B ∨ x are absorbed but A ∨ B is 1-empowering,then A ∨ B is a merge. In particular, if a clause is 1-empowering, then it contains a merge
in its derivation.
▶ Lemma 3. The 1UIP clause is a merge.
Proof. Let Di = Res(Ci+1 , Di+1 ) be the 1UIP. Every clause in F that is not already satisfied
by α<i∗ , and in particular Ci for i > i∗ and D|τ | , contains at least two literals at thelast decision level, otherwise it would have propagated earlier. This also applies to clauses
Di+1 , . . . , D|τ | , since they are not asserting.
We accounted for 4 literals at the last decision level present in the premises of Di , of which
2 are not present in the conclusion because they are the pivots. In order for Di to contain
only one literal at the last decision level, the remaining two literals must be equal.
◀

3

Merge Resolution

Andrews’ definition of merge resolution [1] considers tree-like proofs with the additional
restriction that in every inference at least one premise is an axiom or a merge. He also
observes that such derivations can be made input-structured.
▶ Observation 4 ([1]). A tree-like merge resolution derivation can be decomposed into an
input-structured sequence where all the lemmas are merges.
This observation is key when working with such derivations, as is apparent in Section 4,
to the point that we define our proof systems in terms of the input-structured framework.
Every resolution proof can be thought of as being input-structured if we consider it as asequence of unit-length input resolutions and every clause as a lemma; it is when we impose
restrictions on which clauses are permitted as lemmas that we obtain different proof systems.
Andrews’ main result is that the merge restriction does not affect tree-like resolution.
1

The original result does not prove 1-consistency, but the proof is analogous.

S AT 2 0 2 3

27:6

Limits of CDCL Learning via Merge Resolution▶ Lemma 5 ([1, Lemma 5]). If there is a tree-like resolution derivation of C of length L
where at most the root is a merge, then there is an input resolution derivation of some C ′ ⊆ Cof length at most L.
▶ Theorem 6 ([1, Theorem 1]). If there is a tree-like resolution derivation of C of length L,then there is a tree-like merge resolution derivation of some C ′ ⊆ C of length at most L.
If we lift the tree-like restriction from the input-structured view of merge resolution proofs
we obtain a proof system between tree- and DAG-like resolution where clauses can be reused(i.e., have outdegree larger than 1) if and only if they are merges or, in other words, lemmas
in the input-structured decomposition. As a consequence of Lemma 3 this proof systemalready includes CDCL refutations produced by solvers that use the 1UIP learning scheme.
In order to model all asserting learning schemes we allow reusing clauses that contain amerge not only when they are inferred but anywhere in their derivation.
▶ Definition 7. A merge resolution derivation is an input-structured sequence of input
resolution derivations where all derivations but the last contain a merge.
It follows from Lemmas 1 and 2 that refutations produced by solvers that use any asserting
learning scheme are in merge resolution form.
We immediately have from the simulation of resolution by CDCL [23, 2] that merge
resolution polynomially simulates standard resolution. In Section 4 we make this simulation
more precise and prove that the simulation overhead can be made linear, and in Section 5that the simulation is optimal because there exist formulas that have resolution refutationsof linear length but require merge resolution refutations of quadratic length.

4

Simulation

As an auxiliary tool to simulate resolution in merge resolution we define the input-resolution
closure of a set G, denoted Cli (G) = {C | ∃C ′ ⊆ C, G ⊢i C ′ }, as the set of clauses derivablefrom G via input resolution plus weakening. It is well-known that, since input resolution
derivations can be assumed to be regular—using each variable at a pivot at most once—
without loss of generality, we can also assume them to have length at most linear in thenumber of variables.
▶ Observation 8. If G is a CNF formula over n variables and C ∈ Cli (G) then there is aregular input resolution derivation of some C ′ ⊆ C from G of length at most n.
Combining Theorem 6 with the idea that in order to simulate a resolution derivation we
do not need to generate each clause, but only do enough work so that in the following steps
we can pretend that we had derived it [23, 2], we can prove that merge resolution simulates
resolution with at most a multiplicative linear overhead in the number of variables.
▶ Theorem 9. If F is a CNF formula over n variables that has a resolution refutation oflength L then it has a merge resolution refutation of length O(nL).
Proof. Let π = (C1 , . . . , CL ) be a resolution refutation. We construct a sequence of sets
F = G0 ⊆ · · · ⊆ GL with the following properties.
1. Gt \ F is the set of lemmas in a merge resolution derivation from F of length at most
(2n + 1)t.
2. π[1, t] ⊆ Cli (Gt ).

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:7

This is enough to prove the theorem: since ⊥ ∈ Cli (GL ) we can obtain ⊥ from GL in
length n, so the total length of the refutation is (2n + 1)L + n.
We build the sets by induction, starting with G0 = F . Assume we have built Gt and let
C = Ct+1 . If C ∈ Cli (Gt ) we set Gt+1 = Gt and we are done. Otherwise C = Res(A, B)
with A, B ∈ π[1, t], and by induction we have A, B ∈ Cli (Gt ), therefore by Observation 8
there are input resolution derivations of A′ ⊆ A and B ′ ⊆ B of length at most n. Since
neither A′ ⊨ C nor B ′ ⊨ C, A′ and B ′ can be resolved and therefore there is a tree-likederivation η of C ′ ⊆ C from Gt of length at most 2n + 1. By Theorem 6 there is a tree-likemerge resolution derivation η ′ of C ′′ ⊆ C from Gt of length at most 2n + 1. By Observation 4
the derivation η ′ can be decomposed into a sequence of input derivations of total length at
most 2n + 1. Let E be the lemmas in that sequence and set Gt+1 = Gt ∪ E. We have thatC ∈ Cli (F ∪ E) ⊆ Cli (Gt+1 ), and that we can obtain E from Gt in at most 2n + 1 steps.
Thus Gt+1 has all the required properties.
◀

5

Separation

We prove the following separation between standard and merge resolution.
▶ Theorem 10. There exists a family of formulas Fn over O(n log n) variables and O(n log n)clauses that have resolution refutations of length O(n log n) but every merge resolution
refutation requires length Ω(n2 log n).

5.1

FormulaLet ℓ, m, n be positive integers. We have variables xi for i ∈ [mℓ − 1] and wj,k for j ∈ [ℓ]and k ∈ [n]. For convenience we define x0 = 1 and xmℓ = 0, which are not variables. LetS
X = {xi | i ∈ [mℓ − 1]}, Wj = {wj,k | k ∈ [n]} and W = j∈[ℓ] Wj . For each j ∈ [ℓ] we build
the following gadget:
wj,k = wj,k+1

for k ∈ [n − 1](1)

Each equality is expanded into the two clauses Bj,k,1 = wj,k ∨wj,k+1 and Bj,k,0 = wj,k ∨wj,k+1 ,and we collectively call them W = {Bj,k,b | j ∈ [ℓ], k ∈ [n − 1], b ∈ {0, 1}}. Observe that thej-th gadget implies wj,1 = wj,n . Additionally we build the following gadget:(w1,1 = w1,n ) → x1
(wı̂,1 = wı̂,n ) → (xi−1 → xi )(wℓ,1 = wℓ,n ) → xmℓ−1(2)
for i ∈ [2, mℓ − 1]

(3)
(4)

where ı̂ ∈ [ℓ] denotes the canonical form of i (mod ℓ). Each constraint is expanded into
the two clauses Ai,1 = wı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi and Ai,0 = wı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi , and wecollectively call them X = {Ai,b | i ∈ [mℓ], b ∈ {0, 1}}. The formula X ∪ W is called Fℓ,m,n .

5.2

Upper Bound

It is not hard to see that there is a resolution refutation of Fℓ,m,n of length O(ℓ · (m + n)).
Indeed, we first derive the two clauses representing wj,1 = wj,n for each j ∈ [ℓ], which requires

S AT 2 0 2 3

27:8

Limits of CDCL Learning via Merge Resolution

O(nℓ) steps:
wj,1 ∨ wj,2

wj,2 ∨ wj,3

wj,1 ∨ wj,3
..
.

(5)

wj,1 ∨ wj,n−1

wj,n−1 ∨ wj,n
wj,1 ∨ wj,nThen we resolve each of the X axioms with one of these clauses, appropriately chosen so that
we obtain pairs of clauses of the form wı̂b ∨ xi−1 ∨ xi for i ∈ [mℓ], and resolve each pair toobtain the chain of implications x1 , . . . , xi → xi+1 , . . . , xnℓ−1 in O(mℓ) steps.
wı̂,1 ∨ wı̂,nwı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi

wı̂,1 ∨ wı̂,nwı̂,1 ∨ xi−1 ∨ xi

wı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi
wı̂,1 ∨ xi−1 ∨ xi(6)

xi−1 ∨ xi
Since we have derived a chain of implications x1 , x1 → x2 , . . . , xmℓ−1 → xmℓ−1 , xmℓ−1 wecan complete the refutation in O(mℓ) more steps. Let us record our discussion.
▶ Lemma 11. Fℓ,m,n has a resolution refutation of length O(ℓ · (m + n)).
Before we prove the lower bound let us discuss informally what are the natural ways torefute this formula in merge resolution, so that we understand which behaviours we need torule out.
If we try to reproduce the previous resolution refutation, since we cannot reuse the clauses
representing wj,1 = wj,n because they are not merges, we have to rederive them each time
we need them, which means that it takes O(mnℓ) steps to derive the chain of implications
x1 , . . . , xi → xi+1 , . . . , xnℓ−1 . We call this approach refutation 1 . This refutation has mergesb(over wı̂,1 , xi−1 , and xi ) when we produce wı̂,1∨ xi−1 ∨ xi , and (over xi−1 and xi ) when we
produce xi−1 ∨ xi , but since we never reuse these clauses the refutation is in fact tree-like.
An alternative approach, which we call refutation 2 , is to start working with the X
axioms instead. In this proof we clump together all of the repeated constraints of the form
wj,1 =
̸ wj,n for every j ∈ [ℓ], and then resolve them out in one go. In other words, we first
derive some clausal encoding of the sequence of constraints
 _

Di =
wı̂,1 ̸= wı̂,n ∨ xi
for i ∈ [mℓ] ,(7)ı̂∈[min(i,ℓ)]where Di can be obtained from Di−1 and the pair of X axioms Ai,b , then resolve away theWinequalities from Dmℓ = j∈[ℓ] wj,1 ≠ wj,n using the W axioms. However, representing anyof the constraints Di for i ≥ ℓ requires 2ℓ clauses, which is significantly larger than mnℓ andeven superpolynomial for large enough ℓ, so this refutation is not efficient either. Note that
this refutation has merges (over W variables) each time that we derive Di with i ≥ ℓ.
A third and somewhat contrived way to build a refutation is to derive the pair of clauses
representing wj,1 = wj,n using a derivation whose last step is a merge, so that they can bereused. Each of these clauses can be derived individually in O(mnℓ) steps, for a total ofO(mnℓ2 ) steps, by slightly adapting refutation 1, substituting each derivation of xi → xi+1
by a derivation of wj,1 ∨ wj,n ∨ xi ∨ xi+1 whenever i ≡ j (mod ℓ) so that at the end weM. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:9

obtain wj,1 ∨ wj,n instead of the empty clause. Such a substitution clause can be obtained,e.g., by resolving wj,1 ∨ wj,2 ∨ xi ∨ xi+1 with wj,2 ∨ wj,n ∨ xi ∨ xi+1 as follows
wj,2 ∨ wj,3 wj,3 ∨ wj,4
wj,2 ∨ wj,4..
.
wj,2 ∨ wj,n−1

wj,n−1 ∨ wj,n

wj,2 ∨ wj,nwı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi wı̂,1 ∨ wı̂,2 wı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi
wı̂,1 ∨ wı̂,2 ∨ xi−1 ∨ xi

wı̂,2 ∨ wı̂,n ∨ xi−1 ∨ xi

wı̂,1 ∨ wı̂,n ∨ xi−1 ∨ xi

(8)
After deriving wj,1 = wj,n as merges we follow the next steps of refutation 1 and complete
the refutation in O(mℓ) steps. We call this refutation 3 .
Observe that the minimum length of deriving the clauses representing wj,1 = wj,n isonly O(n), even in merge resolution, so if we only used the information that refutation 3
contains these clauses we would only be able to bound its length by Ω(ℓ · (m + n)). Therefore
when we compute the hardness of deriving a clause we need to take into account not only its
semantics but how it was obtained syntactically.

5.3

Lower Bound

Before we begin proving our lower bound in earnest we make two useful observations.
▶ Lemma 12. Let η be a resolution derivation that only depends on W axioms. Then η does
not contain any merges, and all clauses are supported on W .
Proof. We prove by induction that every clause in η is of the form wj,k ∨ wj,k′ with k ̸= k ′ .
This is true for the axioms. By induction hypothesis, a generic resolution step over wj,k is of
the form
wj,k ∨ wj,k′

wj,k ∨ wj,k′′(9)

wj,k′′ ∨ wj,k′and in particular is not a merge.

◀

▶ Lemma 13. Let η be a resolution derivation of a clause C supported on W variables thatuses an X axiom. Then η uses at least one Ai,b axiom for each i ∈ [mℓ].
Proof. We prove the contrapositive and assume that there is an axiom Ai,b that is used, andeither both Ai+1,0 and Ai+1,1 are not used, or both Ai−1,0 and Ai−1,1 are not. In the firstcase the literal xi appears in every clause in the path from Ai,b to C, contradicting that C is
supported on W variables. Analogously with literal xi−1 in the second case.
◀
At a high level, our first step towards proving the lower bound is to rule out that
refutations like refutation 2 can be small, and to do that we show that wide clauses allow forvery little progress. This is a common theme in proof complexity, and the standard tool is
to apply a random restriction to a short refutation in order to obtain a narrow refutation.
However, merge resolution is not closed under restrictions, as we prove later in Corollary 24,
and because of this we need to argue separately about which merges are preserved.

S AT 2 0 2 3

27:10Limits of CDCL Learning via Merge Resolution

We observed that derivation fragments where no X variable appears do not containany merges, but we cannot claim that clauses where no X variable appears are not merges.
However, refutation 3 suggests that deriving a clause supported on W variables that depends
on X axioms should still be hard, so we restrict our attention to the part of the refutation
before any such clause is derived.
We then show that the resulting refutation needs to use all X variables, and picks up apair of W variables each time that a new X variable appears. If we were to introduce the X
variables in order, and since we ruled out wide clauses, every time that we use ℓ many X
variables we also need to eliminate proportionately as many W variables before we move onto
the next interval of X variables. We would expect to eliminate variables Ω(mℓ) times, andeach elimination requires Ω(n) steps. Of course the refutation might not use X variables inorder, but we can still break the proof into parts, each corresponding roughly to an intervalof ℓ many X variables.
Let us begin implementing our plan by defining the class of restrictions that we use andwhich need to respect the structure of the formula. A restriction is an autarky [19] withrespect to a set of clauses G if it satisfies every clause that it touches; in other words for every
clause C ∈ G either C↾ρ = 1 or C↾ρ = C. A restriction is k-respecting if it is an autarky
with respect to W axioms, we have Fℓ,m,n ↾ρ ∼= Fk,m,n up to variable renaming, and every X
variable is mapped to an X variable. Our definition of a narrow clause is also tailored to
the formula at hand, and counts the number of different W -blocks that a clause C mentions.
Formally µ(C) = |{j ∈ [ℓ] | ∃xj,k ∈ vars(C)}|.
▶ Lemma 14. Let π be a resolution refutation of Fℓ,m,n of length L = o((4/3)ℓ/8 ). Thereexists an ℓ/4-respecting restriction ρ such that every clause in π↾ρ has µ(C) ≤ ℓ/8.
Proof. We use the probabilistic method. Consider the following distribution J over {0, 1, ∗}ℓ :each coordinate is chosen independently with Pr[Ji = 0] = Pr[Ji = 1] = 1/4, Pr[Ji = ∗] = 1/2.
Given a random variable J ∼ J sampled according to this distribution, we derive a random
restriction ρ as follows: ρ(wj,i ) = Jj , ρ(xi ) = ∗ if Jı̂ = ∗, and ρ(xi ) = ρ(xi−1 ) otherwise(where ρ(x0 ) = 1).
Observe that Fℓ,m,n ↾ρ ∼= F|J −1 (∗)|,m,n up to variable renaming, and by a Chernoff boundwe have Pr[|J −1 (∗)| < ℓ/4] ≤ e−ℓ/16 .
We also have, for every clause C ∈ π with µ(C) > ℓ/8, that
Pr[C↾ρ ̸= 1] ≤ (3/4)µ(C) ≤ (3/4)ℓ/8 .

(10)

Therefore by a union bound the probability that |J −1 (∗)| < ℓ/4 or that any clause hasµ(C↾ρ ) > ℓ/8 is bounded away from 1 and we conclude that there exists a restriction ρ thatsatisfies the conclusion of the lemma.
◀
Note that s(π↾ρ ) is a resolution refutation of Fn,ℓ,m ↾ρ , but not necessarily a merge resolution refutation, therefore we lose control over which clauses may be reused2 . Nevertheless,
we can identify a fragment of s(π↾ρ ) where we still have enough information.
▶ Lemma 15. Let π be a merge resolution refutation of Fn,ℓ,m and ρ be the restriction from
Lemma 14. There exists an integer t such that ψ = s(π[1, t]↾ρ ) is a resolution derivation of aclause supported on W variables that depends on an X axiom and where no clause supported
on W variables is reused.
2

Recall that s(π) is the syntactic equivalent of π.

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:11

Proof. Let Ct ∈ π be the first clause that depends on an X axiom and such that Dt = s(Ct ↾ρ )is supported on W , which exists because ⊥ is one such clause.
By definition of t, we have that every ancestor Dk ∈ ψ of Dt that is supported on W
variables corresponds to a clause Ck in π that only depends on W axioms, hence by Lemma 12
Ck is not a merge. By definition of merge resolution Ck is not reused, and by constructionof s(·) neither is Dk .
It remains to prove that Dt depends on an X axiom. Since Ct depends on an X axiom, atleast one of its predecessors Cp and Cq also does, say Cp . By definition of t, Dp = s(Cp ↾ρ ) is
not supported on W , and hence by Lemma 12 either Dp depends on an X axiom or Dp = 1.
Analogously, if Cq also depends on an X axiom then so does Dq = s(Cj ↾ρ ) (or it is 1) and
we are done. Otherwise Cq is of the form wj,k ∨ wj,k′ and is either satisfied by ρ or left
untouched. In both cases we have that Dq ̸⊨ Ct ↾ρ (trivially in the first case and because Dq
contains the pivot while Ct does not in the second), hence Dt depends on Dp .
◀
Note that Ct may be semantically implied by the W axioms, and have a short derivation
as in refutation 3, therefore we are forced to use syntactic arguments to argue that deriving
Ct using an X axiom takes many resolution steps.
The next step is to break ψ into m (possibly intersecting) parts, each corresponding
roughly to the part of ψ that uses X axioms with variables in an interval of length ℓ (byLemma 13 we can assume that ψ contains axioms from every interval). To do this we use
the following family of restrictions defined for i ∈ [n]:1σi (xi′ ) = ∗0

if i′ ≤ iℓ
if iℓ < i′ ≤ (i + 1)ℓ
if (i + 1)ℓ < i

σi (wi′ ,j ) = ∗

(11)

′

Let Xi = X ∩ σi−1 (∗) and note that Fℓ,m,n ↾σi ∼= Fℓ,1,n .
Clauses in ψ with many X variables could be tricky to classify, but intuitively it should
be enough to look at the smallest positive literal and the largest negative literal, since these
are the hardest to eliminate. Therefore we define r(C) to be the following operation on aclause: literals over W variables are left untouched, all positive X literals but the smallest
are removed, and all negative X literals but the largest are removed. Formally,
_

_
_
_
bi,j
b
r
xi ∨
xi ∨
wi,j = xmin A ∨ xmax B ∨wi,ji,j
(12)
i∈A

i∈B

(i,j)∈C(i,j)∈C

where xmin A (resp. xmax B ) is omitted if A (resp. B) is empty.
We need the following property of r(C).
▶ Lemma 16. If C↾σi ̸= 1 and vars(r(C)) ∩ Xi = ∅ then C↾σi is supported over W variables.
Proof. The hypothesis that vars(r(C)) ∩ Xi = ∅ implies that the smallest positive X literalin C is either not larger than iℓ or larger than (i + 1)ℓ, but the hypothesis that C↾σi ̸= 1 rulesout the first case. Therefore all positive X literals are falsified by σi . Analogously the largest
negative X literal is not larger than iℓ and all negative X literals are also falsified.
◀
Now we are ready to formally define how to divide ψ.
▶ Definition 17. The i-th part of ψ is the sequence ψi of all clauses C ∈ ψ such that C iseither
1. an X axiom not satisfied by σi ; or

S AT 2 0 2 3

27:12

Limits of CDCL Learning via Merge Resolution

2. the conclusion of an inference with pivot in Xi ; or
3. the conclusion of an inference with pivot in W that depends on an X axiom if r(C)contains a variable in Xi ; or
4. a clause that does not depend on X axioms if the only immediate successor of C is in ψi .
For convenience we use the same indexing for ψi and ψ, so elements of ψi are notnecessarily consecutive. Note that ψi needs not be a valid derivation.
This is the point in the proof where we use crucially that the original derivation is inmerge resolution form: because clauses that do not depend on X axioms are not merges,
they have only one successor and the definition is well-formed.
As an example, if ψ were refutation 1, whose only clause supported over W variables that
depends on X axioms is the final empty clause and therefore satisfies the guarantees givenby the conclusion of Lemma 15, then we would divide it as follows. Axioms A1,b , . . . , Aℓ,b
are all part of ψ1 because of Item 1. The result of resolving axioms Ai,b with the clauses
representing wi,1 = wi,n in order to obtain the implications xi → xi+1 for i ∈ [1, ℓ] are alsopart of ψ1 because of Item 3. This implies that the W axioms and intermediate clauses used
to derive wi,1 = wi,n are also part of ψ1 because of Item 4. Derivations of xi+1 from xi
and xi → xi+1 for i ∈ [1, ℓ] are part of ψ1 because of Item 2. Similarly ψ2 will contain theanalogous clauses with i ∈ [ℓ + 1, 2ℓ] and so on. Note that each part ψi contains derivationsof wj,1 = wj,n for j ∈ [ℓ], but they refer to different copies of the same derivation.
Ideally we would like to argue that parts ψi are pairwise disjoint and of size Ω(nℓ), whichP
would allow us to bound |ψ| = i∈[m] |ψi | = Ω(mnℓ). This is not quite true, but neverthelessclauses do not appear in too many different parts and we have the following bound.
P▶ Lemma 18. Let ψ and {ψi | i ∈ [m]} be as discussed above. Then 2|ψ| ≥ i∈[m] |ψi |.
Proof. Axioms may appear in at most two different ψi , and clauses obtained after resolving
with an X pivot in only one. The only other clauses that depend on an X axiom and may
appear in different ψi are obtained after resolving with a W pivot, but since r(C) only
contains two X variables, such clause only may appear in two different ψi . Finally, clausesthat do not depend on an X axiom appear in the same ψi as one clause of the previous types,
and therefore at most two different parts.
◀
To conclude the proof we need to argue that each ψi has size Ω(nℓ). The intuitive reason
is that ψi must use one X axiom for each j ∈ [(iℓ, (i + 1)ℓ], which introduces a pair of W
variables from each Wj block, but since no clause contains more than ℓ/8 such variables, weneed to use enough W axioms to remove the aforementioned W variables. Formally we firstneed to extract a valid derivation from ψi as we do in the next lemma.
▶ Definition 19. For each i ∈ [m] let ti be the smallest integer such that clause Cti depends
on an X axiom (with respect to ψ), Cti ↾σi is supported on W variables, and Cti ∈ ψi . If nosuch clause exists then we set ti = ∞.
▶ Lemma 20. For each i ∈ [m], ti is finite and s(ψi [1, ti ]↾σi ) is a valid resolution derivation.
Proof. We prove by induction that for all k ≤ min(ti , t), if the clause Ck ∈ ψ depends on
an X axiom and is not satisfied by σi , then there exists a clause Ck′ ∈ ψi with k ′ ≤ k that
implies Ck modulo σi , that is Ck′ ↾σi ⊨ Ck ↾σi , and depends on an X axiom (over ψ).
When Ck is a non-satisfied X axiom we can simply take Ck′ = Ck by Item 1 of Definition 17.
Otherwise let Cp and Cq be the premises of Ck in ψ and we consider a few cases.
Case 1: the pivot is an X variable. Then both premises depend on an X axiom (byLemma 12).

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:13

Case 1.1: the pivot is an Xi variable. Then we can take Ck′ = Ck by Item 2 ofDefinition 17.
Case 1.2: the pivot is an Xi′ variable with i′ ̸= i. Then the pivot is assigned by σi andexactly one of the premises, say Cp , is non-satisfied. By the induction hypothesis we
can take Ck′ = Cp′ .
Case 2: the pivot is a W variable. If either premise were satisfied, and since σi only assigns
X variables, the satisfied literal would carry over to Ck , hence neither premise is satisfied.
Case 2.1: exactly one premise depends on an X axiom, say Cp . Then Cp′ is present in
ψi , and by Item 4 of Definition 17 the other premise Cq is present in ψi if and only if
the conclusion Ck is.
Case 2.2: both premises depend on an X axiom. Then both Cp′ and Cq′ are present inψi .
Therefore in both subcases it is enough to prove that Ck ∈ ψi , since then we can takeCk′ = Ck and we have that Ck ↾σi follows from a valid semantic resolution step. Assume
for the sake of contradiction that Ck ∈/ ψi . Then for Item 3 of Definition 17 not to apply
it must be that r(Ck ) does not contain any variable from Xi . By Lemma 16 Ck ↾σi is aclause supported on W variables, which by definition of Cti implies that k = ti . However,since the pivot is a W variable, Cp′ ↾σi is also supported on W variables and, together
with the fact that Cp′ depends on an X axiom, this contradicts that Cti is the first such
clause.
This finishes the induction argument and proves that ψi [1, ti ]↾σi is a valid semantic
derivation, from where it follows that s(ψi [1, ti ]↾σi ) is a valid syntactic derivation. It also
follows from the induction hypothesis that ti ≤ t: since Ct is left untouched by σi anddepends on an X axiom, there exists a clause Ct′ ∈ ψi that depends on an X axiom andsuch that Ct′ ↾σi ⊨ Ct ↾σi = Ct , which is supported on W variables.
◀
Having established that each ψi is a valid derivation, we show that they are large in thefollowing two lemmas.
▶ Lemma 21. For each i ∈ [m] the clause Cti ↾σi depends on an X axiom with respect toderivation s(ψi [1, ti ]↾σi ).
Proof. We prove by induction that for every clause Dk ∈ s(ψi [1, ti ]↾σi ), if Ck depends on an
X axiom (over ψ) then so does Dk (over s(ψi [1, ti ]↾σi )). This is immediate when Dk is anaxiom.
Otherwise fix Ck , Ek = Ck ↾σi , and Dk = s(Ek ), and let Ep = Cp ↾σi and Eq = Cq ↾σi be
the premises of Ek in the semantic derivation ψi [1, ti ]↾σi . When both Cp and Cq depend on
an X axiom, then by hypothesis so do Dp and Dq and we are done because at least oneof them is used to syntactically derive Dk . Otherwise one premise, say Cp , depends on an
X axiom and the other premise, say Cq , does not. In that case, because σi only affects X
variables, all the axioms used in the derivation of Cq are left untouched by σi , therefore wehave that Dq = Eq = Cq , which contains the pivot used to derive Ck and therefore Eq alone
does not imply Ek . In other words, the other premise Ep is semantically needed to derive
Ek , and thus Dp = s(Ep ) is syntactically used to derive Dk .
◀
▶ Lemma 22. Let η be a resolution derivation from Fℓ,1,n of a clause C supported on W
variables that depends on an X axiom. Then |η| ≥ (n − 2)(ℓ − µ(C))/2.
Proof. By Lemma 13 we can assume that η uses at least one Aj,b axiom for each j ∈ [ℓ].

S AT 2 0 2 3

27:14

Limits of CDCL Learning via Merge Resolution

Let J = {j ∈ [ℓ] | ∃wj,k ∈ vars(C)} be the set of W blocks mentioned by C. We showthat for each j ∈ J = [ℓ] \ J at least (n − 2)/2 axioms over variables in Wj appear in η, whichmakes for at least (n − 2)|J|/2 = (n − 2)(ℓ − µ(C))/2 axioms.
Fix j ∈ J and assume for the sake of contradiction that less than (n − 2)/2 axioms overvariables in Wj appear in η. Then there exists k ∈ [2, n − 1] such that variable wj,k does
not appear in η. Rename variables as follows: wj,k′ 7→ yk′ for k ′ < k, and wj,k′ 7→ yk′ −n fork ′ > k. Then we can prove by induction, analogously to the proof of Lemma 12, that every
clause derived from axiom Aj,b is of the form yk′ ∨ yk′′ ∨ D where D are literals supported
outside Wj . Since that includes C, it contradicts our assumption that j ∈/ J.
◀
To conclude the proof of Theorem 10 we simply need to put the pieces together.
Proof of Theorem 10. We take as the formula family Fℓ=48 log n,n,n , for which a resolution
refutation of length O(n log n) exists by Lemma 11.
To prove a lower bound we assume that a merge resolution refutation π of length
L ≤ n3 = 216ℓ = o((4/3)8ℓ ) exists; otherwise the lower bound trivially holds. We apply the
restriction given by Lemma 14 to π and we use Lemma 15 to obtain a resolution derivation ψof a clause supported on W variables that uses an X axiom. We then break ψ into m parts
ψi , each of size at least nℓ/16 as follows from Lemmas 20, 21, and 22. Finally by Lemma 18
we have |π| ≥ |ψ| ≥ mnℓ/32 = Ω(n2 log n).
◀

5.4Structural Consequences

Theorem 10 immediately gives us two unusual structural properties of merge resolution. One
is that proof length may decrease when introducing a weakening rule.
▶ Corollary 23. There exists a family of formulas over O(n log n) variables and O(n log n)clauses that have merge resolution with weakening refutations of length O(n log n) but every
merge resolution refutation requires length Ω(n2 log n).
Proof. Consider the formula Fn ∧ z, where Fn is the formula given by Theorem 10 and z isa new variable. If we weaken every clause C ∈ Fn to C ∨ z then we can derive F ∨ z ⊢ z inO(n log n) merge resolution steps because each inference is a merge. However, if we cannot
do weakening, then z cannot be resolved with any clause in Fn and the lower bound of
Theorem 10 applies.
◀
The second property is that merge resolution is not a natural proof systems in the senseof [5] because proof length may increase after a restriction.
▶ Corollary 24. There exists a restriction ρ and a family of formulas over O(n log n) variables
and O(n log n) clauses that have merge resolution refutations of length O(n log n) but every
merge resolution refutation of Fn ↾ρ requires length Ω(n2 log n).
Proof. Consider the formula Gn = (Fn ∨ z) ∧ z, where Fn is the formula given by Theorem 10,
F ∨ z = {C ∨ z | C ∈ F }, and z is a new variable. As in the proof of Corollary 23 there is amerge resolution derivation of z of length O(n log n) steps, while Gn ↾ρ = Fn .
◀

6

Further Proof Systems

In order to model CDCL with 1UIP more closely and possibly obtain a stronger separation we
look at restricted versions of merge resolution, which in this section we refer to as Resolution
with Merge Ancestors (RMA) to disambiguate it from the rest. The diagram in Figure 1 canhelp keeping track of these.

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:15

Resolution
10
RMA (Merge Res)
35
REL

33
LRMA

RML
34

34

LRML
35
Asserting CDCLLREML

1UIP CDCL

Figure 1 Relations between proof systems. A solid arrow A
B indicates that A simulates
B with no overhead. A dashed arrow A
B indicates that A simulates B with no overhead, but
B requires linear overhead to simulate A. Statements proving separations are referenced.

▶ Definition 25. A Resolution with Merge Ancestors (RMA) derivation is an input-structured
sequence of input resolution derivations where all derivations but the last contain a merge.
Note that by Lemma 5 it does not matter if we require the sequence of derivations of
an RMA derivation to be input derivations or if we allow general trees. In fact, our lower
bound results hold for a more general proof system where we only ask that every clause withoutdegree larger than 1 has an ancestor that is a merge. Such proof system does not havea simple input structure, but can rather be thought of as a sequence of tree-like resolution
derivations whose roots are merges, followed by a standard resolution derivation using theroots of the previous derivations as axioms.
To make the connection back to CDCL, we can define a proof system called Resolution
with Empowering Lemmas that captures CDCL refutations produced by solvers that use any
asserting learning scheme or 1-empowering learning scheme.
▶ Definition 26. Let C1 , . . . , CL−1 be the lemmas of an input-structured sequence of input
derivations. The sequence is a Resolution with Empowering Lemmas (REL) derivation of aformula F if Ci is 1-empowering with respect to F ∪ {Cj : j < i} for all i ∈ [1, L − 1].
It follows from Lemma 2 that such refutations are in RMA form.
▶ Observation 27. A REL derivation is a RMA derivation.
It might seem more natural to work with the REL proof system rather than its merge-based
counterparts, since REL is defined exactly through the 1-empowering property. However,while the merge property is easy to check because it is local to the derivation at hand, we canonly determine if a clause is 1-empowering by looking at the full history of the derivation,in particular what the previous lemmas are. This makes REL too cumbersome to analyse.
Furthermore, refutations produced by CDCL applying a clause minimization scheme on topof an asserting clause might not be in REL form, but they are still in RMA form.

S AT 2 0 2 3

27:16

Limits of CDCL Learning via Merge Resolution

We also discussed in Section 3 we that 1UIP CDCL solvers produce derivations wherelemmas themselves are merges. We call this proof system Resolution with Merge Lemmas,
or RML for short.
▶ Definition 28. A Resolution with Merge Lemmas (RML) derivation is an input-structured
sequence of input resolution derivations where all lemmas are merges.
We can be even more restrictive and observe that input derivations produced by a CDCL
solver that we describe next is that once a variable is resolved, it does not appear later inthe derivation.
▶ Definition 29. A resolution derivation η is strongly regular if for every resolution step i,the pivot variable xi is not amongst the variables of any clause Ci ∈ η[i, L]. A sequence of
derivations is locally regular if every derivation in the sequence is strongly regular. A LRML
derivation (resp. LRMA) is a locally regular RML derivation (resp. RMA).
Finally we can consider derivations that have empowering, merge lemmas and are locallyregular. These still include 1UIP proofs.
▶ Definition 30. A LREML derivation is a derivation that is both LRML and REL.
All of the proof systems we defined are quadratically separated from resolution simply
because they are weaker than RMA. At the same time, all of these proof systems still simulate
standard resolution up to linear overhead, as we show next.
Going back to the proof of Theorem 9, we first observe that the resulting RMA refutation
is in fact an RML refutation.
Recall that the proof idea is to maintain a set of clauses Gt such that all clauses in the
proof up to time t can be derived from Gt by input derivation. Then, given a new clause Ct+1
that can be obtained from Gt with a derivation η, we transform η into a merge resolution
derivation using Theorem 6, and we add its lemmas to Gt+1 . Since Theorem 6 produces
RML derivations, so is the final derivation we construct.
To make the simulation work also for LREML we need the following lemma.
▶ Lemma 31 ([23]). If F absorbs A ∨ x and B ∨ x, then F ⊢i C ′ ⊆ A ∨ B.
The simulation itself follows the general structure of Theorem 9, except that we needsome additional work to construct Gt+1 from Gt .
▶ Theorem 32. If F is a CNF formula over n variables that has a resolution refutation oflength L then it has a LREML refutation of length O(nL).
Proof. Let π = (C1 , . . . , CL ) be a resolution refutation. As we already showed it is enoughto construct a sequence of sets F = G0 ⊆ · · · ⊆ GL such that Gt \ F is the set of lemmas
in a LREML derivation from F of length at most (2n + 1)t, and π[1, t] ⊆ Cli (Gt ). Assume
we have built Gt and let C = Ct+1 . If C ∈ Cli (Gt ) we set Gt+1 = Gt and we are done.
Otherwise we showed that there are input resolution derivations of A′ ⊆ A and B ′ ⊆ B from
Gt of length at most n, which we can assume are strongly regular, and that A′ and B ′ canbe resolved together.
At this point we deviate from the proof of Theorem 9. We inductively build an intermediate
sequence of sets Gt = G0t ⊆ . . . ⊆ Gkt with the following properties.
1. Gjt is the set of lemmas in a LREML derivation from Gt of length at most p.
2. A′ and B ′ can be derived from Gjt in at most 2n − p resolution steps.

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

27:17

The base case G0t = Gt is trivial. For the inductive case, let us first assume that either A′
or B ′ is 1-empowering, say A′ . Let E be the first 1-empowering clause in the derivation of A′ .
By Lemma 2 E is a merge, therefore we are allowed to take Gj+1
= Gjt ∪ {E}. Furthermore,tj′′
if A and E could be derived from Gt in r and s steps, then A can be derived from Gj+1
intr − s steps, simply by omitting the first s steps in the derivation.
Otherwise, by Lemma 31 we reached a set Gjt such that C ∈ Cli (Gjt ). In this case wechoose k = j and Gt+1 = Gkt . Since Gt+1 can be obtained in p ≤ 2n steps from Gt , itsatisfies the required properties. This concludes both the inner and outer inductions.
◀
One consequence of the proof systems we introduce being polynomially equivalent toresolution is that they are conjectured to be incomparable with respect to the related RTL
and pool resolution proof systems, since these are conjectured to be exponentially weaker
than resolution. This would not be too unexpected given the different purposes of theproof systems: RTL and pool resolution were introduced to study restarts, and include
proofs produced by CDCL without restarts but any kind of learning, while the purpose ofmerge-based proof systems is to study learning, and include proofs produced by CDCL with
our without restarts but only asserting learning.
We can separate the different proof systems that we introduced using a few variations ofFℓ,m,n where we add a constant number of redundant clauses for each i ∈ [ℓ]. We present
the results that we obtain next, and defer the proofs to the appendix.
▶ Proposition 33. There exists a family of formulas over O(n log n) variables and O(n log n)clauses that have RMA refutations of length O(n log n) but every LRMA refutation requires
length Ω(n2 log n).
▶ Proposition 34. There exists a family of formulas over O(n log n) variables and O(n log n)clauses that have RML and LRMA and refutations of length O(n log n) but every LRML
refutation requires length Ω(n2 log n).
▶ Proposition 35. There exists a family of formulas over O(n log n) variables and O(n log n)clauses that have LRML refutations of length O(n log n) but every REL refutation requires
length Ω(n2 log n).

7

Concluding Remarks

In this paper, we address the question of the tightness of simulation of resolution proofs
by CDCL solvers. Specifically, we show that RMA, among other flavours of DAG-likemerge resolution, simulates standard resolution with at most a linear multiplicative overhead.
However, contrary to what we see in the tree-like case, this overhead is necessary. While
the proof systems we introduce help us explain one source of overhead in the simulation ofresolution by CDCL, it is not clear if they capture it exactly. In other words, an interesting
future direction would be to explore whether it is possible for CDCL to simulate some flavourof merge resolution with less overhead than what is required to simulate standard resolution.
References
1
2

Peter B. Andrews. Resolution with merging. J. ACM, 15(3):367–381, 1968.
Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms withmany restarts and bounded-width resolution. Journal of Artificial Intelligence Research,
40:353–373, January 2011. Preliminary version in SAT ’09.

S AT 2 0 2 3

27:18Limits of CDCL Learning via Merge Resolution

3

Gilles Audemard, Lucas Bordeaux, Youssef Hamadi, Saïd Jabbour, and Lakhdar Sais. A
generalized framework for conflict analysis. In Hans Kleine Büning and Xishun Zhao, editors,
Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference,
SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, volume 4996 of Lecture Notes in
Computer Science, pages 21–27. Springer, 2008. doi:10.1007/978-3-540-79719-7\_3.

4

Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve realworld SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence(AAAI ’97), pages 203–208, July 1997.

5

Paul Beame, Henry Kautz, and Ashish Sabharwal. Towards understanding and harnessing thepotential of clause learning. Journal of Artificial Intelligence Research, 22:319–351, December
2004. Preliminary version in IJCAI ’03.

6

Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL
solvers and QBF resolution. In James R. Lee, editor, 12th Innovations in Theoretical Computer
Science Conference, ITCS 2021, January 6-8, 2021, Virtual Conference, volume 185 of
LIPIcs, pages 12:1–12:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:
10.4230/LIPIcs.ITCS.2021.12.

7

Avrim L Blum and Merrick L Furst. Fast planning through planning graph analysis. Artificial
intelligence, 90(1-2):281–300, 1997.

8

Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn
Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of
Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233–350. IOS Press, 2ndedition, 2021. doi:10.3233/FAIA200990.

9

Samuel R. Buss, Jan Hoffmann, and Jan Johannsen. Resolution trees with lemmas: Resolution refinements that characterize DLL-algorithms with clause learning. Logical Methods in
Computer Science, 4(4:13), December 2008.

10

Cristian Cadar, Vijay Ganesh, Peter M Pawlowski, David L Dill, and Dawson R Engler. EXE:
Automatically Generating Inputs of Death. ACM Transactions on Information and System
Security (TISSEC), 12(2):1–38, 2008.

11

Alvaro del Val. Tractable databases: How to make propositional unit resolution complete
through compilation. In Jon Doyle, Erik Sandewall, and Pietro Torasso, editors, Proceedingsof the 4th International Conference on Principles of Knowledge Representation and Reasoning(KR’94). Bonn, Germany, May 24-27, 1994, pages 551–561. Morgan Kaufmann, 1994.

12

Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of thefunctionality of a conflict-driven SAT solver. In João Marques-Silva and Karem A. Sakallah,
editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International
Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in
Computer Science, pages 287–293. Springer, 2007. doi:10.1007/978-3-540-72788-0\_27.

13

Julian Dolby, Mandana Vaziri, and Frank Tip. Finding Bugs Efficiently With a SAT Solver.
In Proceedings of the 6th joint meeting of the European Software Engineering Conference andthe ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages
195–204, 2007. doi:10.1145/1287624.1287653.

14

Nick Feng and Fahiem Bacchus. Clause size reduction with all-uip learning. In Luca Pulina
and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd
International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture
Notes in Computer Science, pages 28–45. Springer, 2020. doi:10.1007/978-3-030-51825-7\_3.

15Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, and Allen Van Gelder. Clause learning caneffectively P-simulate general propositional resolution. In Proceedings of the 23rd National
Conference on Artificial Intelligence (AAAI ’08), pages 283–290, July 2008.

16

Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh. Towards acomplexity-theoretic understanding of restarts in sat solvers. In Theory and Applications of

M. Vinyals, C. Li, N. Fleming, A. Kolokolova, and V. Ganesh

17

18

19
20

21

22

23

24
25

26

27
28

29

30

27:19

Satisfiability Testing–SAT 2020: 23rd International Conference, Alghero, Italy, July 3–10,
2020, Proceedings 23, pages 233–249. Springer, 2020.
João Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers.
In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of
Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications,pages 133–182. IOS Press, 2021. doi:10.3233/FAIA200987.
João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional
satisfiability. IEEE Transactions on Computers, 48(5):506–521, May 1999. Preliminary version
in ICCAD ’96.
Burkhard Monien and Ewald Speckenmeyer. Solving satisfiability in less than 2n steps. Discret.
Appl. Math., 10(3):287–295, 1985. doi:10.1016/0166-218X(85)90050-2.
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik.
Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation
Conference (DAC ’01), pages 530–535, June 2001.
Nathan Mull, Shuo Pang, and Alexander A. Razborov. On CDCL-based proof systems with theordered decision strategy. In Proceedings of the 23rd International Conference on Theory andApplications of Satisfiability Testing (SAT ’20), volume 12178 of Lecture Notes in Computer
Science, pages 149–165. Springer, July 2020.
Knot Pipatsrisawat and Adnan Darwiche. A new clause learning scheme for efficient unsatisfiability proofs. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the Twenty-Third
AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17,
2008, pages 1481–1484. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/
aaai08-243.php.
Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as
resolution engines. Artificial Intelligence, 175(2):512–525, February 2011. Preliminary versionin CP ’09.
Lawrence Ryan. Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon
Fraser University, 2004.
Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Proceedings of the 12th
International Conference on Theory and Applications of Satisfiability Testing (SAT ’09),
volume 5584 of Lecture Notes in Computer Science, pages 237–243. Springer, July 2009.
Allen Van Gelder. Pool resolution and its relation to regular resolution and DPLL with clauselearning. In Proceedings of the 12th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR ’05), volume 3835 of Lecture Notes in Computer
Science, pages 580–594. Springer, 2005.
Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the34th AAAI Conference on Artificial Intelligence (AAAI ’20), pages 1652–1659, February 2020.
Yichen Xie and Alexander Aiken. Saturn: A SAT-Based Tool for Bug Detection. In Proceedingsof the 17th International Conference on Computer Aided Verification, CAV 2005, pages 139–143,
2005. doi:10.1007/11513988\_13.
Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict
driven learning in Boolean satisfiability solver. In Proceedings of the IEEE/ACM International
Conference on Computer-Aided Design (ICCAD ’01), pages 279–285, November 2001.
Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Hui Liang, Krzysztof
Czarnecki, and Vijay Ganesh. The effect of structural measures and merges on SAT solver
performance. In John N. Hooker, editor, Principles and Practice of Constraint Programming- 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings,
volume 11008 of Lecture Notes in Computer Science, pages 436–452. Springer, 2018. doi:
10.1007/978-3-319-98334-9\_29.

S AT 2 0 2 3