Skip to main content
SpringerLink
Log in

Conditional Lower Bounds for Failed Literals and Related Techniques

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2014 (SAT 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8561))

  • 1308 Accesses

Abstract

We prove time-complexity lower bounds for various practically relevant probing-based CNF simplification techniques, namely failed literal detection and related techniques. Specifically, we show that improved algorithms for these simplification techniques would give a 2δn time algorithm for CNF-SAT for some δ < 1, violating the Strong Exponential Time Hypothesis.

This work was supported by Academy of Finland Finnish Centre of Excellence in Computational Inference Research COIN (grant #251170; M.J.) and Helsinki Doctoral Programme in Computer Science – Advanced Computing and Intelligent Systems (J.K.).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc. AAAI, pp. 613–619. AAAI Press / The MIT Press (2002)

    Google Scholar 

  2. Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Berre, D.L.: Exploiting the real power of unit propagation lookahead. Electronic Notes in Discrete Mathematics 9, 59–80 (2001)

    Article  Google Scholar 

  4. Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT Competition 2013. In: Proceedings of SAT Competition 2013. Department of Computer Science Series of Publications B, vol. B-2013-1, pp. 51–52. University of Helsinki (2013)

    Google Scholar 

  5. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 85. IOS Press (2009)

    Google Scholar 

  6. Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Transactions on Systems, Man, and Cybernetics, Part B 34(1), 52–59 (2004)

    Article  MathSciNet  Google Scholar 

  7. Calabro, C., Impagliazzo, R., Kabanets, V., Paturi, R.: The complexity of unique k-SAT: An isolation lemma for k-CNFs. Journal of Computer and System Sciences 74(3), 386–393 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  8. Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 75–85. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Cygan, M., Dell, H., Lokshtanov, D., Marx, D., Nederlof, J., Okamoto, Y., Paturi, R., Saurabh, S., Wahlstrom, M.: On problems as hard as CNF-SAT. In: Proc. CCC, pp. 74–84. IEEE (2012)

    Google Scholar 

  10. Debruyne, R., Bessière, C.: Some practicable filtering techniques for the constraint satisfaction problem. In: Proc. IJCAI, pp. 412–417. Morgan Kaufmann (1997)

    Google Scholar 

  11. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Fourdrinoy, O., Grégoire, É., Mazure, B., Sais, L.: Reducing hard SAT instances to polynomial ones. In: Proc. IRI, pp. 18–23, IEEE Systems, Man, and Cybernetics Society (2007)

    Google Scholar 

  13. Freeman, J.: Improvements to propositional satisfiability search algorithms. PhD thesis. University of Pennsylvania, USA (1995)

    Google Scholar 

  14. Gelder, A.V.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239–253 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  15. Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 423–429. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Gwynne, M., Kullmann, O.: Generalising unit-refutation completeness and SLUR via nested input resolution. J. Autom. Reasoning 52(1), 31–65 (2014)

    Article  MathSciNet  Google Scholar 

  17. Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proc. DAC, pp. 582–587. IEEE (2007)

    Google Scholar 

  18. Heule, M., Dufour, M., van Zwieten, J., van Maaren, H.: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 345–359. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Heule, M., Järvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. Heule, M.J.H., Järvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201–215. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  21. Heule, M.J.H., Järvisalo, M., Biere, A.: Revisiting hyper binary resolution. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 77–93. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  22. Heule, M., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 145–156. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Biere, et al. (eds.) [5], pp. 155–184

    Google Scholar 

  24. Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? Journal of Computer and System Sciences 63(4), 512–530 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  25. Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reasoning 49(4), 583–619 (2012)

    Article  MATH  Google Scholar 

  26. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  27. Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas (2002)

    Google Scholar 

  28. Kullmann, O.: Fundaments of branching heuristics. In: Biere, et al. (eds.) [5], pp. 205–244

    Google Scholar 

  29. Li, C.M.: Equivalency reasoning to solve a class of hard SAT problems. Inf. Process. Lett. 76(1-2), 75–81 (2000)

    Article  MATH  Google Scholar 

  30. Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc. AAAI, pp. 291–296. AAAI Press / The MIT Press (2000)

    Google Scholar 

  31. Li, C.M.: Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proc. IJCAI, pp. 366–371. Morgan Kaufmann (1997)

    Google Scholar 

  32. Lynce, I., Marques-Silva, J.P.: Probing-based preprocessing techniques for propositional satisfiability. In: Proc. ICTAI, p. 105. IEEE Computer Society (2003)

    Google Scholar 

  33. Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 102–117. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  34. Niemelä, I., Simons, P.: Smodels - an implementation of the stable model and well-founded semantics for normal LP. In: Fuhrbach, U., Dix, J., Nerode, A. (eds.) LPNMR 1997. LNCS, vol. 1265, pp. 421–430. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  35. Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: Proc. ECAI. FAIA, pp. 525–529. IOS Press (2008)

    Google Scholar 

  36. Prosser, P., Stergiou, K., Walsh, T.: Singleton consistencies. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 353–368. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  37. Ptracu, M., Williams, R.: On the possibility of faster SAT algorithms. In: Proc. SODA, pp. 1065–1075 (2010)

    Google Scholar 

  38. Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. Formal Methods in System Design 16(1), 23–58 (2000)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HIIT & Department of Computer Science, University of Helsinki, Finland

    Matti Järvisalo & Janne H. Korhonen

Authors
  1. Matti Järvisalo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Janne H. Korhonen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Karlsruher Institut für Technologie (KIT), Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Carsten Sinz

  2. TU Wien, Favoritenstraße 9-11, 1040, Wien, Austria

    Uwe Egly

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Järvisalo, M., Korhonen, J.H. (2014). Conditional Lower Bounds for Failed Literals and Related Techniques. In: Sinz, C., Egly, U. (eds) Theory and Applications of Satisfiability Testing – SAT 2014. SAT 2014. Lecture Notes in Computer Science, vol 8561. Springer, Cham. https://doi.org/10.1007/978-3-319-09284-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-09284-3_7

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-09283-6

  • Online ISBN: 978-3-319-09284-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation