Computation of renameable horn backdoors for quantified boolean formulas

Backdoor sets of SAT problem can quickly decide the satisfiability of real-world SAT instances, and the QBF problem is the generalization of SAT problem, so backdoor sets of QBF are crucial to its solution. We propose a new algorithm of computing QHorn deletion backdoor sets in this paper, which contains two stages. Firstly, we compute renamed QBF formula according to the largest renamable R_max of matrix of QBF formula, here only existent variables are renamed. Then the RQHorn deletion backdoor sets of the renamed QBF formula are computed. Furthermore, we illustrate the advantages of our algorithm through several real-world QBF instances.