Skip to main content
SpringerLink
Log in

Automatic Generation of Propagation Complete SAT Encodings

  • Conference paper
  • First Online:
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

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

Abstract

Almost all applications of SAT solvers generate Boolean formulae from higher level expression graphs by encoding the semantics of each operation or relation into propositional logic. All non-trivial relations have many different possible encodings and the encoding used can have a major effect on the performance of the system. This paper gives an abstract satisfaction based formalisation of one aspect of encoding quality, the propagation strength, and shows that propagation complete SAT encodings can be modelled by our formalism and automatically computed for key operations. This allows a more rigorous approach to designing encodings as well as improved performance.

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 EPUB and 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

Notes

  1. 1.

    As an optimization we add the negation of the minimal unsatisfiable core of \(\lnot \mathsf {pa} '\): \(\mathsf {MUS} (\mathsf {pa} ')\).

References

  1. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  2. Babka, M., Balyo, T., Čepek, O., Gurskỳ, Š., Kučera, P., Vlček, V.: Complexity issues related to propagation completeness. Artif. Intell. 203, 19–34 (2013)

    Article  Google Scholar 

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

  4. Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Workshop on Satisfiability Modulo Theories (2010)

    Google Scholar 

  7. Berkeley Logic Synthesis and Verification Group: ABC: A System for Sequential Synthesis and Verification, Release 70930, http://www.eecs.berkeley.edu/alanmi/abc

  8. Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: International Joint Conference on Artificial Intelligence, pp. 412–418. AAAI Press (2009)

    Google Scholar 

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

    Google Scholar 

  10. Bordeaux, L., Janota, M., Marques-Silva, J., Marquis, P.: On unit-refutation complete formulae with existentially quantified variables. In: Principles of Knowledge Representation and Reasoning. AAAI Press (2012)

    Google Scholar 

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

  12. Brain, M., D’Silva, V., Haller, L., Griggio, A., Kroening, D.: An abstract interpretation of DPLL(T). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 455–475. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

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

  14. Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

  16. Del Val, A.: Tractable databases: how to make propositional unit resolution complete through compilation. In: Principles of Knowledge Representation and Reasoning, pp. 551–561. Morgan Kaufmann (1994)

    Google Scholar 

  17. D’Silva, V., Haller, L., Kroening, D.: Satisfiability solvers are static analysers. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 317–333. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. D’Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Symposium on Principles of Programming Languages, pp. 143–154. ACM (2013)

    Google Scholar 

  19. D’Silva, V., Haller, L., Kroening, D.: Abstract satisfaction. In: Symposium on Principles of Programming Languages, pp. 139–150. ACM (2014)

    Google Scholar 

  20. D’Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48–63. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  21. D’Silva, V., Kroening, D.: Abstraction of syntax. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 396–413. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

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

    Google Scholar 

  23. Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2(1–4), 1–26 (2006)

    MATH  Google Scholar 

  24. Gent, I.P.: Arc consistency in SAT. In: European Conference on Artificial Intelligence, pp. 121–125. IOS Press (2002)

    Google Scholar 

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

  26. Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 409–420. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  27. Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Formal Methods in Computer-Aided Design, pp. 131–140. IEEE (2012)

    Google Scholar 

  28. Hansen, T.: A Constraint Solver and its Application to Machine Code Test Generation. Ph.D. thesis, University of Melbourne (2012)

    Google Scholar 

  29. Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Handbook of Satisfiability, pp. 155–184. IOS Press (2009)

    Google Scholar 

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

  31. King, A., Søndergaard, H.: Automatic abstraction for congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 197–213. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  32. Kleine Büning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Handbook of Satisfiability, pp. 339–401. IOS Press (2009)

    Google Scholar 

  33. Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Ann. Math. Artif. Intelli. 40(3–4), 303–352 (2004)

    Article  MATH  MathSciNet  Google Scholar 

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

  35. Martins, R., Manquinho, V., Lynce, I.: Exploiting cardinality encodings in parallel maximum satisfiability. In: International Conference on Tools with Artificial Intelligence, pp. 313–320. IEEE Computer Society (2011)

    Google Scholar 

  36. Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  37. Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  38. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367–373. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Acknowledgments

This research was partially supported by ERC project 280053 (CPROVER) and by DARPA MUSE award #FA8750-14-2-0270. The views, opinions, and/or findings contained in this article are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, UK

    Martin Brain, Liana Hadarean & Daniel Kroening

  2. University of Texas at Austin, Austin, USA

    Ruben Martins

Authors
  1. Martin Brain
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Liana Hadarean
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniel Kroening
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ruben Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ruben Martins .

Editor information

Editors and Affiliations

  1. EPFL IC-DO, Lausanne, Switzerland

    Barbara Jobstmann

  2. Microsoft Research, Redmond, Washington, USA

    K. Rustan M. Leino

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brain, M., Hadarean, L., Kroening, D., Martins, R. (2016). Automatic Generation of Propagation Complete SAT Encodings. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-49122-5_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-49121-8

  • Online ISBN: 978-3-662-49122-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation