QCDCL with Cube Learning or Pure Literal Elimination - What is Best?

1 Introduction

SAT solving has revolutionised the way we perceive computationally hard problems. Determining the satisfiability of propositional formulas (SAT) has traditionally been viewed as intractable due to its NP completeness. In contrast, modern SAT solvers today routinely solve huge industrial instances of SAT from a wide variety of application domains [Biere et al., 2021a]. This success of solving has not stopped at SAT, but in the last two decades was lifted to increasingly more challenging computational settings, with solving quantified Boolean formulas (QBF)-a PSPACE-complete problem-receiving key attention [Beyersdorff et al., 2021].

Conflict driven clause learning (CDCL) is the main paradigm of modern SAT solving [Marques Silva et al., 2021]. Based on the classic DPLL algorithm from the 1960s, it combines a number of advanced features, including clause learning, efficient Boolean constraint propagation, decision heuristics, restart strategies, and many more. In QBF there exist several competing approaches to solving, with lifting CDCL to the quantified level in the form of QCDCL as one of the main paradigms [Zhang and Malik, 2002], implemented e.g. in the state-of-the-art solvers DepQBF [Lonsing and Egly, 2017] and Qute [Peitl et al., 2019].

For SAT/QBF solving, two questions of prime theoretical and practical importance are: (1) why are SAT/QBF solvers so effective and on which formulas do they fail? (2) Which solving ingredients are most important for their performance?

For (1), proof complexity offers the main theoretical approach to analyse the strength of solving [Buss and Nordstr¨om, 2021]. In a breakthrough result, Pipatsrisawat and Darwiche [2011] and Atserias et al. [2011] established that CDCL on unsatisfiable formulas is equivalent to the resolution proof system, in the sense that from a CDCL run a resolution proof can be efficiently extracted [Beame et al., 2004], and conversely, each resolution proof can be efficiently simulated by CDCL [Pipatsrisawat and Darwiche, 2011]. Hence the well-developed proof-complexity machinery for proof size lower bounds in resolution [Kraj´ıˇcek, 2019] is directly applicable to show lower bounds for running time in CDCL.

The latter simulation of resolution by CDCL assumes a strong 'non-deterministic' version of CDCL, whereas practical CDCL (using decision heuristics such as VSIDS) has been recently proved to be exponentially weaker than resolution [Vinyals, 2020]. In contrast, an analogous proof-theoretic characterisation is not known for QCDCL, and in particular QCDCL has recently been shown to be incomparable to QResolution [Beyersdorff and B¨ohm, 2021], the QBF analogue of propositional resolution [Kleine B¨uning et al., 1995].

Regarding question (2) above, there are some experimental studies [Sakallah and Marques-Silva, 2011; Elffers et al., 2018; Kokkala and Nordstr¨om, 2020], but no rigorous theoretical results are known on which (Q)CDCL ingredients are most crucial for performance. Of course, gaining such a theoretical understanding would also be very valuable in guiding future solving developments.

In this paper, we contribute towards question (2) in QBF.

1.1 Contributions

Following the approach of Beyersdorff and B¨ohm [2021], we model QCDCL as rigorously defined proof systems that are amenable to a proof-complexity analysis. This involves formalising individual QCDCL ingredients, such as clause and cube learning and different variants of Boolean constraint propagation. These can then be 'switched' on or off, resulting in a number of different QCDCL solving models that we can formally investigate. Our results can be summarised as follows.

(a) QCDCL with or without cube learning. In contrast to SAT solving, where there is somewhat of an asymmetry between satisfiable and unsatisfiable formulas, QCDCL implements a dual approach for false and true QBFs. In addition to learning clauses (as in CDCL) when running into a conflict under the current assignment, QCDCL also learns terms (or cubes) in the case a satisfying assignment is found (or a previously learned cube is satisfied). While cube learning is necessary to make QCDCL solving complete on true QBFs, it is less clear what the effect of cube learning is on false QBFs (and we only consider those throughout the paper as we cast all our models in terms of refutational proof systems, in accordance with the proof complexity analysis of SAT [Buss and Nordstr ¨om, 2021]). Here we establish the perhaps surprising result that even for false QBFs, cube learning can be advantageous, in the sense that QCDCL without cube learning (as a proof system for false QBFs) is exponentially weaker than QCDCL with cube learning.

(b) QCDCL with or without pure-literal elimination. In its simplest form, Boolean constraint propagation, used to construct trails in (Q)CDCL, implements unit propagation. However, further methods can be additionally employed (and are considered in pre- and in-processing [Biere et al., 2021b]). One of the classic mechanisms is pure-literal elimination, setting a pure literal (which occurs in only one polarity) to the obvious value. This is e.g. implemented in DepQBF and an efficient implementation is described by Lonsing [2012].

We show that QCDCL with or without pure-literal elimination results in incomparable proof systems, i.e., there are QBFs that are easy in QCDCL with pure literal elimination, but hard in plain QCDCL, and vice versa (the latter is perhaps more surprising).

(c) Comparing QCDCL extensions. Given the preceding results, it is natural (and possibly most interesting for practice) to ask how the different QCDCL extensions compare with each other. We consider QCDCL with cube learning, QCDCL with pure-literal elimination but without cube learning, and QCDCL with both cube learning and pureliteral elimination. Except for the simulation of the second by the third system, we again obtain incomparability results between the systems with exponential separations. We further show that all these systems are incomparable to QResolution, again via exponential separations. An overview of the systems and their relations is given in Figure 1.

Technically, our results rest on formalising QCDCL systems as proof calculi and exhibiting specific QBFs for their separations. The latter includes both the explicit construction of short QCDCL runs and proving exponential proof size lower bounds for the relevant calculi. For the lower bounds, we identify a property of proofs (called primitivity here) that allows to use proof-theoretic machinery of B¨ohm and Beyersdorff [2021] in the context of our QCDCL systems.

Our theoretical results on the strength of different QCDCL models are empirically confirmed by experiments with stateof-the-art QCDCL solvers (cf. Section 8).

Organisation. We start in Section 2 by reviewing QBFs and Q-Resolution. In Section 3 we model variants of QCDCL as formal proof systems and develop a lower technique for such systems in Section 4. Sections 5 to 8 then contain our results on the relative strength of QCDCL variants. We conclude in Section 9 with an outlook on future research.

Due to space constraints, some details are omitted.

2 Preliminaries

We will use standard notions from propositional logic, such as variables, literals, (propositional) formulas, clauses, conjunctive normal form (CNF), disjunctive normal form (DNF), assignments, satisfiability or restrictions. A cube (or term) is a conjunction of literals. A literal ℓ in a formula Φ is pure, if it only appears in one polarity (i.e., if ℓ is contained in Φ, but ¯ ℓ is not). We define two "empty" literals K and J.

A QBF (quantified Boolean formula) Φ � Q � φ consists of a propositional formula φ, called the matrix (denoted by CpΦq), and a prefix Q. A prefix Q � Q11V1 . . .Q1sVs consists of non-empty and pairwise disjoint sets of variables V1, . . . , Vs and quantifiers Q11 , . . . ,Q1s P tD, @u with Q1i � Q1i`1 for i P rs�1s. For a variable x in Q, the quantifier level is lvpxq :� lvΦpxq :� i, if x P Vi. For lvΦpℓ1q � lvΦpℓ2q we write ℓ1 �Φ ℓ2.

We use the proof systems Q-resolution [Kleine B¨uning et al., 1995] and long-distance Q-resolution [Balabanov and Jiang, 2012], containing resolution and reduction rules. In general, a clause C can be reduced universally, while a cube D can be reduced existentially. We denote the maximally universally (resp. existentially) reduced clause (resp. cube) by red@ΦpCq (resp. redDΦpDq).

3 Formal Calculi for QCDCL Versions

In this section we model different versions of QCDCL as formal proof systems (we sketch this only here; for background on QCDCL cf. [Beyersdorff et al., 2021]). For this we need to formalise QCDCL ingredients. We start with trails. A trail T for a QCNF Φ is a finite sequence of literals from Φ, including the empty literals K and J. In general, a trail has the form

where the di are decision literals and ppi,jq are propagated literals. Decision literals are written in boldface. We use a semicolon before each decision to mark the end of a decision level. We write x �T y if x, y P T and x is left of y in T .

Trails can be interpreted as non-tautological sets of literals, and therefore as (partial) assignments. If T is a trail, then T ri, js, for i P t0, . . . , ru and j P t0, . . . , giu, is defined as the subtrail that contains all literals from T left of (and excluding) ppi,jq (resp. di, if j � 0). A trail T has run into conflict if K P T or J P T .

Simply put, our QCDCL proof systems can be interpreted as sequences of trails. These trails cannot be created arbitrary, but have to follow special rules, depending on the model. We consider the following four QCDCL variants:

• QCDCL, which can be seen as the plain model where we can only make decisions following the level order of the quantifier prefix, make propagations using clauses and use classic clause learning. We will never learn or use cubes and pure-literal elimination is turned off.
• QCDCL CUBE is an extension of QCDCL in which we can learn cubes and use them for propagations. Decisions are still level-ordered and pure-literal elimination is turned off.
• QCDCL PL is an extension of QCDCL, where we decide literals out of order if they are pure in the current configuration (pure-literal elimination). All other decisions (which we call regular decisions) are still level ordered. Cube learning is turned off.
• QCDCL CUBE+PL is an extension of QCDCL PL , in which cube learning is now allowed (as in QCDCL CUBE ).

Note that decisions can only be made if there are no more propagations possible and pure literal decisions always have a higher priority than regular decisions. Also, conflicts have a higher priority than propagations of proper (existential or universal) literals. Hence, we will never skip conflicts, propagations or pure literal decisions. For each propagated literal ppi,jq in a trail T the formula must contain a clause or a cube that caused this propagation by becoming a unit clause/cube. We denote such a clause/cube by anteT pppi,jqq.

After a trail has run into a conflict, or if all variables were assigned, we can start the learning process.

Definition 1 (learnable constraints). Let T be a trail for Φ of the form (3.1) with ppr,grq P tK, Ju. Starting with anteT pKq (resp. anteT pJq) we reversely resolve over the antecedent clauses (cubes) that propagated the existential (universal) variables, until we stop at some arbitrarily chosen point. The clause (cube) we so derive is a learnable constraint. We denote the set of learnable constraints by LpT q.

We can also learn cubes from trails that did not run into conflict. If T is a total assignment of the variables from Φ, then we define the set of learnable constraints as the set of cubes LpT q :� tredDΦpDq| D � T and D satisfies CpΦqu.

Definition 2 (QCDCL proof systems). Let S be one of QCDCL, QCDCL CUBE , QCDCL PL , QCDCL CUBE+PL . An S proof ι from a QCNF Φ � Q � φ of a clause or cube C is a sequence of triples

where Cm � C, each Ti is a trail, each Ci P LpTiq is one of the constraints we can learn from the trail, and πi is the longdistance Q-resolution or long-distance Q-consensus proof of Ci we get by performing the steps in Definition 1. We define Rpιq as the proof of C we get by sticking together suitable πi. We denote the set of trails in ι as Tpιq.

If C � pKq, then ι is called an S refutation of Φ. If C � rJs, then ι is an S verification of Φ. The proof ends once we have learned pKq or rJs. The size of ι is |ι| :� �mi"1 |Ti|.

Theorem 1. QCDCL, QCDCL CUBE , QCDCL PL , and QCDCL CUBE+PL are sound and complete proof systems.

We highlight that these systems formally model QCDCL solving as used in practice (cf. [Beyersdorff et al., 2021]).

4 Proving Lower Bounds for QCDCL Systems

Throughout the paper we will concentrate on Σb3 QCNFs which we alway assume to have the form Φ � DX@UDT � φ for non-empty blocks of variables X, U, and T .

A literal ℓ is an X-literal, if varpℓq P X. Analogously, we get U- and T-literals and variables. A clause C P CpΦq is an X-clause, if all its literals are X-literals. The empty clause pKq is also an X-clause. Analogously, we define T-clauses. A clause C P CpΦq is an XT-clause, if it contains at least one X-literal, at least one T -literal, but no U-literals; analogously we define UT-clauses. A clause C P CpΦq is an XUT-clause if it contains at least one X-, U- and T- literal.

Definition 3. We say that Φ fulfils the XT-property, if CpΦq contains no XT-clauses, no T-clauses that are unit (or empty) and no two T-clauses from CpΦq are resolvable.

As shown by B¨ohm and Beyersdorff [2021], clause learning does not affect the XT-property, i.e., a formula Φ with the XT-property will still fulfil it during the whole QCDCL run even after having added new clauses to CpΦq.

Next we recall the definition of formula gauge from [B¨ohm and Beyersdorff, 2021], which represents a measure that can be used for lower bounds.

Definition 4 ([B¨ohm and Beyersdorff, 2021]). For a QCNF Φ as above let WΦ be the set of all Q-resolution derivations π from Φ of some X-clause such that π only contains resolutions over T-variables and reduction steps. We set gaugepΦq :� mint|C| : C is the root of some π P WΦu.

We now define fully reduced and primitive proofs. Our lower bound technique will then work for fully reduced primitive refutations of formulas that fulfil the XT-property.

Definition 5. A long-distance Q-resolution refutation π of a QCNF Φ is called fully reduced, if the following holds: For each clause C P π that contains universal literals that are reducible, the reduction step has to be performed immediately and C cannot be used otherwise in the proof.

Each proof Rpιq that was extracted from a QCDCL proof ι is automatically fully reduced, as we perform reduction steps as soon as possible during clause learning. On the other hand, primitivity does not hold for proofs Rpιq in general. In fact, the main work in proving our hardness results will be to show that specific extracted proofs are primitive.

Definition 6. A long-distance Q-resolution proof π from a Σb3 formula with the XT-property is primitive, if there are no two XUT-clauses in π that are resolved over an X-variable.

Since it is not possible to derive tautological clauses in fully reduced primitive proofs, we may also refer to them as (fully reduced) primitive Q-resolution proofs.

It follows from [B¨ohm and Beyersdorff, 2021], that these two conditions suffice to show lower bounds via gauge.

Theorem 2 ([B¨ohm and Beyersdorff, 2021]). Each fully reduced primitive Q-resolution refutation of a Σb3 QCNF Φ that fulfils the XT-property has size 2ΩpgaugepΦqq .

The next two results represent the main methodology for most of our hardness results throughout the paper.

Lemma 1. Let T be a trail in a QCDCL, QCDCL CUBE , QCDCL PL or QCDCL CUBE+PL proof from a QCNF Φ with the XT-property. Then for each T-literal t1 P T , which was not decided by pure literal elimination, there is a U-literal u P T with u �T t1.

Proposition 1. Let ι be a QCDCL, QCDCL CUBE , QCDCL PL or QCDCL CUBE+PL refutation of a QCNF Φ that fulfils the XTproperty. If Rpιq is not primitive, then there exists a trail T P Tpιq such that there is a U-literal u P T and an Xliteral x P T with u �T x. Additionally, u cannot be a regular decision literal.

Basically, this result tells us that for a non-primitive proof Rpιq of some S proof ι, where S is one of our four QCDCL variants, ι needs to consist of a trail that assigns a U-literal out-of-order (i.e., before we have assigned all X-literals).

Since neither cube learning nor pure literal elimination is allowed in QCDCL, we can immediately conclude:

Corollary 1. Let ι be a QCDCL refutation of a QCNF Φ that fulfils the XT-property. Then Rpιq is primitive.

We remark that some of the QBFs we introduce in the paper are not minimally false, i.e., we have added extra clauses to formulas that were false already. Although this is unusual in proof complexity, practical (false) instances are not guaranteed to be minimally false. Therefore it is natural to also consider these QBFs when investigating QCDCL systems. These algorithmic proof systems have to utilize all clauses, even if they are redundant for Q-resolution refutations.

5 Plain QCDCL vs. QCDCL with Cubes/PL

We start by examining the influence of cube learning on our QCDCL model. For false formulas we can always prevent learning cubes by just deciding the universal variables according to a winning strategy for the universal player, which will cause a conflict on the current trail. Thus cube learning will never be disadvantageous in principle.

Proposition 2. QCDCL CUBE p-simulates QCDCL and QCDCL CUBE+PL p-simulates QCDCL PL .

We recall the equality formulas Eqn of Beyersdorff et al. [2019a]. These are QCNFs with prefix Dx1 . . . xn@u1 . . . unDt1 . . . tn and matrix

The formulas are known to be hard for Q-resolution [Beyersdorff et al., 2019a] and also for QCDCL [Beyersdorff and B¨ohm, 2021]. In contrast, we show that they are easy in QCDCL with cube learning.

Proposition 3. There exist polynomial-size QCDCL CUBE refutations of Eqn .

Proof Sketch. First we learn the cubes xi^¯ui and ¯xi^ui for i P rn � 1s. E.g., to learn x1 ^ ¯u1, we use the trail

Then the partial assignment x1 ^ ¯u1 ^ ¯ t1 ^ t2 ^ . . . ^ tn satisfies the matrix of Eqn . Reducing this cube existentially results in x1 ^ ¯u1, hence x1 ^ ¯u1 P LpT1q.

Having learnt all these 2n � 2 cubes, we learn the clauses Li :� ¯xi _ ¯ui _ �nj"i`1 puj _ ¯ujq _ �i´1 k"1 ¯ tk and Ri :� xi _ui _�nj"i`1 puj _ ¯uj q_�i´1 k"1 ¯ tk, starting with i � n�1 and down to i � 2. E.g., to learn Ln´1 we use the trail

where ui are propagated directly after xi by the learnt cubes. We resolve over xn, ¯ tn, and tn´1 to get Ln´1.

Having finally learnt L2 and R2, we form the trail U1 :� px1, u1, t1, x2,Kq with anteU1 px2q � R2 and anteU1 pKq � L2 and learn p¯x1q. Then the last trail p¯x1, ¯u1, t1, x2, Kq yields the empty clause.

As the formulas Eqn require exponential-sized QCDCL refutations [Beyersdorff and B¨ohm, 2021] we obtain:

Theorem 3. QCDCL CUBE is exponentially stronger than QCDCL.

Next we will look at the influence of pure literal elimination. Now, the effect of pure literal elimination is similar to cube learning: they enable out-of-order decisions that can shorten the refutations. This again manifests in Eqn .

Proposition 4. Eqn has poly-size QCDCL PL (and QCDCL CUBE+PL ) refutations.

Although pure literal elimination helps to refute Eqn , it turns out that pure literal elimination can also be disadvantageous. It might be a fallacy to think that pure existential literals should be satisfied in the same way as unit clauses in unit propagation. We will construct formulas in which pure literal elimination thwarts finding a convenient conflict and therefore short refutations.

We construct these formulas in stages, starting with MirrorCRn. In turn, these QBFs are based on the Completion Principle CRn of Janota [2016], known to be hard for QCDCL [Janota, 2016; B¨ohm and Beyersdorff, 2021]. The "Mirror"-modification adds new symmetries to the formula, causing pure literals to appear too late to make a difference.

Definition 7. The QCNF MirrorCRn consists of the prefix Dxp1,1q, . . . , xpn,nq@uDa1, . . . , an, b1, . . . , bn and the matrix xpi,jq _ u _ ai, ¯a1 _ . . . _ ¯an, ¯xpi,jq _ ¯u _ bj , ¯b1 _ . . . _ ¯bn xpi,jq _ ¯u _ ¯ai, a1 _ . . . _ an, ¯xpi,jq _ u _ ¯bj , b1 _ . . . _ bn for i, j P rns.

It is easy to see that MirrorCRn fulfil the XT-property. Additionally, we can show:

Proposition 5. The CNF CpMirrorCRnq is unsatisfiable and gaugepMirrorCRnq ¥ n � 1.

Applying Theorem 2 we infer:

Corollary 2. MirrorCRn needs exponential-size fully reduced primitive Q-resolution refutations.

All we have to do now is to show that all QCDCL PL refutations of MirrorCRn are primitive. Then the gauge lower bound applies. We will show that for a non-primitive refutation of MirrorCRn we would need to decide literals by pure literal elimination, and before each pure literal elimination we have to perform another one, which is a contradiction.

Proposition 6. From each QCDCL PL refutation of MirrorCRn we can extract a fully reduced primitive Q-resolution refutation of the same size.

Proof Sketch. We show that Rpιq is primitive if ι is a QCDCL PL refutation of MirrorCRn. Assume that some Rpιq is not primitive. Therefore, by Proposition 1, a U-literal was decided as a pure literal before all X-variables were assigned. However, such a situation is impossible due to the formula structure, resulting in a contradiction.

Corollary 3. The QBFs MirrorCRn require exponential-size QCDCL PL refutations.

Next we embed this formula into a new QCNF PLTrapn .

Definition 8. The QCNF PLTrapn has the prefix Dy, xp1,1q, . . . , xpn,nq@uDa1, . . . , an, b1, . . . , bn, a, b. Its matrix contains all clauses from MirrorCRn and additionally py _aq, p¯a_ bq, p¯a_¯bq, pa_ bq, and pa_¯bq.

Proposition 7. PLTrapn needs exponential-size QCDCL PL and QCDCL CUBE+PL refutations.

Not having to follow the PLD rule, we can construct short proofs of PLTrapn by focusing on the new clauses over a, b.

Proposition 8. PLTrapn has polynomial-size QCDCL refutations.

We conclude that pure literal elimination is advantageous for Eqn , but not for PLTrapn . Therefore we obtain:

Theorem 4. QCDCL PL and QCDCL are incomparable as well as QCDCL CUBE+PL and QCDCL.

6 Cube Learning vs. Pure Literal Elimination

As shown in Section 5, cube learning improves QCDCL, while adding pure literal elimination leads to incomparable systems. Thus it is natural to directly compare cube learning and pure literal elimination. Because of the results above, we cannot use Eqn for a potential separation. However, we can modify the QBFs such that they remain easy for QCDCL PL , while eliminating the benefits from cube learning.

Definition 9. The QCNF TwinEqn has the prefix Dx1, . . . , xn@u1, . . . , un,w1, . . . ,wnDt1, . . . , tn. Its matrix contains the clauses from Eqn together with xi _wi _ ti and ¯xi _ ¯wi _ ti for i P rns.

The main idea of this twin construction is to ensure that all potential cubes consist of at least two universal variables. We can do the same construction for other QCNFs.

Obviously, TwinEqn fulfils the XT-property. We compute gaugepTwinEqn q � n and hence infer by Theorem 2:

Proposition 9. Fully reduced primitive Q-resolution refutations of TwinEqn have exponential size.

We show that QCDCL CUBE refutations of TwinEqn are primitive by proving that it is impossible to propagate Uliterals before having assigned all X-literals.

Proposition 10. Each QCDCL CUBE refutation of TwinEqn has at least exponential size.

Having shown that TwinEqn is hard for QCDCL CUBE , it remains to prove that it is easy for QCDCL PL .

Proposition 11. TwinEqn has polynomial-size QCDCL PL refutations.

For the other separation we use PLTrapn , which is hard for QCDCL PL , but still easy for QCDCL CUBE by Proposition 2. Therefore we conclude:

Theorem 5. QCDCL CUBE is incomparable to QCDCL PL .

We have seen earlier that the QCDCL system including pure literal elimination is incomparable to the system without. Now we will prove that this incomparability still holds with cube learning turned on. By Proposition 2, we obtain that QCDCL CUBE+PL p-simulates QCDCL PL . Therefore we get from Proposition 11:

Corollary 4. TwinEqn has poly-size QCDCL CUBE+PL refutations.

Since TwinEqn is hard for QCDCL CUBE , this gives us the first separation between QCDCL CUBE+PL and QCDCL CUBE . The other direction can be shown with PLTrapn .

Proposition 12. PLTrapn has poly-size QCDCL CUBE refutations.

Hence we get:

Theorem 6. QCDCL CUBE+PL and QCDCL CUBE are incomparable.

We now consider the relation between QCDCL CUBE+PL and QCDCL PL . We introduce another modification of Eqn , which we call BulkyEqn , where we add two clauses.

Definition 10. The QCNF BulkyEqn is obtained from Eqn by adding the clauses u1 _ . . . _ un _ t1 _ . . . _ tn and ¯u1 _ . . . _ ¯un _ t1 _ . . . _ tn to the matrix.

As Eqn , this formula fulfils the XT-property and has a high gauge value (¥ n�1). By Theorem 2 we infer that BulkyEqn needs exponential-size fully reduced primitive Q-resolution refutations. Similarly to MirrorCRn, we can then show that pure literal elimination does not shorten proofs because of the two additional 'bulky' clauses that prevent pure literals to occur early in trails. Therefore BulkyEqn is hard for QCDCL PL . On the other hand, we can explicitly construct short proofs in QCDCL CUBE+PL . Therefore we get:

Proposition 13. BulkyEqn has poly-size QCDCL CUBE+PL

refutations, but needs exponential-size QCDCL PL refutations. As for the systems without pure literal elimination, we get: Theorem 7. QCDCL CUBE+PL is exponentially stronger than QCDCL PL .

7 The QCDCL Systems vs. Q-resolution

Beyersdorff and B¨ohm [2021] showed incomparability of Qresolution and QCDCL. We now lift this to the other QCDCL variants introduced here. For one separation, we can use the QCNF QParityn from [Beyersdorff et al., 2019b], which have short QCDCL refutations. These formulas have prefix Dx1 . . . xn@uDt1 . . . tn and clauses

Theorem 8. QCDCL, QCDCL CUBE , QCDCL PL and QCDCL CUBE+PL are all incomparable to Q-resolution.

In detail, the QBFs QParityn have polynomial-size QCDCL, QCDCL CUBE , QCDCL PL , and QCDCL CUBE+PL refutations, but need exponential-size Q-resolution refutations. On the other hand, MirrorCRn have polynomial-size Qresolution refutations, but need exponential-size QCDCL, QCDCL CUBE , QCDCL PL , and QCDCL CUBE+PL refutations.

8 Experiments

We study proof systems in the hope that proof-complexity results will translate to running-time complexity for solvers. In this section we do our reality check to see whether this hypothesis holds up experimentally.

We picked the solver DepQBF [Lonsing and Egly, 2017], as it is the only one that supports pure-literal elimination (PLE) and also has the ability to turn cube learning (SDCL) off. 1 We additionally ran Qute [Peitl et al., 2019] when we wanted to confirm DepQBF's surprising behaviour. Though, Qute only supports QCDCL CUBE of the systems discussed above, and so is poorly suited for most of our experiments.

We ran DepQBF on each of the formulas used for separations in this paper, as well as on the PCNF track of the QBF Evaluation 2020. 2 We set the time limit on each formula to 10 minutes (no memory limit). The computation was performed on a machine with two 16-core Intel® Xeon® E52683 v4@2.10GHz CPUs and 512GB RAM running Ubuntu 20.04.3 LTS on Linux 5.4.0-48, and organized with the help of GNU Parallel [Tange, 2011].

We discovered that heuristics have a significant impact on performance on theoretically easy formulas (theoretically hard formulas must be hard for solvers as well, and we confirm this in every case). We thus decided to run DepQBF

1 In order to obtain vanilla QCDCL in DepQBF, we set

--traditional-qcdcl --long-dist-res

--dep-man=simple --no-dynamic-nenofex

--no-trivial-truth --no-trivial-falsity.

2 http://www.qbflib.org/qbfeval20.php

E q

n

with each available heuristic, in order to paint a full picture. In total, we evaluated 24 configurations of DepQBF-with and without PLE and with and without SDCL, and for each of these four, with each of the 6 possible heuristics. 3

Figure 2 shows the results on Equality. While the formulas are easy using PLE regardless of the heuristic, without PLE DepQBF's performance fluctuates depending on the heuristic, even though the formulas are 'easy' as long as SDCL is on. Qute's performance is stabler, but still much worse than DepQBF with PLE. The formulas get hard without both PLE and SDCL, in line with [Beyersdorff and B¨ohm, 2021].

While both PLE and SDCL make Eq easy, PLE seems easier to exploit. Perhaps there is simply less room for error in applying PLE than in learning the right cubes. A mild advantage from PLE is also confirmed by DepQBF's results on QBF Eval formulas. This suggests that in spite of conceptual simplicity PLE can be quite useful, and perhaps should appear on Qute's feature roadmap.

9 Conclusion

While this paper only studies false formulas (in accordance with proof complexity conventions), we expect similar phenomena of incomparability on true formulas, which we leave for future work to explore. Interestingly, while cube learning is primarily needed for true QBFs, we have shown that it can also improve the running time on false instances.

Technically, we believe that our new notion of primitive proofs has further potential for showing QCDCL lower bounds, also for QBFs of higher quantifier complexity. While previous results tried to lift lower bounds from Q-Resolution [Beyersdorff and B¨ohm, 2021], primitivity also applies to QBFs easy for Q-Resolution, thus supplying new reasons for QCDCL hardness.

3 Using --dec-heur= (--phase-heuristic for Qute).

Acknowledgements

Research was supported by grants from the Carl-Zeiss Foundation, Austrian Science Fund FWF grant no. J4361-N, and DFG grant BE 4209/3-1.