In this section, we will exponentially separate our three new models—where decisions do not necessarily follow the prefix order—from the plain model \(\mathsf{{QCDCL}} \).
The XT-property extends to entire QCDCL proofs, as stated in the next lemma.
Fully reduced proofs are not much of a limitation. In fact, all long-distance Q-resolution proofs that we extract from a \(\mathsf{{QCDCL}} \) run are already fully reduced by default. Also, we can always shorten a given long-distance Q-resolution proof by making it fully reduced.
All notions we introduced so far are combined into the following lower bound method:
The advantage of \(\textsf{QCDCL}^\textsf {{E\tiny {\MakeUppercase {xi}}-A\tiny {\MakeUppercase {ny}}}}\) (compared to \(\mathsf{{QCDCL}} \)) is to decide existential literals out of order while still learning asserting cubes. Since cubes are important for certificates of true formulas, it makes sense to use true QBFs for the separation.
First, we discuss two generic modifications for QBFs. The twin construction doubles all universal variables. For all clauses with universal variables a copy is created in the twin variables.
The second modification is the reversion of a formula.
It is easy to prove that there exists a duality between the truth values of \(\Phi \) and \(\text {Rev}(\Phi )\).
We will use the reversion to lift hardness from false to true QCNFs. To verify a true formula, we need to create a proof using cubes. We will show that \(\text {Rev}(\Phi )\) is designed such that its initial cubes are basically the negated axiom clauses of \(\Phi \). Thus, a certificate of \(\text {Rev}(\Phi )\) can be transformed into a refutation of \(\Phi \).
Our reversion was inspired by the notion of the
negation from [
19]. The only change we made is adding the variable
w. We did this to prevent a direct connection between an
X- or
U-block and an auxiliary variable
\(c_j\) from the last block. Our lower bound technique is based on the fact that on certain formulas we cannot have direct connections (hence: cannot directly propagate) between outer and inner quantifier blocks. The added variable
w helps to maintain this property.
The next two results shows how we can transform certificates of \(\text {Rev}(\Phi )\) into refutations of \(\Phi \) by interpreting the cubes from the certificate as negated clauses of a refutation.
For our next results, we need an even stronger property than the XT-property: We require, that clauses from the formula contain at least one U- and T-literal.
We combine the results above and obtain a new lower bound technique for true formulas, which builds on the gauge technique for false formulas.
We want to create a contradiction by applying the claim, for which we need to show that A does not contain any literal from \(\{ c_r,\bar{c}_r|\,r=1,\ldots ,m \}\).
Assume that there is such a literal. That means we can find the leftmost literal
\(c\in \{ c_r,\bar{c}_r|\,r=1,\ldots ,m \}\) in
\(\mathcal {T}\), hence
\(c<_\mathcal {T}\ell _u<_\mathcal {T}t<_\mathcal {T}x\). Now,
c cannot have been a decision since decisions must be level-ordered. That means that
c has been propagated by an antecedent clause
\(F:=\text {ante}_\mathcal {T}(c)\). Because
c was leftmost,
F cannot be the clause
\(\bar{c}_1\vee \ldots \vee \bar{c}_m\). It is easy to see that
F then has to contain either
w or
\(\bar{w}\) by the structure of a reversion (see Definition
12). W.l.o.g. let
\(w\in F\). Then we need
\(\bar{w}<_\mathcal {T}c<_\mathcal {T}\ell _u\). Because of the quantification order,
\(\bar{w}\) cannot be a decided literal. Hence
\(\bar{w}\) must have been propagated by some antecedent cube
\(E:=\text {ante}_{\mathcal {T}}(\bar{w})\). Let
\(\rho \) be the subproof of
E from
\(\mathfrak {R}(\iota )\). Then there exists an initial cube
\(G\in \rho \) with
\({w}\in G\), which is not getting resolved away in
\(\rho \). Furthermore,
G is also an initial cube in
\(\mathfrak {R}(\iota )\). By Lemma
9, there exists some
\(H\in \mathfrak {C}(\texttt{Twin}\Phi )\) such that
\(\overline{H}\subseteq G\). Since each clause of
\(\Phi \) contains a
U-literal, there is such a
U-literal
\(v\in \overline{H}\subseteq G\) and also
\(v\in E\) because it cannot be resolved or reduced away. This means we need
\(v<_\mathcal {T}\bar{w}<_\mathcal {T}\ell _u\), which is a contradiction to the choice of
\(\ell _u\).
We have now shown that A does not contain any \(c_r,\bar{c}_r\), \(r\in \{ 1,\ldots ,m \}\). However, this is impossible by our claim. We conclude that Case 1 cannot occur.
Case 2: t was propagated.
Consider the antecedent cube
\(J:=\text {ante}_{\mathcal {T}}(t)\). Let
\(\tau \) be the subproof of
J in
\(\mathfrak {R}(\iota )\). Then the first cubes in
\(\tau \) were (reduced) satisfying assignments for
\(\text {Rev}(\texttt{Twin}\Phi _n)\). At least one of these initial cubes in
\(\tau \) contains
\(\bar{t}\) which will not get resolved away since it appears in
J. Let
\(I\in \tau \) be an initial cube with
\(\bar{t}\in I\) that does not get resolved away in
\(\tau \). By Lemma
9, there exists a clause
\(K\in \mathfrak {C}(\texttt{Twin}\Phi _n)\) such that
\(\overline{K}\subseteq I\). By our assumption,
K contains at least one
U- and one
T-literal. But then also
I contains at least one
U-literal
\(\ell \). Because
\(\ell \) is blocked by
\(\bar{t}\) all the time, it does not get reduced away in
\(\tau \), hence
\(\ell \in J\).
Due to \(\ell <_{\text {Rev}(\texttt{Twin}\Phi _n)}t\), we need \(\ell <_\mathcal {T}t \) in order for J to become unit. W.l.o.g. let \(\ell \) be the leftmost U-literal in \(\mathcal {T}\) (the fact that \(\ell \in J\) is not important anymore from this point on). Because of \(x<_{\text {Rev}(\texttt{Twin}\Phi _n)}\ell \), the literal \(\ell \) cannot be a regular decision. That means it must have been propagated.
We can repeat the argument from Case 1. We conclude that such an \(\ell \) does not exist. Thus Case 2 does not occur and we get a contradiction regarding our assumption that \(\pi \) was not primitive. \(\square \)
We now construct specific QBFs that meet the conditions of Theorem
12. We already know from [
9] that the equality formulas
\(\texttt{Eq}_n\) of [
6] have linear gauge and therefore need exponential-size fully reduced primitive
Q-resolution refutations. However, not all clauses from
\(\texttt{Eq}_n\) contain a
U-literal. We modify the formulas by adding an artificial
U-literal
p to the relevant clauses:
Neither this nor the \(\texttt{Twin}\) modification changes the gauge of the formulas. Hence we get:
The lower bound for the true QBFs then follows with Theorem
12.
We now use a direct construction to show that \(\text {Rev}(\texttt{Twin}\texttt{ModEq}_n)\) is easy for \(\textsf{QCDCL}^\textsf {{E\tiny {\MakeUppercase {xi}}-A\tiny {\MakeUppercase {ny}}}}\).
Proof
Let us first list all the clauses of
\(\texttt{Twin}\texttt{ModEq}_n\). It consists of the prefix
$$\begin{aligned} \exists x_1,\ldots ,x_n\forall u_1,\ldots ,u_n,p,v_1,\ldots ,v_n,q\exists t_1,\ldots ,t_n \end{aligned}$$
and the matrix
$$\begin{aligned} C_{(i,1)}:= x_i\vee u_i\vee t_i \,\,\,\,\, C_1:= p\vee \bar{t}_1\vee \ldots \vee \bar{t}_n \\ C_{(i,2)}:= \bar{x}_i\vee \bar{u}_i\vee t_i \,\,\,\,\, C_2:= \bar{p}\vee \bar{t}_1\vee \ldots \vee \bar{t}_n \\ C_{(i,3)}:= x_i\vee v_i\vee t_i \,\,\,\,\, C_3:=q\vee \bar{t}_1\vee \ldots \vee \bar{t}_n \\ C_{(i,4)}:= \bar{x}_i\vee \bar{v}_i\vee t_i \,\,\,\,\, C_4:= \bar{q}\vee \bar{t}_1\vee \ldots \vee \bar{t}_n \\ \end{aligned}$$
for
\(i=1,\ldots ,n\).
Then the true QCNF
\(\text {Rev}(\texttt{Twin}\texttt{ModEq}_n)\) consists of the prefix
$$\begin{aligned} \forall x_1,\ldots ,x_n\exists u_1,\ldots ,u_n,p,v_1,\ldots ,v_n,q\forall t_1,\ldots ,t_n,w\exists M, \end{aligned}$$
with
\(M:=\{ c_{(i,j)},c_j|\, i=1,\ldots ,n,\, j=1,\ldots ,4 \}\), and the matrix
$$\begin{aligned} E:= \bigvee _{i=1}^n\bigvee _{j=1}^4\bar{c}_{(i,j)}\vee \bigvee _{k=1}^4\bar{c}_k \\&\bar{x}_i\vee w\vee c_{(i,1/3)}\,\,\,\,\, \bar{u}_i\vee w\vee c_{(i,1)} \,\,\,\,\, \bar{v}_i\vee w\vee c_{(i,3)} \\&\bar{x}_i\vee \bar{w}\vee c_{(i,1/3)}\,\,\,\,\, \bar{u}_i\vee \bar{w}\vee c_{(i,1)} \,\,\,\,\, \bar{v}_i\vee \bar{w}\vee c_{(i,3)} \\&{x}_i\vee w\vee c_{(i,2/4)}\,\,\,\,\, {u}_i\vee w\vee c_{(i,2)} \,\,\,\,\, {v}_i\vee {w}\vee c_{(i,4)} \\&{x}_i\vee \bar{w}\vee c_{(i,2/4)}\,\,\,\,\, {u}_i\vee \bar{w}\vee c_{(i,2)}\,\,\,\,\, {v}_i\vee \bar{w}\vee c_{(i,4)} \\&\bar{t}_i\vee w\vee c_{(i,1/2/3/4)}\\&\bar{t}_i\vee \bar{w}\vee c_{(i,1/2/3/4)}\\&\bar{p}\vee w\vee c_1\,\,\,\,\, {p}\vee w \vee c_2 \,\,\,\,\, \bar{q}\vee w\vee c_3 \,\,\,\,\, {q}\vee {w}\vee c_4 \\&\bar{p}\vee \bar{w}\vee c_1\,\,\,\,\, {p}\vee \bar{w}\vee c_2\,\,\,\,\, \bar{q}\vee \bar{w}\vee c_3 \,\,\,\,\, {q}\vee \bar{w}\vee c_4 \\&{t}_i\vee w\vee c_{1/2/3/4}\\&{t}_i\vee \bar{w}\vee c_{1/2/3/4} \end{aligned}$$
for
\(i=1,\ldots ,n\), where variables like
\(c_{(i,1/3)}\) decode two versions of this clause: One clause with
\(c_{(i,1)}\) and the other with
\(c_{(i,3)}\) (analogously with
\(c_{(i,2/4)}\),
\(c_{(i,1/2/3/4)}\) and
\(c_{1/2/3/4}\)).
Let us now construct a polynomial size
\(\textsf{QCDCL}^\textsf {{E\tiny {\MakeUppercase {xi}}-A\tiny {\MakeUppercase {ny}}}}\) certificate. At first, we would like to learn the cubes
$$\begin{aligned} D_{(i,1)}&:=\bar{x}_i\wedge \bar{u}_i\wedge \bar{t}_i\\ D_{(i,2)}&:={x}_i\wedge {u}_i \wedge \bar{t}_i\\ D_1&:=\bar{p}\wedge {t}_1\wedge \ldots \wedge {t}_n \end{aligned}$$
for
\(i=1,\ldots ,n\). In order to learn
\(D_{(i,1)}\), we will make (level-ordered) decisions that satisfy all literals from
\(D_{(i,1)}\), but falsify all the other
\(D_{(i',1)}\) for
\(i'\ne i\). For example, we set
\(x_i\),
\(u_i\) and
\(t_i\) to false, and we can assign all the other variables left of
w arbitrarily. Note that until we reach
w, we will never make any propagations since
w or
\(\bar{w}\) is blocking them. After having decided all variables left of
w, we will decide
w and potentially trigger some propagations. However, the variable
\(c_{(i,1)}\) will never be propagated because all clauses containing it are already satisfied. After this we will set
\(c_{(i,1)}\) to false and all the remaining variables to true.
We now have satisfied the clause E. Furthermore, we have set all \(c_{(i',j)}\) and \(c_{k}\) to true except \(c_{(i,1)}\). Hence we have satisfied all clauses except the four clauses containing \(c_{(i,1)}\). But these two clauses were already satisfied because we have satisfied the cube \(D_{(i,1)}\) with the decisions left of w.
Let
\(\mathcal {T}_{(i,1)}\) be the trail we have constructed now. We can extract the cube
$$\begin{aligned} \bar{x}_i\wedge \bar{u}_i\wedge \bar{t}_i\wedge \bar{c}_{(i,1)}\wedge \bigwedge _{(i',j)\in (\{1,\ldots ,n\}\times \{1,2,3,4\})\backslash \{(i,1)\}}c_{(i',j)}\wedge \bigwedge _{k=1}^4c_k, \end{aligned}$$
which, as an assignment, already satisfies all clauses from
\(\text {Rev}(\texttt{Twin}\texttt{ModEq}_n)\). This cube can be existentially reduced to
\(D_{(i,1)}\), which is the cube we learn from
\(\mathcal {T}_{(i,1)}\). Analogously, we can learn the cubes
\(D_{(i,2)}\) for
\(i=1,\ldots , n\) via some analogue trails
\(\mathcal {T}_{(i,2)}\).
It remains to learn the cube \(D_1\), which represents the clause \(C_1\in \mathfrak {C}(\texttt{Twin}\texttt{ModEq}_n)\). We will construct a trail \(\mathcal {T}_1\) which includes (level-ordered) decisions that satisfy \(D_1\). But now we have to make sure not to trigger propagations via \(D_{(i,1)}\) or \(D_{(i,2)}\) since we must not set \(t_i\) to false. This can be done by setting all \(x_i\) to false and all \(u_i\) to true. Then we can set p to false and all \(t_i\) to true. The remaining variables left of w can again be decided arbitrarily. Then we set w to true and potentially trigger some propagations of \(c_{(i,j)}\) or \(c_k\), which is not a problem since \(c_1\) will never be propagated (the clauses containing \(c_1\) are already satisfied). Then we set \(c_1\) to false and all remaining variables can be set to true.
As with
\(\mathcal {T}{(i,1)}\), we have satisfied all clauses from
\(\text {Rev}(\texttt{Twin}\texttt{ModEq}_n)\). We can extract the cube
$$\begin{aligned} \bar{p}\wedge {t}_1\wedge \ldots \wedge {t}_n\wedge \bar{c}_{1}\wedge \bigwedge _{i=1}^n\bigwedge _{j=1}^4c_{(i,j)}\wedge \bigwedge _{k=2}^4c_k, \end{aligned}$$
from
\(\mathcal {T}_1\), which already satisfies the matrix and can be existentially reduced to
\(D_1\).
We will now define the cubes
$$\begin{aligned} R_i:=\bar{x}_i\wedge \bar{u}_i\wedge \bar{p}\wedge \bigwedge _{k=i+1}^n(u_k\wedge \bar{u}_k)\wedge \bigwedge _{\ell =1}^{i-1}{t}_\ell \\ L_i:={x}_i\wedge {u}_i\wedge \bar{p}\wedge \bigwedge _{k=i+1}^n(u_k\wedge \bar{u}_k)\wedge \bigwedge _{\ell =1}^{i-1}{t}_\ell \end{aligned}$$
for
\(i=2,\ldots ,n-1\). We will construct trails
\(\mathcal {U}_{n-1},\mathcal {V}_{n-1},\ldots ,\mathcal {U}_2,\mathcal {V}_2\) with which we will gradually learn the clauses
\(R_{n-1},L_{n-1},\ldots ,R_2,L_2\).
We start with
$$\begin{aligned} \mathcal {U}_{n-1}:=( \varvec{\bar{p}};\varvec{\bar{x}_1};\varvec{\bar{u}_1},{t}_1;\ldots ;\varvec{\bar{x}_{n-1}};\varvec{\bar{u}_{n-1}},{t}_{n-1},\bar{t}_n,\bar{x}_n,\top ) \end{aligned}$$
with antecedent cubes
$$\begin{aligned} \text {ante}_{\mathcal {U}_{n-1}}({t}_j)&=D_{(j,1)}\\ \text {ante}_{\mathcal {U}_{n-1}}(\bar{t}_n)&=D_1\\ \text {ante}_{\mathcal {U}_{n-1}}(\bar{x}_n)&=D_{(n,2)}\\ \text {ante}_{\mathcal {U}_{n-1}}(\top )&=D_{(n,1)} \end{aligned}$$
for
\(j=1,\ldots ,n-1\). We learn the cube
\(R_{n-1}=\left( \left( D_{(n,1)}{\mathop {\bowtie }\limits ^{x_n}}D_{(n,2)}\right) {\mathop {\bowtie }\limits ^{t_n}}D_1\right) {\mathop {\bowtie }\limits ^{t_{n-1}}}D_{(n-1,1)}\).
Analogously, by flipping some polarities, we construct the trail \(\mathcal {V}_{n-1}\) and learn the cube \(L_{n-1}=\left( \left( D_{(n,1)}{\mathop {\bowtie }\limits ^{x_n}}D_{(n,2)}\right) {\mathop {\bowtie }\limits ^{t_n}}D_1\right) {\mathop {\bowtie }\limits ^{t_{n-1}}}D_{(n-1,2)}\). Note that \(R_{n-1}\) will not interfere with the assignments in \(\mathcal {V}_{n-1}\).
Assume we have already learned the clauses
\(R_{n-1},L_{n-1},\ldots , R_i,L_i\) for some
\(i\in \{3,\ldots ,n-1\}\). Then we can construct the following trail:
$$\begin{aligned} \mathcal {U}_{i-1}:=(\varvec{\bar{p}};\varvec{\bar{x}_1};\varvec{\bar{u}_1},{t}_1;\ldots ;\varvec{\bar{x}_{i-1}};\varvec{\bar{u}_{i-1}},{t}_{i-1},{x}_i,\top ) \end{aligned}$$
with antecedent cubes
$$\begin{aligned} \text {ante}_{\mathcal {U}_{i-1}}({t}_j)&=D_{(j,1)}\\ \text {ante}_{\mathcal {U}_{i-1}}({x}_i)&=R_i\\ \text {ante}_{\mathcal {U}_{i-1}}(\top )&=L_i \end{aligned}$$
for
\(j=1,\ldots ,i-1\). We learn the cube
\(R_{i-1}=\left( L_i{\mathop {\bowtie }\limits ^{x_i}}R_i\right) {\mathop {\bowtie }\limits ^{t_{i-1}}}D_{(i-1,1)}\). Analogously, we can construct the trail
\(\mathcal {V}_{i-1}\) and learn
\(L_{i-1}=\left( L_i{\mathop {\bowtie }\limits ^{x_i}}R_i\right) {\mathop {\bowtie }\limits ^{t_{i-1}}}D_{(i-1,2)}\).
After having learned the cubes
\(R_{n-1},L_{n-1},\ldots ,R_2,L_2\), we construct two more trails, namely
$$\begin{aligned} \mathcal {U}_1:=(\varvec{\bar{p}};\varvec{\bar{x}_1};\varvec{\bar{u}_1},{t}_1,{x}_2,\top ) \end{aligned}$$
with antecedent cubes
$$\begin{aligned} \text {ante}_{\mathcal {U}_{1}}({t}_1)&=D_{(1,1)}\\ \text {ante}_{\mathcal {U}_{1}}({x}_2)&=R_2\\ \text {ante}_{\mathcal {U}_{1}}(\top )&=L_2, \end{aligned}$$
from which we learn
\([\bar{x}_1]=\left( L_2{\mathop {\bowtie }\limits ^{x_2}}R_2\right) {\mathop {\bowtie }\limits ^{t_1}}D_{1,1}\), and the trail
$$\begin{aligned} \mathcal {V}_1:=({x}_1;\varvec{\bar{p}};\mathbf {{u}_1},{t}_1,{x}_2,\top ) \end{aligned}$$
with antecedent cubes
$$\begin{aligned} \text {ante}_{\mathcal {V}_{1}}({x}_1)&=[x_1]\\ \text {ante}_{\mathcal {V}_{1}}({t}_1)&=D_{(1,2)}\\ \text {ante}_{\mathcal {V}_{1}}({x}_2)&=R_2\\ \text {ante}_{\mathcal {V}_{1}}(\top )&=L_2, \end{aligned}$$
from which we learn the empty cube
\([\top ]=\text {red}_{\text {Rev}(\texttt{Twin}\mathtt {ModEq_n})}^\exists \left( \left( L_2{\mathop {\bowtie }\limits ^{x_2}}R_2\right) {\mathop {\bowtie }\limits ^{t_1}}D_{(1,2)}\right) {\mathop {\bowtie }\limits ^{x_1}}[x_1]\).
All in all, we have constructed a
\(\textsf{QCDCL}^\textsf {{E\tiny {\MakeUppercase {xi}}-A\tiny {\MakeUppercase {ny}}}}\) certificate using the
\(4n-1\) trails
$$\begin{aligned} \mathcal {T}_{(1,1)},\ldots ,\mathcal {T}_{(n,1)},\mathcal {T}_{(1,2)}\ldots ,\mathcal {T}_{(n,2)},\mathcal {T}_1,\mathcal {U}_{n-1},\mathcal {V}_{n-1},\ldots ,\mathcal {U}_1,\mathcal {V}_1. \end{aligned}$$
\(\square \)
For separating
\(\mathsf{{QCDCL}} \) and
\(\textsf{QCDCL}^\textsf {{U\tiny {\MakeUppercase {ni}}-A\tiny {\MakeUppercase {ny}}}}\), we recall the completion principle
\(\texttt{CR}_n\) of [
18].
For the lower bound, we will use the modification \(\texttt{Twin}\texttt{CR}_n\). As we show, cube learning becomes rather useless with the \(\texttt{Twin}\) modification. This fact helps us to ensure that \(\mathsf{{QCDCL}} \) refutations of \(\texttt{Twin}\texttt{CR}_n\) are primitive, and thus we can apply the gauge lower-bound method.
Similarly as in Proposition
13 we can compute the gauge.
The main work is to check that \(\mathsf{{QCDCL}} \) refutations of \(\texttt{Twin}\texttt{CR}_n\) are primitive.
Proof
It suffices to show that \(\mathfrak {R}(\iota )\) is primitive. Assume not.
Then there exists two XUT-clauses \(C,D\in \mathfrak {R}(\iota )\) that are resolved over an X-literal, say x. One of these two clauses has to be the antecedent clause of x by the definition of clause learning, say \(C=\text {ante}_{\mathcal {T}}(x)\) for some trail \(\mathcal {T}\in \mathfrak {T}(\iota )\). Let \(t_1\in C\) be one of the T-literals. We want to show, that there exists a U-literal w with \(w<_\mathcal {T}x\).
Assume that no such w exists. Since C had to become unit at the propagation of x, we need \(\bar{t}_1<_\mathcal {T}x\). The literal \(\bar{t}_1\) cannot be a decision in \(\mathcal {T}\), since this would mean that we assigned all U-variables earlier in the trail, which contradicts our assumption. Hence \(\bar{t}_1\) must have been a propagation.
Starting with
\(i=1\), we define
\(F_i:=\text {ante}_{\mathcal {T}}(\bar{t}_i)\). Now,
\(F_i\) cannot contain
U-literals since we cannot falsify these literals before assigning
\(\bar{t}_i\). Because of the XT-property (and Lemma
6),
\(F_i\) cannot contain
X-literals, as well (otherwise it would be an XT-clause). But if the XT-property is fulfilled, we cannot derive unit T-clauses, therefore
\(F_i\) has to contain at least one additional
T-literal, say
\(t_{i+1}\in F_i\).
This argument can be repeated for each \(i\in \mathbb {N}\), which means we could find an infinite amount of T-literals \(\bar{t}_i\) that must be all contained in \(\mathcal {T}\), which is obviously not possible. This shows that our assumption was false and we can indeed find such a U-literal \(w<_\mathcal {T}\bar{t}_1<_\mathcal {T}x\).
W.l.o.g. let w be the first (leftmost) U-literal in \(\mathcal {T}\). Define \(A:=\text {ante}_\mathcal {T}(w)\). Clearly, A is a cube. We will show that A contains at least two different U-literals. Then, since w was the first U-literal in \(\mathcal {T}\), A cannot become unit until at least one U-literal was assigned, which would be a contradiction.
Now, A is a cube that was derived during cube learning from cubes that represent satisfying (partial) assignments of the matrix of \(\mathtt {\texttt{Twin}\texttt{CR}_n}\). Let D be a cube that satisfies the matrix of \(\mathtt {\texttt{Twin}\texttt{CR}_n}\). Because we have to satisfy the clauses \(\bar{a}_1\vee \ldots \vee \bar{a}_n\) and \( \bar{b}_1\vee \ldots \vee \bar{b}_n\), there exists an \(r\in \{1,\ldots ,n\}\) with \(\bar{a}_r\in D\) and an \(s\in \{1,\ldots ,n\}\) with \(\bar{b}_s\in D\). Furthermore, we have to satisfy the clauses \(x_{(r,s)} \vee u\vee a_r\), \(x_{(r,s)} \vee v\vee a_r\), \(\bar{x}_{(r,s)}\vee \bar{u}\vee b_s\) and \(\bar{x}_{(r,s)}\vee \bar{v}\vee b_s\). That means we have to assign u in some polarity. W.l.o.g. let \(u\in D\). Then we have to set \(x_{(r,s)}\) to false, hence \(\bar{x}_{(r,s)}\in D\). In order to satisfy \(x_{(r,s)} \vee v\vee a_r\), we have to set v to true, as well. Therefore we get \(v\in D\).
We conclude, that \(u\in D\) if and only if \(v\in D\), and analogously \(\bar{u}\in D\) if and only if \(\bar{v}\in D\). This means that we will never be able to resolve such two learned cubes in \(\iota \) since we cannot create universal tautologies in cubes. In particular, we have proven that A contains at least two U-literals, which leads to a contradiction as described above. \(\square \)
Applying Theorem
7 then yields the lower bound.
On the other hand,
\(\texttt{Twin}\texttt{CR}_n\) is easy for
\(\textsf{QCDCL}^\textsf {{U\tiny {\MakeUppercase {ni}}-A\tiny {\MakeUppercase {ny}}}}\). Basically, we can simulate the
Q-resolution refutation of
\(\texttt{CR}_n\) from [
17], because we can decide universal literals out of order.
Besides
\(\texttt{TwinCR}_n\), we can find further separations between
\(\mathsf{{QCDCL}} \) and
\(\textsf{QCDCL}^\textsf {{U\tiny {\MakeUppercase {ni}}-A\tiny {\MakeUppercase {ny}}}}\). The QCNFs
\(\texttt{MirrorCR}_n\) were introduced in [
4] as a modification of
\(\texttt{CR}_n\), where it was shown that the formula is hard for several variants of QCDCL, including our base model
\(\mathsf{{QCDCL}} \). It is notable that the matrix of
\(\texttt{MirrorCR}_n\) is unsatisfiable, and therefore we will never perform cube learning.
We combine both separations into our main result: