On Probabilistic Generalization of Backdoors in Boolean Satisfiability

No. 9: AAAI-22 Technical Tracks 9

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 36

AAAI Technical Track on Search and Optimization

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables B a ρ-backdoor, if for a fraction of at least ρ of possible assignments of variables from B, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a ρ-backdoor with ρ=1 is an SBS. For a given set B it is possible to efficiently construct an (ε, δ)-approximation of parameter ρ using the Monte Carlo method. Thus, we define an (ε, δ)-SBS as such a set B for which the conclusion "parameter ρ deviates from 1 by no more than ε" is true with probability no smaller than 1 - δ. We consider the problems of finding the minimum SBS and the minimum (ε, δ)-SBS. To solve the former problem, one can use the algorithm described by R. Williams, C. Gomes and B. Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter problem, and show that the asymptotic estimation of the worst-case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams et al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal (ε, δ)-SBS. Results of computational experiments show that the use of (ε, δ)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.

10.1609/aaai.v36i9.21277