Home | english  | Impressum | Sitemap | KIT

Computation of Renameable Horn Backdoors

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. Satisfiability 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.