Abstract
Knowing a Backdoor Set B for a given Sat instance, satisfiability can be decided by only examining each of the 2|B| truth assignments of the variables in B. However, one problem is to efficiently find a small backdoor up to a particular size and, furthermore, if no backdoor of the desired size could be found, there is in general no chance to conclude anything about satisfiability.
In this paper we introduce a complete deterministic algorithm for an NP-hard subclass of 3-Sat, that is also a subclass of Mixed Horn Formulas (MHF). For an instance of the described class the absence of two particular kinds of backdoor sets can be used to prove unsatisfiability. The upper bound of this algorithm is O(p(n)*1.427n) which is less than the currently best upper bound for deterministic algorithms for 3-Sat and MHF.
This work was partly supported by DFG-SPP 1307, project “Structure-based Algorithm Engineering for SAT-Solving”.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Proc. Lett. 8, 121–123 (1979)
Brüggemann, T., Kern, W.: An improved deterministic local search algorithm for 3-sat. Theor. Comput. Sci. 329(1-3), 303–313 (2004)
del Val, A.: On 2-SAT and renamable horn. In: AAAI: 17th National Conference on Artificial Intelligence, AAAI / MIT Press (2000)
Fernau, H.: A top-down approach to search-trees: Improved algorithmics for 3-hitting set. Electronic Colloquium on Computational Complexity, TR04-073 (2004)
Franco, J., Swaminathan, R.: On good algorithms for determining unsatisfiability of propositional formulas. Discrete Appl. Math. 130(2), 129–138 (2003)
Interian, Y.: Backdoor sets for random 3-sat. In: SAT (2003)
Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Universität Tübingen (October 2002)
Nishimura, N., Ragde, P., Szeider, S.: Detecting backdoor sets with respect to horn and binary clauses. In: SAT (2004)
Nishimura, N., Ragde, P., Szeider, S.: Solving #SAT using vertex covers. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 396–409. Springer, Heidelberg (2006)
Porschen, S., Speckenmeyer, E.: Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 251–262. Springer, Heidelberg (2005)
Porschen, S., Speckenmeyer, E.: Satisfiability of mixed Horn formulas. Discrete Applied Mathematics 155(11), 1408–1419 (2007)
Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: AAAI, pp. 124–130 (2004)
Schöning, U.: A probabilistic algorithm for k-sat and constraint satisfaction problems. In: Symposium on Foundations of Computer Science (1999)
Szeider, S.: Matched Formulas and Backdoor Sets. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 94–99. Springer, Heidelberg (2007)
Wahlström, M.: Algorithms, measures, and upper bounds for satisfiability and related problems. PhD thesis, Linköping University, Dissertation no 1079 (2007)
Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: IJCAI (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kottler, S., Kaufmann, M., Sinz, C. (2008). A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors. In: Kleine Büning, H., Zhao, X. (eds) Theory and Applications of Satisfiability Testing – SAT 2008. SAT 2008. Lecture Notes in Computer Science, vol 4996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79719-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-79719-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79718-0
Online ISBN: 978-3-540-79719-7
eBook Packages: Computer ScienceComputer Science (R0)