# Speculative SAT Modulo SAT

Hari Govind V K  University of Waterloo
Waterloo, Canada
<EMAIL_ADDRESS>Isabel Garcia-Contreras  University of Waterloo
Waterloo, Canada
<EMAIL_ADDRESS>Sharon Shoham  Tel-Aviv University
Tel-Aviv, Israel
<EMAIL_ADDRESS>Arie Gurfinkel  University of Waterloo
Waterloo, Canada
<EMAIL_ADDRESS>
###### Abstract

State-of-the-art model-checking algorithms like IC3/PDR are based on uni-
directional modular SAT solving for finding and/or blocking counterexamples.
Modular SAT-solvers divide a SAT-query into multiple sub-queries, each solved
by a separate SAT-solver (called a module), and propagate information (lemmas,
proof obligations, blocked clauses, etc.) between modules. While modular
solving is key to IC3/PDR, it is obviously not as effective as monolithic
solving, especially when individual sub-queries are harder to solve than the
combined query. This is partially addressed in SAT modulo SAT (SMS) by
propagating unit literals back and forth between the modules and using
information from one module to simplify the sub-query in another module as
soon as possible (i.e., before the satisfiability of any sub-query is
established). However, bi-directionality of SMS is limited because of the
strict order between decisions and propagation – only one module is allowed to
make decisions, until its sub-query is SAT. In this paper, we propose a
generalization of SMS, called specSMS, that _speculates_ decisions between
modules. This makes it bi-directional – decisions are made in multiple
modules, and learned clauses are exchanged in both directions. We further
extend DRUP proofs and interpolation, these are useful in model checking, to
specSMS. We have implemented specSMS in Z3 and show that it performs
exponentially better on a series of benchmarks that are provably hard for SMS.

##  I Introduction

IC3/PDR [3] is an efficient SAT-based Model Checking algorithm. Among many
other innovations in IC3/PDR is the concept of a modular SAT-solver that
divides a formula into multiple _frames_ and each frame is solved by an
individual SAT solver. The solvers communicate by exchanging proof obligations
(i.e., satisfying assignments) and lemmas (i.e., learned clauses).

While modular reasoning in IC3/PDR is very efficient for a Model Checker, it
is not as efficient as a classical monolithic SAT-solver. This is not
surprising since modularity restricts the solver to colorable refutations
[11], which are, in the worst case, exponentially bigger than unrestricted
refutations. On the positive side, IC3/PDR’s modular SAT-solving makes
interpolation trivial, and enables generalizations of proof obligations and
inductive generalization of lemmas – both are key to the success of IC3/PDR.

This motivates the study of modular SAT-solving, initiated by SMS [1]. Our
strategic vision is that our study will contribute to improvements in IC3/PDR.
However, in this paper, we focus on modular SAT-solving in isolation.

In modular SAT-solving, multiple solvers interact to check satisfiability of a
partitioned CNF formula, where each part of the formula is solved by one of
the solvers. In this paper, for simplicity, we consider the case of two
solvers $\langle S_{{\sf s}},S_{{\sf m}}\rangle$ checking satisfiability of a
formula pair $\langle\Phi_{\sf s},\Phi_{\sf m}\rangle$. $S_{{\sf m}}$ is a
_main_ solver and $S_{{\sf s}}$ is a _secondary_ solver. In the notation, the
solvers are written right-to-left to align with IC3/PDR, where the main solver
is used for frame 1 and the secondary solver is used for frame 0.

When viewed as a modular SAT-solver, IC3/PDR is uni-directional. First,
$S_{{\sf m}}$ finds a satisfying assignment $\sigma$ to $\Phi_{{\sf m}}$ and
only then, $S_{{\sf s}}$ extends $\sigma$ to an assignment for $\Phi_{{\sf
s}}$. Learned clauses, called _lemmas_ in IC3/PDR, are only shared (or copied)
from the secondary solver $S_{{\sf s}}$ to the main solver $S_{{\sf m}}$.

SAT Modulo SAT (SMS) [1] is a modular SAT-solver that extends IC3/PDR by
allowing inter-modular unit propagation and conflict analysis: whenever an
interface literal is placed on a trail of any solver, it is shared with the
other solver and both solvers run unit propagation, exchanging unit literals.
This makes modular SAT-solving in SMS bi-directional as information flows in
both directions between the solvers. Bi-directional reasoning can simplify
proofs, but it significantly complicates conflict analysis. To manage conflict
analysis, SMS does not allow the secondary solver $S_{{\sf s}}$ to make any
decisions before the main solver $S_{{\sf m}}$ is able to find a complete
assignment to its clauses. As a result, learned clauses are either local to
each solver, or flow only from $S_{{\sf s}}$ to $S_{{\sf m}}$, restricting the
structure of refutations similarly to IC3/PDR.

Both IC3/PDR and SMS require $S_{{\sf m}}$ to find a complete satisfying
assignment to $\Phi_{{\sf m}}$ before the solving is continued in $S_{{\sf
s}}$. This is problematic since $\Phi_{{\sf m}}$ might be hard to satisfy,
causing them to get stuck in $\Phi_{{\sf m}}$, even if considering both
formulas together quickly reveals the (un)satisfiability of $\langle\Phi_{\sf
s},\Phi_{\sf m}\rangle$.

In this paper, we introduce specSMS — a modular SAT-solver that employs a
truly bi-directional reasoning. specSMS builds on SMS, while facilitating
deeper communication between the modules by  (1) allowing learnt clauses to
flow in both directions, and  (2) letting the two solvers interleave their
decisions.  The key challenge is in the adaptation of conflict analysis to
properly handle the case of a conflict that depends on decisions over local
variables of both solvers. Such a conflict cannot be explained to either one
of the solvers using only interface clauses (i.e., clauses over interface
variables). It may, therefore, require backtracking the search without
learning any conflict clauses. To address this challenge, specSMS uses
_speculation_ , which tames decisions of the secondary solver that are
interleaved with decisions of the main solver. If the secondary solver
satisfies all of its clauses during speculation, a _validation_ phase is
employed, where the main solver attempts to extend the assignment to satisfy
its unassigned clauses. If speculation leads to a conflict which depends on
local decisions of both solvers, _refinement_ is employed to resolve the
conflict. Refinement ensures progress even if no conflict clause can be
learnt. With these ingredients, we show that specSMS is sound and complete
(i.e., always terminates).

To certify specSMS’s result when it determines that a formula is
unsatisfiabile, we extract a _modular_ clausal proof from its execution. To
this end, we extend DRUP proofs [12] to account for modular reasoning, and
devise a procedure for trimming modular proofs. Such proofs are applicable
both to specSMS and to SMS. Finally, we propose an interpolation algorithm
that extracts an interpolant [4] from a modular proof. Since clauses are
propagated between the solvers in both directions, the extracted interpolants
have the shape $\bigwedge_{i}(C_{i}\Rightarrow\mathit{cls}_{i}$), where
$C_{i}$ are conjunctions of clauses and each $\mathit{cls}_{i}$ is a clause.

Original SMS is implemented on top of MiniSAT. For this paper, we implemented
both SMS and specSMS in Z3 [5], using the extendable SAT-solver interface of
Z3. Thanks to its bi-directional reasoning, specSMS is able to efficiently
solve both sat and unsat formulas that are provably hard for existing modular
SAT-solvers, provided that speculation is performed at the right time. specSMS
relies on a user-provided callback to decide when to speculate. Developing
good heuristics for speculation is a topic of future work.

In summary, we make the following contributions:  (i) the specSMS algorithm
that leverages bi-directional modular reasoning (Sec. III);  (ii) modular DRUP
proofs for specSMS (Sec. IV-A);  (iii) proof-based interpolation algorithm;
(iv) user interface to guide speculation and search (Sec. V); and  (v)
implementation and validation (Sec. VI).

##  II Motivating examples

In this section, we discuss two examples in which both IC3/PDR-style uni-
directional reasoning and SMS-style shallow bi-directional reasoning are
ineffective. The examples illustrate why existing modular reasoning gets
stuck. To better convey our intuition, we present our problems at word level
using bit-vector variables directly, without explicitly converting them to
propositional variables.

###### Example 1

Consider the following modular sat query:
$\langle\varphi_{\mathit{in}},\varphi_{\operatorname{SHA-1}}\rangle$, where
$\varphi_{\mathit{in}}\triangleq(\mathit{in}=\mathit{in}_{1})\lor(\mathit{in}=\mathit{in}_{2})$,
$\mathit{in}$ is a 512-bit vector, $\mathit{in}_{1}$, $\mathit{in}_{2}$ are
512-bit values,
$\varphi_{\operatorname{SHA-1}}\triangleq(\operatorname{SHA-1}_{\mathit{circ}}(\mathit{in})=\operatorname{SHA-1}_{\mathit{in}_{1}}$),
$\operatorname{SHA-1}_{\mathit{circ}}(\mathit{in})$ is a circuit that computes
$\operatorname{SHA-1}$ of $\mathit{in}$, and
$\operatorname{SHA-1}_{\mathit{in}_{1}}$ is the 20 byte $\operatorname{SHA-1}$
message digest of $\mathit{in}_{1}$.

Checking the satisfiability of
$\varphi_{\mathit{in}}\land\varphi_{\operatorname{SHA-1}}$ is easy because it
contains both the output and the input of the $\operatorname{SHA-1}$ circuit.
However, existing modular SAT-solvers attempt to solve the problem starting by
finding a complete satisfying assignment to $\varphi_{\operatorname{SHA-1}}$.
This is essentially the problem of inverting the $\operatorname{SHA-1}$
function, which is known to be very hard for a SAT-solver. The improvements in
SMS do not help. There are no unit clauses in $\varphi_{\mathit{in}}$.

On the other hand, specSMS proceeds as follows:  (1) when checking
satisfiability of $\varphi_{\operatorname{SHA-1}}$, it decides to speculate,
(2) it starts checking satisfiability of $\varphi_{\mathit{in}}$, branches on
variables $\mathit{in}$, finds an assignment $\sigma$ to $\mathit{in}$ and
unit propagates $\sigma$ to $\varphi_{\operatorname{SHA-1}}$,  (3) if there is
a conflict in $\varphi_{\operatorname{SHA-1}}$, it learns the conflict clause
$\mathit{in}\neq\mathit{in}_{2}$, and  (4) it terminates with a satisfying
assignment $\mathit{in}=\mathit{in}_{1}$.  Speculation in step (1) is what
differentiates specSMS from IC3/PDR and SMS. The specifics of when exactly
specSMS speculates is guided by the user, as explained in Sec. V. □

###### Example 2

Speculation is desirable for unsatisfiable formulas as well. Consider the
modular sat query $\langle\varphi_{+},\varphi_{-}\rangle$, where
$\varphi_{+}\triangleq(a<0\Rightarrow x)\land(a\geq 0\Rightarrow x)\land
PHP^{1}_{32}$ and $\varphi_{-}\triangleq(b<0\Rightarrow\neg x)\land(b\geq
0\Rightarrow\neg x)\land PHP^{2}_{32}$. Here, $a$ and $b$ are 32-wide
bitvectors and local to the respective modules. $PHP_{32}$ encodes the problem
of fitting $32$ pigeons into $31$ holes and $PHP^{1}_{32}$ and $PHP^{2}_{32}$
denote a partitioning of $PHP_{32}$ into 2 problems such that both formulas
contain all variables. The modular problem
$\langle\varphi_{+},\varphi_{-}\rangle$ is unsatisfiable, $x$ and
$PHP^{1}_{32}$ being two possible interpolants. IC3/PDR and SMS only find the
second interpolant. This is because, all satisfying assignments to
$\varphi_{-}$ immediately produce a conflict in $PHP^{1}_{32}$ part of
$\varphi_{+}$. However, learning an interpolant containing $x$ requires
searching (i.e., deciding) in both $\varphi_{+}$ and $\varphi_{-}$. specSMS,
with proper guidance, solves the problem by (1) deciding on all $b$ variables
in $\varphi_{-}$, (2) switching to speculation, (3) branching on all $a$
variables in $\varphi_{+}$ to hit a conflict in $x$, and, finally (4) learning
the conflict clause $x$. □

These examples highlight the need to speculate while doing modular reasoning.
While speculation by itself is quite powerful, it requires proper guidance to
be effective. We explain how the user can provide such a guidance in Sec. V.

##  III Speculative SAT Modulo SAT

This section presents specSMS — a modular bi-directional SAT algorithm. For
simplicity, we restrict our attention to the case of two modules. However, the
algorithm easily generalizes to any sequence of modules.

###  III-A Sat Modulo Sat

We assume that the reader has some familiarity with internals of a MiniSAT-
like SAT solver [6] and with SMS [1]. We give a brief background on SMS,
highlighting some of the key aspects. SMS decides satisfiability of a
partitioned CNF formula $\langle\Phi_{\sf s},\Phi_{\sf m}\rangle$ with a set
of shared interface variables $I$. It uses two modules $\langle S_{{\sf
s}},S_{{\sf m}}\rangle$, where $S_{{\sf m}}$ is a _main_ module used to solve
$\Phi_{{\sf m}}$, and $S_{{\sf s}}$ is a _secondary_ module to solve
$\Phi_{{\sf s}}$. Each module is a SAT solver (with a slightly extended
interface, as described in this section). We refer to them as _modules_ or
_solvers_ , interchangeably. Each solver has its own clause database
(initialized with $\Phi_{i}$ for $i\in\\{{\sf m},{\sf s}\\}$), and a trail of
literals, just as a regular SAT solver. The solvers keep their decision levels
in sync. Whenever a decision is made in one solver, the decision level of the
other solver is incremented as well (adding a _null_ literal to its trail if
necessary). Whenever one solver back-jumps to level $i$, the other solver
back-jumps to level $i$ as well. Assignments to interface variables are shared
between the solvers: whenever such a literal is added to the trail of one
solver (either as a decision or due to propagation), it is also added to the
trail of the other solver. SMS requires that $S_{{\sf s}}$ does not make any
decisions, until $S_{{\sf m}}$ finds a satisfying assignment to its clauses.

#### Inter-modular propagation and conflict analysis

The two key features of SMS are inter-modular unit propagation (called
PropagateAll in [1]) and the corresponding inter-modular conflict analysis. In
PropagateAll, whenever an interface literal is added to the trail of one
solver, it is added to the trail of the other, and both solvers run unit
propagation. Whenever a unit literal $\ell$ is copied from the trail of one
solver to the other, the reason for $\ell$ in the destination solver is marked
using a marker ext. This indicates that the justification for the unit is
external to the destination solver111This is similar to theory propagation in
SMT solvers.. Propagation continues until either there are no more units to
propagate or one of the solvers hits a conflict.

Conflict analysis in SMS is extended to account for units with no reason
clauses. If such a literal $\ell$ is used in conflict analysis, its reason is
obtained by using $\textsf{AnalyzeFinal}(\ell)$ on the other solver to compute
a clause $(s\Rightarrow\ell)$ over the interface literals. This clause is
copied to the requesting solver and is used as the missing reason. Multiple
such clauses can be copied (or learned) during analysis of a single conflict
clause – one clause for each literal in the conflict that is assigned by the
other solver.

In SMS, it is crucial that $\textsf{AnalyzeFinal}(\ell)$ always succeeds to
generate a reason clause over the interface variables. This is ensured by only
calling $\textsf{AnalyzeFinal}(\ell)$ in the $S_{{\sf s}}$ solver on literals
that were added to the trail when $S_{{\sf s}}$ was not yet making decisions.
This can happen in one of two scenarios: either $S_{{\sf m}}$ hits a conflict
due to literals propagated from $S_{{\sf s}}$, in which case AnalyzeFinal is
invoked in $S_{{\sf s}}$ on each literal marked ext in $S_{{\sf m}}$ that is
involved in the conflict resolution to obtain its reason; or $S_{{\sf s}}$
hits a conflict during unit propagation, in which case it invokes AnalyzeFinal
to obtain a conflict clause over the interface variables that blocks the
partial assignment of $S_{{\sf m}}$. In both cases, new reason clauses are
always copied from $S_{{\sf s}}$ to $S_{{\sf m}}$. We refer the reader to [1]
for the pseudo-code of the above inter-modular procedures for details.

###  III-B Speculative Sat Modulo Sat

specSMS extends SMS [1] by a combination of _speculation_ , _refinement_ , and
_validation_. During the search in the main solver $S_{{\sf m}}$, specSMS non-
deterministically _speculates_ by allowing the secondary solver $S_{{\sf s}}$
to extend the current partial assignment of $\Phi_{{\sf m}}$ to a satisfying
assignment of $\Phi_{{\sf s}}$. If $S_{{\sf s}}$ is unsuccessful (i.e., hits a
conflict), and the conflict depends on a combination of a _local_ decision of
$S_{{\sf m}}$ with some decision of $S_{{\sf s}}$, then the search reverts to
$S_{{\sf m}}$ and its partial assignment is _refined_ by forcing $S_{{\sf m}}$
to decide on an interface literal from the conflict. On the other hand, if
$S_{{\sf s}}$ is successful, solving switches to the main solver $S_{{\sf m}}$
that _validates_ the current partial assignment by extending it to all of its
clauses. This either succeeds (meaning, $\langle\Phi_{{\sf s}},\Phi_{{\sf
m}}\rangle$ is sat), or fails and another _refinement_ is initiated. Note that
the two sub-cases where $S_{{\sf s}}$ is unsuccessful but the reason for the
conflict is either local to $S_{{\sf s}}$ or local to $S_{{\sf m}}$ are
handled as in SMS.

#### Search modes

specSMS controls the behavior of the solvers and their interaction through
_search modes_. Each solver can be in one of the following search modes:
Decide, Propagate, and Finished. In Decide, written $D^{i}$, the solver treats
all decisions below level $i$ as assumptions and is allowed to both make
decisions and do unit propagation. In Propagate, written $P$, the solver makes
no decisions, but does unit propagation whenever new literals are added to its
trail. In Finished, written $F$, the clause database of the solver is
satisfied; the solver neither makes decisions nor propagates unit literals.

The pair of search modes of both modules is called the _state_ of specSMS,
where we add a unique state called unsat for the case when the combination of
the modules is known to be unsatisfiable. The possible states and transitions
of specSMS are shown in Fig. 1. States $\mathit{unsat}$ and $\langle
F,F\rangle$ are two final states, corresponding to unsat and sat,
respectively. In all other states, exactly one of the solvers is in a state
$D^{i}$. We refer to this solver as _active_. The part of the transition
system highlighted in yellow correspond to SMS, and the green part includes
the states and transitions that are unique to specSMS.

SMS and specSMSonly specSMS$\langle P,D^{0}\rangle$start$\langle
D^{i},P\rangle$$\langle F,D^{M}\rangle$unsat$\langle D^{N},F\rangle$$\langle
F,F\rangle$$S_{{\sf m}}:\textsc{c}\,@\,0$$\scriptstyle\bigstar$$S_{{\sf
m}}:\textsc{sat}$$S_{{\sf s}}:\textsc{sat}$$S_{{\sf
s}}:\textsc{c}\,@\,{\scriptscriptstyle\leq}\\!i$REFINEREFINE$S_{{\sf
m}}:\textsc{sat}$$S_{{\sf
s}}:\textsc{c}\,@\,{\scriptscriptstyle\leq}\\!N$$S_{{\sf s}}:\textsc{sat}$
Figure 1: State transitions of specSMS. A state $\langle P,D^{0}\rangle$ means
that the secondary solver $S_{{\sf s}}$ is in propagate mode and the main
solver $S_{{\sf m}}$ is in solve mode. Each edge is guarded with a condition.
The condition $S_{{\sf m}}:\textsc{sat}$ means that $S_{{\sf m}}$ found a full
satisfying assignment to $\Phi_{{\sf m}}$. The condition $S_{{\sf
m}}:\textsc{c}\,@\,{\scriptscriptstyle\leq}\\!j$ means that $S_{{\sf m}}$ hit
a conflict at a decision level below $j$. The four states in yellow
corresponds to SMS; two states in green are unique to specSMS.

#### Normal execution with bi-directional propagation

specSMS starts in the state $\langle P,D^{0}\rangle$, with the main solver
being active. In this state, it can proceed like SMS by staying in the yellow
region of Fig. 1. We call this _normal execution with bi-directional
propagation_ , since (only) unit propagation goes between solvers.

#### Speculation

What sets specSMS apart is speculation: at any non-deterministically chosen
decision level $i$, specSMS can pause deciding on the main solver and activate
the secondary solver (i.e., transition to state $\langle D^{i},P\rangle$).
During speculation, only the secondary solver makes decisions. Since the main
solver does not have a full satisfying assignment to its clauses, the
secondary solver propagates assignments to the main solver and vice-versa.

Speculation terminates when the secondary solver $S_{{\sf s}}$ either: (1)
hits a conflict that cannot be resolved by inter-modular conflict analysis;
(2) hits a conflict below decision level $i$; or (3) finds a satisfying
assignment to $\Phi_{{\sf s}}$.

Case (1) is most interesting, and is what makes specSMS differ from SMS. Note
that a conflict clause is not resolved by inter-modular conflict analysis only
if it depends on an external literal on the trail of $S_{{\sf s}}$ that cannot
be explained by an interface clause from $S_{{\sf m}}$. This is possible when
both $S_{{\sf m}}$ and $S_{{\sf s}}$ have partial assignments during
speculation. So the conflict might depend on the _local_ decisions of $S_{{\sf
m}}$. This cannot be communicated to $S_{{\sf s}}$ using only interface
variables.

#### Refinement

In specSMS, this is handled by modifying the Reason method in the solvers to
fail (i.e., return ext) whenever AnalyzeFinal returns a non-interface clause.
Additionally, the literal on which AnalyzeFinal failed is recorded in a global
variable $\mathit{refineLit}$. This is shown in Alg. 1. The inter-modular
conflict analysis is modified to exit early whenever Reason fails to produce a
justification. At this point, specSMS exits speculation, returns to the
initial state $\langle P,D^{0}\rangle$, both solvers back-jump to decision
level $i$ at which speculation was initiated, and $S_{{\sf m}}$ is forced to
decide on $\mathit{refineLit}$.

We call this transition a _refinement_ because the partial assignment of the
main solver $S_{{\sf m}}$ (which we view as an _abstraction_) is updated
(a.k.a., refined) based on the information that was not available to it
(namely, a conflict with a set of decisions in the secondary solver $S_{{\sf
s}}$). Since $\mathit{refineLit}$ was not decided on in $S_{{\sf m}}$ prior to
speculation, deciding on it is a new decision that ensures progress in
$S_{{\sf m}}$. The next speculation is possible only under strictly more
decisions in $S_{{\sf m}}$ than before, or when $S_{{\sf m}}$ back-jumps and
flips an earlier decision.

We illustrate the refinement process on a simple example:

###### Example 3

Consider the query $\langle\Phi_{{\sf s}},\Phi_{{\sf m}}\rangle$ with:
$\Phi_{\sf s}(i,j,k,z)$: $\displaystyle\overline{z}\lor\overline{i}$ (3)
$\displaystyle i\lor j\lor\overline{k}$ (4) $\Phi_{\sf m}(a,i,j,k)$:
$\displaystyle\overline{a}\lor i\lor\overline{j}$ (1) $\displaystyle j\lor k$
(2)
First, $S_{{\sf m}}$ decides $a$ (at level 1), which causes no propagations.
Then, specSMS enters speculative mode, transitions to $\langle D^{1},P\rangle$
and starts making decisions in $S_{{\sf s}}$. $S_{{\sf s}}$ decides $z$ and
calls PropagateAll. Afterwards, the trails for $S_{{\sf m}}$ and $S_{{\sf s}}$
are as follows:

$S_{{\sf m}}$ |  $a$ @ 1 |  $\mathit{null}$ @ 2 |  $\overline{i}$ (ext) |  $\overline{j}$ (1) |  $k$ (2)
---|---|---|---|---|---
$S_{{\sf s}}$ |  $\mathit{null}$ @ 1 |  $z$ @ 2 |  $\overline{i}$ (3) |  $\overline{j}$ (ext) |  $k$ (ext)

where $x$ @ $i$ denotes that literal $x$ is decided at level $i$, and $x\ (r)$
denotes that literal $x$ is propagated using a reason clause $r$, or due to
the other solver (if $r=\text{ext}$). A conflict is hit in $S_{{\sf s}}$ in
clause (4). Inter-modular conflict analysis begins. $S_{{\sf s}}$ first asks
for the reason for $k$, which is clause (2) in $S_{{\sf m}}$. This clause is
copied to $S_{{\sf s}}$. Note that unlike SMS, clauses can move from $S_{{\sf
m}}$ to $S_{{\sf s}}$. The new conflict to be analyzed is $(i\lor j\lor j)$.
Now the reason for $\overline{j}$ is asked of $S_{{\sf m}}$. In this case,
$S_{{\sf m}}$ cannot produce a clause over shared variables to justify
$\overline{j}$, so conflict analysis fails with $\mathit{refineLit}=j$. This
causes specSMS to exit speculation mode and move to state $\langle
P,D^{0}\rangle$ and $S_{{\sf m}}$ must decide variable $j$ before speculating
again. Note that in this case either decision on $j$ results in
$\langle\Phi_{{\sf s}},\Phi_{{\sf m}}\rangle$ being sat. ■□

Case (2) is similar to what happens in SMS when a conflict is detected in
$S_{{\sf s}}$. The reason for the conflict is below level $i$ which is below
the level of any decision of $S_{{\sf s}}$. Since decision levels below $i$
are treated as assumptions in $S_{{\sf s}}$, calling AnalyzeFinal in $S_{{\sf
s}}$ returns an interface clause $c$ that blocks the current assignment in
$S_{{\sf m}}$. The clause $c$ is added to $S_{{\sf m}}$. The solvers back-jump
to the smallest decision level $j$ that makes $c$ an asserting clause in
$S_{{\sf m}}$. Finally, specSMS moves to $\langle P,D^{0}\rangle$.

#### Validation

Case (3), like Case (1), is unique to specSMS. While all clauses of $S_{{\sf
s}}$ are satisfied, the current assignment might not satisfy all clauses of
$S_{{\sf m}}$. Thus, specSMS enters _validation_ by switching to the
configuration $\langle F,D^{M}\rangle$, where $M$ is the current decision
level. Thus, $S_{{\sf m}}$ becomes active and starts deciding and propagating.
This continues, until one of two things happen: (3a) $S_{{\sf m}}$ extends the
assignment to satisfy all of its clauses, or (3b) a conflict that cannot be
resolved with inter-modular conflict analysis is found. In the case (3a),
specSMS transitions to $\langle F,F\rangle$ and declares that
$\langle\Phi_{{\sf m}},\Phi_{{\sf s}}\rangle$ is sat. The case (3b) is handled
exactly the same as Case (1) – the literal on the trail without a reason is
stored in $\mathit{refineLit}$, specSMS moves to $\langle P,D^{0}\rangle$,
backjumps to the level in which speculation was started, and $S_{{\sf m}}$ is
forced to decide on $\mathit{refineLit}$.

Algorithm 1 The Reason method in modular SAT solvers inside specSMS

1:function Reason($\mathit{lit}$)

2: if $\mathit{reason}[\mathit{lit}]=\text{ext}$ then

3: $c\leftarrow\mathit{other}.\textsf{AnalyzeFinal}(\mathit{lit})$

4: if $\exists v\in c\cdot v\not\in I$ then

5: $\mathit{refineLit}\leftarrow\mathit{lit}$

6: return ext

7: $\textsc{AddClause}(c)$

8: $\mathit{reason}[\mathit{lit}]\leftarrow c$

9: return $\mathit{reason}[\mathit{lit}]$

###### Theorem 1

specSMS terminates. If it reaches the state $\langle F,F\rangle$, then
$\Phi_{\sf s}\land\Phi_{\sf m}$ is satisfiable and the join of the trails of
$\langle S_{{\sf s}},S_{{\sf m}}\rangle$ is a satisfying assignment. If it
reaches the state $\mathit{unsat}$, $\Phi_{\sf s}\land\Phi_{\sf m}$ is
unsatisafiable. □

##  IV Validation and interpolation

In this section, we augment specSMS with an interpolation procedure. To this
end, we first introduce modular DRUP proofs, which are generated from specSMS
in a natural way. We then present an algorithm for extracting an interpolant
from a modular trimmed DRUP proof in the spirit of [11].

###  IV-A DRUP proofs for modular SAT

Modular DRUP proofs – a form of clausal proofs [9] – extend (monolithic) DRUP
proofs [12]. A DRUP proof [12] is a sequences of steps, where each step either
asserts a clause, deletes a clause, or adds a new Reverse Unit Propagation
(RUP) clause. Given a set of clauses $\Gamma$, a clause $\mathit{cls}$ is an
RUP for $\Gamma$, written $\Gamma\vdash_{\mathit{UP}}\mathit{cls}$, if
$\mathit{cls}$ follows from $\Gamma$ by unit propagation [8]. For a DRUP proof
$\pi$, let $\textsc{asserted}(\pi)$ denote all clauses of the asserted
commands in $\pi$, then $\pi$ shows that all RUP clauses of $\pi$ follow from
$\textsc{asserted}(\pi)$. If $\pi$ contains a $\bot$ clause, then $\pi$
certifies $\textsc{asserted}(\pi)$ is unsat.

A Modular DRUP proof is a sequence of clause addition and deletion steps,
annotated with indices $\mathit{idx}$ (m or s). Intuitively, steps with the
same index must be validated together (within the same module $\mathit{idx}$),
and steps with different indices may be checked independently. The steps are:

  1. 1.

$(\text{asserted},\mathit{idx},\mathit{cls})$ denotes that $\mathit{cls}$ is
asserted in $\mathit{idx}$,

  2. 2.

$(\text{rup},\mathit{idx},\mathit{cls})$ denotes adding RUP clause
$\mathit{cls}$ to $\mathit{idx}$,

  3. 3.

$(\text{cp}(\mathit{src}),\mathit{dst},\mathit{cls})$ denotes copying a clause
$\mathit{cls}$ from $\mathit{src}$ to $\mathit{dst}$, and

  4. 4.

$(\text{del},\mathit{idx},\mathit{cls})$ denotes removing clause
$\mathit{cls}$ from $\mathit{idx}$.

We denote the prefix of length $k$ of a sequence of steps $\pi$ by $\pi^{k}$.
Given a sequence of steps $\pi$ and a formula index $\mathit{idx}$, we use
$\mathit{act\\_clauses}(\pi,\mathit{idx})$ to denote the set of active clauses
with index $\mathit{idx}$. Formally,

$\\{\mathit{cls}\mid\exists c_{j}\in\pi\cdot\\\
(c_{j}=(t,\mathit{idx},\mathit{cls})\land(t=\text{asserted}\lor
t=\text{rup}\lor t=\text{cp}(\\_)))\\\ {}\land\hphantom{a}\neg\exists
c_{k}\in\pi\cdot k>j\land c_{k}=(\text{del},\mathit{idx},\mathit{cls})\\}$

A sequence of steps $\pi=c_{1},\ldots,c_{n}$ is a _valid modular DRUP proof_
iff for each $c_{i}\in\pi$:

  1. 1.

if $c_{i}=(\text{rup},\mathit{idx},\mathit{cls})$ then
$\mathit{act\\_clauses}(\pi^{i},\mathit{idx})\vdash_{\mathit{UP}}\mathit{cls}$,

  2. 2.

if $c_{i}=(\text{cp}(\mathit{idx}),\\_,\mathit{cls})$ then
$\mathit{act\\_clauses}(\pi^{i},\mathit{idx})\vdash_{\mathit{UP}}\mathit{cls}$,
and

  3. 3.

$c_{|\pi|}$ is either $(\text{rup},{\sf m},\bot)$ or $(\text{cp}({\sf s}),{\sf
m},\bot)$.

Let $\textsc{asserted}(\pi,idx)$ be the set of all asserted clauses in $\pi$
with index $idx$.

###### Theorem 2

If $\pi$ is a valid modular DRUP proof, then $\textsc{asserted}(\pi,{\sf
s})\land\textsc{asserted}(\pi,{\sf m})$ is unsatisfiable. □

Modular DRUP proofs may be validated with either one or two solvers. To
validate with one solver we convert the modular proof into a monolithic one
(i.e., where the steps are asserted, rup, and del). Let modDRUP2DRUP be a
procedure that given a modular DRUP proof $\pi$, returns a DRUP proof
$\pi^{\prime}$ that is obtained from $\pi$ by (a) removing $\mathit{idx}$ from
all the steps; (b) removing all cp steps; (c) removing all del steps. Note
that del steps are removed for simplicity, otherwise it is necessary to
account for deletion of copied and non-copied clauses separately.

###### Lemma 1

If $\pi$ is a valid modular DRUP proof then
$\pi^{\prime}=\textsc{modDRUP2DRUP}(\pi)$ is a valid DRUP proof. □

Modular validation is done with two monolithic solvers working in lock step:
$(\text{asserted},\mathit{cls},\mathit{idx})$ steps are added to the
$\mathit{idx}$ solver; $(\text{rup},\mathit{idx},\mathit{cls})$ steps are
validated locally in solver $\mathit{idx}$ using all active clauses (asserted,
copied, and rup); and for
$(\text{cp}(\mathit{src}),\mathit{dst},\mathit{cls})$ steps, $\mathit{cls}$ is
added to $\mathit{dst}$ but not validated in it, and $\mathit{cls}$ is checked
to exist in the $\mathit{src}$ solver.

From now on, we consider only valid proofs. We say that a (valid) modular DRUP
proof $\pi$ is a proof of unsatisfiability of $\Phi_{{\sf s}}\land\Phi_{{\sf
m}}$ if $\textsc{asserted}(\pi,{\sf s})\subseteq\Phi_{{\sf s}}$ and
$\textsc{asserted}(\pi,{\sf m})\subseteq\Phi_{{\sf m}}$ (inclusion here refers
to the sets of clauses).

specSMS produces modular DRUP proofs by logging the clauses that are learnt,
deleted, and copied between solvers. Note that in SMS clauses may only be
copied from $S_{{\sf s}}$ to $S_{{\sf m}}$, but in specSMS they might be
copied in both directions.

###### Theorem 3

Let $\Phi_{{\sf s}}$ and $\Phi_{{\sf m}}$ be two Boolean formulas s.t.
$\Phi_{{\sf s}}\land\Phi_{{\sf m}}\models\bot$. specSMS produces a valid
modular DRUP proof for unsatisfiability of $\Phi_{{\sf s}}\land\Phi_{{\sf
m}}$. □

Algorithm 2 Trimming a modular DRUP proof

Input: Solver instances $S_{\sf s}$, $S_{\sf m}$ with the empty clause on the
trail, and a modular clausal proof $\pi=c_{1},\ldots,c_{n}$.
Output: A proof $\pi^{\prime}$ s.t. all steps are core.

1:$\pi^{\prime}=\emptyset$

2:$M_{\sf s},M_{\sf m}\leftarrow\\{\bot\\},\emptyset$ $\triangleright$
Relevant clauses

3:for $i=n\textbf{ to }0$ do

4: match $c_{i}$ with $(\mathit{type},\mathit{idx},\mathit{cls})$

5: if $\mathit{cls}\not\in M_{\mathit{idx}}$ then continue

6: if $\mathit{type}=\text{del}$ then

7: $S_{\mathit{idx}}.\textsf{Revive}(\mathit{cls})$

8: continue

9: $\pi^{\prime}.\mathit{append}(c_{i})$

10: if $\mathit{type}=\text{rup}$ then

11: $S_{\mathit{idx}}.$chk_rup($\mathit{cls},M_{\mathit{idx}}$)

12: else if $\mathit{type}=\text{cp}(\mathit{src})$ then

13: $S_{\mathit{idx}}.\textsf{Delete}(\mathit{cls})$

14: $M_{\mathit{src}}.\mathit{add}(cls)$

15:$\pi^{\prime}.\mathit{reverse}()$

16:function solver::chk_rup($\mathit{cls},M$)

17: if IsOnTrail($\mathit{cls}$) then

18: UndoTrail($\mathit{cls}$)

19: Delete($\mathit{cls}$)

20: $\textsf{SaveTrail}()$

21: Enqueue$(\neg\mathit{cls})$

22: $r\leftarrow\textsf{Propagate}()$

23: $\textsf{ConflictAnalysis}(r,M)$ $\triangleright$ Updates $M$ with
conflict clauses

24: $\textsf{RestoreTrail}()$

Trimming modular DRUP proofs. A step in a modular DRUP proof $\pi$ is _core_
if removing it invalidates $\pi$. Under this definition, del steps are never
core since removing them does not affect validation. Alg. 2 shows an algorithm
to trim modular DRUP proofs based on backward validation. The input are two
modular solvers $S_{\sf m}$ and $S_{\sf s}$ in a final conflicting state, and
a valid modular DRUP proof $\pi=c_{1},\ldots,c_{n}$. The output is a trimmed
proof $\pi^{\prime}$ such that all steps of $\pi^{\prime}$ are core.

We assume that the reader is familiar with MiniSAT [6] and use the following
solver methods: Propagate, exhaustively applies unit propagation (UP) rule by
resolving all unit clauses; ConflictAnalysis analyzes the most recent conflict
and marks which clauses are involved in the conflict; IsOnTrail checks whether
a clause is an antecedent of a literal on the trail; Enqueue enqueues one or
more literals on the trail; IsDeleted, Delete, Revive check whether a clause
is deleted, delete a clause, and add a previously deleted clause,
respectively; SaveTrail, RestoreTrail save and restore the state of the trail.

Alg. 2 processes the steps of the proof backwards, rolling back the states of
the solvers. $M_{\mathit{idx}}$ marks which clauses were relevant to derive
clauses in the current suffix of the proof. While the proof is constructed
through inter-modular reasoning, the trimming algorithm processes each of the
steps in the proof completely locally. During the backward construction of the
trimmed proof, steps that include unmarked clauses are ignored (and, in
particular, not added to the proof). For each (relevant) rup step, function
chk_rup, using ConflictAnalysis, adds clauses to $M$. del steps are never
added to the trimmed proof, but the clause is revived from the solver. For cp
steps, if the clause was marked, it is marked as used for the solver it was
copied from and the step is added to the proof. Finally, asserted clauses that
were marked are added to the trimmed proof. Note that, as in [11], proofs may
be trimmed in different ways, depending on the strategy for ConflictAnalysis.

The following theorem states that trimming preserves validity of the proof.

###### Theorem 4

Let $\Phi_{{\sf s}}$ and $\Phi_{{\sf m}}$ be two formulas such that
$\Phi_{{\sf s}}\land\Phi_{{\sf m}}\models\bot$. If $\pi$ is a modular DRUP
proof produced by solvers $S_{\sf s}$ and $\Phi_{{\sf m}}$ for $\Phi_{{\sf
s}}\land\Phi_{{\sf m}}$, then a trimmed proof $\pi^{\prime}$ by Alg. 2 is also
a valid modular DRUP proof for $\Phi_{{\sf s}}\land\Phi_{{\sf m}}$. □

Fig. 2 shows a trimmed proof after specSMS is executed on
$\langle\psi_{0},\psi_{1}\rangle$ such that
$\psi_{0}\triangleq((s_{1}\land\mathit{la}_{1})\Rightarrow
s_{2}))\land((s_{1}\land\neg\mathit{la}_{1})\Rightarrow
s_{2})\land((s_{3}\land\mathit{la}_{2})\Rightarrow
s_{4})\land((s_{3}\land\neg\mathit{la}_{2})\Rightarrow s_{4})$ and
$\psi_{1}\triangleq(\neg s_{1}\Rightarrow\mathit{lb}_{1})\land(\neg
s_{1}\Rightarrow\neg\mathit{lb}_{1})\land((s_{2}\land\mathit{lb}_{2})\Rightarrow
s_{3})\land((s_{2}\land\neg\mathit{lb}_{2})\Rightarrow
s_{3})\land(s_{4}\Rightarrow\mathit{lb}_{3})\land(s_{4}\Rightarrow\neg\mathit{lb}_{3}))$.

seq | step | to | clause
---|---|---|---
1 | asserted | m | $\neg s_{1}\Rightarrow\mathit{lb}_{1}$
2 | asserted | m | $\neg s_{1}\Rightarrow\neg\mathit{lb}_{1}$
3 | asserted | s |  ($s_{1}\land\mathit{la}_{1})\Rightarrow s_{2}$
4 | asserted | s |  ($s_{1}\land\neg\mathit{la}_{1})\Rightarrow s_{2}$
5 | asserted | m |  ($s_{2}\land\mathit{lb}_{2})\Rightarrow s_{3}$
6 | asserted | m |  ($s_{2}\land\neg\mathit{lb}_{2})\Rightarrow s_{3}$
7 | asserted | s |  ($s_{3}\land\mathit{la}_{2})\Rightarrow s_{4}$
8 | asserted | s |  ($s_{3}\land\neg\mathit{la}_{2})\Rightarrow s_{4}$
9 | asserted | m | $s_{4}\Rightarrow\mathit{lb}_{3}$
10 | asserted | m | $s_{4}\Rightarrow\neg\mathit{lb}_{3}$
11 | rup | m | $s_{1}$
12 | rup | m | $\neg s_{4}$
13 | rup | m | $s_{2}\Rightarrow s_{3}$
14 | $\text{cp}({\sf m})$ | s | $s_{2}\Rightarrow s_{3}$
15 | rup | s | $s_{3}\Rightarrow s_{4}$
16 | rup | s | $s_{1}\Rightarrow s_{4}$
17 | $\text{cp}({\sf s})$ | m | $s_{1}\Rightarrow s_{4}$
18 | rup | m | $\bot$
Figure 2: An example of a modular DRUP proof. Clauses are written in human-
readable form as implications, instead of in the DIMACS format.

###  IV-B Interpolation

Algorithm 3 Interpolating a modular DRUP proof.

Input: Propositional formulas $\langle\Phi_{0},\Phi_{1}\rangle$
Input: A modular trimmed DRUP proof $\pi=c_{1},\ldots,c_{n}$ of
unsatisfiability of $\Phi_{0}\land\Phi_{1}$
Output: An interpolant $\mathit{itp}$ s.t. $\Phi_{0}\Rightarrow\mathit{itp}$
and $\mathit{itp}\land\Phi_{1}\models\bot$

1:$S_{\sf s},S_{\sf m}\leftarrow\textsc{SAT\\_Solver}()$

2:$\mathit{itp}\leftarrow\top$

3:for $i=0\textbf{ to }n$ do

4: match $c_{i}$

5: with $(\text{asserted},{\sf s},\mathit{cls})$:

6: $sup(\mathit{cls})\leftarrow\top$

7: with $(\text{cp}({\sf m}),{\sf s},\mathit{cls})$:

8: $sup(\mathit{cls})\leftarrow\mathit{cls}$

9: with $(\text{rup},{\sf s},\mathit{cls})$:

10: $M\leftarrow\emptyset$

11: $S_{\sf s}.$chk_rup($\mathit{cls},M$)

12: $sup(\mathit{cls})\leftarrow\\{sup(c)\mid c\in M\\}$

13: with $(\text{cp}({\sf s}),{\sf m},\mathit{cls})$:

14:
$\mathit{itp}\leftarrow\mathit{itp}\land(sup(\mathit{cls})\Rightarrow\mathit{cls})$

15: $S_{c_{i}.idx}.add(\mathit{cls})$

Given a modular DRUP proof $\pi$ of unsatisfiability of $\Phi_{{\sf
s}}\land\Phi_{{\sf m}}$, we give an algorithm to compute an interpolant of
$\Phi_{{\sf s}}\land\Phi_{{\sf m}}$. For simplicity of the presentation, we
assume that $\pi$ has no deletion steps; this is the case in trimmed proofs,
but we can also adapt the interpolation algorithm to handle deletions by
keeping track of active clauses.

Our interpolation algorithm relies only on the clauses copied between the
modules. Notice that whenever a clause is copied from module $i$ to module
$j$, it is implied by all the clauses in $\Phi_{i}$ together with all the
clauses that have been copied from module $j$. We refer to clauses copied from
$S_{{\sf m}}$ to $S_{{\sf s}}$ as _backward_ clauses and clauses copied from
$S_{{\sf s}}$ to $S_{{\sf m}}$ as _forward_ clauses. The conjunction of
forward clauses is unsatisfiable with $S_{{\sf m}}$. This is because, in the
last step of $\pi$, $\bot$ is added to $S_{{\sf m}}$, either through rup or by
cp $\bot$ from $S_{{\sf s}}$. Since all the clauses in module m are implied by
$\Phi_{{\sf m}}$ together with forward clauses, this means that the
conjunction of forward clauses is unsatisfiable with $\Phi_{{\sf m}}$. In
addition, all forward clauses were learned in module s, with support from
backward clauses. This means that every forward clause is implied by
$\Phi_{{\sf s}}$ together with the subset of the backward clauses used to
derive it. Intuitively, we should therefore be able to learn an interpolant
with the structure: backward clauses imply forward clauses.

Alg. 3 describes our interpolation algorithm. It traverses a modular DRUP
proof forward. For each clause $\mathit{cls}$ learned in module s, the
algorithm collects the set of backward clauses used to learn $\mathit{cls}$.
This is stored in the $\sup$ datastucture — a mapping from clauses to sets of
clauses. Finally, when a forward clause $c$ is copied, it adds
$\sup(c)\Rightarrow c$ to the interpolant.

###### Example 4

We illustrate our algorithm using the modular DRUP proof from Fig. 2. On the
first cp step ($\text{cp}({\sf m}),{\sf s},s_{2}\Rightarrow s_{3}$), the
algorithm assigns the $\sup$ for clause $s_{2}\Rightarrow s_{3}$ as itself
(line 8). The first clause learnt in module s, ($\text{rup},{\sf
s},s_{3}\Rightarrow s_{4}$), is derived from just the clauses in module s and
no backward clauses. Therefore, after RUP, our algorithm sets
$\sup(s_{3}\Rightarrow s_{4})$ to $\top$ (line 12). The second clause learnt
in module s, $s_{1}\Rightarrow s_{4}$, is derived from module s with the
support of the backward clause $s_{2}\Rightarrow s_{3}$. Therefore,
$\sup(s_{1}\Rightarrow s_{4})=\\{s_{2}\Rightarrow s_{3}\\}$. When this clause
is copied forward to module 1, the algorithm updates the interpolant to be
$(s_{2}\Rightarrow s_{3})\Rightarrow(s_{1}\Rightarrow s_{4})$. ■□

Next, we formalize the correctness of the algorithm. Let
$L_{B}(\pi)=\\{\mathit{cls}\mid(\text{cp}({\sf m}),{\sf
s},\mathit{cls})\in\pi\\}$ be the set of clauses copied from module m to s and
$L_{F}(\pi)=\\{\mathit{cls}\mid(\text{cp}({\sf s}),{\sf
m},\mathit{cls})\in\pi\\}$ be clauses copied from module s to m. From the
validity of modular DRUP proofs, we have that:

###### Lemma 2

For any step $c_{i}=(\text{cp}({\sf s}),{\sf m},\mathit{cls})\in\pi$,
$(L_{B}(\pi^{i})\land\Phi_{{\sf s}})\Rightarrow\mathit{cls}$ and for any step
$c_{j}=(\text{cp}({\sf m}),{\sf s},\mathit{cls})\in\pi$,
$(L_{F}(\pi^{j})\land\Phi_{{\sf m}})\Rightarrow\mathit{cls}$. □

For any clause $\mathit{cls}$ copied from one module to the other, we use the
shorthand $\sharp(\mathit{cls})$ to refer to the position of the copy command
in the proof $\pi$. That is, $\sharp(\mathit{cls})$ is the smallest $k$ such
that $c_{k}=(\text{cp}(i),j,\mathit{cls})\in\pi$. The following is an
invariant in a valid modular DRUP proof:

###### Lemma 3

$\forall\mathit{cls}\in L_{F}(\pi)\cdot(\Phi_{{\sf
m}}\land(L_{F}(\pi^{\sharp(\mathit{cls})}))\Rightarrow
L_{B}(\pi^{\sharp(\mathit{cls})}))$

□

These properties ensure that adding
$L_{B}(\pi^{\sharp(\mathit{cls})})\Rightarrow\mathit{cls}$ for every forward
clause $\mathit{cls}$ results in an interpolant. Alg. 3 adds
$(\sup(\mathit{cls})\Rightarrow\mathit{cls})$ as an optimization. Correctness
is preserved since $\sup(\mathit{cls})$ is a subset of
$L_{B}(\pi^{\sharp(\mathit{cls})})$ that together with $\Phi_{{\sf s}}$
suffices to derive $\mathit{cls}$ (formally,
$\sup(\mathit{cls})\land\Phi_{{\sf s}}\vdash_{\mathit{UP}}\mathit{cls}$).

###### Theorem 5

Given a modular DRUP proof $\pi$ for $\Phi_{{\sf s}}\land\Phi_{{\sf m}}$,
$\mathit{itp}\triangleq\\{\sup(c)\Rightarrow c\mid c\in L_{F}(\pi)\\}$ is an
interpolant for $\langle\Phi_{{\sf s}}$, $\Phi_{{\sf m}}\rangle$. □

###### Proof

Since all copy steps are over interface variables, the interpolant is also
over interface variables. By Lemma 2 (and the soundness of $\sup$
optimization), $\Phi_{{\sf s}}\Rightarrow\mathit{itp}$. Next, we prove that
$(\Phi_{{\sf m}}\land\mathit{itp})\Rightarrow\bot$. From Lemma 3, we have that
for all $c\in L_{F}(\pi)$, $(\Phi_{{\sf m}}\land
L_{F}(\pi^{\sharp(c)}))\Rightarrow\sup(c)$. Therefore, $(\Phi_{{\sf m}}\land
L_{F}(\pi^{\sharp(c)})\land(\sup(c)\Rightarrow c))\Rightarrow c$ ■

It is much simpler to extract interpolants from modular DRUP proofs then from
arbitrary DRUP proofs. This is not surprising since the interpolants capture
exactly the information that is exchanged between solvers. The interpolants
are not in CNF, but can be converted to CNF after extraction.

##  V Guiding specSMS via solver callbacks

As the reader may have noticed, deciding when to switch to speculative mode is
non-trivial. Heuristics may be implemented, as typically done in SAT solvers,
but we consider this out of the scope of this paper. Instead, we provide an
interface for users to guide specSMS based on solver callbacks. This scheme
has been recently proven useful to guide SMT solving and to define custom
theories in Z3 [2].

Users may provide a function NextSplit to guide the solver in whether to
speculate and over which variables to decide. specSMS calls NextSplit whenever
the next decision is about to be made. specSMS expects NextSplit to return
$\mathit{none}$ (default, in which case, the underlying heuristics are used)
or a pair $(\mathit{ch\\_mode},\mathit{Vars})$ where $\mathit{ch\\_mode}$ is a
Boolean that indicates a change to speculative mode and $\mathit{Vars}$ is a
(possibly empty) set of variables to assign. To implement NextSplit, users can
ask the solver if a variable has been assigned using the IsFixed function. We
illustrate the API with some examples.

###### Example 5

Consider modular queries of the following form:
$\langle\psi_{\mathit{in}}(\ell,\mathit{in}),\psi_{\operatorname{SHA-1}}(\mathit{in},\mathit{out})\rangle$,
where $\ell$ is a 2-bit vector, $\mathit{in}$ is a 512-bit vector (shared),
$\mathit{out}$ is 160-bit vector. $\psi_{\mathit{in}}$ encodes that there are
four possible messages:

$\displaystyle\psi_{\mathit{in}}$
$\displaystyle\triangleq(\ell=0\land\mathit{in}=\mathit{msg}_{0})\lor(\ell=1\land\mathit{in}=\mathit{msg}_{1})\lor{}$
$\displaystyle\phantom{{}\triangleq{}}(\ell=2\land\mathit{in}=\mathit{msg}_{2})\lor(\ell=3\land\mathit{in}=\mathit{msg}_{3})$

and $\psi_{\operatorname{SHA-1}}(\mathit{in},\mathit{out})$ encodes the
$\operatorname{SHA-1}$ circuit together with some hash:

$\psi_{\operatorname{SHA-1}}\triangleq(\operatorname{SHA-1}_{circ}(in)\land\mathit{out}=\mathit{shaVal})$

Roughly, the modular query
$\langle\psi_{\mathit{in}},\psi_{\operatorname{SHA-1}}\rangle$ asks whether
the $\operatorname{SHA-1}$ of any $\mathit{msg}_{i}$ is $\mathit{shaVal}$. As
we saw in Sec. II, we are interested in using speculation in queries of this
form in order to avoid the hard problem of inverting SHA-1 (as required by
SMS, for example). We can guide the solver with the function ${\sf
NextSplit}()\triangleq(\top,\ell)$. ■□

Speculation is useful for such queries both in cases where the formulas are
satisfiable and unsatisfiable. If unsat, only the 4 inputs for SHA-1 specified
by $\mathit{msg}_{i}$ need to be considered, avoiding the expensive hash
inversion problem. If sat, only two decisions on the bits of $\ell$ result in
fully assigning $\mathit{in}$, which results again in just checking the hash.

###### Example 6

Next, consider a different form of modular query:
$\langle\gamma_{\mathit{in}}(\ell,x,\mathit{in}),\gamma_{\operatorname{SHA-1}}(\mathit{in},x,\mathit{out})\rangle$,
where $x$ is an $512$-bit vector, $\ell$ is a $160$-bit vector,
$\mathit{chks}_{i}$ are 512-bit vector, and the remaining variables are the
same as in $\psi_{\mathit{in}}$ and $\psi_{\operatorname{SHA-1}}$, and

$\displaystyle\gamma_{\mathit{in}}$
$\displaystyle\triangleq\operatorname{SHA-1}_{circ}(x,\ell)\land{}$
$\displaystyle\phantom{{}\triangleq{}}\bigl{(}(\ell=\mathit{chks}_{0}\land\mathit{in}=\mathit{msg}_{0})\lor(\ell=\mathit{chks}_{1}\land\mathit{in}=\mathit{msg}_{1})\lor{}$
$\displaystyle\phantom{{}\triangleq{}}(\ell=\mathit{chks}_{2}\land\mathit{in}=\mathit{msg}_{2})\lor(\ell=\mathit{chks}_{3}\land\mathit{in}=\mathit{msg}_{3})\bigr{)}$
$\displaystyle\gamma_{\operatorname{SHA-1}}$ $\displaystyle\triangleq(x=1\lor
x=4)\land\operatorname{SHA-1}_{\mathit{circ}}(\mathit{in},\mathit{out})\land\mathit{out}=\mathit{shaVal}$

This is an example where bi-directional search is necessary to efficiently
solve the query. If deciding only on $\gamma_{\operatorname{SHA-1}}$, we
encounter the hard problem of inverting
$\operatorname{SHA-1}_{\mathit{circ}}$, if speculating directly in
$\gamma_{\mathit{in}}$, we encounter the same problem, since an assignment for
$x$ needs to be found, based on the four values for $\ell$.

Accordingly, in this case, we are not interested in speculating immediately,
but rather first decide on the value of $x$ in the main solver and then
speculate. The following NextSplit implementation captures this idea:

$\displaystyle{\sf NextSplit}()\triangleq\ $
$\displaystyle\textbf{if}(\textbf{not\ }{\sf IsFixed}(x))\ (\bot,x)$
$\displaystyle\textbf{else if}(\textbf{not\ }{\sf IsFixed}(\ell))\
(\top,\ell)$ elsenone

■□

This example gives an intuition on which instances specSMS is better than SMS.
Even if SMS is guided by NextSplit, at least one inversion of
$\operatorname{SHA-1}_{\mathit{circ}}$ would have to be computed.

##  VI Implementation and Validation

We have implemented specSMS (and SMS) inside the extensible SAT-solver of Z3
[5]. For SMS, we simply disable speculation. The code is publicly available on
GitHub222https://github.com/hgvk94/z3/tree/psms..

We have validated specSMS on a set of handcrafted benchmarks, based on Ex. 5,
using the query
$\langle\psi_{\mathit{in}},\psi_{\operatorname{SHA-1}}\rangle$. In the first
set of experiments, we check sat queries by generating one $\mathit{msg}_{i}$
in $\psi_{\mathit{in}}$ that matches $\mathit{shaVal}$. In the second set, we
check unsat queries, by ensuring that no $\mathit{msg}_{i}$ matches
$\mathit{shaVal}$. To evaluate performance, we make
$\psi_{\operatorname{SHA-1}}$ harder to solve by increasing the number of
rounds of $\operatorname{SHA-1}$ circuit encoded in the
$\operatorname{SHA-1}_{circ}$ clauses. We used SAT-encoding333Available at
https://github.com/saeednj/SAT-encoding. to generate the
$\operatorname{SHA-1}_{circ}$ with the different number of rounds (SAT-
encoding supports 16 to 40 rounds).

We use the same guidance for both SMS and specSMS: ${\sf
NextSplit}()\triangleq(\top,\ell)$. This means that once the secondary solver
is active, both specSMS and SMS branch on the $\ell$ variables first. However,
SMS does not use speculation. Thus, it only switches to the secondary solver
after finding a satisfying assignment to the main solver. In contrast, in
specSMS, the secondary solver becomes active immediately due to speculation,
and, accordingly, the search starts by branching on the $\ell$ variables.

| time (s) – sat
---|---
# rounds | SMS | specSMS
16 | 1.96 | 0.41
21 | – | 0.66
26 | – | 0.66
31 | – | 0.81
36 | – | 1.01
40 | – | 1.16

| time (s) – unsat
---|---
# rounds | SMS | specSMS
16 | 0.77 | 0.65
21 | – | 0.89
26 | – | 0.91
31 | – | 1.08
36 | – | 1.45
40 | – | 1.77

TABLE I: Solving time with a timeout of 600s.

Results for each set of the queries are shown in Tab. I. Column “# rounds”
shows the number of $\operatorname{SHA-1}$ rounds encoded in
$\psi_{\operatorname{SHA-1}}$. The problems quickly become too hard for SMS.
At the same time, specSMS solves all the queries quickly. Furthermore, the
run-time of specSMS appears to grow linearly with the number of rounds.

The experiments show that prioritizing decisions on $\ell$, which is effective
in specSMS with speculation, is ineffective in SMS. This is expected since
this guidance becomes relevant to SMS only after the main solver guessed a
satisfying assignment to $\psi_{\operatorname{SHA-1}}$. This, essentially
amounts to SMS noticing the guidance only after inverting the
$\operatorname{SHA-1}$ circuit, which defeats the purpose of the guidance. As
far as we can see, no other guidance can help SMS since there are no good
variables to branch on in the main solver and SMS does not switch to the
secondary solver until the main solver is satisfied.

##  VII Conclusion and Future Work

Modular SAT-solving is crucial for efficient SAT-based unbounded Model
Checking. Existing techniques, embedded in IC3/PDR [3] and extended in SMS
[1], trade the efficiency of the solver for the simplicity of conflict
resolution. In this paper, we propose a new modular SAT-solver, called
specSMS, that extends SMS with truly bi-directional reasoning. We show that it
is provably more efficient than SMS (and, therefore, IC3/PDR). We implement
specSMS in Z3 [5], extend it with DRUP-style [12] proofs, and proof-based
interpolation. We believe this work is an avenue to future efficient SAT- and
SMT-based Model Checking algorithms.

In this paper, we rely on user callbacks to guide specSMS when to start
speculation and (optionally) what variables to prefer in the decision
heuristic. This is sufficient to show the power of bi-directional reasoning
over uni-directional one of IC3/PDR and SMS. However, this does limit the
general applicability of specSMS. In the future, we plan to explore guiding
speculation by the number of conflicts in the main solver, possibly using
similar strategy used for guiding restarts in a modern CDCL SAT-solver [6].

A much earlier version of speculation, called _weak abstraction_ , has been
implemented in the Spacer Constrained Horn Clause (CHC) solver [10]. Since
Spacer extends IC3/PDR to SMT, the choice of speculation is based on theory
reasoning. Speculation starts when the main solver is satisfied modulo some
theories (e.g., Linear Real Arithmetic or Weak Theory of Arrays). Speculation
often prevents Spacer from being stuck in any one SMT query. However, Spacer
has no inter-modular propagation and no _refinement_. If _validation_ fails,
speculation is simply disabled and the query is tried again without it. We
hope that extending specSMS to theories can be used to make Spacer heuristics
much more flexible and effective.

DPLL(T)-style [7] SMT-solvers can be seen as modular SAT-solvers where the
main module is a SAT solver and the secondary solver is a theory solver (often
EUF-solver that is connected to other theory solvers such as a LIA solver).
This observation credited as an intuition for SMS [1]. In modern SMT-solvers,
all decisions are made by the SAT-solver. For example, if a LIA solver wants
to split on a bound of a variable $x$, it first adds a clause $(x\leq(b-1)\lor
x\geq b)$, where $b$ is the desired bound, to the SAT-solver and then lets the
SAT-solver branch on the clause. specSMS extends this interaction by allowing
the secondary solver (i.e., the theory solver) to branch without going back to
the main solver. Control is returned to the main solver only if such decisions
tangle local decisions of the two solvers. We hope that the core ideas of
specSMS can be lifted to SMT and allow more flexibility in the interaction
between the DPLL-core and theory solvers.

## References

  * [1] S. Bayless, C. G. Val, T. Ball, H. H. Hoos, and A. J. Hu.  Efficient modular SAT solving for IC3.  In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 149–156. IEEE, 2013.
  * [2] N. S. Bjørner, C. Eisenhofer, and L. Kovács.  Satisfiability modulo custom theories in Z3.  In C. Dragoi, M. Emmi, and J. Wang, editors, Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings, volume 13881 of Lecture Notes in Computer Science, pages 91–105. Springer, 2023\.
  * [3] A. R. Bradley.  SAT-based model checking without unrolling.  In R. Jhala and D. A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 70–87. Springer, 2011.
  * [4] W. Craig.  Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory.  J. Symb. Log., 22(3):269–285, 1957.
  * [5] L. M. de Moura and N. S. Bjørner.  Z3: an efficient SMT solver.  In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer, 2008.
  * [6] N. Eén and N. Sörensson.  An extensible sat-solver.  In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003\. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502–518. Springer, 2003.
  * [7] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli.  DPLL( T): fast decision procedures.  In R. Alur and D. A. Peled, editors, Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of Lecture Notes in Computer Science, pages 175–188. Springer, 2004.
  * [8] A. V. Gelder.  Verifying RUP proofs of propositional unsatisfiability.  In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008, 2008\.
  * [9] E. I. Goldberg and Y. Novikov.  Verification of proofs of unsatisfiability for CNF formulas.  In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10886–10891. IEEE Computer Society, 2003.
  * [10] A. Gurfinkel.  Program verification with constrained horn clauses (invited paper).  In S. Shoham and Y. Vizel, editors, Computer Aided Verification \- 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 19–29. Springer, 2022.
  * [11] A. Gurfinkel and Y. Vizel.  DRUPing for interpolates.  In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pages 99–106. IEEE, 2014.
  * [12] M. Heule, W. A. H. Jr., and N. Wetzler.  Trimming while checking clausal proofs.  In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 181–188. IEEE, 2013.

##  Appendix A specSMS as a set of Rules

A configuration of a specSMS module is a 4-tuple:
$\langle\mathit{SM},C,\Phi,\mathcal{M}\rangle$, where $\mathit{SM}$ is the
search mode (either $D^{i}$, $P$, or $F$), $C$ is either a (conflict) clause
implied by $\Phi$ or the marker $\mathit{none}$, $\Phi$ is the clause
database, and $\mathcal{M}$ is the trail of the solver. The overall
configuration of specSMS consists of configurations of both of its solvers.

$Initialize$ | $\langle P,no,\Phi_{{\sf s}},[\hphantom{a}]\rangle,\langle D^{0},no,\Phi_{{\sf m}},[\hphantom{a}]\rangle$ |
---|---|---
$Prop_{{\sf s}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}}:(C\lor\ell),\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}}:(C\lor\ell),\mathcal{M}_{{\sf s}}:\ell^{C\lor\ell}\rangle,NC_{{\sf m}}\end{multlined}\langle\ast,no,\Phi_{{\sf s}}:(C\lor\ell),\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}}:(C\lor\ell),\mathcal{M}_{{\sf s}}:\ell^{C\lor\ell}\rangle,NC_{{\sf m}}$ |  $\ell$ unassigned in $\mathcal{M}_{{\sf s}}$, $\neg C\subseteq\mathcal{M}_{{\sf s}}$
$Prop_{{\sf s}S}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{X}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{X}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{C\lor\ell}\rangle\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{X}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{X}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{C\lor\ell}\rangle$ |  $\neg C\subseteq\mathcal{M}_{{\sf m}}$, $\ell$, $C$ shared, $C\lor\ell\in\Phi_{{\sf s}}$, $\ell$ unassigned in $\mathcal{M}_{{\sf m}}$
$PropD_{{\sf s}S}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\bot}\rangle\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\bot}\rangle$ |  $\ell$ is shared, $\ell$ is unassigned in $\mathcal{M}_{{\sf m}}$, there does not exists a clause $C\lor\ell\in\Phi_{{\sf m}}$ s.t. $C$ is shared and $\neg C\subseteq\mathcal{M}_{{\sf s}}$
$Conflict_{{\sf s}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\end{multlined}\langle\ast,no,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}$ |  $\neg C\subseteq\mathcal{M}_{{\sf s}}$
$Explain_{{\sf s}}$ | $\begin{multlined}\langle\ast,(\neg\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor D)}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,(D\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor D)}\rangle,NC_{{\sf m}}\end{multlined}\langle\ast,(\neg\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor D)}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,(D\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor D)}\rangle,NC_{{\sf m}}$ |
TABLE II: Rules independent of solving modes. For each rule, except $Initialize$, there is a symmetrical rule to update Solver ${\sf m}$. These rules are not shown here for brevity.$NC_{B}=\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}\rangle$ $Decide_{{\sf m}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\dagger\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell\rangle\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\dagger\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell\rangle$ |  $\ell$ unassigned in $\mathcal{M}_{{\sf m}}$, $\ell$ not shared
---|---|---
$Decide_{{\sf m}S}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\dagger,\ell^{\bot}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell\rangle\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\dagger,\ell^{\bot}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell\rangle$ |  $\ell$ unassigned in $\mathcal{M}_{{\sf m}}$, $\ell$ shared
$Reason_{{\sf s}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor C)}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,(\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor C)}\rangle,NC_{{\sf m}}\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor C)}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle\ast,(\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{(\ell\lor C)}\rangle,NC_{{\sf m}}$ |  $\ell$ is shared
$Explain_{{\sf m}{\sf s}}$ | $\begin{multlined}\langle P,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle P,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle$ |  $C$ is shared, $C\in\Phi_{{\sf m}}$
$Learn_{{\sf m}}$ | $\begin{multlined}NC_{{\sf s}},\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] NC_{{\sf s}},\langle D,C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle\end{multlined}NC_{{\sf s}},\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] NC_{{\sf s}},\langle D,C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle$ | $C\not\in\Phi_{{\sf m}}$
$Learn_{{\sf m}{\sf s}}$ | $\begin{multlined}\langle\ast,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle\ast,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle$ |  $C$ is shared $C\not\in\Phi_{{\sf m}}$
$Backtrack_{{\sf m}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},M^{k}_{{\sf s}}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},M^{k}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k-1}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k-1}\rangle\end{multlined}\langle\ast,no,\Phi_{{\sf s}},M^{k}_{{\sf s}}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},M^{k}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k-1}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k-1}\rangle$ |  $k>j$
$Backjump_{{\sf m}}$ | $\begin{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle\end{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle$ |  $i$ is the second highest decision level in $\neg C$
$Fail_{{\sf m}}$ | $\begin{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,\neg C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle\Rightarrow unsat\end{multlined}\langle\ast,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle\ast,\neg C,\Phi_{{\sf m}}:C,\mathcal{M}_{{\sf m}}\rangle\Rightarrow unsat$ |  $\neg C$ is decided at level 0
TABLE III: Rules when $S_{{\sf m}}$ makes decisions and $S_{{\sf s}}$ does not. $\dagger$ denotes a null literal, a dummy literal that increments the decision level without assigning values to any variable. $FA_{\sf m}$ | $\begin{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}^{i}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}^{i}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle\end{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}^{i}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}^{i}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle$ |  $\mathcal{M}^{i}_{{\sf m}}$ is a full satisfying assignment to $\Phi_{{\sf m}}$
---|---|---
TABLE IV: Rule to enter fin mode $SPECM_{{\sf m}}$ | $\begin{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}^{i}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}^{i}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle\end{multlined}\langle P,no,\Phi_{{\sf s}},\mathcal{M}^{i}_{{\sf s}}\rangle,\langle D,no,\Phi_{{\sf m}},\mathcal{M}^{i}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}\rangle$ |  No clause is unit in $\Phi_{{\sf m}}$ under $\mathcal{M}_{{\sf m}}$ and $\Phi_{{\sf s}}$ under $\mathcal{M}_{{\sf s}}$
---|---|---
TABLE V: Rule to enter speculation $Decide_{{\sf s}}$ | $\begin{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\dagger\rangle\end{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\dagger\rangle$ |  $\ell$ unassigned in $\mathcal{M}_{{\sf s}}$, $\ell$ not shared
---|---|---
$Decide_{{\sf s}S}$ | $\begin{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle S,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\dagger,\ell^{\bot}\rangle\end{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle S,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\dagger,\ell^{\bot}\rangle$ |  $\ell$ unassigned in $\mathcal{M}_{{\sf s}}$, $\ell$ shared
$Reason_{{\sf m}}$ | $\begin{multlined}NC_{{\sf s}},\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{(\ell\lor C)}\rangle\Rightarrow\\\\[-8.61108pt] NC_{{\sf s}},\langle\ast,(\ell\lor C),\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{(\ell\lor C)}\rangle\end{multlined}NC_{{\sf s}},\langle\ast,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{(\ell\lor C)}\rangle\Rightarrow\\\\[-8.61108pt] NC_{{\sf s}},\langle\ast,(\ell\lor C),\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{(\ell\lor C)}\rangle$ |  $\ell$ is shared
$Explain_{{\sf s}{\sf m}}$ | $\begin{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle D,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle$ |  $C$ is shared, $C\in\Phi_{{\sf s}}$
$Learn_{{\sf s}}$ | $\begin{multlined}\langle D,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle D,C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\end{multlined}\langle D,C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}\Rightarrow\\\\[-8.61108pt] \langle D,C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,NC_{{\sf m}}$ | $C\not\in\Phi_{{\sf s}}$
$Learn_{{\sf s}{\sf m}}$ | $\begin{multlined}\langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle$ |  $C$ is shared $C\not\in\Phi_{{\sf s}}$
$Backtrack_{{\sf s}}$ | $\begin{multlined}\langle D^{i},C,\Phi_{{\sf s}},\mathcal{M}^{k}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}^{k}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k-1}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k-1}\rangle\end{multlined}\langle D^{i},C,\Phi_{{\sf s}},\mathcal{M}^{k}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}^{k}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k-1}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k-1}\rangle$ |  $k>i$
$Backjump_{{\sf s}}$ | $\begin{multlined}\langle D^{i},C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle\end{multlined}\langle D^{i},C,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle$ |  $j$ is the second highest decision level in $\neg C$, $k=max(j,i)$
TABLE VI: Rules when $S_{{\sf s}}$ is making decisions and $S_{{\sf m}}$ is not. All rules are symmetric to the ones in Tab. III. The only difference is that there is no counterpart for $Fail_{{\sf m}}$. This rule is presented in Tab. VII $Explain\bot_{{\sf s}}$ | $\begin{multlined}\langle D^{i},(\neg\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\bot}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\ast}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle\end{multlined}\langle D^{i},(\neg\ell\lor C),\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\bot}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\ast}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle$ |  $\ell$ is at a higher decision level than all other literals in $C$
---|---|---
$Explain\bot_{{\sf s}{\sf m}}$ | $\begin{multlined}\langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle\end{multlined}\langle D^{i},no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle P,C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle$ |  $\exists m\in C$ s.t $\neg m$ is a local decision in $S_{{\sf m}}$, $\ell$ is shared, $\ell$ unassigned in $\mathcal{M}^{i}_{{\sf m}}$
$FA_{A}$ | $\begin{multlined}\langle D^{i},no,\Phi_{{\sf s}},M^{j}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}^{j}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}^{j}_{{\sf s}}\rangle,\langle D^{i,j}/F,no,\Phi_{{\sf m}},\mathcal{M}^{j}_{{\sf m}}\rangle\end{multlined}\langle D^{i},no,\Phi_{{\sf s}},M^{j}_{{\sf s}}\rangle,\langle P/F,no,\Phi_{{\sf m}},\mathcal{M}^{j}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}^{j}_{{\sf s}}\rangle,\langle D^{i,j}/F,no,\Phi_{{\sf m}},\mathcal{M}^{j}_{{\sf m}}\rangle$ |  $\mathcal{M}_{{\sf s}}$ is a full satisfying assignment to $\Phi_{{\sf s}}$
$Fail_{{\sf s}}$ | $\begin{multlined}\langle D^{i},\neg C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},\neg C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,\top,\Phi_{{\sf m}}:\bot,\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle D^{i},\neg C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle D^{i},\neg C,\Phi_{{\sf s}}:C,\mathcal{M}_{{\sf s}}\rangle,\langle P,\top,\Phi_{{\sf m}}:\bot,\mathcal{M}_{{\sf m}}\rangle$ |  $\neg C$ is decided at level $0$
TABLE VII: All rules to exit speculation. $BackjumpV_{{\sf m}}$ | $\begin{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle\end{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle$ |  $d$ is the second highest decision level in $\neg C$, $d\geq i$, $k=max(j,d)$
---|---|---
TABLE VIII: Adaptation to the backjump rule for validate mode $Explain\bot_{{\sf m}}$ | $\begin{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle D^{i,j},(\neg\ell\lor C),\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\bot}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle\end{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}:\ell^{\ast}\rangle,\langle D^{i,j},(\neg\ell\lor C),\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}:\ell^{\bot}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{i}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{i}:\neg\ell\rangle$ |  $\ell$ is at a higher decision level than all literals in $C$
---|---|---
$BackjumpVE_{{\sf m}}$ | $\begin{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle\end{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},C,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle P,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}^{k}\rangle,\langle D^{0},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}^{k}\rangle$ |  $k$ is the second highest decision level in $\neg C$, $k<i$
$FAV_{{\sf m}}$ | $\begin{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\end{multlined}\langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle D^{i,j},no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle\Rightarrow\\\\[-8.61108pt] \langle F,no,\Phi_{{\sf s}},\mathcal{M}_{{\sf s}}\rangle,\langle F,no,\Phi_{{\sf m}},\mathcal{M}_{{\sf m}}\rangle$ |  $\mathcal{M}_{{\sf m}}$ is a full satisfying assignment to $\Phi_{{\sf m}}$
TABLE IX: All rules to transition out of validate mode


# Towards an Elementary Formulation of the Riemann Hypothesis in Terms of
Permutation Groups

Will Cavendish and Jacob Tsimerman

In a series of papers starting in the late 1960s (see e.g., [6], [5], [2]),
Nicolas and his collaborators established an intriguing relationship between
the Riemann Hypothesis and the theory of permutation groups. To describe their
results, let $g:\mathbb{N}\to\mathbb{N}$ denote Landau’s function, i.e. the
function that takes $n\in\mathbb{N}$ to the maximum order of an element of
$S_{n}$, the symmetric group on $n$ elements. The central result of [2] is
that the Riemann Hypothesis is equivalent to the statement

$g(n)\leq e^{\sqrt{li^{-1}(n)}}\textrm{~{} for all }n.$

Note that by the prime number theorem, $li^{-1}(n)$ is approximately equal to
the $n$-th prime number $p_{n}$. This brings us to the central question of
this note: Can $li^{-1}(n)$ can be replaced by $p_{n}$ in the above
equivalence? In what follows, we give a partial answer to this question.

Throughout this note we let $p_{n}$ denote the $n$-th prime number and
$\zeta(s)$ denote the Riemann $\zeta$ function.

######  Theorem 1.

If the Riemann Hypothesis is true, then

$g(n)\leq e^{\sqrt{p_{n}}}$

for all $n\geq 1$.

######  Theorem 2.

If the Riemann Hypothesis is false and
$\sup\\{\Re(\rho)~{}|~{}\zeta(\rho)=0\\}\neq 1$, then there exists $n$ such
that $g(n)>e^{\sqrt{p_{n}}}$.

The question of whether the Riemann Hypothesis is equivalent to $g(n)\leq
e^{\sqrt{p_{n}}}$ for all $n$ therefore comes down to the question of whether
$g(n)$ takes sufficiently large values in the case that the Riemann Hypothesis
is “as false as possible,” i.e. when there exists a sequence $\\{\rho_{i}\\}$
of zeros of $\zeta(s)$ such that $\lim_{i\to\infty}\Re(\rho_{i})=1$.

Acknowledgements. We are grateful to Jean-Louis Nicolas for his encouragement
and for helpful correspondence on the topic of this paper.

##  1 Bounding $g(n)$ under the Riemann Hypothesis

We begin by establishing Theorem 1. Following [2], we define

$a_{n}=\frac{\sqrt{li^{-1}(n)}-\log g(n)}{(n~{}\log(n))^{1/4}}$ (1)

The central ingredient in our proof is the following result from [2]:

######  Theorem 3 (Theorem 1.1(ii) in [2]).

Under the Riemann Hypothesis,

$a_{n}\geq\frac{2-\sqrt{2}}{3}-c-\frac{0.43\log\log n}{\log n}~{}\textrm{for
all }n\geq 2$

where $c=\sum_{\rho}\frac{1}{|\rho(\rho+1)|}\approx 0.046117644421509...$ and
the sum is taken over the set of non-trivial zeros of the Riemann $\zeta$
function.

The second estimate we will need is the following:

######  Lemma 1.0.1.

Under the Riemann Hypothesis,

$\left|li^{-1}(n)-p_{n}\right|\leq\frac{\sqrt{2}}{8\pi}\log^{2}(2n\log(n))\sqrt{n\log(n)}$

for all $n\geq 2657$.

###### Proof.

Under the Riemann Hypothesis, a well-known result of Schoenfeld [9] gives

$|\pi(x)-li(x)|<\frac{\sqrt{x}\log(x)}{8\pi}$

for all $x\geq 2657$ where $\pi(x)$ denotes the prime-counting function.
Plugging in the $n$-th prime $p_{n}$ and observing that $\pi(p_{n})=n$ we get:

$|n-li(p_{n})|<\frac{\sqrt{p_{n}}\log(p_{n})}{8\pi}$ (2)

Applying the mean value theorem to $li$ at the points $p_{n}$ and
$li^{-1}(n)$, we have

$\frac{li(li^{-1}(n))-li(p_{n})}{li^{-1}(n)-p_{n}}=li^{\prime}(x_{n})=\frac{1}{\log(x_{n})}$

for some $x_{n}$ between $li^{-1}(n)$ and $p_{n}$. Taking the absolute value
of both sides and multiplying through by denominators, we therefore have

$|li^{-1}(n)-p_{n}|=\log(x_{n})|n-li(p_{n}))|$ (3)

Combining this with equation (2), we have

$|li^{-1}(n)-p_{n}|<\log(x_{n})\frac{\sqrt{p_{n}}}{8\pi}\log(p_{n})$ (4)

for $n\geq 2657$. A crude estimate shows $li^{-1}(n)<2n\log(n)$ and
$p_{n}<2n\log(n)$ for $n\geq 3$, and since $x_{n}$ lies between $li^{-1}(n)$
and $p_{n}$, that $x_{n}<2n\log(n)$ for all $n\geq 3$ as well. Substituting
these inequalities into (4) above, we get

$|li^{-1}(n)-p_{n}|<\log(2n\log(n))\left|\frac{1}{8\pi}\sqrt{2n\log(n)}\log(2n\log(n)))\right|$

$=\frac{\sqrt{2}}{8\pi}\log^{2}(2n\log(n))\sqrt{n\log(n)}$

for all $n\geq 2657$.

∎

######  Lemma 1.0.2.

Under the Riemann Hypothesis,

$\sqrt{li^{-1}(n)}-\sqrt{p_{n}}<a_{n}\cdot(n\log(n))^{1/4}$

for all $n>10^{10}$.

###### Proof.

By the mean value theorem applied to the function $x\mapsto\sqrt{x}$ at the
points $li^{-1}(n)$ and $p_{n}$,

$\sqrt{li^{-1}(n)}-\sqrt{p_{n}}=\frac{li^{-1}(n)-p_{n}}{2\sqrt{x_{n}}}$ (5)

for some $x_{n}$ lying between $li^{-1}(n)$ and $p_{n}$. By Rosser’s theorem
[7], $p_{n}>n\log(n)$ for all $n$. A simple calculation shows that
$li^{-1}(n)>n\log(n)$ for all $n>40$. Since $x_{n}$ lies between $p_{n}$ and
$li^{-1}(n)$, it follows that $x_{n}>n\log(n)$ and hence

$\sqrt{n\log(n)}<\sqrt{x_{n}}$

for $n>40$. We therefore have

$\sqrt{li^{-1}(n)}-\sqrt{p_{n}}<\frac{li^{-1}(n)-p_{n}}{2\sqrt{n\log(n)}}$

for $n>40$ by equation (5).

Applying Lemma 1.0.1 to the numerator of the right-hand side of the above, we
get

$\sqrt{li^{-1}(n)}-\sqrt{p_{n}}<\frac{\sqrt{2}}{16\pi}\log^{2}(2n\log(n))$ (6)

for all $n\geq 2657$.

Using Theorem 3, we have that

$0.14-\frac{0.43\log\log n}{\log
n}\leq\frac{2-\sqrt{2}}{3}-c-\frac{0.43\log\log n}{\log n}\leq a_{n}$

for all $n\geq 2$. Direct calculation shows that the left-hand side of the
above equation is always larger than 0.08 for $n>10^{10}$, hence

$0.08\cdot(n\log(n))^{1/4}<a_{n}\cdot(n\log(n))^{1/4}$ (7)

for all $n>10^{10}$.

Direct calculation also gives that

$\frac{\sqrt{2}}{16\pi}\log^{2}(2n\log(n))<0.08\cdot(n\log(n))^{1/4}$

for all $n>10^{10}$, so combining the above with equation (7) we get

$\frac{\sqrt{2}}{16\pi}\log^{2}(2n\log(n))<a_{n}\cdot(n\log(n))^{1/4}$

for all $n>10^{10}$. Putting this together with equation (6) above, we get

$\sqrt{li^{-1}(n)}-\sqrt{p_{n}}<a_{n}\cdot(n\log(n))^{1/4}$

for all $n>10^{10}$.

∎

We are now ready to prove that for all $n\geq 1$, $g(n)<e^{\sqrt{p_{n}}}$ (or
equivalently $\sqrt{p_{n}}-\log(g(n))>0$) assuming the Riemann Hypothesis:

###### Proof.

For $n>10^{10}$, Lemma 1.0.2 together with the definition of $a_{n}$ give us

$\sqrt{p_{n}}-\log(g(n))=\sqrt{li^{-1}(n)}-\log(g(n))-(\sqrt{li^{-1}(n)}-\sqrt{p_{n}})$
$>\sqrt{li^{-1}(n)}-\log(g(n))-a_{n}\cdot(n\log(n))^{1/4}=0$

For $n\leq 10^{10}$, the inequality follows by observing that $li^{-1}(n)\leq
p_{n}$ if and only if $\pi(p_{n})\leq li(p_{n})$, where $\pi$ is the prime
counting function. The inequality $\pi(m)\leq li(m)$ holds up for all $m$ up
to $10^{14}$ by a result of Kotnik [4] (and has subsequently been proven for
all $n$ up to $10^{19}$ by Büthe [1].) Since $p_{n}<2\cdot n\log(n)$ for
$n>2$, $n<10^{10}$ implies $p_{n}<2\cdot 10^{10}\log(10^{10})<10^{12}$,
$li^{-1}(n)\leq p_{n}$ for all $n<10^{10}$.

Applying the square roots to both sides of this inequality, we have
$\sqrt{p_{n}}>\sqrt{li^{-1}(n)}$ and hence

$\sqrt{p_{n}}-\log(g(n))>\sqrt{li^{-1}(n)}-\log(g(n))$

for all $n<10^{10}$.

Since $\sqrt{li^{-1}(n)}>\log(g(n))$ under the Riemann Hypothesis by the
central result of [2], the righthand side of the above is always positive.

∎

##  2 Finding large values of $g(n)$ when the Riemann Hypothesis is false

We now turn to proving the second part of Theorem 1. Throughout this section,
we let $\Theta=\sup\\{\Re(\rho)~{}|~{}\zeta(\rho)=0\\}$ and we assume
$\Theta>\frac{1}{2}$.

Our approach follows the work of Massias, Nicolas and Robin in [5]. We begin
by recalling some terminology and results from [5]. Following Nicolas in [6],
the authors define a non-decreasing function $\mathbb{R}^{+}\to\mathbb{N}$
mapping $\rho\mapsto N_{\rho}$ with the property $N_{\rho}\in g(\mathbb{N})$
for all $\rho$. Given any $n\in\mathbb{N}$, the authors define $\rho=\rho(n)$
to be such that $N_{\rho}=\max\\{N_{\rho}~{}|~{}N_{\rho}\leq g(n)\\}$, and let
$x_{1}=x_{1}(\rho)$ be such that $x_{1}/\log x_{1}=\rho$.

We will not need the details of the construction of the function $\rho\mapsto
N_{\rho}$, however we will need several facts about its growth as a function
of $\rho$. The first is the following bound (equation (6) from [5] ):

######  Lemma 2.0.1.

$\theta(x_{1})\leq\log(N_{\rho})\leq\psi(x_{1})$

The authors also prove (equation (28) in [5]) that

$Li(\log^{2}(g(n)))-n=-\left(\Pi_{1}(x_{1})-Li(\psi^{2}(x_{1}))\right)+O(x_{1}^{3/2}/\log(x_{1}))$

where $\Pi_{1}(x)=\sum_{p^{k}\leq x}\frac{p^{k}}{k}$ and $\psi$ is Chebyshev’s
function $\psi(x)=\sum_{p^{k}\leq x}\log(p)$. As the authors point out, the
convexity of the function $t\mapsto Li(t^{2})$ implies

$Li(\psi^{2}(x_{1}))\geq Li(x_{1}^{2})+\frac{x_{1}}{\log
x_{1}}(\psi(x_{1})-x_{1}),$

therefore

$Li(\log^{2}(g(n))-n\geq Li(x_{1}^{2})-\Pi_{1}(x_{1})+\frac{x_{1}}{\log
x_{1}}(\psi(x_{1})-x_{1})+O(x_{1}^{3/2}/\log(x_{1}))$ (8)

The authors also prove (Lemma C part (iii)) that if $\Theta<1$,

$Li(x^{2})-\Pi_{1}(x)+\frac{x}{\log
x}(\psi(x)-x)=\Omega_{+}(x^{\Theta+1}/\log(x)),$

where $f(x)=\Omega_{+}(h(x))$ for a real function $f$ and a positive function
$h$ denotes
$\limsup_{x\to\infty}\frac{f(x)}{h(x)}>0$. Since $\Theta+1>3/2$ by assumption,
the $O\left(x_{1}^{3/2}/\log(x_{1})\right)$ term of Equation (8) is negligible
and we get:

######  Lemma 2.0.2.

If $\frac{1}{2}<\Theta<1$,

$Li(\log^{2}(g(n))-n=\Omega_{+}\left(x_{1}^{\Theta+1}/\log(x_{1})\right)$

where $x_{1}/\log(x_{1})=\rho$ and $\rho=\rho(n)$ is such that $N_{\rho}$ is
the smallest element of the image of the map $\rho\mapsto N_{\rho}$ that is
less than $g(n)$.

The other result we will need is that any element of the image $g(\mathbb{N})$
of Landau’s function is close to an element of the image of $\rho\mapsto
N_{\rho}$ as given by the following lemma (equation (11) from [5]):

######  Lemma 2.0.3.

Let $N_{\rho}$ be the largest element of the image of the map $\rho\mapsto
N_{\rho}$ that is less that $g(n)$. Then
$\log(g(n))=\log(N_{\rho})+O(\log(x_{1}))$

The final ingredients we will need are bounds on the error of the prime number
theorem $R(x)=\sup_{s\leq x}|\pi(s)-Li(s)|$.

######  Lemma 2.0.4.

$R(a+b)\leq R(a)+b+1$

###### Proof.

Note that by the sublinearity and monotonicity of $Li(x)$ for $x>e$,

$Li(s)\leq Li(s+b)\leq Li(s)+b$

Similarly, since $\pi$ is monotone and there are at most $b+1$ primes between
$s$ and $s+b$ for any $b$,

$\pi(s)\leq\pi(s+b)\leq\pi(s)+b+1$

It follows that

$|\pi(s+b)-Li(s+b)|\leq\max\\{|\pi(s)+b+1-Li(s)|,|Li(s)+b-\pi(s)|\\}$
$\leq|\pi(s)-Li(s)|+b+1$

Taking the suprema of both sides of the above inequality over $s\leq a$ we get
$R(a+b)\leq R(a)+b+1$ as required. ∎

######  Lemma 2.0.5.

If $1/2<\Theta<1$, then $R(\log^{2}(g(n)))=O(x_{1}^{2\Theta}\log(x_{1}))$

###### Proof.

Let $N_{\rho}$ be the largest element of the image of the map $\rho\mapsto
N_{\rho}$ less than $g(n)$ as above. By Lemma 2.0.3,

$\log(g(n))\leq\log(N_{\rho})+C\log(x_{1})$

for some $C>0$, so

$\log^{2}(g(n))\leq\log^{2}(N_{\rho})+2C\log(N_{\rho})\log(x_{1})+C^{2}\log^{2}(x_{1})$

By the monotonicity of $R$ and Lemma 2.0.4, we have

$R(\log^{2}(g(n)))\leq
R(\log^{2}(N_{\rho})+2C\log(N_{\rho})\log(x_{1})+C^{2}\log^{2}(x_{1}))$ $\leq
R(\log^{2}(N_{\rho}))+2C\log(N_{\rho})\log(x_{1})+C^{2}\log^{2}(x_{1})+1$

By Lemma 2.0.1, we have that the above is bounded by

$R(\psi^{2}(x_{1}))+2C\psi(x_{1})\log(x_{1})+C^{2}\log^{2}(x_{1})=R(\psi^{2}(x_{1}))+O(x_{1}\log(x_{1}))$

since $\psi(x_{1})=O(x_{1})$ by the prime number theorem. Since
$x_{1}\log(x_{1})$ is negligible relative to $x_{1}^{2\Theta}\log(x_{1})$ when
$\Theta>1/2$, it therefore suffices to show that
$R(\psi^{2}(x_{1}))=O(x_{1}^{2\Theta}\log(x_{1}))$.

Since $\Theta<1$ by assumption, we have that
$R(x_{1})=O(x_{1}^{\Theta}\log(x_{1}))$ (cf [3] Theorem 30). Using
$\psi(x_{1})=O(x_{1})$ once again,

$R(\psi^{2}(x_{1}))=O(R(x_{1}^{2}))=O(x_{1}^{2\Theta}\log(x_{1}))$

as required.

∎

We are now ready to prove Theorem 2, i.e. that if $\Theta>\frac{1}{2}$, there
exists an integer $n$ such that $g(n)>e^{\sqrt{p_{n}}}$. We will prove this by
establishing the equivalent statement $\pi(\log^{2}(g(n)))-n>0$ for some $n$.

###### Proof of Theorem 2.

Let $N_{\rho}$ be the largest element of the image of the map $\rho\mapsto
N_{\rho}$ less than $g(n)$. Then

$\pi(\log^{2}(g(n)))-n=Li(\log^{2}(g(n)))-n+\pi(\log^{2}(g(n)))-Li(\log^{2}(g(n)))$
$\geq Li(\log^{2}(g(n)))-n-R(\log^{2}(g(n)))$ (9)

By Lemma 2.0.2, we have

$Li(\log^{2}(g(n)))-n=\Omega_{+}(x^{\Theta+1}/\log(x))$

and by Lemma 2.0.5, we have that
$R(\log^{2}(g(n)))=O(x_{1}^{2\Theta}\log(x_{1}))$, so applying this to
equation (9) we have

$\pi(\log^{2}(g(n)))-n\geq\Omega_{+}(x_{1}^{\Theta+1}/\log(x_{1}))-O(x_{1}^{2\Theta}\log(x_{1}))$

Since $\Theta<1$, $2\Theta<\Theta+1$, so $R(\psi^{2}(x_{1}))$ is negligible
relative to $x_{1}^{\Theta+1}/\log(x_{1})$ and therefore

$\pi(\log^{2}(g(n)))-n\geq\Omega_{+}(x_{1}^{\Theta+1}/\log(x_{1}))$

It follows that $\pi(\log^{2}(g(n))-n$ must take a positive value for some
$n$.

∎

## References

  * [1] Jan Büthe, An analytic method for bounding $\psi(x)$, Math. Comp. 87 (2018), 1991-2009.
  * [2] Marc Deleglise and Jean-Louis Nicolas, The Landau function and the Riemann Hypothesis, Journal of Combinatorics and Number Theory 11 no. 2 (2019), 45-95
  * [3] Albert E. Ingham, The distribution of prime numbers. Cambridge Tracts in Mathematics and Mathematical Physics, No. 30 Stechert-Hafner, Inc., New York 1990.
  * [4] Tadej Kotnik, The prime-counting function and its analytic approximations, Advances in Computational Mathematics 29 (2008), 55–70.
  * [5] J.-P.Massias, J.-L. Nicolas and G. Robin. Évaluation asymptotique de l’ordre maximum d’un élément du groupe symétrique, Acta Arith. 50 (1988), 221–242.
  * [6] Jean-Louis Nicolas, Sur l’ordre maximum d’un élément dans le groupe $S_{n}$ des permutations, Acta Arithmetica 14 (1968), 315-332.
  * [7] John B. Rosser, The n-th Prime is Greater than $n\log n$. Proceedings of the London Mathematical Society 45 (1939), 21-44.
  * [8] John B. Rosser and Lowell Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois Journal of Mathematics, 1962.
  * [9] Lowell Schoenfeld, Sharper Bounds for the Chebyshev Functions $\theta(x)$ and $\psi(x)$ II”. Math. Comp. 30 no. 134 (1976), 337–360.
  * [10] Ch. J. de la Vallée-Poussin, Recherches analytiques sur la théorie des nombres premiers Ann. Soc. Sci. Bruxelles 20 (1899), 183–256.