Paper deep dive
Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
Victor Kondratiev, Irina Gribanova, Alexander Semenov
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 89%
Last extracted: 7/21/2026, 12:22:23 AM
Summary
The paper presents a novel parallel algorithm for decomposing hard CircuitSAT instances using specialized constraints to partition SAT instances into weakened formulas. Implemented as a parameterized MPI application, the algorithm uses hardness estimations to guide the decomposition process. It is applied to Logical Equivalence Checking (LEC) of Boolean circuits and preimage attacks on cryptographic hash functions, demonstrating practical efficacy on instances intractable for sequential solvers.
Entities (9)
Relation Signals (7)
Proposed Algorithm → solves → CircuitSAT
confidence 95% · We propose a novel parallel algorithm for decomposing hard CircuitSAT instances.
Proposed Algorithm → appliedto → Logical Equivalence Checking
confidence 92% · We demonstrate the algorithm's practical efficacy on challenging CircuitSAT instances, including those encoding Logical Equivalence Checking
Boolean Circuits → reducedto → SAT
confidence 90% · Tseitin transformations provide a polynomial-time reduction from the satisfiability problem of an arbitrary Boolean formula
Proposed Algorithm → uses → MPI
confidence 90% · We implement the algorithm as a parallel MPI application.
SAT Solvers → basedon → CDCL Algorithm
confidence 88% · Today, CDCL-based SAT solvers are widely used in verification and software analysis
Proposed Algorithm → appliedto → MD4
confidence 85% · inversion problems for the MD4 function.
Boolean Circuits → modeledby → And-Inverter Graph
confidence 80% · If the basis {¬,∧} is used, the resulting graph is called an And-Inverter Graph (AIG)
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
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 formulas. 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 challenging CircuitSAT instances, including those encoding Logical Equivalence Checking of Boolean circuits and preimage attacks on cryptographic hash functions.
Tags
Links
- Source: https://arxiv.org/abs/2602.17130v1
- Canonical: https://arxiv.org/abs/2602.17130v1
Trouble viewing inline? Open PDF directly →
Full Text
45,552 characters extracted from source content.
Expand or collapse full text
Victor Kondratiev, Irina Gribanova, and Alexander Semenov 11institutetext: ISDCT SB RAS, Irkutsk, Russia 11email: vikseko@gmail.com Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances Victor Kondratiev(🖂) ( )[0000−0003−0356−5149]^[ https://orcid.org/0000-0003-0356-5149] Irina Gribanova[0000−0001−7155−4455]^[ https://orcid.org/0000-0001-7155-4455] Alexander Semenov[0000−0001−6172−4801]^[ https://orcid.org/0000-0001-6172-4801] 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 formulas. 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 challenging 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 combinational 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 complexity of modern circuits, they are typically designed using specialized tools in the field of electronic design automation (EDA). The Logical Equivalence Checking (LEC) problem [32] is critically important 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 [29, 27, 28]. Today, CDCL-based SAT solvers are widely used in verification and software analysis [3, 24], cryptography [1, 37, 38], planning [33], combinatorics [48], and as sub-engines in solvers from satisfiability modulo theories (SMT) [13]. 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 [21], 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 cryptanalysis 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 concluding 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,1n→0,1mf \0,1\^n→\0,1\^m. Let GfG_f 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) [25]. We refer to GfG_f, labeled in this way, as a Boolean circuit and denote it by SfS_f. Given an input vector α∈0,1nα∈\0,1\^n, the interpretation of SfS_f 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, SfS_f defines a total function f:0,1n→0,1mf \0,1\^n→\0,1\^m. One of the central problems in EDA is Logical Equivalence Checking (LEC), which verifies whether two Boolean circuits SfS_f and SgS_g specify the same function, i.e., whether f≅gf 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 is satisfiable if there exists an assignment for which it evaluates to 11 (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 problem for a formula in conjunctive normal form (CNF), i.e., a conjunction of elementary disjunctions called clauses. As a result of this reduction, SAT is most commonly considered as the problem of determining the satisfiability of an arbitrary CNF. By applying Tseitin transformations to a Boolean circuit SfS_f, we can construct a CNF CfC_f in polynomial time relative to the number of gates in SfS_f. Following [36], we refer to CfC_f as a template CNF. Algorithms for constructing CfC_f from SfS_f are well-known and described in, e.g., [36, 8]. Various properties of Boolean circuits can be analyzed by applying SAT solvers to formulas derived from template CNFs. Let f:0,1n→0,1f \0,1\^n→\0,1\ be an arbitrary total Boolean function, and let SfS_f be a Boolean circuit implementing f. The CircuitSAT problem asks whether there exists an input to SfS_f for which the circuit outputs 11 (True). Using Tseitin transformations, this problem can be reduced (in linear time relative to the number of gates in SfS_f) to SAT for a CNF obtained by augmenting the template CNF CfC_f with a clause consisting of one variable. Consider two Boolean circuits SfS_f and SgS_g, f,g:0,1n→0,1mf,g \0,1\^n→\0,1\^m. Given SfS_f and SgS_g, we construct a miter circuit (see [32, 8]) and then derive a CNF Cf⊕gC_f g. This CNF is unsatisfiable if and only if SfS_f and SgS_g are equivalent. The transformation from SfS_f and SgS_g to Cf⊕gC_f g takes linear time relative to the total number of gates in SfS_f and SgS_g. Thus, the LEC problem for SfS_f and SgS_g can be efficiently reduced to SAT for Cf⊕gC_f g. Recall that SAT is a well-known NP-complete problem [9, 23], meaning it cannot be solved in polynomial time (in the general case) if it is assumed that P≠NP≠ NP. 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 implementing the CDCL algorithm [28] perform well on various industrial problems, including LEC instances. Nevertheless, many combinatorial problems produce extremely hard SAT instances 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 relatively small-scale instances in a reasonable time, and their runtime behavior in these cases remains unpredictable. This motivates the problem of estimating formula 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 original instance. This approach has been developed in [35, 40, 7, 17], among others. Below, we outline its core idea. Let C be an arbitrary CNF over a set X of variables, and let A be a complete SAT-solving algorithm (e.g., a CDCL-based solver). We refer to a Boolean variable x∈Xx∈ X or its negation ¬x x as a literal. Following [41], we use the notation x^σ = x, σ= 1,¬x, σ= 0. Assume |X|=k|X|=k; the set of all assignments to X then forms a Boolean hypercube 0,1k\0,1\^k. For an arbitrary subset B⊆XB X, the assignments to B similarly form a hypercube 0,1|B|\0,1\^|B|. For an arbitrary subset B⊆XB X and assignment β∈0,1|B|β∈\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]C[β/B]. For any B⊆XB X, we associate the set of 2|B|2^|B| possible formulas of the form C[β/B]C[β/B], where β∈0,1|B|β∈\0,1\^|B|. Let tA(C)t_A(C) denote the runtime of SAT solver A on formula C. Following [35], we define the decomposition hardness of C with respect to algorithm A and decomposition set B as μA,B(C)=∑β∈0,1|B|tA(C[β/B]). _A,B(C)= _β∈\0,1\^|B|t_A(C[β/B]). (1) Here, the key quantity of interest is μA(C)=minB⊆XμA,B(C). _A(C)= _B X _A,B(C). (2) 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]C[β/B]. The computation of (2) can be approached using black-box optimization algorithms. We emphasize that the set C[β/B]∣β∈0,1|B|\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 [40]). 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 [21]). Definition 3.1 ([21]). Let C be a CNF formula over a set of Boolean variables X, and let Π=G1,…,Gs =\G_1,…,G_s\ 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)C (G_1 ·s G_s) are equisatisfiable; 2. for all distinct i,j∈1,…,si,j∈\1,…,s\, the formula C∧Gi∧GjC G_i G_j is unsatisfiable. The construction that divides C into formulas of the form C[β/B]C[β/B] for some B⊆XB 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 problem or an inversion problem for a function f:0,1n→0,1mf \0,1\^n→\0,1\^m implemented by a circuit SfS_f. Given γ∈Range(f)⊆0,1mγ (f) \0,1\^m, the inversion problem requires finding α∈0,1nα∈\0,1\^n such that f(α)=γ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 Xin=x1,…,xnX^in=\x_1,…,x_n\ be the subset of X corresponding to inputs of circuit SfS_f. We interpret each assignment α∈0,1|Xin|α∈\0,1\^|X^in| as the coefficients of a binary number in N0n=0,…,2n−1N_0^n=\0,…,2^n-1\, establishing a bijection ϕ:0,1n→N0nφ \0,1\^n→ N_0^n. For a,b∈N0na,b∈ N_0^n, the set p∈N0n∣a≤p<b\p∈ N_0^n a≤ p<b\ is called an interval, denoted by [a,b)[a,b), with length b−ab-a. The corresponding set of Boolean vectors satisfies the integer inequality a≤x1+2x2+⋯+2n−1xn<b,a≤ x_1+2x_2+·s+2^n-1x_n<b, (3) where xi∈0,1x_i∈\0,1\, i∈1,…,ni∈\1,…,n\. Definition 3.2. A set ℛnR^n 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α∈ N_0^n belongs to some interval in ℛnR^n. Any interval I=[a,b)∈ℛnI=[a,b) ^n with b−a≥2b-a≥ 2 can itself be decomposed into a complete system of intervals, which we denote by ℛ(I)R(I). The following construction was introduced in [8]. Construction 1 ([8]) Let ℛnR^n be a complete system of intervals. For each I=[a,b)∈ℛnI=[a,b) ^n, associate the inequality (3) and let CIC_I be the CNF produced by this inequality using standard translation methods [15]. We say that CIC_I encodes the interval I. Define Π=CII∈ℛn =\C_I\_I ^n. Theorem 3.3 ([8]). For any CNF C encoding a CircuitSAT problem and any complete interval system ℛnR^n, the set Π=CII∈ℛn =\C_I\_I ^n forms a SAT partitioning of C. This interval partitioning method has proven effective for solving challenging 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 instances 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. 4.1 Basic Algorithm Consider a CNF C over variables X, constructed for a Boolean circuit SfS_f implementing f:0,1n→0,1mf \0,1\^n→\0,1\^m. Accordingly, the set X contains a subset XinX^in, |Xin|=n|X^in|=n, consisting of variables assigned to the inputs of SfS_f. The algorithm uses a CDCL SAT solver AtA^t 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, AtA^t 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 [28]. 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 ℛnR^n consisting of q intervals is constructed. We denote this system by ℛ0n=I1,…,IqR_0^n=\I_1,…,I_q\. Each interval IjI_j, j∈1,…,qj∈\1,…,q\, is associated with its CNF encoding C0jC_0^j. 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 C0jC_0^j, j∈1,…,qj∈\1,…,q\, are distributed. For each j∈1,…,qj∈\1,…,q\, the SAT solver AtA^t is applied to the formula C∧C0jC C_0^j. If At(C∧C0j)A^t(C C_0^j) returns INDET, then C0jC_0^j encodes an interval Ij∈ℛ0nI_j _0^n 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 AtA^t finds a satisfying assignment for some CNF C(I)C(I) encoding interval I. 2. When the unsatisfiability of C∧C(I)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)T(C) with q branches from the root. The root is associated with the pair (C,ℛ0n)(C,R_0^n), and its branches correspond to the formulas C0jC_0^j for j∈1,…,qj∈\1,…,q\. If AtA^t finds a satisfying assignment for C0j∧C_0^j C, then the algorithm terminates with a solution for C. If AtA^t proves C0j∧C_0^j C is unsatisfiable, then the corresponding child node in the tree T(C)T(C) is marked with ⊥ and becomes a leaf. When AtA^t returns INDET for C0j∧C_0^j C, the child node is associated with (C,ℛ(Ij))(C,R(I_j)), where ℛ(Ij)R(I_j) divides IjI_j into shorter intervals. This node then becomes the new root for further recursive processing. Let v be an arbitrary vertex in the tree T(C)T(C) at depth l, where l equals the number of edges from the root to v (thus l=0l=0 for the root). We will use the term “vertex at level l” to refer to v. 1 Input: CNF formula C, number of initial intervals q, splitting factor d, timeout t Output: SAT (satisfying assignment) or UNSAT 2 31exLet ℛ0q=I1,…,IqR_0^q=\I_1,…,I_q\ be the initial set of intervals 4 Initialize an empty LIFO queue Q 5 foreach j∈1,…,qj∈\1,…,q\ do 6 Construct CNF CjC_j encoding interval IjI_j 7 Push (C∧Cj,Ij)(C C_j,I_j) onto Q 8 9 101exwhile Q is not empty do 11 Pop (Ccurrent,Icurrent)(C_current,I_current) from Q 12 Run SAT solver AtA^t on CcurrentC_current with timeout t 13 if AtA^t returns SAT then return SAT // Return the satisfying assignment 14 15 else 16 if AtA^t returns UNSAT then Continue // Discard the current interval 17 18 else 19 Split IcurrentI_current into d subintervals I1′,…,Id′\I_1 ,…,I_d \ 20 foreach i∈1,…,di∈\1,…,d\ do 21 Construct CNF Ci′C_i encoding interval Ii′I_i 22 Push (C∧Ci′,Ii′)(C C_i ,I_i ) onto Q 23 24 25 26 27 281exreturn UNSAT Algorithm 1 DFS-based CircuitSAT decomposition Our goal is to prove that under certain general conditions on AtA^t, 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 4.1. Consider a Boolean circuit SfS_f specifying a total function f:0,1n→0,1mf \0,1\^n→\0,1\^m, and let CfC_f be its template CNF in the sense of [36]. Let X denote the variables in CfC_f, with Xin=x1,…,xnX^in=\x_1,…,x_n\ being the variables from X associated with the inputs of SfS_f. For any input α=(α1,…,αn)∈0,1nα=( _1,…, _n)∈\0,1\^n, consider the CNF x1α1∧⋯∧xnαn∧Cf.x_1 _1 ·s x_n _n C_f. (4) Applying only the Unit Propagation rule [28] to (4) derives values for all variables in X (as literals) without conflicts. For variables y1,…,ymy_1,…,y_m associated with outputs of SfS_f, this yields y1=γ1,…,ym=γmy_1= _1,…,y_m= _m, where f(α)=γf(α)=γ and γ=(γ1,…,γm)γ=( _1,…, _m). This lemma is well-known and appears in several contemporaneous works [2, 22, 39]. Its validity follows directly from the properties of Tseitin transformations. We now prove the completeness of the tree construction algorithm for T(C)T(C) described above. Theorem 4.2. Let AtA^t be a CDCL-based sub-solver that performs at most t conflicts for any t≥1t≥ 1. Then the algorithm for constructing T(C)T(C) terminates after finitely many calls to AtA^t. Proof 4.3. Consider any internal vertex v of T(C)T(C) associated with a pair (C,ℛ(I))(C,R(I)) for some interval I∈ℛnI ^n. Let ℛ(I)=I1′,…,Ip′R(I)=\I_1 ,…,I_p \ be a partition of I. Assume that each I′∈ℛ(I)I (I) has length 1 and its unique number has binary representation α=(α1,…,αn)α=( _1,…, _n). Obviously, the CNF encoding I′I becomes the conjunction of literals x1α1∧⋯∧xnαn.x_1 _1 ·s x_n _n. In this case, AtA^t receives x1α1∧⋯∧xnαn∧Cx_1 _1 ·s x_n _n C as input and outputs all variable values in C according to Lemma 4.1. If C contains additional constraints beyond the template CfC_f (e.g., miter circuit constraints for LEC [32, 8]), then AtA^t 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)I=[a,b) splits into intervals of length less than b−ab-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′I , the algorithm AtA^t solves the satisfiability problem for CNF C(I′)∧C(I ) C with at most one conflict. In the worst case, the tree T(C)T(C) has 2n2^n leaves, each requiring one AtA^t call on a CNF of the form x1α1∧⋯∧xnαn∧Cx_1 _1 ·s x_n _n C. Thus, Theorem 4.2 holds. ■ The algorithm’s implementation traverses T(C)T(C) using depth-first search (DFS). Each branch ending in a ⊥ -labeled leaf is pruned. During construction, if AtA^t proves satisfiability for any CNF C(I)∧C(I) C, the algorithm terminates; if all branches are pruned, C is unsatisfiable. The corresponding pseudocode is given in Algorithm 1. Input: current level lcurrentl_current, maximum level lmaxl_max, splitting factor d, array solvelevels Output: number of new intervals dcurrentd_current 1 if solvelevels is not empty then 2 lavg←⌊Average()⌋l_avg← ( solvelevels) 3 dcurrent←dlavg−lcurrentd_current← d^l_avg-l_current 4 lnew←lavgl_new← l_avg 5 6else 7 if lmax>lcurrentl_max>l_current then 8 dcurrent←dlmax−lcurrentd_current← d^l_max-l_current 9 lnew←lmaxl_new← l_max 10 11 else 12 dcurrent←d_current← d 13 lnew←lcurrent+1l_new← l_current+1 14 15 return dcurrentd_current Algorithm 2 SplitInterval 4.2 Additional Heuristics and Final Algorithm To enhance the efficiency of the basic algorithm from Subsection 4.1, we introduce two key heuristics that preserve the T(C)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 computational resource usage through intelligent branching management and subtask prioritization. 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 ℛ0q=I1,…,IqR_0^q=\I_1,…,I_q\ and empty priority queue Q 3 foreach j∈1,…,qj∈\1,…,q\ do 4 Push (Ij,1)(I_j,1) onto Q 5 6Initialize lmax←1l_max← 1; ←∅ solvelevels← 7 while (Q is not empty) or (≠∅ runningworkers≠ ) do // Wait for message from worker 8 ←_ message← worker\_message 9 if Got READY message from worker then 10 Pop (Icurrent,lcurrent)(I_current,l_current) from Q 11 ((Icurrent,lcurrent,t)) SendTaskToWorker((I_current,l_current,t)) 12 Add worker to runningworkers 13 14 else // Got DONE message from worker 15 Get result, lcurrentl_current, IcurrentI_current from message 16 lmax←max(lmax,lcurrent)l_max← (l_max,l_current) 17 if =SAT result=SAT then 18 Send EXIT signal to all workers. 19 return SAT (satisfying assignment) 20 else 21 if =UNSAT result=UNSAT then 22 Append lcurrentl_current to solvelevels Continue // Discard the current interval 23 24 else // result is INDET 25 dcurrent=d_current= SplitInterval(lcurrentl_current, lmaxl_max, d, solvelevels) 26 Split IcurrentI_current into dcurrentd_current subintervals I1′,…,Idcurrent′\I_1 ,…,I_d_current \ 27 foreach i∈1,…,dcurrenti∈\1,…,d_current\ do 28 Push (Ii′,lnew)(I_i ,l_new) onto Q 29 30 31 32 Remove worker from runningworkers 33 34 35Send EXIT signal to all workers 36 return UNSAT Algorithm 3 Parallel CircuitSAT decomposition (master process) Heuristic 1 (Priority processing by tree level) Each node of the tree T(C)T(C) is assigned a level l that reflects the depth of decomposition: the root has level l=0l=0, the q initial subtasks have level l=1l=1, and each subsequent split increases 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 AtA^t can solve the subtask. 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)←_(I_current,l_current,t)← master\_message 4 CIcurrent←(C,Icurrent)C_I_current← EncodeIntervalToCNF(C,I_current) 5 ←(CIcurrent,At) result← SolveCNF(C_I_current,A^t) // result can be SAT, UNSAT, or INDET 6 Send DONE(,Icurrent,lcurrent result,I_current,l_current) to master 7 Algorithm 4 Parallel CircuitSAT decomposition (worker process) Heuristic 2 (Adaptive interval splitting) The number of new subtasks generated by splitting an interval depends on parameter d, current level of T(C)T(C) lcurrentl_current, average solving level lavgl_avg, and maximum level lmaxl_max reached during execution. When the SAT solver proves SAT or UNSAT for a subtask, its level is added to array solvelevels. If ||>0| solvelevels|>0, we can compute lavg=⌊average()⌋l_avg= ( solvelevels) . For an interval I at level lcurrentl_current, assume that C∧CIC C_I returns INDET. The number of subintervals dcurrentd_current in the splitting of interval I is determined by the following rules: 1. If ||>0| solvelevels|>0 and lcurrent<lavgl_current<l_avg, then dcurrent=dlavg−lcurrentd_current=d^l_avg-l_current. This enables reaching levels with higher solution probability while minimally increasing queue size. 2. Else, if lcurrent<lmaxl_current<l_max, then dcurrent=dlmax−lcurrentd_current=d^l_max-l_current, immediately adapting to the current maximum tree depth. 3. Else, if lcurrent=lmaxl_current=l_max, then dcurrent=d_current=d and lmaxl_max is incremented by 11. The pseudocode implementing Heuristic 2 appears in Algorithm 2. These heuristics significantly reduce computational resources while preserving 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. 5 Computational Experiments This section presents experimental results demonstrating the effectiveness of our adaptive CircuitSAT partitioning algorithm. 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 natural numbers represented by l-bit vectors. Specifically, we examined the following sorting algorithms: bubble sort, selection sort [10], and pancake sort [16]. The corresponding tests are denoted as k,l BvS_k,l (Bubble versus Selection), k,l BvP_k,l (Bubble versus Pancake), and k,l PvS_k,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 construction [31, 11]. While vulnerable to collision attacks [43] and now considered obsolete, no practical preimage attack exists even for its compression function. The best known attack [26] requires 2962^96 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≤48k≤ 48). The first successful attack on MD4-32 appeared in [14]. Later, attacks for k≤39k≤ 39 achievable on personal computers were published in [12, 18]. To our knowledge, the largest tractable variant is MD4-43, with attacks described in [46, 47, 8]. 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 computing cluster at the Irkutsk Supercomputer Center of the Siberian Branch of the Russian Academy of Sciences [30]. 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 which our algorithm successfully solved using one cluster node (36 cores). Table 1 presents the results. Table 1: Results of applying Algorithm 3 to LEC instances for sorting algorithms (36-core wall-clock time) Instance q d t Number of INDETs Max. reached level CPU time (s) Wall-clock time (s) CPU/wall ratio 11,3 BvP_11,3 1000 3 500 25 2 332 392 9698 34.2 17,2 BvP_17,2 1000 3 500 922 3 1 333 851 38 523 34.6 9,4 PvS_9,4 1000 3 500 1548 3 2 000 801 57 649 34.7 14,2 PvS_14,2 1000 3 500 0 1 73 971 2170 34.0 11,3 PvS_11,3 1000 3 500 1251 3 1 723 511 49 553 34.7 Let us analyze the table contents. All experiments began with q=1000q=1000 initial partitions, constructed using the interval division scheme from [8], enabling the division of any interval of length greater than 11 (in the sense of the definition 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)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 unsolvable within 100 000 seconds on one node, utilizing five cluster nodes (180 cores). Table 2 presents these results. Table 2: Results of applying Algorithm 3 to hard LEC instances (180-core wall-clock time) Instance q d t Number of INDETs Max. reached level CPU time (s) Wall-clock time (s) CPU/wall ratio 12,3 BvP_12,3 1000 3 500 2858 4 4 862 491 27 771 175.0 13,3 BvS_13,3 1000 3 500 2106 5 8 478 171 48 015 176.5 The third experiment series addressed inversion problems for MD4-k cryptographic hash functions (described previously). We examined MD4-k for k∈40,41,42,43k∈\40,41,42,43\, targeting the inversion of the hash 11281^128 (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 satisfying 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. Table 3: Results of applying Algorithm 3 to MD4 hash function inversion problems (180-core wall-clock time) Instance q d t Number of INDETs Max. reached level CPU time (s) Wall-clock time (s) CnC wall-clock 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 “CnC wall-clock time” column shows results from the Cube-and-Conquer strategy [19] with default settings. We generated cubes using march_cu111https://github.com/marijnheule/CnC. 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 seconds without finding solutions. MD4-43 required 264 039 seconds to find a satisfying 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 CircuitSAT 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 experimental results demonstrate the method’s effectiveness on hard Logical Equivalence 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 adjustment of parameters q, d, and t could significantly improve performance. Second, sharing learned clauses between different branches of the decomposition tree T(C)T(C) presents a promising optimization opportunity. We intend to investigate 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] G. V. Bard (2009) Algebraic Cryptanalysis. Springer US. Cited by: §1. [2] C. Bessière, G. Katsirelos, N. Narodytska, and T. Walsh (2009) Circuit Complexity and Decompositions of Global Constraints. In IJCAI, p. 412–418. Cited by: §4.1. [3] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu (1999) Symbolic Model Checking without BDDs. In TACAS, p. 193–207. Cited by: §1. [4] A. Biere, K. Fazekas, M. Fleury, and M. Heisinger (2020) 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, p. 51–53. Cited by: §5.3. [5] A. Biere, M. Heule, H. van Maaren, and T. Walsh (Eds.) (2021) Handbook of satisfiability - second edition. FAIA, Vol. 336, IOS Press. Cited by: §1. [6] C. Chang and R. C. T. Lee (1973) Symbolic logic and mechanical theorem proving. Computer science classics, Academic Press. Cited by: §2. [7] D. Chivilikhin, A. Pavlenko, and A. Semenov (2023) Decomposing hard sat instances with metaheuristic optimization. arXiv. Cited by: §2. [8] K. Chukharev, I. Gribanova, D. Ivanov, S. Kochemazov, V. Kondratiev, and A. Semenov (2025) Effective partitioning method with predictable hardness for circuitsat. IEEE Access 13, p. 4218–4234. External Links: ISSN 2169-3536 Cited by: item 1, §2, §2, Theorem 3.3, §3, §3, §3, Proof 4.3, §5.1, §5.3, §5.3, §5.3, §5.3, §6, Construction 1. [9] S. A. Cook (1971) The complexity of theorem-proving procedures. In STOC, p. 151–158. Cited by: §2. [10] T. H. Cormen, C. E. Leiserson, and R. L. Rivest (1990) Introduction to algorithms. 1 edition, MIT Press. Cited by: §5.1. [11] I. Damgård (1989) A design principle for hash functions. In Advances in Cryptology - CRYPTO, LNCS, Vol. 435, p. 416–427. Cited by: §5.1. [12] D. De, A. Kumarasubramanian, and R. Venkatesan (2007) Inversion attacks on secure hash functions using satsolvers. In SAT, LNCS, Vol. 4501, p. 377–382. Cited by: §5.1. [13] L. M. de Moura and N. S. Bjørner (2008) Z3: an efficient SMT solver. In TACAS, LNCS, Vol. 4963, p. 337–340. Cited by: §1. [14] H. Dobbertin (1998) The first two rounds of MD4 are not one-way. In FSE, LNCS, Vol. 1372, p. 284–292. Cited by: §5.1. [15] N. Eén and N. Sörensson (2006) Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput. 2 (1-4), p. 1–26. Cited by: Construction 1. [16] W. H. Gates and C. H. Papadimitriou (1979) Bounds for sorting by prefix reversal. Discrete Mathematics 27 (1), p. 47–57. Cited by: §5.1. [17] A. Gladush, I. Gribanova, V. Kondratiev, A. Pavlenko, and A. Semenov (2022) Measuring the effectiveness of sat-based guess-and-determine attacks in algebraic cryptanalysis. In Parallel Computational Technologies, L. Sokolinsky and M. Zymbler (Eds.), Cham, p. 143–157. External Links: ISBN 978-3-031-11623-0 Cited by: §2. [18] I. Gribanova and A. A. Semenov (2018) 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, p. 1174–1179. Cited by: §5.1. [19] M. J. H. Heule, O. Kullmann, S. Wieringa, and A. Biere (2012) Cube and conquer: guiding cdcl sat solvers by lookaheads. In HVC, p. 50–65. Cited by: §5.3. [20] A. E. J. Hyvärinen, T. Junttila, and I. Niemelä (2006) A distribution method for solving sat in grids. In Theory and Applications of Satisfiability Testing - SAT 2006, p. 430–435. External Links: ISBN 9783540372073, ISSN 1611-3349 Cited by: §3. [21] A. E. J. Hyvärinen (2011) Grid based propositional satisfiability solving. Ph.D. Thesis, Aalto University, Helsinki, Finland. Cited by: §1, Definition 3.1, §3. [22] M. Järvisalo and T. A. Junttila (2009) Limitations of restricted branching in clause learning. Constraints An Int. J. 14 (3), p. 325–356. Cited by: §4.1. [23] R. M. Karp (1972) Reducibility among combinatorial problems. In Complexity of Computer Computations, p. 85–103. External Links: ISBN 9781468420012 Cited by: §2. [24] D. Kroening (2021) Software verification. In Handbook of Satisfiability - Second Edition, FAIA, Vol. 336, p. 791–818. Cited by: §1. [25] A. Kuehlmann, V. Paruthi, F. Krohm, and M. K. Ganai (2002) Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21 (12), p. 1377–1394. Cited by: §2. [26] G. Leurent (2008) MD4 is not one-way. In FSE, LNCS, Vol. 5086, p. 412–428. Cited by: §5.1. [27] J.P. Marques-Silva and K.A. Sakallah (1999-05) GRASP: a search algorithm for propositional satisfiability. IEEE Transactions on Computers 48 (5), p. 506–521. External Links: ISSN 0018-9340 Cited by: §1. [28] J. Marques-Silva, I. Lynce, and S. Malik (2021) Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability - Second Edition, FAIA, Vol. 336, p. 133–182. Cited by: §1, §2, §4.1, Lemma 4.1. [29] J. P. Marques-Silva and K. A. Sakallah (1996) GRASP - a new search algorithm for satisfiability. In ICCAD, p. 220–227. Cited by: §1. [30] Irkutsk Supercomputer Center of SB RAS. External Links: Link Cited by: §5.2. [31] R. C. Merkle (1989) A certified digital signature. In CRYPTO, Lecture Notes in Computer Science, Vol. 435, p. 218–238. Cited by: §5.1. [32] P. Molitor, J. Mohnke, B. Becker, and C. Scholl (2004) Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods. Kluwer Academic Publishers. Cited by: §1, §2, Proof 4.3. [33] J. Rintanen (2021) Planning and sat. In Handbook of Satisfiability - Second Edition, FAIA, Vol. 336, p. 765–789. Cited by: §1. [34] R. L. Rivest (1990) The MD4 message digest algorithm. In Advances in Cryptology - CRYPTO, LNCS, p. 303–311. Cited by: §5.1. [35] A. A. Semenov, D. Chivilikhin, A. Pavlenko, I. V. Otpuschennikov, V. Ulyantsev, and A. Ignatiev (2021) Evaluating the hardness of SAT instances using evolutionary optimization algorithms. In CP, LIPIcs, Vol. 210, p. 47:1–47:18. Cited by: §2, §2. [36] A. A. Semenov, I. V. Otpuschennikov, I. Gribanova, O. Zaikin, and S. Kochemazov (2020) Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Log. Methods Comput. Sci. 16 (1). Cited by: §2, Lemma 4.1. [37] A. A. Semenov, O. Zaikin, D. Bespalov, and M. Posypkin (2011) Parallel logical cryptanalysis of the generator A5/1 in bnb-grid system. In PaCT, LNCS, Vol. 6873, p. 473–483. Cited by: §1. [38] A. A. Semenov, O. Zaikin, I. V. Otpuschennikov, S. Kochemazov, and A. Ignatiev (2018) On cryptographic attacks using backdoors for SAT. In AAAI, p. 6641–6648. Cited by: §1. [39] A. A. Semenov (2009) Decomposition representations of logical equations in problems of inversion of discrete functions. Journal of Computer and Systems Sciences International 48, p. 718–731. Cited by: §4.1. [40] A. Semenov, O. Zaikin, and S. Kochemazov (2021) Finding effective sat partitionings via black-box optimization. In Black Box Optimization, Machine Learning, and No-Free Lunch Theorems, p. 319–355. External Links: ISBN 9783030665159, ISSN 1931-6836 Cited by: §2, §2. [41] S. Szeider (2005) Backdoor sets for DLL subsolvers. J. Autom. Reason. 35 (1-3), p. 73–88. Cited by: §2. [42] G. S. Tseitin (1970) On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, Part I, p. 115–125. Cited by: §2. [43] X. Wang, X. Lai, D. Feng, H. Chen, and X. Yu (2005) Cryptanalysis of the hash functions MD4 and RIPEMD. In EUROCRYPT, LNCS, Vol. 3494, p. 1–18. Cited by: §5.1. [44] I. Wegener (1987) The complexity of Boolean functions. John Wiley & Sons. Cited by: §2. [45] R. Williams, C. P. Gomes, and B. Selman (2003) Backdoors to typical case complexity. In IJCAI, p. 1173–1178. Cited by: §4.1. [46] O. Zaikin (2022) Inverting 43-step MD4 via Cube-and-Conquer. In IJCAI, p. 1894–1900. Cited by: §5.1. [47] O. Zaikin (2024) Inverting cryptographic hash functions via Cube-and-Conquer. J. Artif. Intell. Res. 81, p. 359–399. Cited by: §5.1. [48] H. Zhang (2021) Combinatorial designs by sat solvers. In Handbook of Satisfiability - Second Edition, FAIA, Vol. 336, p. 818–858. Cited by: §1.