Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

Victor Kondratiev; Irina Gribanova; Alexander Semenov

cs.AIFeb 19, 2026

Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

Authors: Victor Kondratiev, Irina Gribanova, Alexander Semenov

Organizations: ISDCT SB RAS, Irkutsk, Russia

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.

Figures & tables

Instance	q	d	t	Number of INDETs	Max. reached level	CPU time (s)	Wall-clock time (s)	CPU/wall ratio
$\mathtt{BvP}_{11,3}$	1000	3	500	25	2	332 392	9698	34.2
$\mathtt{BvP}_{17,2}$	1000	3	500	922	3	1 333 851	38 523	34.6
$\mathtt{PvS}_{9,4}$	1000	3	500	1548	3	2 000 801	57 649	34.7
$\mathtt{PvS}_{14,2}$	1000	3	500	0	1	73 971	2170	34.0
$\mathtt{PvS}_{11,3}$	1000	3	500	1251	3	1 723 511	49 553	34.7

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
$\mathtt{BvP}_{12,3}$	1000	3	500	2858	4	4 862 491	27 771	175.0
$\mathtt{BvS}_{13,3}$	1000	3	500	2106	5	8 478 171	48 015	176.5

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)	CnC wall-clock time (s)
$\mathtt{MD4\text{-}40}$	60 000	2	220	3089	4	6 763 298	43 054	—
$\mathtt{MD4\text{-}41}$	60 000	2	220	7455	4	9 128 960	57 660	$>$ 300 000
$\mathtt{MD4\text{-}42}$	60 000	2	220	1904	4	5 858 125	37 498	$>$ 300 000
$\mathtt{MD4\text{-}43}$	60 000	2	220	4020	3	7 027 119	43 288	264 039

Table 3: Results of applying Algorithm 3 to MD4 hash function inversion problems (180-core wall-clock time)

Boolean Satisfiability

See all 22 papers

GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
Mar 25, 2026Curie Kim, Carsten Portner, Mingju Liu +6Boolean Satisfiability Constraint Satisfaction
University of Maryland, College Park, MD, USA. · NVIDIA Research, Santa Clara, CA, USA. · NVIDIA Research, Austin, TX, USA. +3
Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning
Jul 23, 2026Chufeng Jiang, Neng-Fa ZhouElectronic Design Automation
Graduate Center, The City University of New York · The City University of New York New York, USA
Orthologic for SAT Solving
May 14, 2026Vladislas de Haldat, Simon Guilloud, Viktor KunčakLogical Reasoning Automated Theorem Proving
1EPFL

Mar 25, 2026J/K move · Enter open · S save

GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

Curie Kim, Carsten Portner, Mingju Liu, Steve Dai+5

University of Maryland, College Park, MD, USA. · NVIDIA Research, Santa Clara, CA, USA. · NVIDIA Research, Austin, TX, USA.+3

Boolean Satisfiability Constraint Satisfaction

Open paper AskPDF arXiv

Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite significant algorithmic advances over the past two decades, the performance of SAT solvers has improved at a limited pace. Notably, the 2025 competition winner shows only about a 2X improvement over the 2006 winner in SAT Competition performance after nearly 20 years of effort. This paper introduces GaloisSAT, a novel hybrid GPU-CPU SAT solver that integrates a differentiable SAT solving engine powered by modern machine learning infrastructure on GPUs, followed by a traditional CDCL-based SAT solving stage on CPUs. GaloisSAT is benchmarked against the latest versions of state-of-the-art solvers, Kissat and CaDiCaL, using the SAT Competition 2024 benchmark suite. Results demonstrate substantial improvements in the official SAT Competition metric PAR-2 (penalized average runtime with a timeout of 5,000 seconds and a penalty factor of 2). Specifically, GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category compared to the strongest baselines.

Abstract

Boolean Satisfiability

Explore similar work

GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra

Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning

Orthologic for SAT Solving