Skip to main content
SpringerLink
Log in

Mining Backbone Literals in Incremental SAT

A New Kind of Incremental Data

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing -- SAT 2015 (SAT 2015)

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

Abstract

In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores. In most settings in which incremental satisfiability is applied, many of the instances along the sequence of formulas being solved are unsatisfiable. We show that in such cases, with a P-time analysis of the proof, we can compute a set of literals that are logically implied by the next instance. By adding those literals as assumptions, we accelerate the search.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. HaifaMUC. http://ie.technion.ac.il/ofers/haifasolvers/

  2. Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Reducing the size of resolution proofs in linear time. STTT 13(3), 263–272 (2011)

    Article  Google Scholar 

  3. Belov, A., Marques-Silva, J.: MUSer2: An efficient MUS extractor. J. on Satisfiability, Boolean Modeling and Computation (JSAT) 8(1/2), 123–128 (2012)

    MATH  Google Scholar 

  4. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48(2), 149–169 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36–41. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161–177 (2015)

    MathSciNet  MATH  Google Scholar 

  10. Kroening, D., Strichman, O.: Decision procedures - an algorithmic point of view. Theoretical Computer Science. Springer-Verlag, February 2008 (to be published)

    Google Scholar 

  11. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Nadel, A.: Understanding and Improving a Modern SAT Solver. PhD thesis, Tel Aviv University, Tel Aviv, Israel, August 2009

    Google Scholar 

  13. Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Bloem, R., Sharygina, N. (eds.) FMCAD (2010)

    Google Scholar 

  14. Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: FMCAD, pp. 197–200. IEEE (2013)

    Google Scholar 

  15. Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174–187. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Shtrichman, O.: Sharing information between instances of a propositional satisfiability (SAT) problem, December 2000. US provisional patent (60/257,384). Later became patent US2002/0123867 A1

    Google Scholar 

  17. Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58–70. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Whittemore, J., Kim, J., Sakallah, K.: Satire: a new incremental satisfiability engine. In: IEEE/ACM Design Automation Conference (DAC) (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Research Lab, Haifa, Israel

    Alexander Ivrii

  2. Design Technology Solutions, Intel Co., Haifa, Israel

    Vadim Ryvchin

  3. Information Systems Engineering, IE, Technion, Haifa, Israel

    Ofer Strichman

Authors
  1. Alexander Ivrii
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vadim Ryvchin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ofer Strichman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ofer Strichman .

Editor information

Editors and Affiliations

  1. Algorithms, University of Texas, Austin, Texas, USA

    Marijn Heule

  2. Trusted Systems Research Group, Fort Meade, Texas, USA

    Sean Weaver

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ivrii, A., Ryvchin, V., Strichman, O. (2015). Mining Backbone Literals in Incremental SAT. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24318-4_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24317-7

  • Online ISBN: 978-3-319-24318-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation