×

Optimization modulo the theories of signed bit-vectors and floating-point numbers. (English) Zbl 07433028

Summary: Optimization modulo theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or Pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling bit-precise representations of numbers, which in SMT are handled by means of the theory of bit-vectors \((\mathcal{BV})\) for the integers and that of floating-point numbers \((\mathcal{FP})\) for the reals respectively. Whereas an approach for OMT with (unsigned) \(\mathcal{BV}\) objectives has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with \(\mathcal{FP}\) objectives. In this paper we fill this gap, and we address for the first time OMT with \(\mathcal{FP}\) objectives. We present a novel OMT approach, based on the novel concept of attractor and dynamic attractor, which extends the work of Nadel and Ryvchin to work with signed-\(\mathcal{BV}\) objectives and, most importantly, with \(\mathcal{FP}\) objectives. We have implemented some novel OMT procedures on top of OptiMath-SAT and tested them on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of our novel approach.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] http://disi.unitn.it/trentin/resources/floatingpoint_test.tar.gz
[2] https://hub.docker.com/repository/docker/patricktrentin88/jar2020_floatingpoint_test
[3] nuXmv. https://nuxmv.fbk.eu
[4] SmtLibv2. www.smtlib.cs.uiowa.edu/
[5] IEEE standard 754, 2008. http://grouper.ieee.org/groups/754/
[6] Albuquerque, H.F., Araujo, R.F., de Bessa, I.V., Cordeiro, L.C., de Lima Filho, E.B.: OptCE: a counterexample-guided inductive optimization solver. In: SBMF, volume 10623 of Lecture Notes in Computer Science, pp. 125-141. Springer (2017)
[7] Araujo, RF; Albuquerque, HF; de Bessa, IV; Cordeiro, LC; Filho, JEC, Counterexample guided inductive optimization based on satisfiability modulo theories, Sci. Comput. Program., 165, 3-23 (2018)
[8] Araújo, R., Bessa, I., Cordeiro, L.C., Filho, J.E.C.: SMT-based verification applied to non-convex optimization problems. In: 2016 VI Brazilian Symposium on Computing Systems Engineering (SBESC), pp. 1-8 (2016)
[9] Bjorner, N., Phan, A.-D.: \( \nu{}Z\)-Maximal satisfaction with Z3. In: Proceedings of International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC)
[10] Bjorner, N., Phan, A.-D, Fleckenstein, L.: \( \nu Z\)—an optimizing SMT solver. In: Proceedings of TACAS, volume 9035 of LNCS. Springer (2015)
[11] Bozzano, M., Bruttomesso, R., Cimatti, A., Franzèn, A., Hanna, Z., Khasidashvili, Z., Palti, A. Sebastiani, R.: Encoding RTL constructs for MathSAT: a preliminary report. In: Proceedings of 3rd Workshop of Pragmatics on Decision Procedure in Automated Reasoning, PDPAR’05, ENTCS. Elsevier (2005) · Zbl 1272.68230
[12] Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D:. Interpolation-based verification of floating-point programs with abstract CDCL. In: SAS, pp. 412-432 (2013)
[13] Brain, M., D’Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods Syst. Des. 45(2), 213-245 (2014) · Zbl 1317.68110
[14] Brain, M., Tinelli, C., Rümmer, P., Wahl, T:. An automatable formal semantics for IEEE-754 floating-point arithmetic. In: ARITH, pp. 160-167. IEEE (2015)
[15] Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: 2009 Formal Methods in Computer-Aided Design, pp. 69-76 (2009)
[16] Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proceedings of ASP-DAC 2002, pp. 741-746. IEEE (2002)
[17] Brummayer, R.: Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. PhD thesis, Informatik, Johannes Kepler University Linz (2009) · Zbl 1187.68168
[18] Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: TACAS, pp. 174-177. Springer, Berlin (2009)
[19] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: A lazy and layered SMT \(( \cal{BV} )\) solver for hard industrial verification problems. In CAV, volume 4590 of LNCS, pp. 547-560. Springer (2007)
[20] Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: TACAS, volume 6015 of LNCS, pp. 99-113. Springer (2010) · Zbl 1284.68388
[21] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: International Conference on Theory and Applications of Satisfiability Testing, SAT, volume 7962 of LNCS, July 2013 · Zbl 1390.68572
[22] Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: CAV, pp. 394-409 (2012)
[23] Fazekas, K., Bacchus, F., Biere, A.: Implicit hitting set algorithms for maximum satisfiability modulo theories. In: IJCAR, volume 10900 of Lecture Notes in Computer Science, pp. 134-151. Springer (2018)
[24] Ganesh, V., Dill, D.L:. A decision procedure for bit-vectors and arrays. In: CAV (2007) · Zbl 1135.68472
[25] Hadarean, L.: An Efficient and Trustworthy Theory Solver for Bit-vectors in Satisfiability Modulo Theories. PhD thesis, New York University (2015)
[26] Hadarean, L., Bansal, K., Jovanovic, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: CAV, volume 8559 of Lecture Notes in Computer Science, pp. 680-695. Springer (2014)
[27] Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Proceedings of FMCAD (2012) · Zbl 1317.68110
[28] Kovásznai, G., Biró, C., Erdélyi, B.: Puli-a problem-specific OMT solver. EasyChair Preprint no. 371, EasyChair (2018)
[29] Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: SAT (2014) · Zbl 1423.68457
[30] Li, Y., Albarghouthi, A., Kincad, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL (2014) · Zbl 1284.68410
[31] Manolios, P., Papavasileiou, V.: Ilp modulo theories. In: CAV, pp. 662-677 (2013)
[32] Nadel, A., Ryvchin, V.: Bit-vector optimization. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016, volume 9636 of LNCS. Springer (2016)
[33] Niemetz, A.: Bit-Precise Reasoning Beyond Bit-Blasting. PhD thesis, Informatik, Johannes Kepler University Linz (2017) · Zbl 1377.68134
[34] Niemetz, A., Preiner, M., Fröhlich, A., Biere, A.: Improving local search for bit-vector logics in SMT with path propagation. In: Proceedings of 4th International Working on Design and Implementation of Formal Tools and Systems (DIFTS’15), p. 10 (2015)
[35] Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Proceedings of Theory and Applications of Satisfiability Testing—SAT 2006, volume 4121 of LNCS. Springer (2006) · Zbl 1187.68558
[36] Roc, O.: Optimization Modulo Theories. Master’s thesis, Polytechnic University of Catalonia (2011). http://hdl.handle.net/2099.1/14204
[37] Ruemmer, P., Wahl, T.: An SMT-LIB Theory of Binary Floating-Point Arithmetic. SMT 2010 Workshop, July 2010. http://www.philipp.ruemmer.org/publications/smt-fpa.pdf
[38] Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) Cost Functions. In: IJCAR, volume 7364 of LNAI, pp. 484-498. Springer (2012) · Zbl 1358.68264
[39] Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logics 16(2) (2015) · Zbl 1354.68233
[40] Sebastiani, R., Trentin, P.: OptiMathSAT: A tool for optimization modulo theories. In: Proceedings of International Conference on Computer-Aided Verification, CAV 2015, volume 9206 of LNCS. Springer (2015) · Zbl 1468.68206
[41] Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’15, volume 9035 of LNCS. Springer (2015) · Zbl 1420.68197
[42] Sebastiani, R., Trentin, P.: On optimization modulo theories, MaxSMT and sorting networks. In Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’17, volume 10205 of LNCS. Springer (2017)
[43] Sebastiani, R., Trentin, P.: OptiMathSAT: A tool for optimization modulo theories. J. Autom. Reason. (2018) · Zbl 1468.68206
[44] Trentin, P., Sebastiani, R.: Optimization modulo the theory of floating-point numbers. In: In proceedings of 27th International Conference on Automated Deduction—CADE-27., LNCS, pp. 550-567. Springer (2019) · Zbl 07178998
[45] Zeljić, A.; Backeman, P.; Wintersteiger, CM; Rümmer, P.; Galmiche, D.; Schulz, S.; Sebastiani, R., Exploring approximations for floating-point arithmetic using uppsat, Automated Reasoning, 246-262 (2018), Cham: Springer, Cham · Zbl 06958103
[46] Zeljić, A.; Wintersteiger, CM; Rümmer, P.; Demri, S.; Kapur, D.; Weidenbach, C., Approximations for model construction, Automated Reasoning, 344-359 (2014), Cham: Springer, Cham · Zbl 1409.68264
[47] Zeljić, A.; Wintersteiger, CM; Rümmer, P., An approximation framework for solvers and decision procedures, J. Autom. Reason., 58, 1, 127-147 (2017) · Zbl 1409.68265
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.