Computation of Renameable Horn Backdoors
-
Autor:
Stephan Kottler, Michael Kaufmann, and Carsten Sinz
-
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.
Links