# Decomposing Hard SAT Instances with Metaheuristic Optimization

arXiv: https://arxiv.org/abs/2312.10436 · HTML: https://mlsanity.com/paper/2312.10436/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 87 references that are in the map.
- First posted on arXiv 16 Dec 2023.

## Builds on (most cited first, 8 of 8)

- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)
- [Fast Genetic Algorithms](https://mlsanity.com/paper/1703.03334/) (2017)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [On Cryptographic Attacks Using Backdoors for SAT](https://mlsanity.com/paper/1803.04646/) (2018)
- [Using Automatic Generation of Relaxation Constraints to Improve the Preimage Attack on 39-step MD4](https://mlsanity.com/paper/1802.06940/) (2018)
- [Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem](https://mlsanity.com/paper/1507.00862/) (2015)
- [Upper and Lower Bounds for Weak Backdoor Set Detection](https://mlsanity.com/paper/1304.5518/) (2013)

## Built on by (most cited first, 1 of 1)

- [Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances](https://mlsanity.com/paper/2602.17130/) (2026)

## Abstract (arXiv)

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 on the well-known Strong Backdoor Set (SBS) concept, we introduce the notion of decomposition hardness (d-hardness). If B is an arbitrary subset of the set of variables occurring in a SAT formula C, and A is an arbitrary complete SAT solver , then the d-hardness expresses an estimate of the hardness of C w.r.t. A and B. We show that the d-hardness of C w.r.t. a particular B can be expressed in terms of the expected value of a special random variable associated with A, B, and C. For its computational evaluation, algorithms based on the Monte Carlo method can be used. The problem of finding B with the minimum value of d-hardness is formulated as an optimization problem for a pseudo-Boolean function whose values are calculated as a result of a probabilistic experiment. To minimize this function, we use evolutionary algorithms. In the experimental part, we demonstrate the applicability of the concept of d-hardness and the methods of its estimation to solving hard unsatisfiable SAT instances.