nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Bit-Vector Optimization

verfasst von : Alexander Nadel, Vadim Ryvchin

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

A variety of applications of Satisfiability Modulo Theories (SMT) require finding a satisfying assignment which optimizes some user-given function. Optimization in the context of SMT is referred to as Optimization Modulo Theories (OMT). Current OMT research is mostly dedicated to optimization in arithmetic domains. This paper is about Optimization modulo Bit-Vectors (OBV). We introduce two OBV algorithms which can easily be implemented in an eager bit-vector solver. We show that an industrial problem of fixing cell placement during the physical design stage of the CAD process can be reduced to optimization modulo either Bit-Vectors (BV) or Linear Integer Arithmetic (LIA). We demonstrate that our resulting OBV tool can solve industrial instances which are out of reach of existing BV and LIA OMT solvers.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Characteristic Formulae for Session Types

Nächstes Kapitel Runtime Monitoring with Union-Find Structures

Baier, C., Tinelli, C. (eds.): TACAS 2015. LNCS, vol. 9035. Springer, Heidelberg (2015)

Balas, E.: Disjunctive programming: properties of the convex hull of feasible points. Discrete Appl. Math. 89(1–3), 3–44 (1998)MathSciNetCrossRefMATH

Balas, E., Bonami, P.: New variants of lift-and-project cut generation from the LP tableau: open source implementation and testing. In: Fischetti, M., Williamson, D.P. (eds.) IPCO 2007. LNCS, vol. 4513, pp. 89–103. Springer, Heidelberg (2007)CrossRef

Barrett, C., Fontaine, P., Stump, A., Tinelli, C.: The SMT LIB standard. Version 2.5. http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf

Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)

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

Bjørner, N.: Private communication, March 2015

Bjørner, N., Phan, A.: \({\nu }\)z - maximal satisfaction with Z3. In: Kutsia, T., Voronkov, A. (eds.) 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014. EPiC Series, vol. 30, Gammarth, La Marsa, Tunisia, 7–8 December 2014, pp. 1–9. EasyChair (2014)

Bjørner, N., Phan, A., Fleckenstein, L.: \(\nu \)z - an optimizing SMT solver. In: Baier and Tinelli [1], pp. 194–199

10.

Bozzano, M., Cimatti, A., Griggio, A., Mattarei, C.: Efficient anytime techniques for model-based safety analysis. In: Kroening and Pasareanu [22], pp. 603–621

11.

Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski and Philippou [21], pp. 174–177

12.

Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 99–113. Springer, Heidelberg (2010)CrossRef

13.

Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394–409. Springer, Heidelberg (2012)CrossRef

14.

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)CrossRef

15.

Franzén, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 121–128. IEEE (2010)

16.

Frost, D., Dechter, R.: In search of the best constraint satisfaction search. In: AAAI, pp. 301–306 (1994)

17.

Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)CrossRef

18.

Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)CrossRef

19.

Hadarean, L.: An Efficient and Trustworthy Theory Solver for Bit-vectors in Satisfiability Modulo Theories. Dissertation, New York University (2015)

20.

Katelman, M., Meseguer, J.: vlogsl: a strategy language for simulation-based verification of hardware. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 504, pp. 129–145. Springer, Heidelberg (2011)CrossRef

21.

Kowalewski, S., Philippou, A. (eds.): TACAS 2009. LNCS, vol. 5505. Springer, Heidelberg (2009)

22.

Kroening, D., Păsăreanu, C.S. (eds.): CAV 2015. LNCS, vol. 9206. Springer, Heidelberg (2015)

23.

Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 607–618. ACM (2014)

24.

Manolios, P., Papavasileiou, V.: ILP modulo theories. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 662–677. Springer, Heidelberg (2013)CrossRef

25.

Marić, F., Janičić, P.: URBiVA: uniform reduction to bit-vector arithmetic. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 346–352. Springer, Heidelberg (2010)CrossRef

26.

Michel, R., Hubaux, A., Ganesh, V., Heymans, P.: An SMT-based approach to automated configuration. In: SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP 2012, p. 107 (2012)

27.

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18–22 June 2001, pp. 530–535. ACM (2001)

28.

Nadel, A.: Bit-vector rewriting with automatic rule generation. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 663–679. Springer, Heidelberg (2014)

29.

Nadel, A., Ryvchin, V.: Bit-vector optimization: benchmarks and detailed results. https://goo.gl/epFbO1

30.

Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242–255. Springer, Heidelberg (2012)CrossRef

31.

Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 206–218. Springer, Heidelberg (2014)

32.

Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)CrossRef

33.

Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)CrossRef

34.

Romano, A., Engler, D.: Expression reduction from programs in a symbolic binary executor. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 301–319. Springer, Heidelberg (2013)CrossRef

35.

Sebastiani, R., Tomasi, S.: Optimization in SMT with \({\cal LA}\) (Q) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 484–498. Springer, Heidelberg (2012)CrossRef

36.

Sebastiani, R., Tomasi, S., Trentin, P.: Optimathsat. http://optimathsat.disi.unitn.it

37.

Sebastiani, R., Trentin, P.: Optimathsat: a tool for optimization modulo theories. In: Kroening and Pasareanu [22], pp. 447–454

38.

Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Baier and Tinelli [1], pp. 335–349

39.

Sherwani, N.A.: Algorithms for VLSI Physical Design Automation, 3rd edn. Kluwer Press, Dordrecht (1998)MATH

40.

Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRef

41.

Strichman, O.: Tuning SAT checkers for bounded model checking. In: Allen Emerson, E., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)

42.

Wille, R., Große, D., Haedicke, F., Drechsler, R.: SMT-based stimuli generation in the SystemC verification library. In: Borrione, E. (ed.) Advances in Design Methods from Modeling Languages for Embedded Systems and SoCs. LNEE, vol. 63, pp. 227–244. Springer, Heidelberg (2010)

Titel: Bit-Vector Optimization
verfasst von: Alexander Nadel
Vadim Ryvchin
Verlag: Springer Berlin Heidelberg
Buch: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49674-9_53

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"