Abstract. Satisﬁability of real-world SAT instances can be often decided by focusing on a particular subset of variables - a so-called Backdoor Set. In this paper we suggest two algorithms to compute Renameable Horn deletion backdoors. Both methods are based on the idea to transform the computation into a graph problem. This approach could be used as a preprocessing to solve hard real-world SAT instances.We also give some experimental results of the computations of Renameable Horn backdoors for several real-world instances.
Computation of Renameable Horn Backdoors
Stephan Kottler, Michael Kaufmann, and Carsten Sinz
In Proc. of the 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2008), pages 154-160, Guangzhou, China