Abstract
Solving constraint optimization problems is widely applicable in computer science. The computer algebra system Mathematica provides MaxValue, MinValue and other functions to solve constraint optimization problems. However many cases of constraint optimization problems cannot be solved by these functions directly. In this paper, based on these Mathematica functions and abstraction, a practical approach is presented for computing the upper bounds and the lower bounds of the optimization values of constraint optimization problems. The optimization values of many constraint optimization problems, which cannot be solved by Mathematica functions directly, can be computed automatically by using the approach presented in this paper. The experimental results demonstrate the practicality of this approach.
This work was supported by the National Natural Science Foundation of China (Grant No. 61672525).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Manolios, P., Papavasileiou, V.: ILP modulo theories. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 662–677. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_44
Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J. (ed.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30885-7_13
Su, W., Abrial, J.-R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program 94, 164–202 (2014)
Abrial, J.-R: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, United Kingdom (2010)
Rugina, R., Rinard, M.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementations, pp. 182–195. ACM, NewYork (2000)
Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on Expression Abstraction and Max Operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 370–384. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_35
Granvilliers, L., Benhamou, F.: Algorithm 852: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32(1), 138–156 (2006)
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_14
Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 607–618. ACM, NewYork (2014)
Li, M.: A practical loop invariant generation approach based on random testing, constraint solving and verification. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 447–461. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34281-3_31
Li, M.: Automatic proving or disproving equality loop invariants based on finite difference techniques. Inf. Process. Lett. 115(4), 468–474 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Pan, G., Li, M., Ou, G. (2020). Solving Constraint Optimization Problems Based on Mathematica and Abstraction. In: Miao, H., Tian, C., Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2019. Lecture Notes in Computer Science(), vol 12028. Springer, Cham. https://doi.org/10.1007/978-3-030-41418-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-41418-4_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41417-7
Online ISBN: 978-3-030-41418-4
eBook Packages: Computer ScienceComputer Science (R0)