zbMATH — the first resource for mathematics

Complexity of fixed-size bit-vector logics. (English) Zbl 1357.68086
Summary: 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 [the authors, “On the complexity of fixed-size bit-vector logics with binary encoded bit-width”, in: Proceedings of the 10th international workshop on satisfiability modulo theories, SMT’12. Amsterdam: Elsevier. 44–55 (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 [the authors, Lect. Notes Comput. Sci. 7913, 378–390 (2013; Zbl 1345.68172)], we then gave additional complexity results for several fragments of the quantifier-free case. In this paper, we revisit our complexity results from the authors’ papers cited above 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.

68Q25 Analysis of algorithms and problem complexity
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI
[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) · Zbl 0974.94033
[2] Balabanov, V., Chiang, H.-J.K., Jiang, J.-H.R.: Henkin quantifiers and boolean formulae. In: Proceedings of the SAT’12 (2012) · Zbl 1273.03046
[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) · Zbl 0471.03034
[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) · Zbl 0379.68035
[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) · Zbl 0188.33502
[6] Bradley, A.R.: Sat-based model checking without unrolling. In: Proceedings of the VMCAI’11, pp. 70-87 (2011) · Zbl 1317.68109
[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) · Zbl 1176.68116
[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) · Zbl 0632.68034
[9] Brummayer, R., Boolector, A.B.: An efficient smt solver for bit-vectors and arrays. Springer (2009) · Zbl 1331.68199
[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) · Zbl 0188.33502
[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) · Zbl 1186.68281
[15] Bubeck, U; Büning, HK, Encoding nested Boolean functions as quantified Boolean formulas, JSAT, 8, 101-116, (2012) · Zbl 1331.68199
[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) · Zbl 0604.68053
[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) · Zbl 1010.68766
[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) · Zbl 1284.68172
[20] Cook, S., Soltys, M.: Boolean programs and quantified propositional proof systems. Bulletin of the Section of Logic (1999) · Zbl 0951.03052
[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) · Zbl 1345.68172
[31] Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer Aided Verification (CAV ’07). Springer, Berlin (2007) · Zbl 1135.68472
[32] Garey, MR; Johnson, DS, NP-completeness results: motivation, examples, and implications, J. ACM, 25, 499-508, (1978) · Zbl 0379.68035
[33] Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (NDSS). Internet Society (2008) · Zbl 0471.03034
[34] Henkin, L.: Some remarks on infinitely long formulas. In: Infinistic Methods, pp. 167-183. Pergamon Press (1961) · Zbl 0121.25308
[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) · Zbl 0989.03500
[39] Knuth, D.E.: The Art of Computer Programming, Volume 4A: Combinatorial Algorithms. Addison-Wesley (2011) · Zbl 1354.68001
[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) · Zbl 1165.68462
[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) · Zbl 1345.68172
[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) · Zbl 1149.68071
[45] Lewis, HR, Complexity results for classes of quantificational formulas, J. Comput. Syst. Sci., 21, 317-353, (1980) · Zbl 0471.03034
[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) · Zbl 0833.68049
[49] Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information (2001) · Zbl 0991.91007
[50] Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: FOCS, pp. 348-363. IEEE Computer Society (1979) · Zbl 1331.68199
[51] Prasad, MR; Biere, A; Gupta, A, A survey of recent advances in SAT-based formal verification, STTT, 7, 156-173, (2005)
[52] Savitch, WJ, Relationships between nondeterministic and deterministic tape complexities, J. Comput. Syst. Sci., 4, 177-192, (1970) · Zbl 0188.33502
[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, EM, The complexity of propositional linear temporal logics, J. ACM, 32, 733-749, (1985) · Zbl 0632.68034
[55] Spielmann, A., Kuncak, V.: On synthesis for unbounded bit-vector arithmetic. Technical report, EPFL, Lausanne, Switzerland (2012) · Zbl 1358.68198
[56] Spielmann, A., Kuncak, V.: Synthesis for unbounded bitvector arithmetic. In: International Joint Conference on Automated Reasoning (IJCAR), LNAI. Springer (2012) · Zbl 1358.68198
[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) · Zbl 0632.68034
[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) · Zbl 1284.03212
[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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.