Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Theory of Computing Systems
Published in: Theory of Computing Systems 2/2016

01-08-2016

Complexity of Fixed-Size Bit-Vector Logics

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

Published in: Theory of Computing Systems | Issue 2/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.
previous article An Improved Approximation Scheme for Variable-Sized Bin Packing
next article Information Lower Bounds via Self-Reducibility

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Appendix
Available only for authorised users
Footnotes
2
This kind of result is often called unary NP-completeness [32].
 
3
Recall that only a variable, a constant, or an uninterpreted function can have explicit bit-width.
 
4
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.
 
Literature
1.
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)
2.
Balabanov, V., Chiang, H.-J.K., Jiang, J.-H.R.: Henkin quantifiers and boolean formulae. In: Proceedings of the SAT’12 (2012)
3.
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)
4.
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)
5.
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)
6.
Bradley, A.R.: Sat-based model checking without unrolling. In: Proceedings of the VMCAI’11, pp. 70–87 (2011)
7.
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)
8.
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)
9.
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.
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.
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.
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.
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)
Metadata
Title
Complexity of Fixed-Size Bit-Vector Logics
Authors
Gergely Kovásznai
Andreas Fröhlich
Armin Biere
Publication date
01-08-2016
Publisher
Springer US
Published in
Theory of Computing Systems / Issue 2/2016
Print ISSN: 1432-4350
Electronic ISSN: 1433-0490
DOI
https://doi.org/10.1007/s00224-015-9653-1

Other articles of this Issue 2/2016

Theory of Computing Systems 2/2016 Go to the issue

OriginalPaper

QuickHeapsort: Modifications and Improved Analysis

OriginalPaper

Weak Abelian Periodicity of Infinite Words

OriginalPaper

An Improved Approximation Scheme for Variable-Sized Bin Packing

EditorialNotes

Preface

OriginalPaper

Multi-weighted Automata and MSO Logic

OriginalPaper

Walking on Data Words

Premium Partner

    Image Credits