Abstract
Reasoning methods based on resolution and DPLL have enjoyed many success stories in real-life applications. One of the challenges is whether we can go beyond and extend this technology to other domains such as arithmetic. In our recent work we introduced two methods for solving systems of linear inequalities called conflict resolution (CR) [6,7] and bound propagation (BP) [3,8] which aim to address this challenge. In particular, conflict resolution can be seen as a refinement of resolution and bound propagation is analogous to DPLL with constraint propagation, backjumping and lemma learning. There are non-trivial issues when considering arithmetic constraints such as termination, dynamic variable ordering and dealing with large coefficients. In this talk I will overview our approach and some related work [1,2,4,5,9]. This is a joint work with Ioan Dragan, Laura Kovács, Nestan Tsiskaridze and Andrei Voronkov.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Mahboubi, A., Mebsout, A., Melquiond, G.: A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 67–81. Springer, Heidelberg (2012)
Cotton, S.: Natural Domain SMT: A Preliminary Assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77–91. Springer, Heidelberg (2010)
Dragan, I., Korovin, K., Kovács, L., Voronkov A.: Bound propagation for arithmetic reasoning in Vampire (submitted, 2013)
Jovanović, D., de Moura, L.: Cutting to the Chase Solving Linear Integer Arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 338–353. Springer, Heidelberg (2011)
Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012)
Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict Resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509–523. Springer, Heidelberg (2009)
Korovin, K., Tsiskaridze, N., Voronkov, A.: Implementing conflict resolution. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 362–376. Springer, Heidelberg (2012)
Korovin, K., Voronkov, A.: Solving Systems of Linear Inequalities by Bound Propagation. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 369–383. Springer, Heidelberg (2011)
McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to Richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korovin, K. (2013). From Resolution and DPLL to Solving Arithmetic Constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-40885-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40884-7
Online ISBN: 978-3-642-40885-4
eBook Packages: Computer ScienceComputer Science (R0)