Top

Published in:

2021 | OriginalPaper | Chapter

Optimization Modulo Non-linear Arithmetic via Incremental Linearization

Authors : Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonáš, Marco Roveri, Roberto Sebastiani, Patrick Trentin

Published in: Frontiers of Combining Systems

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems on the theories of non-linear arithmetic over the reals and the integers. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions. In this paper, we show how incremental linearization can be extended to OMT in a simple way, producing an incomplete though effective OMT procedure. We describe the main ideas and algorithms, we provide an implementation within the OptiMathSAT OMT solver, and perform an empirical evaluation. The results support the effectiveness of the approach.

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

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

previous chapter Vampire with a Brain Is a Good ITP Hammer

next chapter Quantifier Simplification by Unification in SMT

In the following, we only consider quantifier-free theories, and we abuse the accepted notation and omit the “QF_” prefix in the names of the theories.

https://github.com/Z3Prover/z3/issues/2247

https://github.com/Z3Prover/z3/issues/5339.

More generally the formula can be built on a combination of \(\mathcal {T}\) with other theories, see e.g. [35]. However, to simplify the narration and the notation, here we refer to one single theory.

As in [13] and with no loss of generality, hereafter we assume that all multiplications in \(\varphi \) are either between two variables or between one constant and one variable, because more complex terms occurring in a multiplication can be renamed by fresh variables. Notice that this assumption is not necessary in practice, but it simplifies the explanation.

In order to keep the narration simple, in Fig. 1 we have omitted some details. First, the input formula can be simplified by some preprocessing steps. Furthermore, for each fresh \(f_{*}(x, y) \) term, \(\hat{\varphi } \) can be extended from the beginning with simple multiplication lemmas. We refer the reader to [13] for details.

The same considerations as in Footnote 5 apply here as well.

We stress the fact that SMT-Check-Refine returning false does not mean that \(\hat{\varphi } \wedge \bigwedge \varTheta \) is \(\text {NIRA}\)-unsatisfiable, rather that it failed to prove it satisfiable.

For the sake of simplicity, here we do not take into consideration the special termination condition based on a finite budget described in [13].

This option has the effect of enabling the legacy arithmetic solver. Without this option, Z3 produced a significant number of incorrect results.

The modified version of OMTPlan, together with the planning domain and problems used to generate this benchmark set, is available at [2].

Here we describe the case for minimization; the case for maximization is dual.

nl_counters_simple/fn-counters-simp__instance_2_75.smt2.

https://es-static.fbk.eu/people/mjonas/papers/frocos21_oms/

https://github.com/roveri-marco/OMTNPlan

Ábrahám, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119, 100633 (2021)MathSciNetCrossRef

Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2010). http://www.smtlib.org

Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories, chapter 26, pp. 825–885. Volume 185 of Biere et al. [7], February 2009

Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Volume 2 of Foundations of Artificial Intelligence, pp. 571–603. Elsevier (2006)

Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, February 2009

Bjørner, N., Phan, A.-D., Fleckenstein, L.: \(\nu \)Z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_14CrossRef

Borralleras, C., Larraz, D., Rodríguez-Carbonell, E., Oliveras, A., Rubio, A.: Incomplete SMT techniques for solving non-linear formulas over the integers. ACM Trans. Comput. Log. 20(4), 25:1–25:36 (2019)

10.

Borralleras, C., Lucas, S., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reason. 48(1), 107–131 (2012). https://doi.org/10.1007/s10817-010-9196-8MathSciNetCrossRefMATH

11.

Brauße, F., Korovin, K., Korovina, M., Müller, N.: A CDCL-style calculus for solving non-linear constraints. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 131–148. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29007-8_8CrossRef

12.

Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383–398. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_23CrossRefMATH

13.

Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1–19:52 (2018)

14.

Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7CrossRefMATH

15.

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition-preliminary report. ACM SIGSAM Bull. 8(3), 80–90 (1974)CrossRef

16.

Contaldo, F., Trentin, P., Sebastiani, R.: From MiniZinc to optimization modulo theories, and back. In: Hebrard, E., Musliu, N. (eds.) CPAIOR 2020. LNCS, vol. 12296, pp. 148–166. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58942-4_10CrossRef

17.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

18.

Dixon, C., Finger, M. (eds.): FroCoS 2017. LNCS (LNAI), vol. 10483. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4CrossRef

19.

Fontaine, P., Ogawa, M., Sturm, T., Vu, X.: Subtropical satisfiability. In: Dixon and Finger [18], pp. 189–206

20.

Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72788-0_33CrossRefMATH

21.

Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14CrossRef

22.

Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330–346. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_18CrossRef

23.

Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3/4), 104–105 (2012)CrossRef

24.

Kong, S., Solar-Lezama, A., Gao, S.: Delta-decision procedures for exists-forall problems over the reals. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 219–235. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_15CrossRef

25.

Kremer, G., Ábrahám, E.: Fully incremental cylindrical algebraic decomposition. J. Symb. Comput. 100, 11–37 (2020)MathSciNetCrossRef

26.

Kremer, G., Corzilius, F., Ábrahám, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315–335. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45641-6_21CrossRefMATH

27.

Leofante, F., Giunchiglia, E., Ábrahám, E., Tacchella, A.: Optimal planning modulo theories. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pp. 4128–4134. ijcai.org (2020)

28.

Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 166–184. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_8CrossRef

29.

Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers, chapter 4, pp. 131–153. Volume 185 of Biere et al. [7], February 2009

30.

Matiyasevich, Y.V.: Hilbert’s Tenth Problem. Foundations of Computing, MIT Press, Cambridge (1993)MATH

31.

Nadel, A., Ryvchin, V.: Bit-vector optimization. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 851–867. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_53CrossRef

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). https://doi.org/10.1007/11814948_18CrossRefMATH

33.

Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C.W.: Designing theory solvers with extensions. In: Dixon and Finger [33], pp. 22–40

34.

Sebastiani, R., Tomasi, S.: Optimization in SMT with \({\cal{L}A}\)(\({\mathbb{Q}}\)) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 484–498. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_38CrossRef

35.

Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 1–46 (2015)MathSciNetCrossRef

36.

Sebastiani, R., Trentin, P.: Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 335–349. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_27CrossRefMATH

37.

Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. J. Autom. Reason. 64, 423–460 (2020). https://doi.org/10.1007/s10817-018-09508-6MathSciNetCrossRefMATH

38.

Stump, A., Barrett, C.W., Dill, D.L.: CVC: a cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500–504. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_40CrossRef

39.

Trentin, P., Sebastiani, R.: Optimization modulo the theory of floating-point numbers. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 550–567. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_33CrossRef

40.

Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997). https://doi.org/10.1007/s002000050055MathSciNetCrossRefMATH

41.

Zankl, H., Middeldorp, A.: Satisfiability of non-linear (Ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 481–500. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_27CrossRef

Title: Optimization Modulo Non-linear Arithmetic via Incremental Linearization
Authors: Filippo Bigarella
Alessandro Cimatti
Alberto Griggio
Ahmed Irfan
Martin Jonáš
Marco Roveri
Roberto Sebastiani
Patrick Trentin
Publisher: Springer International Publishing
Book: Frontiers of Combining Systems
Print ISBN: 978-3-030-86204-6

Electronic ISBN: 978-3-030-86205-3

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-86205-3_12

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner