Abstract
Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted \(\mathsf {SC}^\mathsf{2} \) project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified \(\mathsf {SC}^\mathsf{2} \) community.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
It is usual in the SMT community to refer to these constraints as arithmetic. But, as they involve quantities as yet unknown, manipulating them is algebra. Hence both words occur, with essentially the same meaning, throughout this document.
- 2.
- 3.
Email contact: J.H.Davenport@bath.ac.uk.
References
Abbott, J., Bigatti, A.M., Lagorio, G.: CoCoA-5: a system for doing computations in commutative algebra. http://cocoa.dima.unige.it
Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Proceedings ISSAC 2015, pp. 1–6. ACM (2015)
Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings ISSAC 2014, pp. 1–8. ACM (2014)
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: \(\mathtt CVC4\). In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)
Barrett, C., Kroening, D., Melham, T.: Problem solving for the 21st century: efficient solvers for satisfiability modulo theories. Technical report 3, London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering, Knowledge Transfer Report (2014). http://www.cs.nyu.edu/~barrett/pubs/BKM14.pdf
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Chap. 26, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2010). www.SMT-LIB.org
Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Bixby, R.E.: Computational progress in linear and mixed integer programming. In: Presentation at ICIAM 2015 (2015)
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)
Borralleras, C., Lucas, S., Navarro-Marset, R., Rodríguez-Carbonell, E., Rubio, A.: Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 294–305. Springer, Heidelberg (2009)
Bosma, W., Cannon, J., Playoust, C.: The MAGMA algebra system I: the user language. J. Symbolic Comput. 24(3–4), 235–265 (1997). Computational Algebra and Number Theory (London, 1993). http://dx.doi.org/10.1006/jsco.1996.0125
Bouton, T., Caminha, D., de Oliveira, B., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009)
Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2014. LNCS, vol. 8660, pp. 44–58. Springer, Heidelberg (2014)
Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symbol. Comput. 76, 1–35 (2016)
Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 623–637. Springer International Publishing, Switzerland (2015)
Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003)
Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings ISSAC 2007, pp. 54–60. ACM (2007)
Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT2 solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)
Buchberger, B.: Ein Algorithmus zum Auffinden des basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck (1965). English translation: J. Symbolic Computation 41, 475–511 (2006)
Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings ISSAC 2009, pp. 95–102. ACM (2009)
Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)
Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. In: Proceedings SMT 2013. EPiC Series, vol. 20, pp. 88–97. EasyChair (2013)
Collins, G.E.: The SAC-1 system: an introduction and survey. In: Proceedings SYMSAC 1971, pp. 144–152. ACM (1971)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Conchon, S., Iguernelala, M., Mebsout, A.: A collaborative framework for non-linear integer arithmetic reasoning in Alt-Ergo. In: Proceedings SYNASC 2013, pp. 161–168. IEEE (2013)
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings STOC 1971, pp. 151–158. ACM (1971). http://doi.acm.org/10.1145/800157.805047
Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: An open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Switzerland (2015)
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbol. Comput. 5, 29–35 (1988)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Decker, W., Greuel, G.M., Pfister, G., Schönemann, H.: Singular 4-0-2 – A computer algebra system for polynomial computations (2015). http://www.singular.uni-kl.de
Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Eraşcu, M., Hong, H.: Synthesis of optimal numerical algorithms using real quantifier elimination (Case study: Square root computation). In: Proceedings ISSAC 2014, pp. 162–169. ACM (2014)
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiability Boolean Model. Comput. 1(3–4), 209–236 (2007)
Grayson, D.R., Stillman, M.E.: Macaulay2, a software system for research in algebraic geometry. http://www.math.uiuc.edu/Macaulay2/
Hearn, A.C.: REDUCE: The first forty years. In: Proceedings A3L, pp. 19–24. Books on Demand GmbH (2005)
Jenks, R.D., Sutor, R.S.: AXIOM: The Scientific Computation System. Springer, New York (1992)
Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS(LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012)
Kahrimanian, H.G.: Analytic differentiation by a digital computer. Master’s thesis, Temple University Philadelphia (1953)
Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, New York (2008)
Maple. http://www.maplesoft.com/
Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506–521 (1999)
Martin, W.A., Fateman, R.J.: The Macsyma system. In: Proceedings SYMSAC 1971, pp. 59–75. ACM (1971)
Moses, J.: Symbolic integration. Ph.D. thesis, MIT & MAC TR-47 (1967)
de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15–44. Springer, Heidelberg (2013)
de Moura, L.M., 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)
Nelson, G., Oppen, D.C.: Simplifications by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Nolan, J.: Analytic differentiation on a digital computer. Master’s thesis, MIT (1953)
Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 485–501. Springer, Heidelberg (2009)
Risch, R.H.: The problem of integration in finite terms. Trans. Am. Math. Soc. 139, 167–189 (1969)
Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. In: Proceedings MBMV 2013, pp. 231–241. Institut für Angewandte Mikroelektronik und Datentechnik, Fakultät für Informatik und Elektrotechnik, Universität Rostock (2013)
Slagle, J.: A heuristic program that solves symbolic integration problems in freshman calculus. Ph.D. thesis, Harvard University (1961)
Strzeboński, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings ISSAC 2012, pp. 335–342. ACM (2012)
Weispfenning, V.: Comprehensive Gröbner bases. J. Symbol. Comput. 14(1), 1–29 (1992)
Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997)
Wolfram Research, Inc.: Mathematica, version 10.4. Wolfram Research, Inc., Champaign, Illinois (2016)
Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010)
Acknowledgements
We thank the anonymous reviewers for their comments. We are grateful for support by the H2020-FETOPEN-2016-2017-CSA project \(\mathsf {SC}^\mathsf{2} \) (712689) and the ANR project ANR-13-IS02-0001-01 SMArT. Earlier work in this area was also supported by the EPSRC grant EP/J003247/1.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ábrahám, E. et al. (2016). \(\mathsf {SC}^\mathsf{2} \): Satisfiability Checking Meets Symbolic Computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds) Intelligent Computer Mathematics. CICM 2016. Lecture Notes in Computer Science(), vol 9791. Springer, Cham. https://doi.org/10.1007/978-3-319-42547-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-42547-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42546-7
Online ISBN: 978-3-319-42547-4
eBook Packages: Computer ScienceComputer Science (R0)