[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2016 (SAT 2016)

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

Abstract

The theory of bit-vectors in SMT solvers is very important for many applications due to its ability to faithfully model the behavior of machine instructions. A crucial step in solving bit-vector formulas is the translation from high-level bit-vector terms down to low-level boolean formulas that can be efficiently mapped to CNF clauses and fed into a SAT solver. In this paper, we demonstrate how a combination of program synthesis and machine learning technology can be used to automatically generate code to perform this translation in a way that is tailored to particular problem domains. Using this technique, the paper shows that we can improve upon the basic encoding strategy used by CVC4 (a state of the art SMT solver) and automatically generate variants of the solver tailored to different domains of problems represented in the bit-vector benchmark suite from SMT-COMP 2015.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

References

  1. Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A parametric approach for smaller and better encodings of cardinality constraints. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 80–96. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. Dependable Softw. Syst. Eng. 40, 1–25 (2015)

    Google Scholar 

  3. Ansel, J., Kamil, S., Veeramachaneni, K., Ragan-Kelley, J., Bosboom, J., O’Reilly, U., Amarasinghe, S.P.: OpenTuner: an extensible framework for program autotuning. In: Amaral, J.N., Torrellas, J., (eds.) International Conference on Parallel Architectures and Compilation, PACT 2014, Edmonton, AB, Canada, 24–27 August 2014, pp. 303–316. ACM (2014)

    Google Scholar 

  4. Ansótegui, C., Sellmann, M., Tierney, K.: A gender-based genetic algorithm for the automatic configuration of algorithms. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 142–157. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bacchus, F.: GAC via unit propagation. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 133–147. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Barrett, C., Deters, M., Moura, L., Oliveras, A., Stump, A.: 6 years of SMT-COMP. J. Autom. Reasoning 50(3), 243–277 (2012)

    Article  Google Scholar 

  8. Barrett, C.W., de Moura, L., Stump, A.: SMT-COMP: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, 11–17 July 2009, pp. 412–418 (2009)

    Google Scholar 

  10. Bordeaux, L., Marques-Silva, J.: Knowledge compilation with empowerment. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 612–624. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Bounimova, E., Godefroid, P., Molnar, D.: Billions and billions of constraints: whitebox fuzz testing in production. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, Piscataway, pp. 122–131. IEEE Press (2013)

    Google Scholar 

  12. Brain, M., Hadarean, L., Kroening, D., Martins, R.: Automatic generation of propagation complete SAT encodings. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 536–556. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_26

    Chapter  Google Scholar 

  13. Brand, S., Narodytska, N., Quimper, C.-G., Stuckey, P.J., Walsh, T.: Encodings of the sequence constraint. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 210–224. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2009, pp. 1590–1595. European Design and Automation Association, Belgium (2009)

    Google Scholar 

  16. Cheung, A., Solar-Lezama, A., Madden, S.: Partial replay of long-running applications. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of software engineering, ESEC/FSE 2011, pp. 135–145. ACM, New York (2011)

    Google Scholar 

  17. Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 236–250. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. (JAIR) 17, 229–264 (2002)

    MathSciNet  MATH  Google Scholar 

  19. de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Doyle, J., Sandewall, E., Torasso, P., (eds.) Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR 1994), Bonn, Germany, 24–27 May 1994, pp. 551–561. Morgan Kaufmann (1994)

    Google Scholar 

  21. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Heidelberg (2014)

    Google Scholar 

  22. 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 

  23. Eén, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Gent, I.P.: Arc consistency in SAT. In: van Harmelen, F. (ed.) Proceedings of the 15th European Conference on Artificial Intelligence, ECAI 2002, Lyon, July 2002 pp. 121–125. IOS Press (2002)

    Google Scholar 

  25. Godefroid, P.: Test generation using symbolic execution. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, 15–17 December 2012, Hyderabad, vol. 18. LIPIcs, pp. 24–33. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)

    Google Scholar 

  26. Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120–135. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  27. Gwynne, M., Kullmann, O.: Generalising and unifying SLUR and unit-refutation completeness. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 220–232. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  28. Gwynne, M., Kullmann, O.: Towards a theory of good SAT representations. CoRR, abs/1302.4421 (2013)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  30. 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 

  31. Hurley, B., Kotthoff, L., Malitsky, Y., O’Sullivan, B.: Proteus: a hierarchical portfolio of solvers and transformations. In: Simonis, H. (ed.) CPAIOR 2014. LNCS, vol. 8451, pp. 301–317. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  32. Hutter, F., Babic, D., Hoos, H.H., Hu, A.J.: Boosting verification by automatic tuning of decision procedures. In: Proceedings of the Formal Methods in Computer Aided Design, FMCAD 2007, pp. 27–34. IEEE Computer Society, Washington, DC (2007)

    Google Scholar 

  33. Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507–523. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  34. Hutter, F., Hoos, H.H., Leyton-Brown, K., Stützle, T.: ParamILS: an automatic algorithm configuration framework. J. Artif. Int. Res. 36(1), 267–306 (2009)

    MATH  Google Scholar 

  35. Hutter, F., Hoos, H.H., Stützle, T.: Automatic algorithm configuration based on local search. In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, 22–26 July 2007, Vancouver, pp. 1152–1157. AAAI Press (2007)

    Google Scholar 

  36. Hutter, F., Lindauer, M.T., Balint, A., Bayless, S., Hoos, H.H., Leyton-Brown, K.: The configurable SAT solver challenge (CSSC). CoRR, abs/1505.01221 (2015)

    Google Scholar 

  37. Inala, J.P., Singh, R., Solar-Lezama, A.: Technical report: Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers (2016). http://jinala.github.io/assets/papers/sat2016tr.pdf. (Accessed on 24 April 2016)

  38. Jha, S., Limaye, R., Seshia, S.A.: Beaver: engineering an efficient SMT solver for bit-vector arithmetic. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 668–674. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  39. 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 

  40. Martins, R., Manquinho, V.M., Lynce, I.: Exploiting cardinality encodings in parallel maximum satisfiability. In: IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, 7–9 November 2011, pp. 313–320. IEEE Computer Society (2011)

    Google Scholar 

  41. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001, pp. 530–535. ACM, New York (2001)

    Google Scholar 

  42. Nguyen, C., Yoshida, H., Prasad, M.R., Ghosh, I., Sen, K.: Generating succinct test cases using don’t care analysis. In: Proceedings of the Eighth IEEE International Conference on Software Testing, Verification and Validation, pp. 1–10. IEEE (2015)

    Google Scholar 

  43. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pp. 179–190. ACM, New York (1989)

    Google Scholar 

  44. Sen, K., Kalasapur, S., Brutch, T., Gibbs, S.: Jalangi: A selective record-replay and dynamic analysis framework for Javascript. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp. 488–498. ACM, New York (2013)

    Google Scholar 

  45. Singh, R., Solar-Lezama, A.: Automatic generation of formula simplifiers based on conditional rewrite rules arXiv:1602.07285 (2016)

  46. Solar-Lezama, A.: Program Synthesis By Sketching. PhD thesis, EECS Dept., UC Berkeley (2008)

    Google Scholar 

  47. Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 313–326. ACM, New York (2010)

    Google Scholar 

  48. Stump, A., Sutcliffe, G., Tinelli, C.: Introducing StarExec: a cross-community infrastructure for logic solving. In: Klebanov, V., Beckert, B., Biere, A., Sutcliffe, G. (eds.) COMPARE, CEUR Workshop Proceedings, vol. 873, p. 2 (2012). CEUR-WS.org

  49. Tanno, H., Zhang, X., Hoshino, T., Sen, K.: TesMa and CATG: automated test generation tools for models of enterprise applications. In: Proceedings of the 37th International Conference on Software Engineering, ICSE 2015, vol. 2, pp. 717–720. IEEE Press, Piscataway (2015)

    Google Scholar 

  50. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning, pp. 466–483. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  51. Vallati, M., Hutter, F., Chrpa, L., McCluskey, T.L.: On the effective configuration of planning domain models. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, 25–31 July 2015, pp. 1704–1711. AAAI Press (2015)

    Google Scholar 

  52. Velev, M.N.: Efficient translation of boolean formulas to cnf in formal verification of microprocessors. In: Proceedings of the 2004 Asia and South Pacific Design Automation Conference, ASP-DAC 2004, pp. 310–315. IEEE Press, Piscataway (2004)

    Google Scholar 

  53. Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: A differential approach to undefined behavior detection. Commun. ACM 59(3), 99–106 (2016)

    Article  Google Scholar 

Download references

Acknowledgments

This research was partially supported by NSF award #1139056 (ExCAPE) and by DARPA MUSE award #FA8750-14-2-0270.

Author information

Authors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, MA, USA

    Jeevana Priya Inala, Rohit Singh & Armando Solar-Lezama

Authors
  1. Jeevana Priya Inala
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rohit Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armando Solar-Lezama
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jeevana Priya Inala .

Editor information

Editors and Affiliations

  1. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Inala, J.P., Singh, R., Solar-Lezama, A. (2016). Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_19

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation