Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Decomposing Hard SAT Instances with Metaheuristic Optimization
In the article, within the framework of the Boolean Satisfiability problem (SAT), the problem of estimating the hardness of specific Boolean formulas w.r.t. a specific complete SAT solving algorithm is considered. Based …
Evolutionary AlgorithmsMetaheuristic OptimizationAn island-parallel ensemble metaheuristic algorithm for large graph coloring problems
Graph Coloring Problem (GCP) is an NP-Hard vertex labeling problem in graphs such that no two adjacent vertices can have the same color. Large instances of GCP cannot be solved in reasonable execution times by exact algo…
Ensemble LearningParBalans: Parallel Multi-Armed Bandits-based Adaptive Large Neighborhood Search
Solving Mixed-Integer Programming (MIP) problems often requires substantial computational resources due to their combinatorial nature. Parallelization has emerged as a critical strategy to accelerate solution times and e…
Multi-Armed BanditsAccelerating supply chains with Ant Colony Optimization across range of hardware solutions
Ant Colony algorithm has been applied to various optimization problems, however most of the previous work on scaling and parallelism focuses on Travelling Salesman Problems (TSPs). Although, useful for benchmarks and new…
CPUA Circuit-Level Amoeba-Inspired SAT Solver
AmbSAT (or AmoebaSAT) is a biologically-inspired stochastic local search (SLS) solver to explore solutions to the Boolean satisfiability problem (SAT). AmbSAT updates multiple variables in parallel at every iteration ste…