University of California, San Diego, La Jolla, CA, USA
https://orcid.org/0000-0003-3837-334X Lorica Cybersecurity, Canada
https://orcid.org/0000-0001-5378-1136 Georgia Institute of Technology,
Atlanta, USA https://orcid.org/0000-0002-6029-2047 Technical University of
Catalonia, Barcelona https://orcid.org/0000-0002-5893-1911 Supported by grant
PID2021-122830OB-C43, funded by MCIN/AEI/ 10.13039/501100011033 and by “ERDF:
A way of making Europe” and by Barcelogic through research grant C-11423. Sam
Buss, Jonathan Chung, Vijay Ganesh and Albert Oliveras [100]Theory of
computation 0 Preprint Preprint Preprint 2024 June 2024 1

# Extended Resolution Clause Learning via Dual Implication Points

Sam Buss  Jonathan Chung  Vijay Ganesh  Albert Oliveras

###### Abstract

We present a new extended resolution clause learning (ERCL) algorithm,
implemented as part of a conflict-driven clause-learning (CDCL) SAT solver,
wherein new variables are dynamically introduced as definitions for Dual
Implication Points (DIPs) in the implication graph constructed by the solver
at runtime. DIPs are generalizations of unique implication points and can be
informally viewed as a pair of dominator nodes, from the decision variable at
the highest decision level to the conflict node, in an implication graph. We
perform extensive experimental evaluation to establish the efficacy of our
ERCL method, implemented as part of the MapleLCM SAT solver and dubbed
xMapleLCM, against several leading solvers including the baseline MapleLCM, as
well as CDCL solvers such as Kissat 3.1.1, CryptoMiniSat 5.11, and
SBVA+CaDiCaL, the winner of SAT Competition 2023. We show that xMapleLCM
outperforms these solvers on Tseitin and XORified formulas. We further compare
xMapleLCM with GlucoseER, a system that implements extended resolution in a
different way, and provide a detailed comparative analysis of their
performance.

###### keywords:

SAT, Extended resolution, Conflict Analysis

###### category:

##  1 Introduction

Over the last several years, Conflict-Driven Clause-Learning (CDCL) SAT
solvers have had a dramatic impact on many fields including software
engineering [23], security [39], and AI [22, 21]. As solvers continue to be
adopted in increasing complex settings, the demand for greater efficiency and
reasoning power by users continues unabated.

While developers continue to improve CDCL SAT solvers, it is simultaneously
true that these solvers are provably no more powerful than the relatively weak
general resolution (Res) proof system [1, 32], and therefore are fundamentally
limited. Hence, solver developers have been actively researching novel
algorithms that implement stronger proof systems that go beyond Res. Examples
of such algorithms include satisfaction-driven clause-learning (SDCL) SAT
solvers [17, 31], bounded variable addition (BVA) [26], symmetry breaking
[35], and extended resolution (ER) solvers such as GlucoseER [3].

Continuing this trend of strong proof system implementations, we present a new
extended resolution clause learning (ERCL) algorithm, incorporated into a CDCL
SAT solver, where new variables are dynamically introduced as definitions for
dual implication points (DIPs) in the implication graph constructed by the
solver at run time. The concept of a DIP is best understood as a
generalization of unique implication points (UIPs). Informally, a UIP can be
defined as a dominator node in an implication graph, corresponding to a
variable at the highest decision level (DL), that dominates all paths from the
decision variable node at the highest DL to the conflict node. By contrast, a
DIP is a pair of dominator nodes in an implication graph such that any path
from the decision variable node at the highest DL to the conflict node must
pass through at least one node in the pair111While it is natural to generalize
the concept of a DIP to K-Implication Points or $k$-IPs, we do not discuss
them in this paper..

Implementation of the ERCL algorithm requires several additional methods.
First, we need a method to identify DIPs, i.e., a technique that takes as
input an implication graph and outputs a DIP and does so in time linear in the
size of the input. Second, we need a technique replaces this DIP pair with a
new variable and appropriately modifies the clause learning algorithm to learn
new clauses involving DIPs. Third, we need an ER framework, built on top of a
CDCL SAT solver, that enables new variable addition, ER clause addition and
deletion, etc. Finally, we need heuristics that specialize the above mentioned
methods in a variety of ways, such as clause learning and clause deletion
policies that are based on different kinds of DIPs. We implement all of these
methods as part of the MapleLCM solver [25], and refer to the resulting solver
as xMapleLCM. In fact our proposed ERCL method, and its implementation, is
very general and easily extensible thus encouraging future exploration and
specialization efforts with a variety of heuristics.

##### Contributions.

  1. 1.

DIP: We introduce the concept of dual implication points (DIP), a
generalization of UIPs in conflict graphs. We also came up with an algorithm
that computes them in linear time. However, due to space limitations and to
the non-trivial nature of the procedure, we discuss this in a separate paper
[11].

  2. 2.

ERCL Algorithm: We introduce a highly parameterizable DIP-based ERCL
algorithm. The existence of a multitude of different DIPs in a single conflict
graph allows us to derive a large variety of ERCL algorithms. This flexibility
is crucial in adapting the procedure to different scenarios, unlike previous
methods that couple CDCL with extended resolution.

  3. 3.

xMapleLCM: We present a highly extensible and general ER framework as part of
xMapleLCM, which allows developers to easily add their own new variable
addition, ER clause learning/deletion, and branching policies. Given that DIP-
based ERCL is highly flexible by nature, such a framework is necessary to
quickly prototype new procedures.

  4. 4.

Experiments: We perform extensive empirical evaluation and ablation studies on
four different classes of instances, namely, SAT Competition 2023 Main Track,
random-k-XOR, Tseitin, and interval matching, and compare xMapleLCM against
leading solvers such as Kissat 3.1.1 [8], CryptoMiniSat 5.11 [36], SBVA
CaDiCaL [14], and the extended-resolution solver GlucoseER [4]. Results show
that on the last three sets of hard combinatorial formulas, CDCL SAT solvers
perform very poorly, whereas both xMapleLCM and GlucoseER excel on them.
Hence, we can now finally state that extended resolution can be added to CDCL
and improve the performance of these solvers, and that there are at least two
completely different ways to achieve this. Moreover, a simple heuristic
dynamically allows us to detect whether extended resolution is being helpful
and turn back to standard CDCL in order to get the best of both worlds. This
technique enables xMapleLCM to perform similarly to MapleLCM on the SAT
Competition 2023 Main Track instances.

##  2 Related Work

The idea of using ER in SAT solving has been studied in various forms in the
literature for nearly two decades. The closest approach to ours is GlucoseER
[3], where extended variables are introduced dynamically during the CDCL
search: whenever two consecutive learned lemmas are of the form $\lnot
l_{1}\lor C$ and $\lnot l_{2}\lor C$, with $l_{1}$ and $l_{2}$ being their
UIPs, then an extended variable $z\leftrightarrow l_{1}\lor l_{2}$ is
generated and any future lemma of the form $l_{1}\lor l_{2}\lor D$ is replaced
by $z\lor D$.

Our method differs significantly from GlucoseER in the way extended variables
are identified: we choose DIPs, which can be seen as pairs of variables for
which adding a definition would create a better first UIP (often written as
1UIP) in the conflict graph, whereas GlucoseER definitions are constructed
using already existing UIPs. Also, unlike in GlucoseER, our approach does not
always learn the standard 1UIP clause, but multiple clauses might be learned
that take into account the newly introduced variable. On the other hand, there
are similarities at the heart of both procedures: a certain restriction of ER
is considered and introduced variables are used to shorten subsequently found
clauses.

More recent uses of ER in SAT solvers are Bounded Variable Addition (BVA) [26]
and its structured version SBVA [14], that due to clever strategies are able
to identify new extended variables whose introduction can reduce the number of
clauses. Essentially, the ultimate goal of BVA techniques is to reduce the
size of the formula by reducing the number of clauses at the cost of adding a
new variable. One big difference with our work is that this process is done
only in a preprocessing step. Finally, one additional direction that has been
researched is the development of a BDD-based solver to generate ER proofs
[10].

Other approaches aiming at improving CDCL solvers by allowing them to use a
more powerful proof system are related to the Propagation Redundancy notion
[16, 18], either via preprocessing steps [34] or via the use of the SDCL
algorithm [19, 31]. While these methods implement proof systems that are
stronger than Res, many of them (without new variable addition) are known to
be weaker than ER.

##  3 Preliminaries

We assume that the reader is familiar with the satisfiability (SAT) problem
and the CDCL algorithm, and we refer her to the Handbook of Satisfiability for
an excellent overview of these topics [27]. Below we focus on conflict
analysis, which is the most relevant ingredient from the CDCL algorithm for
this paper. We do so by means of the following example.

######  Example 3.1.

Consider the following clauses

$\begin{array}[]{llllll}(1)&y_{1}\lor\lnot x_{1}\lor x_{2}&(6)&\lnot x_{5}\lor
x_{7}&(11)&\lnot x_{11}\lor x_{12}\\\ (2)&\lnot x_{1}\lor\lnot
x_{3}&(7)&x_{6}\lor\lnot x_{7}\lor x_{8}&(12)&x_{10}\lor\lnot x_{11}\lor
x_{13}\\\ (3)&y_{2}\lor\lnot x_{1}\lor x_{4}&(8)&\lnot y_{3}\lor\lnot
y_{4}\lor\lnot x_{5}\lor\lnot x_{9}&(13)&x_{12}\lor\lnot x_{13}\\\ (4)&\lnot
y_{3}\lor\lnot x_{2}\lor x_{3}\lor\lnot x_{4}\lor x_{5}&(9)&\lnot y_{4}\lor
x_{9}\lor\lnot x_{10}\\\ (5)&y_{1}\lor\lnot x_{5}\lor\lnot x_{6}&(10)&\lnot
y_{5}\lor y_{6}\lor\lnot x_{8}\lor x_{9}\lor x_{11}\\\ \end{array}$

Assume that CDCL has constructed an assignment that contains, among others,
literals $\\{\lnot y_{1},\lnot y_{2},y_{3},y_{4},y_{5},\lnot y_{6}\\}$. Since
no propagation is possible, it now decides to add the decision literal
$x_{1}$. Due to clause (1), we can unit propagate literal $x_{2}$, being (1)
the reason of $x_{2}$ and its antecedents $\\{\lnot y_{1},x_{1}\\}$.
Similarly, $\lnot x_{3}$ is propagated due to reason (2), with antecedents
$\\{x_{1}\\}$, and $x_{4}$ due to reason (3) with antecedents $\\{\lnot
y_{2},x_{1}\\}$. If we continue this process we eventually find that clause
(13) is conflicting and we can construct the conflict graph in Figure 1, where
every literal in the current decision level has incoming edges corresponding
to its antecedents (except of course the decision literal). A special conflict
node $\perp$ with incoming edges $\\{\overline{x_{12}},x_{13}\\}$ represents
conflicting clause (13).

The graph clearly shows that if we set $x_{1}$ to true, together with the
literals of previous decision levels (the $y$’s), we obtain a conflict.
However, the same happens with $x_{5}$, since any path from $x_{1}$ to the
conflict necessarily goes through $x_{5}$. Literals with this property are
called Unique Implication Points (UIPs), of which we only have $x_{1}$ and
$x_{5}$. Since $x_{5}$ is the one closest to the conflict we call it First
Unique Implication Point (1UIP) [40]. It is easy to see that if we set $x_{5}$
and the $y$ literals that enter the cut delimited by the blue line, unit
propagation derives the same conflict. Hence, since they cannot be
simultaneously true, we can learn $\lnot y_{3}\lor\lnot y_{4}\lor\lnot
y_{5}\lor y_{6}\lor x_{5}$. The quality of a lemma can be assessed by its
Literal Block Distance (LBD) [4]: the number of different decision levels of
the literals in the lemma. The lower the LBD, the better the lemma. In our
case, if we are at decision level 5, $y_{4}$ and $y_{6}$ belong to decision
level 2, and $y_{5}$ to decision level 4, the LBD of the lemma is 3. $\Box$

$x_{1}$$x_{2}$$\overline{x_{3}}$$x_{4}$$\overline{y_{2}}$$\overline{y_{1}}$$x_{5}$$y_{3}$$\overline{x_{6}}$$x_{7}$$\overline{x_{9}}$$y_{5}$$x_{8}$$\overline{y_{6}}$$x_{11}$$\overline{x_{10}}$$y_{4}$$\overline{x_{12}}$$x_{13}$$\perp$
Figure 1: Conflict graph associated with Example 3.1. If 1UIP learning is
applied, we generate lemma $\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor x_{5}$.
White nodes belong to the current decision level, whereas blue ones are from
previous decision levels.

Resolution. Given two clauses $l\lor C$ and $\lnot l\lor D$, the resolution
inference rule allows one to derive the logical consequence $C\lor D$. It is
well known that the lemma derived in Example 3.1 can be obtained via a series
of resolution steps that start with the conflicting clause, and resolve with
reasons of literals in the reverse order in which they were added to the
assignment. In fact, it has been proved [33, 2] that resolution and CDCL (with
restarts) are polynomially equivalent, and hence classes of formulas that are
hard for resolution; e.g., the pigeonhole principle - PHP [15], or Tseitin
formulas [38]) are also hard for CDCL SAT solvers.

Extended Resolution (ER). Given two literals $l_{1}$ and $l_{2}$, the extended
resolution [37] rule allows us to introduce clauses representing the
definition $z\leftrightarrow l_{1}\lor l_{2}$. ER can be substantially more
powerful than resolution; for instance, it allows polynomial size proofs of
PHP [13]. Incorporating ER to CDCL solvers could potentially enable them to
solve such formulas in polynomial time. However, we lack good methods to
incorporate ER into CDCL proof search. This is precisely the aim of this
paper, namely, incorporating a restricted version of ER into CDCL.

##  4 Dual Implication Points

As discussed in the previous section, UIPs are crucial for conflict clause
learning in the CDCL algorithm. We now introduce a new concept of a _Dual
Implication Point_ (DIP) that gives a tool for analyzing the conflict graph.
Its applications include discovering new implied 2-clauses, introducing new
variables by extension, and learning clauses involving the extension
variables. The idea behind a dual implication point is that it consists of a
pair of vertices (literals) in the conflict graph that disconnects or
“separates” the decision literal from the contradiction.222Perhaps “Dual
Implication Pair” would be a better name than “Dual Implication Point’, since
a DIP is a pair of literals. We use “Point” however to match the terminology
of “Unique Implication Points”. More precisely, a DIP is defined to be a pair
$\\{x,y\\}$ of literals such that all paths in the conflict graph to the
vertex $\perp$ pass through at least one of $x$ and $y$ and such that neither
$x$ nor $y$ is a UIP. In contrast, UIP is a single literal that separates the
decision literal from the conflict.

We use the example in Figure 1 to illustrate the concept of DIPs and their
potential applications. Recall that $x_{5}$ is the first UIP. In our
applications, we are seeking DIPs between the first UIP and the conflict node
$\perp$. An obvious DIP is the pair $\overline{x_{10}}$ and $x_{11}$, since it
is immediately clear that any path from $x_{5}$ (or from $x_{1}$) must pass
through one of $\overline{x_{10}}$ or $x_{11}$. On the other hand, the pair
$\overline{x_{10}}$ and $x_{8}$ is not a DIP since there are paths from
$x_{1}$ to $\perp$ that avoid these two literals; namely, any path that
includes the edge from $\overline{x_{9}}$ to $x_{11}$. There are several other
DIPs in Figure 1: a complete list is given in Figure 2.

Dual |  |  |
---|---|---|---
Implication | Extension | Post-DIP | Pre-DIP
Point (DIP) | Variable | Learned Clause | Learned Clause
$\overline{x_{12}},x_{13}$ | $z\leftrightarrow(\overline{x_{12}}\land x_{13})$ | $\lnot z$ | $\lnot x_{5}\lor y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor z$
$x_{11},x_{13}$ | $z\leftrightarrow(x_{11}\land x_{13})$ | $\lnot z$ | $\lnot x_{5}\lor y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor z$
$\overline{x_{10}},x_{11}$ | $z\leftrightarrow(\overline{x_{10}}\land x_{11})$ | $\lnot z$ | $\lnot x_{5}\lor y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor z$
$\overline{x_{9}},x_{11}$ | $z\leftrightarrow(\overline{x_{9}}\land x_{11})$ | $\lnot z\lor\lnot y_{4}$ | $\lnot x_{5}\lor y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor z$
$x_{8},\overline{x_{9}}$ | $z\leftrightarrow(x_{8}\land\overline{x_{9}})$ | $\lnot z\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}$ | $\lnot x_{5}\lor y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor z$
Figure 2: The complete list of DIPs for the conflict graph of Figure 1. The
DIP-learnable clauses involve the new extension variable $z$ that can be
introduced for that DIP. (The extension clauses defining $z$ must also be
learned; e.g., for the first line, the extension clauses express that
$z\leftrightarrow\overline{x_{12}}\land x_{13}$.)

Figure 2 also shows how a DIP pair can be used to introduce a variable $z$ via
extension, and the associated clauses that can be learned. For example, in the
third line, the new extension variable $z$ is introduced with the three
clauses $\lnot z\lor\lnot x_{10}$, $\lnot z\lor x_{11}$ and $x_{10}\lor\lnot
x_{11}\lor\lnot z$ which express the condition $z\leftrightarrow(\lnot
x_{10}\land x_{11})$. From the conflict graph, this allows inferring the
clauses $\lnot z$ (the “post-DIP” learned clause) and $\lnot x_{5}\lor
y_{1}\lor\lnot y_{3}\lor\lnot y_{4}\lor\lnot y_{5}\lor y_{6}\lor z$ (the “pre-
DIP” learned clause). Since the post-DIP learned clause does not have any
variables from lower decision levels, we can also infer the 2-clause
$x_{10}\lor\lnot x_{11}$ either instead of or in addition to introducing $z$
and the pre- and post-DIP clauses. Introducing 2-clauses in this way might be
helpful for CDCL solvers that do special processing of 2-clauses; for
instance, in the work of Bacchus [5] or the recent work of Biere et al. [9] or
Buss et al. [12].

In general, for any literals $a,b$ that form a DIP in the above fashion, we
may introduce an extension variable $z\leftrightarrow a\land b$, and learn (1)
a pre-DIP clause of the form $\lnot f\lor\lnot C\lor z$ (i.e. $f\land
C\rightarrow z$), where $f$ is the first UIP and $C$ the set of literals from
previous decision levels that have an edge in the conflict graph to any
literal appearing after the first UIP and no later than the DIP pair; and (2)
a post-DIP clause of the form $\lnot z\lor\lnot D$ (i.e. $z\land
D\rightarrow\perp$), where $D$ contains those literals from previous decision
levels with an edge to any literal appearing strictly after the DIP pair.

For example, the last line of the table in Figure 2 shows the case
$z\leftrightarrow(x_{8}\land\overline{x_{9}})$, where $f$ is $x_{5}$, and $C$
and $D$ are $\lnot y_{1}\land y_{3}\land y_{4}$ and $y_{4}\land
y_{5}\land\lnot y_{6}$, respectively. In Section 5.2 we discuss many possible
ways that DIP extension variables and clauses may be introduced into CDCL
solvers. The rest of this section describes how to find DIPs.

###  4.1 An Algorithm for Finding DIPs

A conventional CDCL algorithm maintains a trail of the literals set true, in
the order they were set, and this allows finding the UIP very quickly. Finding
the DIPs is much more complex than finding the UIP, and requires several
traversals of the conflict graph between the first-UIP and the conflict node.
Nonetheless, it is possible to find all DIPs very quickly, even in linear
time.

We recast the DIP-finding problem in terms of a general directed graph $G$.
Let $G=(V,E)$ be a directed graph with two distinguished vertices $s$ and $t$.
We assume that $s$ is 2-connected to $t$ in that there is a pair of vertex-
disjoint paths $\pi_{1}$ and $\pi_{2}$ from $s$ to $t$ that share no vertices
apart from $s$ and $t$. By the vertex-version of Menger’s theorem [28], either
there are in fact three vertex-disjoint paths from $s$ to $t$ or there is at
least one pair of vertices $\\{a,b\\}$ with neither $a$ nor $b$ in $\\{s,t\\}$
so that every path from $s$ to $t$ passes through at least one of $a$ or $b$.
Such a pair $\\{a,b\\}$, if it exists, is called a Two Vertex Bottleneck
(TVB).

Our goal is to find all possible TVBs efficiently and in linear time. An
algorithm for this is discussed in our companion paper [11]; for space
reasons, we give only an abbreviated discussion of the algorithm here. The
first step is to find two vertex disjoint paths from $s$ to $t$: this is done
by greedily finding a path from $s$ to $t$ and then using an augmenting path
construction to find two vertex-disjoint paths from $s$ to $t$. An example is
shown in Figure 3, where the two paths are $a_{0},\ldots,a_{\ell}$ and
$b_{0},\ldots,b_{k}$ where $a_{0}=b_{0}=s$ and $a_{\ell}=b_{k}=t$. These paths
are called $\pi_{a}$ and $\pi_{b}$, respectively. Henceforth, a path is a
directed path without any repeated nodes. The _internal_ vertices of a path
$\pi$ are the vertices on $\pi$ other than the first and last vertices. Two
paths are said to be _vertex-disjoint_ if they have no internal vertices in
common. A path $\pi$ _avoids $\pi_{a}$ and $\pi_{b}$_ if it is vertex-disjoint
from both paths.

$s$$a_{1}{=}a^{\prime}_{1}$$a_{2}{=}a^{\prime}_{2}$$a_{3}{=}a^{\prime}_{3}$$a_{4}$$a_{5}{=}a^{\prime}_{4}$$b_{1}{=}b^{\prime}_{1}$$b_{2}{=}b^{\prime}_{2}$$b_{3}$$b_{4}$$b_{5}{=}b^{\prime}_{3}$$t$$c$$d$
Figure 3: Nodes $a_{4}$, $b_{3}$ and $b_{4}$ are bypassed and thus not in any
TVB. The path $b_{2},c,d,a_{4}$ is a crossing separator that prevents any of
$a_{1}$, $a_{2}$ and $a_{3}$ from being paired with $b_{5}$ to form a TVB
pair. All other pairs $\\{a^{\prime}_{i},b^{\prime}_{j}\\}$ are valid TVB
pairs.

Once the two vertex-disjoint paths are fixed, we can state the following
definitions and theorems:

######  Definition 4.1.

[11] A node $a_{i}$ on $\pi_{a}$ is _bypassed_ if there are $j<i<j^{\prime}$
and a path $\pi$ from $a_{j}$ to $a_{j^{\prime}}$ such that $\pi$ avoids
$\pi_{a}$ and $\pi_{b}$. A node $b_{i}$ being bypassed is defined similarly.

######  Definition 4.2.

Two nodes $a_{i}$ and $b_{j}$ have a _crossing separator_ if there are nodes
$a_{i^{\prime}}$ and $b_{j^{\prime}}$ joined by a path $\pi$ that avoids both
$\pi_{a}$ and $\pi_{b}$ such that either (a) $i^{\prime}<i$ and $j^{\prime}>j$
and $\pi$ is a path from $a_{i^{\prime}}$ to $b_{j^{\prime}}$, or (b)
$i^{\prime}>i$ and $j^{\prime}<j$ and $\pi$ is a path from $b_{j^{\prime}}$ to
$a_{i^{\prime}}$.

######  Theorem 4.3.

[11] For $0<i<\ell$ and $0<j<k$, the two nodes $a_{i}$ and $b_{j}$ form a two-
vertex bottleneck (TVB) if and only if $a_{i}$ and $b_{j}$ do not have a
crossing separator and neither $a_{i}$ nor $b_{j}$ is bypassed.

Theorem 4.3 is proved in [11]. The theorem holds for both acyclic and cyclic
directed graphs; however, for our applications to CDCL we are interested only
in acyclic graphs since the conflict graph is always acyclic.

A consequence of Theorem 4.3 is that the set of all TVBs can be compactly
represented in linear size, even though there can be quadratically many TVBs.
Let $a^{\prime}_{1},\ldots a^{\prime}_{\ell^{\prime}}$ be the subsequence of
the internal nodes $a_{1}.\ldots,a_{\ell-1}$ of path $\pi_{a}$ that, according
to the conditions of Theorem 4.3, are in at least one TVB pair. Let
$b^{\prime}_{1},\ldots,b^{\prime}_{k^{\prime}}$ be the corresponding
subsequence of the internal nodes of $\pi_{b}$. Then, for each
$a^{\prime}_{i}$ there are $m\leq n$ such that $a^{\prime}_{i}$ forms a TVB
pair with each $b^{\prime}_{j}$ with $m\leq j\leq n$. Dually, for each
$b^{\prime}_{i}$ there are $m\leq n$ such that $b^{\prime}_{i}$ forms a TVB
pair with each $a^{\prime}_{j}$ with $m\leq j\leq n$.

######  Example 4.4.

In the conflict graph of Figure 1, consider the portion of the graph between
the first UIP $x_{5}$ and the contradiction $\perp$. We can take path
$\pi_{a}$ to be $x_{5},x_{7},x_{8},x_{11},\overline{x_{12}},\perp$ and path
$\pi_{b}$ to be $x_{5},\overline{x_{9}},\overline{x_{10}},x_{13},\perp$. The
node $x_{7}$ is bypassed by the path $x_{5},\overline{x_{6}},x_{8}$, so it
cannot be part of a TVB. There are two crossing separator paths: the first is
the edge from $\overline{x_{9}}$ to $x_{11}$; the second is the edge from
$x_{11}$ to $x_{13}$. Therefore, the possible TVB pairs can be described in a
table as:

Node | forms a TVB | Node | forms a TVB
---|---|---|---
on $\pi_{a}$ | pair with |  on $\pi_{b}$ | pair with
$x_{8}$ | $\overline{x_{9}}$ | $\overline{x_{9}}$ | $x_{8},x_{11}$
$x_{11}$ | $\overline{x_{9}},\overline{x}_{{10}},x_{13}$ | $\overline{x_{10}}$ | $x_{11}$
$\overline{x_{12}}$ | $x_{13}$ | $x_{13}$ | $x_{11},\overline{x}_{12}$

In this example, one node, $x_{7}$, was bypassed. It is also possible that
non-bypassed nodes are eliminated just by the crossing separators. For
example, if there were an additional edge from $x_{7}$ to $\overline{x_{10}}$,
then the crossing separator condition would imply that $x_{8}$ and $x_{11}$
are not part of any TVB pair. In this case, $x_{8}$ and $x_{11}$ would not be
included among the $a^{\prime}_{i}$ nodes.

Theorem 4.3 is used in [11] to give an efficient, linear time algorithm for
finding all TVBs. The algorithm has five phases. The first two phases find two
vertex-disjoint paths from $s$ to $t$; the next phase scans the graph from $t$
to $s$ to discover all relevant paths that avoid $\pi_{a}$ and $\pi_{b}$; the
fourth phase uses this to discard bypassed nodes and collect information on
crossing separators; finally the fifth phase computes the compressed
representation of all possible TVBs. Full details are given [11], which is
available online in preprint form. In our experiments with the implication
graphs constructed by the underlying CDCL solver, the time overhead in finding
the TVBs is negligible.

##  5 Extension Variables from Dual Implication Points

This section discusses how DIPs can be used for introducing extension
variables and implement the ERCL method for learning ER clauses in CDCL
solver. We first present an example.

###  5.1 An example with a grid Tseitin principle

Given a graph where every vertex has a charge, a number which is $0$ or $1$, a
Tseitin formula [37] is created by considering one variable per edge, and
adding one constraint per vertex $v$ expressing that the sum of the variables
of all edges incident to $v$ modulo 2 is equal to its charge. The CNF version
that we consider converts each xor constraint into clauses by simple
enumeration of falsifying assignments. It is easy to see that the formula is
unsatisfiable if and only if the sum of all charges is even. Here we consider
as a graph the $3\times 3$-grid depicted in Figure 4 and only one vertex has
charge 1, so the clauses are unsatisfiable.

$\scriptsize
1$$0$$0$$0$$0$$0$$0$$0$$0$$e_{1}$$e_{2}$$e_{3}$$e_{4}$$e_{5}$$e_{6}$$e_{7}$$e_{8}$$e_{9}$$e_{10}$$e_{11}$$e_{12}$

$e_{1}\oplus e_{3}$ $=$ | 1 |  $e_{5}\oplus e_{7}\oplus e_{10}$ $=$ | 0
---|---|---|---
$e_{1}\oplus e_{2}\oplus e_{4}$ $=$ | 0 |  $e_{8}\oplus e_{11}$ $=$ | 0
$e_{2}\oplus e_{5}$ $=$ | 0 |  $e_{9}\oplus e_{11}\oplus e_{12}$ $=$ | 0
$e_{3}\oplus e_{6}\oplus e_{8}$ $=$ | 0 |  $e_{10}\oplus e_{12}$ $=$ | 0
$e_{4}\oplus e_{6}\oplus e_{7}\oplus e_{9}$ $=$ | 0 |  |

Figure 4: An instance of the $3\times 3$-grid Tseitin principle. The nodes are
assigned a polarity in $\\{0,1\\}$. The edges are labeled with variables.

The first steps of the CDCL solver are as follows: First $e_{1}$ is set true
as a decision literal, and $\overline{e_{3}}$ is (unit) propagated. Second,
$e_{2}$ is set true as a decision literal, and $\overline{e_{4}}$ and $e_{5}$
are propagated. Third, $e_{6}$ is set true as a decision literal, and $e_{8}$
and $e_{11}$ are propagated. Fourth, $e_{7}$ is set true as a decision
literal, and $\overline{e_{9}}$, $\overline{e_{10}}$, and $e_{12}$ are
propagated. This gives a contradiction, since the clause
$e_{10}\lor\overline{e_{12}}$ (one of the two clauses from $e_{10}\oplus
e_{12}=0$) is falsified. Figure 5(a) shows the complete conflict graph at this
point.

Examining the conflict graph at decision level 4, the first UIP is $e_{7}$ and
there are two DIPs available, $\\{\overline{e_{9}},\overline{e_{10}}\\}$ and
$\\{\overline{e_{10}},e_{12}\\}$. Selecting the former DIP, we introduce a new
variable $x$ by extension as
$x\leftrightarrow\overline{e_{9}}\land\overline{e_{10}}$. We can learn the
additional pre- and post-DIP clauses:
$e_{4}\lor\overline{e_{5}}\lor\overline{e_{6}}\lor\overline{e_{7}}\lor x$ and
$\overline{x}\lor\overline{e_{11}}$.

We next backtrack to decision level 3, unsetting $e_{7}$, $e_{9}$, $e_{10}$
and $e_{12}$. Unit propagation at decision level 3 sets the new literal $x$
and the first UIP $\overline{e_{7}}$ false and then sets literals $e_{9}$,
$e_{10}$, and $\overline{e_{12}}$ true. This yields a contradiction with the
clause $\overline{e_{10}}\lor e_{12}$. In the conflict graph at decision level
3, the first UIP is $e_{6}$ and there are two DIPs available, namely
$\\{\overline{e_{7}},\overline{e_{12}}\\}$ and
$\\{e_{10},\overline{e_{12}}\\}$. If we select the first one, then we
introduce a new literal $y$ defined by extension as
$y\leftrightarrow\overline{e_{7}}\land\overline{e_{12}}$ and can in addition
learn the clauses $e_{3}\lor e_{4}\lor\overline{e_{5}}\lor\overline{e_{6}}\lor
y$ and $\overline{e_{5}}\lor\overline{y}$.

We do not carry this example further, but note that our experiments show that
Tseitin tautologies (not just on grid graphs) are examples where our
experiments show the DIP clause learning method is especially effective.

$e_{1}$Level 1:$\overline{e_{3}}$$e_{2}$Level
2:$\overline{e_{4}}$$e_{5}$$e_{6}$Level 3:$e_{8}$$e_{11}$$e_{7}$Level
4:$\overline{e_{9}}$$e_{12}$$\overline{e_{10}}$$\perp$(a):

$e_{1}$Level 1:$\overline{e_{3}}$$e_{2}$Level
2:$\overline{e_{4}}$$e_{5}$$e_{6}$Level
3:$e_{8}$$e_{11}$$\overline{x}$$\overline{e_{7}}$$e_{10}$$e_{9}$$\overline{e_{12}}$$\perp$(b):

Figure 5: The complete conflict graph from the example; (a) at the first
conflict and (b) at the second conflict. Boxed literals are decision literals.
Implications at the top decision level are in bold.

It is interesting to relate the Figure 5(b) to Theorem 4.3 on DIPs. In this
example, there is only one way to choose the two vertex-disjoint paths.
Namely, to let $\pi_{a}$ and $\pi_{b}$ be the paths
$e_{6},e_{8},e_{11},\overline{x},\overline{e_{7}},e_{10},\perp$ and
$e_{6},e_{9},\overline{e_{12}},\perp$. The edge from $e_{6}$ to
$\overline{e_{7}}$ bypasses $e_{8}$, $e_{11}$ and $\overline{x}$; and the edge
from $e_{11}$ to $\overline{e_{12}}$ is a crossing separator. (The edge from
$\overline{e_{7}}$ to $e_{9}$ is a “vacuous” crossing separator that does not
actually remove any possible DIP pairs.)

It should be evident from this example that many conflicts have DIPs; indeed
our experiments reported below show that approximately 2/3 of the conflicts
have at least one DIP and, very frequently there are quite a few choices for
DIPs.

###  5.2 Extending CDCL with Dual Implication Points

The use of DIPs in conflict analysis opens a large spectrum of possibilities.
This section discusses some of them, with particular attention to the
techniques that we have implemented. Our present implementation, xMapleLCM, is
a flexible framework that allows one to implement extended-resolution based
techniques in a simple way. It offers a set of clearly-specified functions
that facilitate determining which extension variables to add, performing the
corresponding addition, the possible posterior deletion or replacing
definitions in clauses. Additionally, a set of heuristic choices to control
when and how these steps are performed are provided, and replacing them by
custom ones is a smooth task. We want to remark that there are many more
possible strategies for using DIPs than could be discussed. We believe that in
this paper we merely scratched the surface of heuristics for exploiting DIPs,
which is an indication of the potential of this approach.

Choice of DIP. As mentioned, there is possibly a quadratic number of DIPs.
Even though we could learn multiple DIPs at every conflict, with their
corresponding lemmas, we decided to choose only one. The first possibility we
considered is to learn the DIP that is closest to the conflict, as we do with
UIPs. This may often create a short post-DIP conflict but a long pre-DIP
clause. Therefore, we considered the possibility of choosing a DIP that splits
the conflict graph into two balanced regions. Ideally, that would result in
two equally long pre and post-DIP clauses. Finally, we also implemented
choosing a random DIP, to check whether any of the other two schemes could
outperform a random strategy. These heuristics are referred to as closest,
middle, and random, respectively.

Filtering out bad-quality DIPs. Learning a DIP whenever we find one would be
too prolific and overwhelm the solver. In order to determine whether the DIP
chosen in the previous step had to be discarded, the first possibility we
explored was again inspired by 1-UIP learning, where learning glue clauses,
i.e. having LBD equal to $2$, is a desired situation. The first filtering
mechanism we implemented discarded all DIPs that did not have a glue post-DIP
clause. Another possibility we considered is to wait for a DIP to occur a
certain number of times before using it in DIP-based learning. In our
implementation, we tried $20$ and $5$ occurrences, as the minimum threshold to
introduce a DIP. A third possibility is to use the activity-based heuristic of
the literals in the DIP to assess its quality: DIPs whose literals have high
decision-heuristic scores should be prioritized. In our implementation, we
check whether the activity level of the current DIP is higher than the average
activity level of the 20 most recently encountered DIPs; if so, the current
DIP is a candidate for DIP-learning, otherwise it is discarded. We refer to
these various techniques as glue, occ5 and act, respectively.

Learning pre-DIP and post-DIP clauses. In our implementation, we only
considered two variants: one that always learns both the pre- and the post-DIP
clauses (2-clause) and one that only learns the post-DIP clause (1-clause).

Backjumping and asserting clauses. Recall that when a new DIP extension
variable $z$ is introduced, it is possible to learn a pre-DIP clause of the
form $\lnot f\lor\lnot C\lor z$ and a post-DIP clause of the form $\lnot
z\lor\lnot D$, where $f$ is the first UIP and where $C$ and $D$ are
conjunctions of literals that were set true at lower levels. (Note that $C$
and $D$ may have literals in common.) Letting $\ell_{C}$ and $\ell_{D}$ be the
maximum of the levels at which literals in $C$ and $D$ (respectively) were
set, our implementation always backtracks to level $\ell_{D}$. This makes the
post-DIP clause asserting, so $\lnot z$ is set at decision level $\ell_{D}$.
Furthermore, if $\ell_{C}\leq\ell_{D}$ and the pre-DIP clause is learned, then
it is asserting and $\lnot f$ is set by unit propagation at decision level
$\ell_{D}$, as it should be.

It would make no sense to backtrack to level $\ell_{C}$ when
$\ell_{C}<\ell_{D}$ since then neither $\lnot z$ nor $\lnot f$ would be
propagated. However, another possible strategy would be to backtrack to the
maximum of the decision levels $\ell_{C}$ and $\ell_{D}$. This would mean
$\lnot z$ and $\lnot f$ are both propagated. The disadvantage of this when
$\ell_{C}>\ell_{D}$ is that it would mean $\lnot z$ is asserted by the post-
DIP clause at level $\ell_{C}$, whereas it could have been propagated at the
previous decision level $\ell_{D}$. This breaks a usual invariant for CDCL
solvers. This would only be possible in a solver that permits chronological
backtracking [30, 29]; xMapleLCM, however, does not support this.

The previous reasoning needs some clarification for the case when the
extension variable $z$ with definition $z\leftrightarrow l_{1}\land l_{2}$ we
want to introduce already exists. If $z$ is undefined or defined at the
current decision level nothing changes. We know it cannot be true at some
previous level, because otherwise $l_{1}$ and $l_{2}$ would have been
propagated at that level, and not in the current one as all literals belonging
to a DIP do. If it is false at some previous level, then we have no guarantee
that the pre or the post-DIP clause is asserting at any decision level.
Fortunately, that rarely happens in practice. However, we can always perform
standard 1UIP learning or try to apply DIP-based conflict analysis starting
with the clause $z\lor\lnot l_{1}\lor\lnot l_{2}$ that we can guarantee is
conflicting at the current decision level.

Replacing literals by extended variables. In xMapleLCM, every time a new lemma
is learned, we try to replace some of its literals by extended variables. An
extended variable $z\leftrightarrow l_{1}\lor l_{2}$ allows one to replace a
lemma of the form $l_{1}\lor l_{2}\lor C$ by $z\lor C$. This is done by
checking, for all pairs of literals in the lemma that appear in some extended
variable definition whether they are part of the same definition. Lemmas that
are too long or have large LBD are discarded to mitigate the cost of this
operation.

If one wants to introduce literal $\lnot z$ and obtain some reduction in
formula size, the lemma should be of the form $\lnot l_{1}\lor C$ and there
should be another clause of the form $\lnot l_{2}\lor C$. In this case, they
can be replaced by a single clause $\lnot z\lor C$. However, this situation
can be expensive to detect since one has to traverse the whole database
looking for a certain clause, and this operation should be repeated for every
literal in the lemma. For this reason, xMapleLCM does not implement this.

Deleting extended variables. As it happens with lemma learning, where keeping
too many lemmas slows down unit propagation, managing too many extended
variables might also be counterproductive. Again following the analogy with
learned lemmas, which are useful at some point of the search but might become
inactive after a while, it is natural to think that extended variables follow
the same behavior. All in all, it seems mandatory to consider the deletion of
extended variables.

Deletion of variables in xMapleLCM is scheduled to be performed every $1000$
conflicts. At that point, several strategies are possible: delete all
variables, delete the ones with a minimum decision-heuristic activity, or
delete the worst $k\%$ variables according to some criterion (e.g. their
decision-heuristic activity). In our implementation, we do the latter with
$k=50$. Note that variables appearing in the right-hand side of an extended-
variable definition cannot be deleted. This is addressed by maintaining a
counter for every variable that corresponds to the number of definitions where
it is involved.

##  6 Experimental Evaluation

We have implemented the DIP-based clause learning schemes described in Section
5.2 on top of the xMapleLCM ER framework333All sources used for this
evaluation can be found in https://github.com/chjon/xMapleSAT/tree/main.. We
started our experimental evaluation running a variant of DIP-based learning on
all benchmarks of the 2023 SAT Competition [6] and comparing it to MapleLCM
[25], the CDCL SAT solver on which it is based. Even though there did not seem
to be a systematic improvement on all benchmarks, a few families with
important speedups were identified. We start this section by analyzing the
impact of DIP-based learning on these families and then move to final
considerations about the performance on the overall 2023 SAT competition
benchmarks.

###  6.1 Performance Analysis Methodology

For each family, we start by describing the problem they encode. After that,
we report on the performance of a variety of state-of-the-art solvers, each
with some distinguished characteristic: Kissat 3.1.1 [8] (an extremely
efficient CDCL solver), CryptoMiniSat 5.11 [36] (support for XOR reasoning),
SBVA+CaDiCaL [14] (introduction of new variables via SBVA and winner of the
main track of the 2023 SAT Competition), GlucoseER [3] (extended-resolution
based CDCL solver) and a variant of xMapleLCM-DIP, which we refer to as the
baseline, that we describe next.

Finally, we evaluate the impact of the different techniques explained in
Section 5.2. In particular, we first consider as a baseline a version that (i)
finds DIPs in the middle of the conflict graph, (ii) only adds a DIP if it has
occurred at least 20 times and (iii) always learns the both pre- and post-DIP
learning clauses. Different variants can be obtained by changing only one of
the three previous design decisions at a time. Regarding the type of DIP used,
we analyze the performance of closest and random, that is, the systems whose
only difference w.r.t. baseline is that the type of DIP is changed. Regarding
the criterion used to discard a DIP, we analyze the glue, act and occ5
configurations, where the latter discards any DIP that has not occurred at
least 5 times. Finally, the 1-clause variant only learns the post-DIP clause.
Our goal is to understand why certain configurations do not work well on
particular families.

####  6.1.1 Matching of Properly Intersecting Intervals

We are given a sequence of numbers $(a_{1},\ldots,a_{n})$, initially all set
to zero, and a set of operations, each consisting of assigning a certain
number to a contiguous subsequence of the $a_{i}$’s, defined by an interval.
The goal is to perform each operation exactly once while maximizing the number
of pairs of consecutive numbers $(a_{i},a_{i+1})$ that are different at the
end of the process. Given some additional conditions, this can be formulated
as maximum bipartite matching problem on a certain graph. By removing some
edges from this graph, an unsatisfiable problem is generated. A more detailed
description can be found in [6].

We downloaded the 23 instances submitted to the 2023 SAT Competition, using
the Global Benchmark Database [20], and observed that no system without
extended-resolution reasoning could solve any benchmark in a time limit of 1
hour. On the other hand, there are 14 benchmarks that GlucoseER could solve,
of which our DIP-based variants could solve 7. Detailed results for our
variants can be seen in Table 1.

| Baseline | 1-Clause | Closest | Rand | Glue | Occ5 | Act
---|---|---|---|---|---|---|---
PROPERLY INTERSECTING INTERVALS FORMULAS
SOLVED | 6 | 5 | 7 | 7 | 0 | 0 | 0
BEST | 1 | 1 | 2 | 3 | 0 | 0 | 0
Median (secs.) | 2777 | 2566 | 2358 | 2189 | 3600 | 3600 | 3600
TSEITIN FORMULAS
SOLVED | 11 | 13 | 13 | 11 | 0 | 15 | 3
BEST | 2 | 5 | 0 | 0 | 0 | 8 | 0
Median (secs.) | 897 | 628 | 2707 | 2782 | 3600 | 425 | 3600
(X)ORIFIED RANDOM $k$-xor FORMULAS
SOLVED | 10 | 8 | 11 | 9 | 0 | 9 | 7
BEST | 5 | 2 | 1 | 2 | 0 | 1 | 0
Median (secs.) | 430 | 803 | 1080 | 820 | 3600 | 936 | 3112
Table 1: Performance of DIP-learning variants on three sets of formulas.
Median running times are in seconds and, for each row, the best performing
system is in bold.

For this particular type of formulas, the rand variant performs the best, but
detailed results indicate that we cannot claim it is systematically faster.
One clear conclusion we can infer is that glue, occ5 and act exhibit very poor
performance. A more detailed analysis on the runs of these systems reveal
that, at least in these benchmarks, both act and occ5 apply DIP learning in
many more conflicts than the other variants, whereas the distinctive
characteristic of glue is that the percentage of decisions on extended
variables was extremely low. As can be seen at the end of this section, the
latter is a situation than tends to indicate the DIP learning is not helping
the solver in this context.

####  6.1.2 Tseitin Formulas

These formulas have already been described in Section 5.1. In this section, we
consider unsatisfiable formulas generated by CNFgen [24]. We started
generating instances with grids of size $n\times n$ and ran all systems with a
time limit of 300 seconds in order to analyze how different solvers scale. The
performance of all systems can be seen on the left plot in the first row of
Figure 6 (note the logarithmic scale on the $y$ axis). A point $(x,y)$ in a
solver line indicates that the solver took $y$ seconds to solve the Tseitin
formula on grid size $x\times x$.

Figure 6: Performance analysis of different solvers on Tseitin formulas.

These formulas are easy for CryptoMiniSat, since the application of Gaussian
elimination in a preprocessing step solves them. Regarding the rest of the
systems, only our DIP-based tool and GlucoseER have good scaling properties.
We want to remark that this behavior is not unique to Tseitin formulas on the
grid. We generated Tseitin formulas over random $4$-regular and $6$-regular
graphs and the conclusions are the same as can be seen in the other two plots
in the first row of Figure 6. These results start suggesting that, even though
GlucoseER and our DIP-based learning are quite different approaches to
integrating ER into CDCL solvers, they seem to perform well on the same sets
of benchmarks.

In order to understand whether the behavior of xMapleLCM-DIP was polynomial,
we generated more challenging instances. Results can be seen in the left plot
on the second row of Figure 6, with logarithmic scale on the $y$ axis. There
is little doubt that the runtime of our solver ends up being exponential
w.r.t. the size of the problem. However, we went one step further and studied
how large the generated DRAT proofs were. In the same row, but on the right,
we show the number of resolution steps in the proof. Despite having no
theoretical support for that, it seems that although the solver takes
exponential time in finding a proof, its size might be polynomial w.r.t. the
problem size. That would indicate that our problem is having search heuristics
that are not good enough to quickly find a short proof.

Finally, as we did in the previous section, we want to study the effect of the
possible variants of DIP-based learning. For that purpose, we selected 5
challenging benchmarks of each type (grid, 4-regular, 6-regular) and evaluated
the 7 DIP variants that we want to examine. Results can again be found in
Table 1.

For Tseitin formulas, occ5 performs much better than the rest. Its only
difference is that the minimum number of occurrences for a DIP to be
introduced is smaller; this suggests that, in these instances, being more
aggressive in the introduction of DIP extension variables provides a
competitive advantage. On the other hand, glue solves no instance. We realized
that DIP-learning was hardly ever applied, that is, requiring glue clauses was
too restrictive here. Regarding act, whose performance is similarly poor, the
main noticeable difference in its behavior is exhibiting a very large number
of conflicts where DIP learning is applied, between 20 and 50%, which is
around ten times more than the variants that performed best.

####  6.1.3 (X)Orified Random k-XOR Formulas

One last family where DIP-based systems perform very well are random $k$-xor
formulas, where orification or xorification [7] has been applied, i.e.,
replacing variables by (x)ors of fresh variables. We used CNFgen to obtain 4
sets of formulas: xor constraints of length 3 applying orification with 2 and
3 variables, and also with xorification of 2 and 3 variables. All formulas we
consider are unsatisfiable, the number of variables before (x)orification is
equal to the number of clauses, and we increase this number to get
progressively more difficult formulas.

We studied the scaling properties of all systems by running them on
increasingly larger benchmarks with a time limit of 300 seconds. Results can
be seen in Figure 7, where the $y$ axis has logarithmic scale. Maybe
surprisingly, CryptoMiniSat can only benefit from its preprocessing step in
one of the families (2-xorified). Also, SBVA-CaDiCaL performs very well in two
of them (2 and 3-orified). Again, both GlucoseER and our DIP-based
implementations show the best average overall performance over all
competitors.

Figure 7: Performance analysis of different solvers on (x)orified random
$k$-xor formulas.

Finally, an analysis of the impact of the different DIP-learning variants can
be found in Table 1. Our baseline implementation seems to perform the best,
but there are several other configurations that perform very well. On the
negative side, glue did not solve any such formula within the time limit. The
identifying characteristic of that version is that the percentage of conflicts
with DIP-learning is very low compared to the others (around 0.1%).

###  6.2 Performance Analysis on 2023 SAT Competition Benchmarks

Our experimental evaluation concludes with the lessons we have learned from
executing our DIP-variants444We do not present a comparison with state-of-the-
art solvers like Kissat or CaDiCaL since there are not many lessons to be
learned. In a few words, our MapleLCM baseline CDCL solver is slower that
those systems, and adding DIP-reasoning to it does not bridge this gap. on all
benchmarks from the 2023 SAT Competition. We first report on the overhead
caused by the DIP detection algorithm and the subsequent additional work to
retrieve the clauses to be learned. For our baseline DIP-based system, where
two clauses are learned and hence is the most computationally demanding
method, in 4.5% of the benchmarks the DIP-related work represented between 10
and 15% of the total runtime; in 11.5% of the benchmarks between 5 and 10%; in
35.5% between 2.5 and in 48.5% less than 2.5%. These data show that DIP
computation does not significantly slow down the solver. Another interesting
information concerns the percentage of conflicts where there is at least one
DIP, which was on average 63%. This implies that we do need to have filtering
mechanisms to discard some of them. Otherwise, the search would be totally
dominated by DIPs.

A cactus plot with the results of executing all our DIP variants on the 2023
SAT Competition benchmarks with a time limit of one hour is in the left plot
of Figure 8. Three variants are much worse than the rest: act, occ5 and glue,
whereas the other are relatively similar. These three configurations have a
much larger percentage of conflicts where DIP-based learning is applied than
the rest, being around 30% in act and around 5% in the other two. In the best
performing variant this is around 1%, which seems to be a very low number and
one might wonder whether this is enough to have any effect at all. This can be
answered by analyzing the percentage of decisions on extended variables. For
all benchmarks where DIP-based systems outperform the baseline CDCL solver,
this number is surprisingly large, being usually over 10% of the decisions,
whereas for most of the benchmarks is very low (in 70% of the benchmarks less
than 1% of decisions are on extended variables). Moreover, this does not only
happen in problems with a very low number of initial variables, where the
introduction of a few extended variables could quickly dominate the decision
heuristic.

This is remarkable since it shows that already existing decision heuristics
like VSIDS or LRB somehow infer whether the newly introduced variables improve
the behavior of the system. This is why we implemented, on top of our baseline
DIP system, a procedure that computes the percentage of decisions on extended
variables. If after a given number of conflicts it is still lower than 3%, it
discontinues DIP learning and performs 1-UIP learning from that moment
onwards. This is a very preliminary step in the direction of trying to
automate the decision of whether to apply DIP reasoning or not, but the
outcome, which is found in the right plot of Figure 8, is very positive.

Figure 8: Performance of DIP variants on 2023 SAT Competition benchmarks.

##  7 Conclusions and Future Work

We introduce a novel extended resolution clause learning (ERCL) algorithm,
that when implemented on top of a CDCL solver, turns out to be beneficial for
a variety of problems, in particular Tseitin, random k-xor and interval
matching formulas. This is remarkable since automating powerful proof systems
is well-known to be a difficult task. Somewhat surprisingly, the only
previously existing attempt to incorporate ER into CDCL performs similarly on
the same instances. Considering the different nature of the two methods, this
clearly deserves further study. Further, we also introduce a new heuristic
that allows our ERCL solver xMapleSAT to perform similarly to the baseline
CDCL solver MapleLCM, thus being able to get the best of both worlds, i.e.,
the benefit of ERCL, without sacrificing performance of the CDCL solver on,
say, SAT Competition Main Track 2023 instances. As future work, we plan to
investigate a variety of machine learning based heuristics (e.g., branching)
specialized for the ERCL method. Also, the use of $k$-IPs with $k>2$ is part
of our next steps. On the theoretical side, challenging questions like
determining whether DIP- or $k$-IP based ER simulates unrestricted ER are
going to be central to our research efforts.

## References

  * [1] Albert Atserias, Johannes Klaus Fichte, and Marc Thurley.  Clause-learning algorithms with many restarts and bounded-width resolution.  Journal of Artificial Intelligence Research, 40:353–373, January 2011.  Preliminary version in _SAT ’09_.
  * [2] Albert Atserias, Johannes Klaus Fichte, and Marc Thurley.  Clause-learning algorithms with many restarts and bounded-width resolution.  J. Artif. Intell. Res., 40:353–373, 2011.  doi:10.1613/jair.3152.
  * [3] Gilles Audemard, George Katsirelos, and Laurent Simon.  A restriction of extended resolution for clause learning sat solvers.  In AAAI, 2010.
  * [4] Gilles Audemard and Laurent Simon.  Predicting learnt clauses quality in modern SAT solvers.  In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399–404, 2009.  URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  * [5] Fahiem Bacchus.  Enhancing Davis Putnam with extended binary clause learning.  In Proc. 18th Annual Conference on Artificial Intelligence and 15th Conference on Innovative Applications of Artificial Intelligence, pages 613–619. AAAI Press and MIT Press, 2002.
  * [6] Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors.  Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions.  Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023.
  * [7] Eli Ben-Sasson.  Size space tradeoffs for resolution.  SIAM Journal on Computing, 38(6):2511–2525, 2009.
  * [8] Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger.  CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020.  In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51–53. University of Helsinki, 2020\.
  * [9] Armin Biere, Nils Froleyks, and Wenzi Wang.  CadiBack: Extracting backbones with CaDiCal.  In Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing SAT, pages 3:1–12. Leibniz-Zentrum für Informatik, 2023.
  * [10] Randal E. Bryant and Marijn J. H. Heule.  Generating extended resolution proofs with a bdd-based SAT solver.  ACM Trans. Comput. Log., 24(4):31:1–31:28, 2023.  doi:10.1145/3595295.
  * [11] Sam Buss, Vijay Ganesh, and Albert Oliveras.  A linear time algorithm for two-vertex bottlenecks.  In preparation. Preliminary version available at https://math.ucsd.edu/~sbuss/ResearchWeb/TwoVertBottlenecks, March 2024\.
  * [12] Sam Buss, Oliver Kullmann, and Virginia Vassilevska Williams.  Dual depth first search for binary clause reasoning.  Preliminary version, March 2024.
  * [13] Stephen A. Cook.  A short proof of the pigeon hole principle using extended resolution.  SIGACT News, 8(4):28–32, 1976.  doi:10.1145/1008335.1008338.
  * [14] Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule.  Effective auxiliary variables via structured reencoding.  In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 11:1–11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.SAT.2023.11, doi:10.4230/LIPICS.SAT.2023.11.
  * [15] Armin Haken.  The intractability of resolution.  Theoretical computer science, 39:297–308, 1985.
  * [16] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere.  Short proofs without new variables.  In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 130–147. Springer, 2017.  doi:10.1007/978-3-319-63046-5\\_9.
  * [17] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere.  Encoding redundancy for satisfaction-driven clause learning.  In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference (TACAS 2019), Part I, Lecture Notes in Computer Science 11427, pages 41–58. Springer Verlag, 2019.
  * [18] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere.  Strong extension-free proof systems.  J. Autom. Reason., 64(3):533–554, 2020.  doi:10.1007/s10817-019-09516-0.
  * [19] Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere.  Pruning through satisfaction.  In Ofer Strichman and Rachel Tzoref-Brill, editors, Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings, volume 10629 of Lecture Notes in Computer Science, pages 179–194. Springer, 2017.  doi:10.1007/978-3-319-70389-3\\_12.
  * [20] Markus Iser and Carsten Sinz.  A problem meta-data library for research in sat.  In Daniel Le Berre and Matti J\"arvisalo, editors, Proceedings of Pragmatics of SAT 2015 and 2018, volume 59 of EPiC Series in Computing, pages 144–152. EasyChair, 2019.  URL: https://easychair.org/publications/paper/jQXv, doi:10.29007/gdbb.
  * [21] Henry A. Kautz.  Deconstructing planning as satisfiability.  In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA, pages 1524–1526. AAAI Press, 2006.  URL: http://www.aaai.org/Library/AAAI/2006/aaai06-241.php.
  * [22] Henry A. Kautz and Bart Selman.  Planning as satisfiability.  In Bernd Neumann, editor, 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, pages 359–363. John Wiley and Sons, 1992.
  * [23] Daniel Kroening.  Software verification.  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 791–818. IOS Press, 2021.  doi:10.3233/FAIA201004.
  * [24] Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals.  Cnfgen: A generator of crafted benchmarks.  In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 464–473. Springer, 2017.  doi:10.1007/978-3-319-66263-3\\_30.
  * [25] Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü.  An effective learnt clause minimization approach for CDCL SAT solvers.  In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 703–711. ijcai.org, 2017.  URL: https://doi.org/10.24963/ijcai.2017/98, doi:10.24963/IJCAI.2017/98.
  * [26] Norbert Manthey, Marijn Heule, and Armin Biere.  Automated reencoding of boolean formulas.  In Armin Biere, Amir Nahir, and Tanja E. J. Vos, editors, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science, pages 102–117. Springer, 2012.  doi:10.1007/978-3-642-39611-3\\_14.
  * [27] 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.
  * [28] Karl Menger.  Zur algemeinen Kurventheorie.  Fundamenta Mathematicae, 10:96–115, 1927.
  * [29] Sibyle Möhle and Armin Biere.  Backing backtracking.  In 22nd Intl Conf. on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science 11628, pages 250–266. Springer, 2019.
  * [30] Alexander Nadel and Vadim Ryvchin.  Chronological backtracking.  In 21nd Intl Conf. on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science 10929, pages 111–121. Springer, 2018.
  * [31] Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh.  Learning shorter redundant clauses in SDCL using maxsat.  In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 18:1–18:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.  URL: https://doi.org/10.4230/LIPIcs.SAT.2023.18, doi:10.4230/LIPICS.SAT.2023.18.
  * [32] Knot Pipatsrisawat and Adnan Darwiche.  On modern clause-learning satisfiability solvers.  Journal of Automated Reasoning, 44(3):277–301, 2010.
  * [33] Knot Pipatsrisawat and Adnan Darwiche.  On the power of clause-learning SAT solvers as resolution engines.  Artif. Intell., 175(2):512–525, 2011.  doi:10.1016/j.artint.2010.10.002.
  * [34] Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant.  Preprocessing of propagation redundant clauses.  In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 106–124. Springer, 2022.  doi:10.1007/978-3-031-10769-6\\_8.
  * [35] Karem A. Sakallah.  Symmetry and satisfiability.  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 509–570. IOS Press, 2021.  doi:10.3233/FAIA200996.
  * [36] Mate Soos, Karsten Nohl, and Claude Castelluccia.  Extending SAT solvers to cryptographic problems.  In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244–257. Springer, 2009.  doi:10.1007/978-3-642-02777-2\\_24.
  * [37] Grigori S Tseitin.  On the complexity of derivation in propositional calculus.  Automation of reasoning: 2: Classical papers on computational logic 1967–1970, pages 466–483, 1983.
  * [38] Alasdair Urquhart.  Hard examples for resolution.  J. ACM, 34(1):209–219, 1987.  doi:10.1145/7531.8928.
  * [39] Yichen Xie and Alexander Aiken.  Saturn: A SAT-Based Tool for Bug Detection.  In Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005, pages 139–143, 2005.  doi:10.1007/11513988\\_13.
  * [40] Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik.  Efficient conflict driven learning in boolean satisfiability solver.  In Rolf Ernst, editor, Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001, pages 279–285. IEEE Computer Society, 2001.  doi:10.1109/ICCAD.2001.968634.


\end{align}

This evolution corresponds to a QCA obtained with two layers of controled-phase gates $C_{\phi'}$ and one layer of local unitary gates given by $\exp(-i\sigma_z\theta')$, with

\begin{align}
\begin{cases}
\phi'=-2\phi,\\
\theta'=\phi.
\end{cases}
\end{align}

* $l(k)=c_1$ or $j(k)=c_1$ constant. Let us assume without loss of generality that $l(k)=c_1$. It is easy to see that eq.(<ref>) reduces to :

\begin{align*}
\omega_1(\mathbf{k})\omega_2(\mathbf{k})=\prod_{\alpha=0}^3e^{2i\{\phi+\pi\}\delta_{c_1,l(k)}}=\\
\end{align*}

Again, we can express the two possible choices of $l(k)$ as $\frac{1}{2}+s_2(\frac{1}{2}-k)$ for $s_2=\pm 1$. Up to an irrelevant phase factor, this reduces to:

\begin{align*}
\omega_1(\mathbf{k})\omega_2(\mathbf{k})=\prod_{\alpha=0}^3e^{-2is_2(2c_1-1)k_\alpha\{\phi+\pi\}}.
\end{align*}

This evolution corresponds to a QCA obtained one layer of local unitary gates given by $\exp(-i\sigma_z\theta')$, with

\begin{align}
\theta'=-s_2(2c_1-1)\phi.
\end{align}

§ DERIVATION OF THE FORM OF G FOR THE QUBIT CASE

Here we show the details of the derivation of the explicit form of $G_{CG}^\mathcal{M}$ and $G_{CG}^\mathcal{A}$. First of all it is convenient to introduce the following parametrization for G in eq.$(\ref{eq:Gqubit})$:

\begin{equation}
\begin{split}
&=C_\phi(R_z(\epsilon))^{\otimes 2} (R_y(\gamma))^{\otimes 2}(R_z(\epsilon-\theta))^{\otimes 2}C_\phi
\end{split}
\label{eq:gparam}
\end{equation}

Here we simply used the Euler decomposition of $U$:

\begin{equation}
\end{equation}

§.§ Factorised $G$

Here we prove that if $G=V\otimes V$, then the controlled-phase gate $C_\phi$ has either $\phi=2\pi$ (i.e. $C_\phi=I$), or $\phi=\pi$. Let us start
expressing $G$ in the following block form

in the computational basis

\begin{equation}
U_{00}U & U_{01}U\eiph\\
U_{10}\eiph U & U_{11} \eiph U \eiph\end{pmatrix}
\label{eq:gU}
\end{equation}

and we want

\begin{equation}
G=V\otimes V = \begin{pmatrix} V_{00} V & V_{01} V\\
V_{10} V & V_{11} V.
\end{pmatrix}
\label{eq:gV}
\end{equation}

This means that, if $U$ is neither diagonal nor anti-diagonal in the computational basis, it must be

\begin{equation}
\resizebox{0.95\hsize}{!}{$U \propto U\eiph \propto \eiph U \propto \eiph U \eiph$}
\end{equation}

and this clearly implies

\begin{equation}
\begin{split}
\phi=&2n\pi,\quad n\in\mathbb Z\\
G=&U\otimes U.
\end{split}
\end{equation}

If now we take $U$ to be diagonal, i.e. we set $\gamma=n\pi$ with $n\in\mathbb Z$ in eq.$(\ref{eq:gparam})$, we have, up to a global phase:

\begin{equation}
U=\begin{pmatrix}e^{i(2\epsilon-\theta)} & 0 \\ 0 & e^{-i({2\epsilon-\theta})} \,,\end{pmatrix}
\end{equation}

and comparing eq.$(\ref{eq:gU})$ and eq.$(\ref{eq:gV})$ we have:

\begin{equation}
U\propto \eiph U \eiph\,,
\end{equation}

which is solved for:

\begin{equation}
\phi=m\pi,\quad m\in\mathbb Z.
\end{equation}

This reduces to

\begin{align}
G&=C_{\pi} (R_z(2\epsilon-\theta)\otimes R_z(2\epsilon-\theta)) C_{\pi}\\
&=(R_z(2\epsilon-\theta)\otimes R_z(2\epsilon-\theta)),
\end{align}

i.e., once again, $G=U\otimes U$.
Finally, if $U$ is anti-diagonal, i.e. $\gamma=\frac{2n+1}{2}\pi$ for $n\in\mathbb Z$, we have

\begin{equation}
0& 1\\ -1 & 0
\end{pmatrix}\,.
\end{equation}

Moreover, it must be

\begin{equation}
\eiph U \propto U \eiph.
\end{equation}

But this reduces to the known condition

\begin{equation}
\phi=m\pi,\quad m\in\mathbb Z.
\end{equation}

Also in this case, $G=U\otimes U$ with $U=i\sigma_x$ for $\phi=(2k+1)\pi$, while $U=i\sigma_y$ for $\phi=2k\pi$.

[1]
Richard P. Feynman.
Simulating physics with computers.
International Journal of Theoretical Physics, 21(6):467–488,

[2]
John Von Neumann and Arthur W. Burks.
Theory of Self-Reproducing Automata.
University of Illinois Press, USA, 1966.

[3]
K.P. Hadeler and J. Müller.
Cellular Automata: Analysis and Applications.
Springer Monographs in Mathematics. Springer International
Publishing, 2017.

[4]
Gerhard Grössing and Anton Zeilinger.
Quantum cellular automata.
Complex Syst., 2(2):197–208, apr 1988.

[5]
J. Watrous.
On one-dimensional quantum cellular automata.
In Proceedings of IEEE 36th Annual Foundations of Computer
Science, pages 528–537, 1995.

[6]
Christoph Dürr, Huong Lê Thanh, and Miklos Santha.
A decision procedure for well-formed linear quantum cellular
In Claude Puech and Rüdiger Reischuk, editors, STACS 96,
pages 281–292, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.

[7]
Christoph Dürr and Miklos Santha.
A decision procedure for unitary linear quantum cellular automata.
SIAM Journal on Computing, 31(4):1076–1089, 2002.

[8]
Jozef Gruska.
Quantum Computing, pages 2297–2310.
John Wiley & Sons, Ltd, 2009.

[9]
B. Schumacher and R. F. Werner.
Reversible quantum cellular automata.
quant-ph/0405174, 2004.

[10]
Pablo Arrighi, Vincent Nesme, and Reinhard Werner.
One-dimensional quantum cellular automata over finite, unbounded
In Carlos Martín-Vide, Friedrich Otto, and Henning Fernau,
editors, Language and Automata Theory and Applications, pages 64–75,
Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

[11]
D. J. Shepherd, T. Franz, and R. F. Werner.
Universally programmable quantum cellular automaton.
Phys. Rev. Lett., 97:020502, Jul 2006.

[12]
Pablo Arrighi, Renan Fargetton, and Zizhu Wang.
Intrinsically universal one-dimensional quantum cellular automata in
two flavours.
Fundamenta Informaticae, 91(2):197–230, 2009.

[13]
Giacomo Mauro D'Ariano and Paolo Perinotti.
Derivation of the dirac equation from principles of information
Phys. Rev. A, 90:062106, Dec 2014.

[14]
Alessandro Bisio, Giacomo Mauro D'Ariano, and Paolo Perinotti.
Quantum cellular automaton theory of light.
Annals of Physics, 368:177–190, 2016.

[15]
Arindam Mallick and C. M. Chandrashekar.
Dirac cellular automaton from split-step quantum walk.
Scientific Reports, 6(1):25779, 2016.

[16]
Pablo Arrighi, Cédric Bény, and Terry Farrelly.
A quantum cellular automaton for one-dimensional qed.
Quantum Information Processing, 19(3):88, 2020.

[17]
Alessandro Bisio, Giacomo Mauro D'Ariano, Paolo Perinotti, and Alessandro
Thirring quantum cellular automaton.
Physical Review A, 97(3):032132, 2018.

[18]
Alessandro Bisio, Nicola Mosco, and Paolo Perinotti.
Scattering and perturbation theory for discrete-time dynamics.
Physical Review Letters, 126(25):250503, 2021.

[19]
Nathanaël Eon, Giuseppe Di Molfetta, Giuseppe Magnifico, and Pablo
A relativistic discrete spacetime formulation of 3+1 QED.
Quantum, 7:1179, November 2023.

[20]
Lorenzo Piroli and J. Ignacio Cirac.
Quantum cellular automata, tensor networks, and area laws.
Phys. Rev. Lett., 125:190402, Nov 2020.

[21]
Alexander Jahn, Zoltán Zimborás, and Jens Eisert.
Tensor network models of AdS/qCFT.
Quantum, 6:643, February 2022.

[22]
Logan E. Hillberry, Lorenzo Piroli, Eric Vernier, Nicole Yunger Halpern,
Tomaž Prosen, and Lincoln D. Carr.
Integrability of goldilocks quantum cellular automata.
arXiv:2404.02994, 2024.

[23]
David T Stephen, Hendrik Poulsen Nautrup, Juani Bermejo-Vega, Jens Eisert, and
Robert Raussendorf.
Subsystem symmetries, quantum cellular automata, and computational
phases of quantum matter.
Quantum, 3:142, 2019.

[24]
Hoi Chun Po, Lukasz Fidkowski, Takahiro Morimoto, Andrew C Potter, and Ashvin
Chiral floquet phases of many-body localized bosons.
Physical Review X, 6(4):041070, 2016.

[25]
Lukasz Fidkowski, Hoi Chun Po, Andrew C Potter, and Ashvin Vishwanath.
Interacting invariants for floquet phases of fermions in two
Physical Review B, 99(8):085115, 2019.

[26]
Alexei Kitaev and John Preskill.
Topological entanglement entropy.
Physical review letters, 96(11):110404, 2006.

[27]
Paolo Perinotti.
Cellular automata in operational probabilistic theories.
Quantum, 4:294, July 2020.

[28]
We stress that the universality notion invoked here is different from
computational universality, which in simple words refers to the ability of a
computational model to simulate any other conceivable computer.

[29]
Jean Zinn-Justin.
Phase Transitions and Renormalization Group.
Oxford University Press, 07 2007.

[30]
Leo P. Kadanoff.
Scaling laws for ising models near ${T}_{c}$.
Physics Physique Fizika, 2:263–272, Jun 1966.

[31]
Kenneth G. Wilson.
Renormalization group and critical phenomena. i. renormalization
group and the kadanoff scaling picture.
Phys. Rev. B, 4:3174–3183, Nov 1971.

[32]
Kenneth G. Wilson.
Renormalization group and critical phenomena. ii. phase-space cell
analysis of critical behavior.
Phys. Rev. B, 4:3184–3205, Nov 1971.

[33]
Navot Israeli and Nigel Goldenfeld.
Computational irreducibility and the predictability of complex
physical systems.
Phys. Rev. Lett., 92:074105, Feb 2004.

[34]
Navot Israeli and Nigel Goldenfeld.
Coarse-graining of cellular automata, emergence, and the
predictability of complex systems.
Phys. Rev. E, 73:026203, Feb 2006.

[35]
Pierre-Gabriel Rozon, Michael J. Gullans, and Kartiek Agarwal.
Constructing quantum many-body scar hamiltonians from floquet
Phys. Rev. B, 106:184304, Nov 2022.

[36]
John Preskill.
Quantum Computing in the NISQ era and beyond.
Quantum, 2:79, August 2018.

[37]
Mauro Faccin, Michael T Schaub, and Jean-Charles Delvenne.
Entrograms and coarse graining of dynamics on complex networks.
Journal of Complex Networks, 6(5):661–678, 11 2017.

[38]
Sometimes in the literature QCAs can be defined without the homogeneity
property, and what we call a QCA would then be a homogeneous
QCA (see e.g. Ref. <cit.>).

[39]
The most general structure on which homogeneous QCAs can be defined is the
Cayley graph of some finitely presented group $G$ <cit.>.
However here we will restrict to the case where $G$ is abelian.

[40]
Giacomo Mauro D'Ariano and Paolo Perinotti.
Quantum cellular automata and free quantum field theory.
Frontiers of Physics, 12(1):120301, 2016.

[41]
O. Bratteli and D.W. Robinson.
Operator Algebras and Quantum Statistical Mechanics 1: C*- and
W*-Algebras. Symmetry Groups. Decomposition of States.
Operator Algebras and Quantum Statistical Mechanics. Springer, 1987.

[42]
R. Haag.
Local Quantum Physics: Fields, Particles, Algebras.
R.Balian, W.Beiglbock, H.Grosse. Springer-Verlag, 1992.

[43]
D. Gross, V. Nesme, H. Vogts, and R. F. Werner.
Index theory of one dimensional quantum walks and cellular automata.
Communications in Mathematical Physics, 310(2):419–454, jan

[44]
Paolo Zanardi.
Stabilizing quantum information.
Phys. Rev. A, 63:012301, Dec 2000.

[45]
It is easy to prove that the support algebra does not depend on the choice of
the basis $\protect \{e_\mu \protect \}$.

[46]
Jean-Luc Brylinski and Ranee Brylinski.
Universal quantum gates.
In Mathematics of quantum computation, pages 117–134. Chapman
and Hall/CRC, 2002.

[47]
Actually, it is shown in the Appendix that it is sufficient to consider a
lattice $\protect \mathbb {Z}_n$ with n even and greater than $6$.

[48]
Pablo Arrighi, S. Martiel, and V. Nesme.
Cellular automata over generalized Cayley graphs.
Mathematical Structures in Computer Science, 18:340–383,