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 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.