Home | english  | Impressum | Sitemap | KIT

Computation of Renameable Horn Backdoors

Computation of Renameable Horn Backdoors
Autor:

Stephan Kottler, Michael Kaufmann, and Carsten Sinz

Links:
Quelle:

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.