Finding Effective SAT Partitionings Via Black-Box Optimization

In the present chapter we study one method for partitioning hard instances of the Boolean satisfiability problem (SAT). It uses a subset of a set of variables of an original formula to partition it into a family of subproblems that are significantly easier to solve individually. While it is usually very hard to estimate the time required to solve a hard SAT instance without actually solving it, the partitionings of the presented kind make it possible to naturally construct such estimations via the well-known Monte Carlo method. We show that the problem of finding a SAT partitioning with minimal estimation of time required to solve all subproblems can be formulated as the problem of minimizing a special pseudo-Boolean black-box function. The experimental part of the paper clearly shows that in the context of the proposed approach relatively simple black-box optimization algorithms show good results in application to minimization of the functions of the described kind even when faced with hard SAT instances that encode problems of finding preimages of cryptographic functions.