nach oben

Theory of Computing Systems

Erschienen in:

01.08.2016

Complexity of Fixed-Size Bit-Vector Logics

verfasst von: Gergely Kovásznai, Andreas Fröhlich, Armin Biere

Erschienen in: Theory of Computing Systems | Ausgabe 2/2016

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Bit-precise reasoning is important for many practical applications of Satisfiability Modulo Theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector formulas have been developed. From the theoretical point of view, only few results on the complexity of fixed-size bit-vector logics have been published. Some of these results only hold if unary encoding on the bit-width of bit-vectors is used. In our previous work (Kovásznai et al. 2012), we have already shown that binary encoding adds more expressiveness to various fixed-size bit-vector logics with and without quantification. In a follow-up work (Fröhlich et al. 2013), we then gave additional complexity results for several fragments of the quantifier-free case. In this paper, we revisit our complexity results from (Fröhlich et al. 2013; Kovásznai et al. 2012) and go into more detail when specifying the underlying logics and presenting the proofs. We give a better insight in where the additional expressiveness of binary encoding comes from. In order to do this, we bring together our previous work and propose several new complexity results for new fragments and extensions of earlier bit-vector logics. We also discuss the expressiveness of various bit-vector operations in more detail. Altogether, we provide the currently most complete overview on the complexity of common bit-vector logics.

Vorheriger Artikel An Improved Approximation Scheme for Variable-Sized Bin Packing

Nächster Artikel Information Lower Bounds via Self-Reducibility

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 "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

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

Nur mit Berechtigung zugänglich

http://www.smtlib.org/

This kind of result is often called unary NP-completeness [32].

Recall that only a variable, a constant, or an uninterpreted function can have explicit bit-width.

Although we do not intend the present a reduction of a general shift to the respective shift by constant, it is worth to mention that a common approach for such a reduction is the barrel shifter.

http://ecee.colorado.edu/wpmu/iimc/

http://fmv.jku.at/

http://www.satcompetition.org/

Ayari, A., Basin, D.A., Klaedtke, F.: Decision procedures for inductive boolean functions based on alternating automata. In: CAV, volume 1855 of LNCS. Springer (2000)

Balabanov, V., Chiang, H.-J.K., Jiang, J.-H.R.: Henkin quantifiers and boolean formulae. In: Proceedings of the SAT’12 (2012)

Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)

Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for bit-vector arithmetic. In: Proceedings of the 35th Design Automation Conference, pp 522–527 (1998)

Bjørner, N., Pichora, M.C.: Deciding fixed and non-fixed size bit-vectors. In: TACAS, volume 1384 of LNCS, pages 376–392. Springer (1998)

Bradley, A.R.: Sat-based model checking without unrolling. In: Proceedings of the VMCAI’11, pp. 70–87 (2011)

Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI, volume 3855 of Lecture Notes in Computer Science, pp. 427–442. Springer (2006)

Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: Proceedings of the FMCAD’11, pp. 144–153 (2011)

Brummayer, R., Boolector, A.B.: An efficient smt solver for bit-vectors and arrays. Springer (2009)

10.

Brummayer, R., Biere, A., Florian, L.: BTOR: bit-precise modelling of word-level problems for model checking. In: Proceedings of the 1st International Workshop on Bit-Precise Reasoning, pp. 33–38. ACM, New York (2008)

11.

Bruttomesso, R.: RTL Verification: From SAT to SMT(BV). PhD thesis, University of Trento (2008)

12.

Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT SMT solver. In: CAV, volume 5123 of LNCS, pp. 299–303. Springer (2008)

13.

Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width bit-vectors. In: ICCAD, pp. 13–20. IEEE (2009)

14.

Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems, TACAS’07, pp. 358–372. Springer, Berlin (2007)

15.

Bubeck, U., Büning, H.K.: Encoding nested boolean functions as quantified boolean formulas. JSAT 8(1/2), 101–116 (2012)MathSciNetMATH

16.

Butler, R.W., Miner, P.S., Srivas, M.K., Greve, D.A., Miller, S.P.: A bitvectors library for pvs. Technical report. NASA Langley Research Center, Hampton (1996)

17.

Chlebus, B.S.: From domino tilings to a new model of computation. In: Symposium on Computation Theory, vol. 208 of LNCS. Springer (1984)

18.

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv version 2: An opensource tool for symbolic model checking. In: Proceedings of the CAV02 (2002)

19.

Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: TACAS, vol. 6015 of LNCS. Springer (2010)

20.

Cook, S., Soltys, M.: Boolean programs and quantified propositional proof systems. Bulletin of the Section of Logic (1999)

21.

Cyrluk, D., Oliver, M., Harald, R.: An efficient decision procedure for a theory of fixed-sized bitvectors with composition and extraction. In: Computer-Aided Verification (CAV 97), pp. 60–71. Springer (1997)

22.

De Moura, L., Bjørner, N.: Z3: an efficient smt solver. Springer, Berlin (2008)

23.

Donini, F.M., Liberatore, P., Massacci, F., Schaerf, M.: Solving QBF with SMV. In: Proceedings of the KR’02, pp 578–589 (2002)

24.

Downey, R.G., Fellows, M.R.: Parameterized Complexity, p 530. Springer (1999)

25.

Dutertre, B., de Moura, L.: The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf (2006)

26.

Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: FMCAD’10, pp. 137–144 (2010)

27.

Franzén, A.: Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD thesis, University of Trento (2010)

28.

Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Proceedings of the POS’12 (2012)

29.

Fröhlich, A., Kovásznai, G., Biere, A.: Efficiently solving bit-vector problems using model checkers. In: Proceedings of the SMT’13 (2013)

30.

Fröhlich, A., Kovásznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Proceedings of the CSR’13 (2013)

31.

Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification (CAV ’07). Springer, Berlin (2007)

32.

Garey, M.R., Johnson, D.S.: NP-completeness results: Motivation, examples, and implications. J. ACM 25(3), 499–508 (1978)MathSciNetCrossRefMATH

33.

Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (NDSS). Internet Society (2008)

34.

Henkin, L.: Some remarks on infinitely long formulas. In: Infinistic Methods, pp. 167–183. Pergamon Press (1961)

35.

Johannsen, P.: Reducing bitvector satisfiability problems to scale down design sizes for RTL property checking. In: Proceedings of the High-Level Design Validation and Test Workshop, vol. 2001, pp 123–128 (2001)

36.

Johannsen, P.: Speeding Up Hardware Verification by Automated Data Path Scaling. PhD thesis. CAU Kiel, Germany (2002)

37.

Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying equivalence of memories using a first order logic theorem prover. In: FMCAD’09, pp. 128–135 (2009)

38.

Klarlund, N., Anders, M., Schwartzbach, M.I.: Mona implementation secrets. In: Proceedings of the CIAA’00, pp. 182–194 (2000)

39.

Knuth, D.E.: The Art of Computer Programming, Volume 4A: Combinatorial Algorithms. Addison-Wesley (2011)

40.

Korovin, K.: iProver — an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of the IJCAR’08, IJCAR ’08. Springer (2008)

41.

Kovásznai, G., Fröhlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proceedings of the SMT’12, pp. 44–55 (2012)

42.

Kovásznai, G., Fröhlich, A., Biere, A.: bv2epr: A tool for polynomially translating quantifier-free bit-vector formulas into epr. In: Proceedings of the CADE’13 (2013)

43.

Kovásznai, G., Fröhlich, A., Biere, A.: Quantifier-free bit-vector formulas with binary encoding: Benchmark description. In: Balint, A., Belov, A., Heule, M., Järvisalo, M. (eds.) Proceedings of the SAT Competition 2013, vol. B-2013-1 of Department of Computer Science Series of Publications B, pp. 107–108. University of Helsinki (2013)

44.

Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer (2008)

45.

Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980)MathSciNetCrossRefMATH

46.

Marx, M.: Complexity of modal logic. In: Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pp. 139–179. Elsevier (2007)

47.

Niewerth, M., Schwentick, T.: Two-variable logic and key constraints on data words. In: ICDT, pp. 138–149 (2011)

48.

Papadimitriou, C.H.: Computational complexity. Addison-Wesley (1994)

49.

Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information (2001)

50.

Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: FOCS, pp. 348–363. IEEE Computer Society (1979)

51.

Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. STTT 7(2), 156–173 (2005)CrossRef

52.

Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)MathSciNetCrossRefMATH

53.

Schuele, T., Schneider, K.: Verification of data paths using unbounded integers: automata strike back. In: Proceedings of the 2nd international Haifa verification conference on Hardware and software, verification and testing, HVC’06, pp. 65–80. Springer-Verlag, Berlin (2007)

54.

Prasad Sistla, A., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetCrossRefMATH

55.

Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical report, EPFL, Lausanne, Switzerland (2012)

56.

Spielmann, A., Kuncak, V.: Synthesis for unbounded bitvector arithmetic. In: International Joint Conference on Automated Reasoning (IJCAR), LNAI. Springer (2012)

57.

Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Raymond Strong, H. (eds.) STOC, pp. 1–9. ACM (1973)

58.

Warren, H.S.: Hacker’s Delight. Addison-Wesley Longman (2002)

59.

Wintersteiger, C.M.: Termination Analysis for Bit-Vector Programs. PhD thesis. ETH Zurich, Switzerland (2011)

60.

Wintersteiger, C.M., Hamadi, Y., de Moura, M.L.: Efficiently solving quantified bit-vector formulas. In: Proceedings of the FMCAD, pp. 239–246. IEEE (2010)

61.

Wolper, P., Boigelot, B.: An automata-theoretic approach to presburger arithmetic constraints (extended abstract). In: Procedings of the Static Analysis Symposium, LNCS 983, pp. 21–32. Springer LNCS (1995)

Titel: Complexity of Fixed-Size Bit-Vector Logics
verfasst von: Gergely Kovásznai
Andreas Fröhlich
Armin Biere
Publikationsdatum: 01.08.2016
Verlag: Springer US
Erschienen in: Theory of Computing Systems / Ausgabe 2/2016
Print ISSN: 1432-4350
Elektronische ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-015-9653-1

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 "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2016

An Improved Approximation Scheme for Variable-Sized Bin Packing

Walking on Data Words

Information Lower Bounds via Self-Reducibility

QuickHeapsort: Modifications and Improved Analysis

Weak Abelian Periodicity of Infinite Words

Preface