Probabilistic Generalization of Backdoor Trees with Application to SAT


  • Alexander Semenov ITMO University
  • Daniil Chivilikhin ITMO University
  • Stepan Kochemazov ITMO University
  • Ibragim Dzhiblavi ITMO University



CSO: Satisfiability, CSO: Search, CSO: Solvers and Tools, SO: Evolutionary Computation, SO: Heuristic Search, SO: Metareasoning and Metaheuristics


The concept of Strong Backdoor Sets (SBS) for Constraint Satisfaction Problems is well known as one of the attempts to exploit structural peculiarities in hard instances. However, in practice, finding an SBS for a particular instance is often harder than solving it. Recently, a probabilistic weakened variant of the SBS was introduced: in the SBS, all subproblems must be polynomially solvable, whereas in the probabilistic SBS only a large fraction ρ of them should have this property. This new variant of backdoors called ρ-backdoors makes it possible to use the Monte Carlo method and metaheuristic optimization to find ρ-backdoors with ρ very close to 1, and relatively fast. Despite the fact that in a ρ-backdoor-based decomposition a portion of hard subproblems remain, in practice the narrowing of the search space often allows solving the problem faster with such a backdoor than without it. In this paper, we significantly improve on the concept of ρ-backdoors by extending this concept to backdoor trees: we introduce ρ-backdoor trees, show the interconnections between SBS, ρ-backdoors, and the corresponding backdoor trees, and establish some new theoretical properties of backdoor trees. In the experimental part of the paper, we show that moving from the metaheuristic search for ρ-backdoors to that of ρ-backdoor trees allows drastically reducing the time required to construct the required decompositions without compromising their quality.




How to Cite

Semenov, A., Chivilikhin, D., Kochemazov, S., & Dzhiblavi, I. (2023). Probabilistic Generalization of Backdoor Trees with Application to SAT. Proceedings of the AAAI Conference on Artificial Intelligence, 37(4), 4095-4103.



AAAI Technical Track on Constraint Satisfaction and Optimization