Endowed professorship for reliable software systems in the automotive industry

Computation of Renameable Horn Backdoors

  • Author:

    Stephan Kottler, Michael Kaufmann, and Carsten Sinz

  • Source:

    In Proc. of the 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2008), pages 154-160, Guangzhou, China

  • Date: 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.