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
- Datum: May 2008
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.