Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

Victor Kondratiev, Irina Gribanova, Alexander Semenov

TL;DR

A novel parallel algorithm for decomposing hard CircuitSAT instances that employs specialized constraints to partition an original SAT instance into a family of weakened formulas, guided by hardness estimations computed in parallel.

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.

Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

TL;DR

A novel parallel algorithm for decomposing hard CircuitSAT instances that employs specialized constraints to partition an original SAT instance into a family of weakened formulas, guided by hardness estimations computed in parallel.

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.
Paper Structure (5 sections, 3 theorems, 5 equations, 1 algorithm)

This paper contains 5 sections, 3 theorems, 5 equations, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Construction of SAT Partitioning for CircuitSAT
  4. Adaptive Parallel Algorithm for Constructing Partitionings in CircuitSAT
  5. Basic Algorithm

Key Result

theorem thmcountertheorem

For any CNF $C$ encoding a CircuitSAT problem and any complete interval system $\mathcal{R}^n$, the set $\Pi = \{C_I\}_{I \in \mathcal{R}^n}$ forms a SAT partitioning of $C$.

Theorems & Definitions (5)

  • definition thmcounterdefinition: Hyvarinen2011
  • definition thmcounterdefinition
  • theorem thmcountertheorem: IEEE2025
  • lemma thmcounterlemma
  • theorem thmcountertheorem