Efficient Parallel Algorithm for Decomposing

Hard CircuitSAT Instances

Victor Kondratiev(B)[0000−0003−0356−5149] ,
Irina Gribanova[0000−0001−7155−4455] , and
Alexander Semenov[0000−0001−6172−4801]

ISDCT SB RAS, Irkutsk, Russia

arXiv:2602.17130v1 [[Link]] 19 Feb 2026

vikseko@[Link]

Abstract. We propose a novel parallel algorithm for decomposing hard

CircuitSAT instances. The technique employs specialized constraints to
partition an original SAT instance into a family of weakened formu-
las. Our approach is implemented as a parameterized parallel algorithm,
where adjusting the parameters allows efficient identification of high-
quality decompositions, guided by hardness estimations computed in
parallel. We demonstrate the algorithm’s practical efficacy on challeng-
ing CircuitSAT instances, including those encoding Logical Equivalence
Checking of Boolean circuits and preimage attacks on cryptographic hash
functions.

Keywords: Boolean circuits · Logical Equivalence Checking · SAT ·

CircuitSAT · SAT partitioning · Cryptographic hash functions · Preimage
attacks

1 Introduction

Digital circuits form the foundation of the modern world, from microprocessors
to specialized electronics (e.g., FPGA, ASIC). As a mathematical model of com-
binational digital circuits, Boolean circuits are particularly convenient because
they capture most logical and structural properties. They enable the study of
mathematical and combinatorial characteristics of digital circuits and facilitate
the development of testing and verification algorithms. Due to the high com-
plexity of modern circuits, they are typically designed using specialized tools in
the field of electronic design automation (EDA).
The Logical Equivalence Checking (LEC) problem [31] is critically impor-
tant in EDA. Modern EDA tools typically employ complete SAT solvers [5] to
address LEC. The applications of SAT solvers have expanded significantly over
the past 25 years, particularly since the introduction of the conflict-driven clause
learning (CDCL) algorithm [26–28]. Today, CDCL-based SAT solvers are widely
used in verification and software analysis [3, 23], cryptography [1, 39, 40], plan-
ning [33], combinatorics [48], and as sub-engines in solvers from satisfiability
modulo theories (SMT) [32].
2 V. Kondratiev et al.

However, reducing LEC to SAT often produces instances that are extremely
challenging for state-of-the-art SAT solvers, motivating the development of parallel-
solving methods. Several strategies exist for parallel SAT solving. In this paper,
we employ the partitioning strategy [19], specifically a variant tailored to SAT
instances derived from Boolean circuits.
The main contributions of our work are as follows:

1. We present a novel parallel algorithm for solving a broad class of CircuitSAT

problems, leveraging a partitioning construction introduced in [8].
2. We implement the algorithm as a parallel MPI application.
3. We apply our tool to solve hard LEC instances and algebraic cryptanaly-
sis problems that are intractable for even the best sequential SAT solvers,
demonstrating its practical utility.

The paper is organized as follows. Section 2 introduces the basic concepts,

terms, and notation used throughout the paper. Section 3 details the method
for constructing SAT partitionings based on pseudo-Boolean intervals. Section 4
presents a novel parallel algorithm designed for solving a broad class of Circuit-
SAT problems. Section 5 reports the results of computational experiments in
which we evaluated the proposed methods in application to LEC problems for
sorting algorithms and inversion problems for the MD4 function. In the conclud-
ing section we summarize the obtained results and outline possible directions for
further work.

2 Preliminaries

Boolean circuits are directed graphs that specify discrete functions of the form
f : {0, 1}n → {0, 1}m . Let Gf be such a graph with a set of vertices V and a set
of arcs A. The set V contains two subsets: (1) a set of n parentless vertices called
the circuit inputs, and (2) a set of m vertices called the circuit outputs. Each
vertex that does not belong to the set of inputs is associated with an element of
a complete basis [44], representing an elementary Boolean function. These basis
elements are called gates. If the basis {¬, ∧} is used, the resulting graph is called
an And-Inverter Graph (AIG) [24]. We refer to Gf , labeled in this way, as a
Boolean circuit and denote it by Sf .
Given an input vector α ∈ {0, 1}n , the interpretation of Sf on α is the
sequence of computations of the elementary Boolean functions at each gate. The
output of this interpretation is the vector formed by the values at the output
gates. Thus, Sf defines a total function f : {0, 1}n → {0, 1}m .
One of the central problems in EDA is Logical Equivalence Checking (LEC),
which verifies whether two Boolean circuits Sf and Sg specify the same function,
i.e., whether f ∼= g (point-wise equivalence).
The standard approach to LEC involves SAT solvers. Recall that the Boolean
satisfiability problem (SAT) asks whether a given Boolean formula is satisfiable.
An assignment is any set of values for the variables in the formula. A formula
 Efficient Parallel CircuitSAT Decomposition 3

is satisfiable if there exists an assignment for which it evaluates to 1 (True). If a

formula evaluates to 0 (False) for any assignment, it is said to be unsatisfiable.
Tseitin transformations [42] provide a polynomial-time reduction from the
satisfiability problem of an arbitrary Boolean formula to the satisfiability prob-
lem for a formula in conjunctive normal form (CNF), i.e., a conjunction of ele-
mentary disjunctions called clauses. As a result of this reduction, SAT is most
commonly considered as the problem of determining the satisfiability of an ar-
bitrary CNF.
By applying Tseitin transformations to a Boolean circuit Sf , we can con-
struct a CNF Cf in polynomial time relative to the number of gates in Sf .
Following [38], we refer to Cf as a template CNF. Algorithms for constructing
Cf from Sf are well-known and described in, e.g., [8, 38]. Various properties of
Boolean circuits can be analyzed by applying SAT solvers to formulas derived
from template CNFs.
Let f : {0, 1}n → {0, 1} be an arbitrary total Boolean function, and let Sf
be a Boolean circuit implementing f . The CircuitSAT problem asks whether
there exists an input to Sf for which the circuit outputs 1 (True). Using Tseitin
transformations, this problem can be reduced (in linear time relative to the
number of gates in Sf ) to SAT for a CNF obtained by augmenting the template
CNF Cf with a clause consisting of one variable.
Consider two Boolean circuits Sf and Sg , f, g : {0, 1}n → {0, 1}m . Given
Sf and Sg , we construct a miter circuit (see [8, 31]) and then derive a CNF
Cf ⊕g . This CNF is unsatisfiable if and only if Sf and Sg are equivalent. The
transformation from Sf and Sg to Cf ⊕g takes linear time relative to the total
number of gates in Sf and Sg . Thus, the LEC problem for Sf and Sg can be
efficiently reduced to SAT for Cf ⊕g .
Recall that SAT is a well-known NP-complete problem [9, 22], meaning it
cannot be solved in polynomial time (in the general case) if it is assumed that
P ̸= N P . However, many special cases involving large formulas (with tens or
hundreds of thousands of variables and clauses) can be solved efficiently using
algorithms based on simple, natural techniques. In particular, SAT solvers imple-
menting the CDCL algorithm [26] perform well on various industrial problems,
including LEC instances.
Nevertheless, many combinatorial problems produce extremely hard SAT in-
stances when reduced to SAT. For LEC, this occurs with circuits implementing
arithmetic functions such as integer multiplication or sorting algorithms for sets
of natural numbers. Even the best modern SAT solvers cannot solve such rela-
tively small-scale instances in a reasonable time, and their runtime behavior in
these cases remains unpredictable. This motivates the problem of estimating for-
mula hardness relative to a specific algorithm (e.g., a SAT solver). One approach
is to decompose the original formula into a family of simpler subproblems with
a relatively small solver runtime. The total solving time across all subproblems
in the decomposition then provides an upper bound on the hardness of the orig-
inal instance. This approach has been developed in [7, 16, 35, 37], among others.
Below, we outline its core idea.
4 V. Kondratiev et al.

Let C be an arbitrary CNF over a set X of variables, and let A be a com-

plete SAT-solving algorithm (e.g., a CDCL-based solver). We refer to a Boolean
variable x ∈ X or its negation ¬x as a literal. Following [41], we use the notation
(
σ x, σ = 1,
x =
¬x, σ = 0.

Assume |X| = k; the set of all assignments to X then forms a Boolean hypercube
{0, 1}k . For an arbitrary subset B ⊆ X, the assignments to B similarly form a
hypercube {0, 1}|B| .
For an arbitrary subset B ⊆ X and assignment β ∈ {0, 1}|B| , the substitution
of β into formula C is performed in the standard way (see, e.g., [6]). The resulting
formula is denoted by C[β/B]. For any B ⊆ X, we associate the set of 2|B|
possible formulas of the form C[β/B], where β ∈ {0, 1}|B| .
Let tA (C) denote the runtime of SAT solver A on formula C. Following [37],
we define the decomposition hardness of C with respect to algorithm A and
decomposition set B as
X
µA,B (C) = tA (C[β/B]). (1)
β∈{0,1}|B|

Here, the key quantity of interest is

µA (C) = min µA,B (C). (2)

B⊆X

Both (1) and (2) serve as upper bounds on the hardness of C, since there
exists an algorithm that solves SAT for C by applying a complete SAT solver to
all formulas C[β/B]. The computation of (2) can be approached using black-box
optimization algorithms. We emphasize that the set {C[β/B] | β ∈ {0, 1}|B| }
can be processed in parallel.
This approach has proven effective in several cases, enabling, for example,
the construction of non-trivial attacks on certain cryptographic functions (see
[35]). However, for hard LEC instances, more specialized constructions often
yield better results. We present one such construction in the next section.

3 Construction of SAT Partitioning for CircuitSAT

The concept of SAT partitioning was introduced in [20] (see also [19]).

Definition 1 ([19]). Let C be a CNF formula over a set of Boolean variables

X, and let Π = {G1 , . . . , Gs } be a set of Boolean formulas over X. The set Π
is called a SAT partitioning of C if the following conditions hold:

1. formulas C and C ∧ (G1 ∨ · · · ∨ Gs ) are equisatisfiable;

2. for all distinct i, j ∈ {1, . . . , s}, the formula C ∧ Gi ∧ Gj is unsatisfiable.
 Efficient Parallel CircuitSAT Decomposition 5

The construction that divides C into formulas of the form C[β/B] for some
B ⊆ X trivially yields a SAT partitioning of C. Below, we employ an alternative
partitioning construction from [8], specifically designed for CircuitSAT problems.
Consider a CircuitSAT problem, which could represent either an LEC prob-
lem or an inversion problem for a function f : {0, 1}n → {0, 1}m implemented
by a circuit Sf . Given γ ∈ Range(f ) ⊆ {0, 1}m , the inversion problem requires
finding α ∈ {0, 1}n such that f (α) = γ.
Let C be the CNF encoding this CircuitSAT problem, which we refer to
as the associated CNF. Let X denote the set of variables in C, and let X in =
{x1 , . . . , xn } be the subset of X corresponding to inputs of circuit Sf . We in-
in
terpret each assignment α ∈ {0, 1}|X | as the coefficients of a binary number in
n
N0 = {0, . . . , 2 − 1}, establishing a bijection ϕ : {0, 1}n → N0n .
n

For a, b ∈ N0n , the set {p ∈ N0n | a ≤ p < b} is called an interval, denoted by

[a, b), with length b − a. The corresponding set of Boolean vectors satisfies the
integer inequality
a ≤ x1 + 2x2 + · · · + 2n−1 xn < b, (3)
where xi ∈ {0, 1}, i ∈ {1, . . . , n}.
Definition 2. A set Rn of intervals is called a complete system of intervals if
it satisfies the following conditions:
1. all intervals are pairwise disjoint;
2. every number α ∈ N0n belongs to some interval in Rn .
Any interval I = [a, b) ∈ Rn with b − a ≥ 2 can itself be decomposed into a
complete system of intervals, which we denote by R(I).
The following construction was introduced in [8].
Construction 1 ([8]) Let Rn be a complete system of intervals. For each I =
[a, b) ∈ Rn , associate the inequality (3) and let CI be the CNF produced by this
inequality using standard translation methods [14]. We say that CI encodes the
interval I. Define Π = {CI }I∈Rn .
Theorem 1 ([8]). For any CNF C encoding a CircuitSAT problem and any
complete interval system Rn , the set Π = {CI }I∈Rn forms a SAT partitioning
of C.
This interval partitioning method has proven effective for solving challeng-
ing LEC problems [8]. In the next section, we present a novel algorithm for
constructing SAT partitionings based on the described construction.

4 Adaptive Parallel Algorithm for Constructing

Partitionings in CircuitSAT
We present a new algorithm for building SAT partitionings for CircuitSAT in-
stances using the interval construction described above. The section is divided
into two parts: the first describes the basic algorithm and provides a proof of
its completeness, while the second introduces additional heuristics that improve
the practical performance of the basic algorithm.
6 V. Kondratiev et al.

4.1 Basic Algorithm

Consider a CNF C over variables X, constructed for a Boolean circuit Sf im-

plementing f : {0, 1}n → {0, 1}m . Accordingly, the set X contains a subset X in ,
|X in | = n, consisting of variables assigned to the inputs of Sf .
The algorithm uses a CDCL SAT solver At whose running time is limited by
a constant t. Such a solver is a polynomial sub-solver in the sense of [45]. On
input CNF C, At returns one of three possible outputs:

– SAT (C is satisfiable);
– UNSAT (C is unsatisfiable);
– INDET (satisfiability cannot be determined within time t).

The time limit t can be expressed either as physical time (in seconds) or as
the number of elementary operations performed by the solver. For CDCL SAT
solvers, it is convenient to limit the runtime by the number of conflicts [26].
The algorithm involves several parameters. The first parameter, q, represents
the size of the initial interval partitioning. At the initial step, a complete interval
system Rn consisting of q intervals is constructed. We denote this system by
Rn0 = {I1 , . . . , Iq }. Each interval Ij , j ∈ {1, . . . , q}, is associated with its CNF
encoding C0j . The value of q is selected based on the computing environment’s
capabilities; for example, q may equal the number of available computing cores
to which the formulas C0j , j ∈ {1, . . . , q}, are distributed.
For each j ∈ {1, . . . , q}, the SAT solver At is applied to the formula C ∧ C0j .
If At (C ∧ C0j ) returns INDET, then C0j encodes an interval Ij ∈ Rn0 that can
be divided into smaller intervals. For simplicity, we assume each subsequent
partition splits into at most d intervals, where d is another pre-specified algorithm
parameter.
The process terminates in one of two cases:

1. When At finds a satisfying assignment for some CNF C(I) encoding inter-
val I.
2. When the unsatisfiability of C ∧ C(I) for every interval I generated during
the algorithm’s execution was proved.

The algorithm’s operation is represented as a tree T (C) with q branches from

the root. The root is associated with the pair (C, Rn0 ), and its branches corre-
spond to the formulas C0j for j ∈ {1, . . . , q}. If At finds a satisfying assignment
for C0j ∧ C, then the algorithm terminates with a solution for C. If At proves
C0j ∧ C is unsatisfiable, then the corresponding child node in the tree T (C) is
marked with ⊥ and becomes a leaf.
When At returns INDET for C0j ∧ C, the child node is associated with
(C, R(Ij )), where R(Ij ) divides Ij into shorter intervals. This node then be-
comes the new root for further recursive processing.
Let v be an arbitrary vertex in the tree T (C) at depth l, where l equals the
number of edges from the root to v (thus l = 0 for the root). We will use the
term “vertex at level l” to refer to v.
 Efficient Parallel CircuitSAT Decomposition 7

Algorithm 1: DFS-based CircuitSAT decomposition

Input: CNF formula C, number of initial intervals q, splitting factor d,
timeout t
Output: SAT (satisfying assignment) or UNSAT
1: Let Rq0 = {I1 , . . . , Iq } be the initial set of intervals
2: Initialize an empty LIFO queue Q
3: foreach j ∈ {1, . . . , q} do
4: Construct CNF Cj encoding interval Ij
5: Push (C ∧ Cj , Ij ) onto Q

6: while Q is not empty do

7: Pop (Ccurrent , Icurrent ) from Q
8: Run SAT solver At on Ccurrent with timeout t
9: if At returns SAT then
10: return SAT // Return the satisfying assignment
11: else
12: if At returns UNSAT then
13: Continue // Discard the current interval
14: else
15: Split Icurrent into d subintervals {I1′ , . . . , Id′ }
16: foreach i ∈ {1, . . . , d} do
17: Construct CNF Ci′ encoding interval Ii′
18: Push (C ∧ Ci′ , Ii′ ) onto Q

19: return UNSAT

Our goal is to prove that under certain general conditions on At , the described
procedure will find a satisfying assignment for satisfiable CNF C and construct
a finite tree with ⊥-labeled leaves for unsatisfiable C. We preface this result with
the following lemma.
Lemma 1. Consider a Boolean circuit Sf specifying a total function f : {0, 1}n →
{0, 1}m , and let Cf be its template CNF in the sense of [38]. Let X denote the
variables in Cf , with X in = {x1 , . . . , xn } being the variables from X associated
with the inputs of Sf . For any input α = (α1 , . . . , αn ) ∈ {0, 1}n , consider the
CNF
xα αn
1 ∧ · · · ∧ xn ∧ Cf .
1
(4)
Applying only the Unit Propagation rule [26] to (4) derives values for all vari-
ables in X (as literals) without conflicts. For variables y1 , . . . , ym associated
with outputs of Sf , this yields y1 = γ1 , . . . , ym = γm , where f (α) = γ and
γ = (γ1 , . . . , γm ).
This lemma is well-known and appears in several contemporaneous works [2,
21,36]. Its validity follows directly from the properties of Tseitin transformations.
We now prove the completeness of the tree construction algorithm for T (C)
described above.
8 V. Kondratiev et al.

Theorem 2. Let At be a CDCL-based sub-solver that performs at most t con-

flicts for any t ≥ 1. Then the algorithm for constructing T (C) terminates after
finitely many calls to At .
Proof sketch. Consider any internal vertex v of T (C) associated with a pair
(C, R(I)) for some interval I ∈ Rn . Let R(I) = {I1′ , . . . , Ip′ } be a partition of
I. Assume that each I ′ ∈ R(I) has length 1 and its unique number has binary
representation α = (α1 , . . . , αn ). Obviously, the CNF encoding I ′ becomes the
conjunction of literals
xα αn
1 ∧ · · · ∧ xn .
1

In this case, At receives xα αn

1 ∧ · · · ∧ xn ∧ C as input and outputs all variable
1

values in C according to Lemma 1. If C contains additional constraints beyond

the template Cf (e.g., miter circuit constraints for LEC [8, 31]), then At will
either prove that C is unsatisfiable or find a satisfying assignment (terminating
the algorithm).
Since partitioning always decreases interval lengths, any interval I = [a, b)
splits into intervals of length less than b−a. This means that after a finite number
of partitioning steps, any interval will eventually be partitioned into intervals of
length 1.
It follows from the above that, for each such interval I ′ , the algorithm At
solves the satisfiability problem for CNF C(I ′ ) ∧ C with at most one conflict. In
the worst case, the tree T (C) has 2n leaves, each requiring one At call on a CNF
of the form xα αn
1 ∧ · · · ∧ xn ∧ C. Thus, Theorem 2 holds. ■
1

The algorithm’s implementation traverses T (C) using depth-first search (DFS).

Each branch ending in a ⊥-labeled leaf is pruned. During construction, if At
proves satisfiability for any CNF C(I) ∧ C, the algorithm terminates; if all
branches are pruned, C is unsatisfiable. The corresponding pseudocode is given
in Algorithm 1.

4.2 Additional Heuristics and Final Algorithm

To enhance the efficiency of the basic algorithm from Subsection 4.1, we intro-
duce two key heuristics that preserve the T (C) tree structure while optimizing its
construction process and enabling parallel solving of subtasks. These heuristics
reduce the time needed to find satisfying assignments and minimize computa-
tional resource usage through intelligent branching management and subtask
prioritization.
Heuristic 1 (Priority processing by tree level) Each node of the tree T (C)
is assigned a level l that reflects the depth of decomposition: the root has level
l = 0, the q initial subtasks have level l = 1, and each subsequent split in-
creases the level by one. The subtasks are placed in a priority queue ordered by
decreasing level l, which focuses processing on intervals of smaller size. These
higher-level intervals (with larger l values) contain fewer possible solutions to
inequality (3), thereby increasing the probability that the SAT solver At can
solve the subtask.
 Efficient Parallel CircuitSAT Decomposition 9

Algorithm 2: SplitInterval
Input: current level lcurrent , maximum level lmax , splitting factor d, array
solvelevels
Output: number of new intervals dcurrent
1: if solvelevels is not empty then
2: lavg ← ⌊Average(solvelevels)⌋
3: dcurrent ← dlavg −lcurrent
4: lnew ← lavg
5: else
6: if lmax > lcurrent then
7: dcurrent ← dlmax −lcurrent
8: lnew ← lmax
9: else
10: dcurrent ← d
11: lnew ← lcurrent + 1

12: return dcurrent

Heuristic 2 (Adaptive interval splitting) The number of new subtasks gen-

erated by splitting an interval depends on parameter d, current level of T (C)
lcurrent , average solving level lavg , and maximum level lmax reached during ex-
ecution. When the SAT solver proves SAT or UNSAT for a subtask, its level
is added to array solvelevels. If |solvelevels| > 0, we can compute lavg =
⌊average(solvelevels)⌋.
For an interval I at level lcurrent , assume that C ∧ CI returns INDET. The
number of subintervals dcurrent in the splitting of interval I is determined by the
following rules:

1. If |solvelevels| > 0 and lcurrent < lavg , then dcurrent = dlavg −lcurrent . This
enables reaching levels with higher solution probability while minimally in-
creasing queue size.
2. Else, if lcurrent < lmax , then dcurrent = dlmax −lcurrent , immediately adapting to
the current maximum tree depth.
3. Else, if lcurrent = lmax , then dcurrent = d and lmax is incremented by 1.

The pseudocode implementing Heuristic 2 appears in Algorithm 2.

These heuristics significantly reduce computational resources while preserv-
ing the basic algorithm’s completeness and correctness. They efficiently explore
the search space by focusing on promising levels of the decomposition tree.
Based on these heuristics, we developed a parallel CNF-solving algorithm
using MPI. The master process (Algorithm 3) manages the task queue, while
worker processes (Algorithm 4) solve individual tasks.
10 V. Kondratiev et al.

Algorithm 3: Parallel CircuitSAT decomposition (master

process)
Input: CNF formula C, number of initial intervals q, splitting factor d,
timeout t
Output: SAT (satisfying assignment) or UNSAT
1: Send C to all workers
2: Initialize Rq0 = {I1 , . . . , Iq } and empty priority queue Q
3: foreach j ∈ {1, . . . , q} do
4: Push (Ij , 1) onto Q
5: Initialize lmax ← 1; solvelevels ← ∅
6: while (Q is not empty) or (runningworkers ̸= ∅) do
// Wait for message from worker
7: message ← worker message
8: if Got READY message from worker then
9: Pop (Icurrent , lcurrent ) from Q
10: SendTaskToWorker((Icurrent , lcurrent , t))
11: Add worker to runningworkers
12: else
// Got DONE message from worker
13: Get result, lcurrent , Icurrent from message
14: lmax ← max(lmax , lcurrent )
15: if result = SAT then
16: Send EXIT signal to all workers.
17: return SAT (satisfying assignment)
18: else
19: if result = UNSAT then
20: Append lcurrent to solvelevels
21: Continue // Discard the current interval
22: else
// result is INDET
23: dcurrent = SplitInterval(lcurrent , lmax , d, solvelevels)
24: Split Icurrent into dcurrent subintervals {I1′ , . . . , Id′ current }
25: foreach i ∈ {1, . . . , dcurrent } do
26: Push (Ii′ , lnew ) onto Q

27: Remove worker from runningworkers

28: Send EXIT signal to all workers

29: return UNSAT

5 Computational Experiments

This section presents experimental results demonstrating the effectiveness of our

adaptive CircuitSAT partitioning algorithm.
 Efficient Parallel CircuitSAT Decomposition 11

Algorithm 4: Parallel CircuitSAT decomposition (worker

process)
Input: CNF formula C, SAT solver A
1: while no EXIT signal do
2: Send READY message to master
// Wait for message from master
3: (Icurrent , lcurrent , t) ← master message
4: CIcurrent ← EncodeIntervalToCNF(C, Icurrent )
5: result ← SolveCNF(CIcurrent , At )
// result can be SAT, UNSAT, or INDET
6: Send DONE(result, Icurrent , lcurrent ) to master

5.1 Benchmarks
We evaluated our approach on two benchmark classes. The first class comprises
Logical Equivalence Checking (LEC) instances for algorithms that sort k natu-
ral numbers represented by l-bit vectors. Specifically, we examined the following
sorting algorithms: bubble sort, selection sort [10], and pancake sort [15]. The
corresponding tests are denoted as BvSk,l (Bubble versus Selection), BvPk,l (Bub-
ble versus Pancake), and PvSk,l (Pancake versus Selection) LEC problems.
The second benchmark class consists of CNF formulas encoding preimage
attacks on the MD4 cryptographic hash function. We focus on attacks against
a step-reduced variant of MD4’s compression function. MD4 [34], one of the
earliest practical cryptographic hash algorithms, uses the Merkle–Damgård con-
struction [11, 30]. While vulnerable to collision attacks [43] and now considered
obsolete, no practical preimage attack exists even for its compression function.
The best known attack [25] requires 296 function calls, making it impractical.
Realistic attacks target the compression function with reduced steps. The
original 48-step algorithm’s variants are denoted MD4-k (k ≤ 48). The first suc-
cessful attack on MD4-32 appeared in [13]. Later, attacks for k ≤ 39 achievable
on personal computers were published in [12, 17]. To our knowledge, the largest
tractable variant is MD4-43, with attacks described in [8, 46, 47]. We apply our
Section 4 algorithm to improve upon [8]’s results.

5.2 Computational Platform

All experiments were conducted on the Academician V. M. Matrosov comput-
ing cluster at the Irkutsk Supercomputer Center of the Siberian Branch of the
Russian Academy of Sciences [29]. The cluster’s main module contains 60 nodes,
each with two 18-core Intel Xeon E5-2695 v4 “Broadwell” processors. For our
tests, we utilized between one (36 cores) and five (180 cores) nodes.

5.3 Experimental Results

The first series of experiments addressed LEC problems for sorting algorithms
that the sequential solver Kissat 4.0.1 [4] could not solve within 24 hours but
12 V. Kondratiev et al.

Table 1. Results of applying Algorithm 3 to LEC instances for sorting algorithms

(36-core wall-clock time)

Number Max.
CPU Wall-clock CPU/wall
Instance q d t of reached
time (s) time (s) ratio
INDETs level
BvP11,3 1000 3 500 25 2 332 392 9698 34.2
BvP17,2 1000 3 500 922 3 1 333 851 38 523 34.6
PvS9,4 1000 3 500 1548 3 2 000 801 57 649 34.7
PvS14,2 1000 3 500 0 1 73 971 2170 34.0
PvS11,3 1000 3 500 1251 3 1 723 511 49 553 34.7

Table 2. Results of applying Algorithm 3 to hard LEC instances (180-core wall-clock

time)

Number Max.
CPU Wall-clock CPU/wall
Instance q d t of reached
time (s) time (s) ratio
INDETs level
BvP12,3 1000 3 500 2858 4 4 862 491 27 771 175.0
BvS13,3 1000 3 500 2106 5 8 478 171 48 015 176.5

which our algorithm successfully solved using one cluster node (36 cores). Table 1
presents the results.
Let us analyze the table contents. All experiments began with q = 1000 ini-
tial partitions, constructed using the interval division scheme from [8], enabling
the division of any interval of length greater than 1 (in the sense of the defini-
tion given in Section 3) into equal intervals of smaller length. The parameter d
determines how many subintervals to create when splitting an interval, while t
specifies the time limit (in seconds) for the SAT solver (Kissat 4.0.1) to solve
one task at each decomposition level.
The instances in Table 1 exceeded the 100 000-second limit on a single Intel
E5-2695 core. The table columns show

– Number of INDETs: count of interrupted tasks requiring further splitting;

– Max. reached level: maximum depth in the T (C) tree;
– CPU time: total runtime (36 or 180 cores);
– Wall-clock time: actual elapsed time (36 or 180 cores);
– CPU/wall ratio: parallel speedup factor for 36 cores (180 cores in Table 2).

For the second experiment series, we addressed harder LEC instances unsolv-
able within 100 000 seconds on one node, utilizing five cluster nodes (180 cores).
Table 2 presents these results.
 Efficient Parallel CircuitSAT Decomposition 13

Table 3. Results of applying Algorithm 3 to MD4 hash function inversion problems

(180-core wall-clock time)

Number Max. CnC

CPU Wall-clock
Instance q d t of reached wall-clock
time (s) time (s)
INDETs level time (s)

MD4-40 60 000 2 220 3089 4 6 763 298 43 054 —

MD4-41 60 000 2 220 7455 4 9 128 960 57 660 >300 000
MD4-42 60 000 2 220 1904 4 5 858 125 37 498 >300 000
MD4-43 60 000 2 220 4020 3 7 027 119 43 288 264 039

The third experiment series addressed inversion problems for MD4-k cryp-
tographic hash functions (described previously). We examined MD4-k for k ∈
{40, 41, 42, 43}, targeting the inversion of the hash 1128 (a 128-bit vector of ones).
Initial parameters q and t were chosen similar to those in [8] for MD4-40 and
MD4-43 inversions.
Notably, the algorithm continued processing intervals even after finding sat-
isfying assignments, stopping only when queue Q emptied and all subtasks were
completed. This ensured a fair comparison with results from [8]. Table 3 presents
these findings.
The “CnC wall-clock time” column shows results from the Cube-and-Conquer
strategy [18] with default settings. We generated cubes using march cu1 and
solved them with Kissat 4.0.1. For MD4-40, march cu failed to construct cubes
within 100 000 seconds. For MD4-41 and MD4-42, solving exceeded 300 000 sec-
onds without finding solutions. MD4-43 required 264 039 seconds to find a sat-
isfying assignment.
Our algorithm demonstrated superior performance over both [8] and default
Cube-and-Conquer for MD4-40 through MD4-43 inversion problems.

6 Conclusions and Future Work

We presented a novel approach for solving hard SAT instances arising from Cir-
cuitSAT problems. The algorithm’s key innovation involves employing a time-
limited SAT solver within a SAT partitioning framework. When the solver cannot
complete a task within its allotted time, the task is interrupted and decomposed
into simpler subtasks using the interval partitioning scheme from [8]. Our exper-
imental results demonstrate the method’s effectiveness on hard Logical Equiva-
lence Checking (LEC) instances and preimage attacks against weakened variants
of the MD4 compression function.
The algorithm shows considerable potential for further enhancement through
several avenues. First, developing heuristics for automated selection and dynamic
1
[Link]
14 V. Kondratiev et al.

adjustment of parameters q, d, and t could significantly improve performance.

Second, sharing learned clauses between different branches of the decomposition
tree T (C) presents a promising optimization opportunity. We intend to investi-
gate these directions in future work.

Acknowledgments.

This research was financially supported by the Ministry of Education and Science
of the Russian Federation (State Registration № 121041300065-9).
We thank Stepan Kochemazov for his advice, which helped us improve the
presentation of the manuscript.

References

1. Bard, G.V.: Algebraic Cryptanalysis. Springer US (2009)

2. Bessière, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit Complexity and
Decompositions of Global Constraints. In: IJCAI, pp. 412–418 (2009)
3. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without
BDDs. In: TACAS, pp. 193–207 (1999)
4. Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba,
Plingeling and Treengeling entering the SAT Competition 2020. In: Proc. of SAT
Competition 2020 – Solver and Benchmark Descriptions, Department of Computer
Science Report Series B, vol. B-2020-1, pp. 51–53. University of Helsinki (2020)
5. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability
- Second Edition, FAIA, vol. 336. IOS Press (2021)
6. Chang, C., Lee, R.C.T.: Symbolic logic and mechanical theorem proving. Computer
science classics. Academic Press (1973)
7. Chivilikhin, D., Pavlenko, A., Semenov, A.: Decomposing hard sat instances with
metaheuristic optimization (2023)
8. Chukharev, K., Gribanova, I., Ivanov, D., Kochemazov, S., Kondratiev, V., Se-
menov, A.: Effective partitioning method with predictable hardness for circuitsat.
IEEE Access 13, 4218–4234 (2025)
9. Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151–
158. ACM (1971)
10. Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms, 1 edn.
MIT Press (1990)
11. Damgård, I.: A design principle for hash functions. In: Advances in Cryptology -
CRYPTO, LNCS, vol. 435, pp. 416–427 (1989)
12. De, D., Kumarasubramanian, A., Venkatesan, R.: Inversion attacks on secure hash
functions using satsolvers. In: SAT, LNCS, vol. 4501, pp. 377–382 (2007)
13. Dobbertin, H.: The first two rounds of MD4 are not one-way. In: FSE, LNCS, vol.
1372, pp. 284–292 (1998)
14. Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisf.
Boolean Model. Comput. 2(1-4), 1–26 (2006)
15. Gates, W.H., Papadimitriou, C.H.: Bounds for sorting by prefix reversal. Discrete
Mathematics 27(1), 47–57 (1979)
 Efficient Parallel CircuitSAT Decomposition 15

16. Gladush, A., Gribanova, I., Kondratiev, V., Pavlenko, A., Semenov, A.: Measuring
the effectiveness of sat-based guess-and-determine attacks in algebraic cryptanaly-
sis. In: L. Sokolinsky, M. Zymbler (eds.) Parallel Computational Technologies, pp.
143–157. Springer International Publishing, Cham (2022)
17. Gribanova, I., Semenov, A.A.: Using automatic generation of relaxation constraints
to improve the preimage attack on 39-step MD4. In: 41st International Convention
on Information and Communication Technology, Electronics and Microelectronics,
MIPRO 2018, Opatija, Croatia, May 21-25, 2018, pp. 1174–1179. IEEE (2018)
18. Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding
cdcl sat solvers by lookaheads. In: HVC, pp. 50–65 (2012)
19. Hyvärinen, A.E.J.: Grid based propositional satisfiability solving. Ph.D. thesis,
Aalto University, Helsinki, Finland (2011)
20. Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: A Distribution Method for Solving
SAT in Grids, p. 430–435. Springer Berlin Heidelberg (2006)
21. Järvisalo, M., Junttila, T.A.: Limitations of restricted branching in clause learning.
Constraints An Int. J. 14(3), 325–356 (2009)
22. Karp, R.M.: Reducibility among Combinatorial Problems, p. 85–103. Springer US
(1972)
23. Kroening, D.: Software verification. In: Handbook of Satisfiability - Second Edition,
FAIA, vol. 336, pp. 791–818. IOS Press (2021)
24. Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning
for equivalence checking and functional property verification. IEEE Trans. Com-
put. Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002)
25. Leurent, G.: MD4 is not one-way. In: FSE, LNCS, vol. 5086, pp. 412–428 (2008)
26. Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers.
In: Handbook of Satisfiability - Second Edition, FAIA, vol. 336, pp. 133–182. IOS
Press (2021)
27. Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional sat-
isfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
28. Marques-Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfia-
bility. In: ICCAD, pp. 220–227. IEEE Computer Society / ACM (1996)
29. Irkutsk Supercomputer Center of SB RAS. URL [Link]
30. Merkle, R.C.: A certified digital signature. In: CRYPTO, Lecture Notes in Com-
puter Science, vol. 435, pp. 218–238. Springer (1989)
31. Molitor, P., Mohnke, J., Becker, B., Scholl, C.: Equivalence Checking of Digital
Circuits: Fundamentals, Principles, Methods. Kluwer Academic Publishers (2004)
32. de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: TACAS, LNCS,
vol. 4963, pp. 337–340. Springer (2008)
33. Rintanen, J.: Planning and sat. In: Handbook of Satisfiability - Second Edition,
FAIA, vol. 336, pp. 765–789. IOS Press (2021)
34. Rivest, R.L.: The MD4 message digest algorithm. In: Advances in Cryptology -
CRYPTO, LNCS, pp. 303–311 (1990)
35. Semenov, A., Zaikin, O., Kochemazov, S.: Finding Effective SAT Partitionings Via
Black-Box Optimization, p. 319–355. Springer International Publishing (2021)
36. Semenov, A.A.: Decomposition representations of logical equations in problems
of inversion of discrete functions. Journal of Computer and Systems Sciences
International 48, 718–731 (2009)
37. Semenov, A.A., Chivilikhin, D., Pavlenko, A., Otpuschennikov, I.V., Ulyantsev,
V., Ignatiev, A.: Evaluating the hardness of SAT instances using evolutionary
optimization algorithms. In: CP, LIPIcs, vol. 210, pp. 47:1–47:18 (2021)
16 V. Kondratiev et al.

38. Semenov, A.A., Otpuschennikov, I.V., Gribanova, I., Zaikin, O., Kochemazov, S.:
Translation of algorithmic descriptions of discrete functions to SAT with applica-
tions to cryptanalysis problems. Log. Methods Comput. Sci. 16(1) (2020)
39. Semenov, A.A., Zaikin, O., Bespalov, D., Posypkin, M.: Parallel logical cryptanal-
ysis of the generator A5/1 in bnb-grid system. In: PaCT, LNCS, vol. 6873, pp.
473–483 (2011)
40. Semenov, A.A., Zaikin, O., Otpuschennikov, I.V., Kochemazov, S., Ignatiev, A.:
On cryptographic attacks using backdoors for SAT. In: AAAI, pp. 6641–6648
(2018)
41. Szeider, S.: Backdoor sets for DLL subsolvers. J. Autom. Reason. 35(1-3), 73–88
(2005)
42. Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies
in Constructive Mathematics and Mathematical Logic, Part II pp. 115–125 (1970)
43. Wang, X., Lai, X., Feng, D., Chen, H., Yu, X.: Cryptanalysis of the hash functions
MD4 and RIPEMD. In: EUROCRYPT, LNCS, vol. 3494, pp. 1–18 (2005)
44. Wegener, I.: The Complexity of Boolean Functions. John Wiley & Sons (1987)
45. Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In:
IJCAI, pp. 1173–1178 (2003)
46. Zaikin, O.: Inverting 43-step MD4 via Cube-and-Conquer. In: IJCAI, pp. 1894–
1900 (2022)
47. Zaikin, O.: Inverting cryptographic hash functions via Cube-and-Conquer. J. Artif.
Intell. Res. 81, 359–399 (2024)
48. Zhang, H.: Combinatorial designs by sat solvers. In: Handbook of Satisfiability -
Second Edition, FAIA, vol. 336, pp. 818–858. IOS Press (2021)