×

SC\(^2\): satisfiability checking meets symbolic computation. (Project paper). (English) Zbl 1344.68198

Kohlhase, Michael (ed.) et al., Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25–29, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-42546-7/pbk; 978-3-319-42547-4/ebook). Lecture Notes in Computer Science 9791. Lecture Notes in Artificial Intelligence, 28-43 (2016).
Summary: 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 SC\(^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 SC\(^2\) community.
For the entire collection see [Zbl 1342.68025].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abbott, J., Bigatti, A.M., Lagorio, G.: CoCoA-5: a system for doing computations in commutative algebra. http://cocoa.dima.unige.it
[2] Ábrahám, E.: Building bridges between symbolic computation and satisfiability checking. In: Proceedings ISSAC 2015, pp. 1–6. ACM (2015) · Zbl 1345.68279
[3] Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings ISSAC 2014, pp. 1–8. ACM (2014) · Zbl 1325.68212 · doi:10.1145/2608628.2627488
[4] 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) · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[5] 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
[6] 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)
[7] Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2010). www.SMT-LIB.org
[8] 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) · Zbl 1183.68568
[9] Bixby, R.E.: Computational progress in linear and mixed integer programming. In: Presentation at ICIAM 2015 (2015)
[10] 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) · Zbl 1358.68249 · doi:10.1007/978-3-642-31365-3_8
[11] 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) · Zbl 1250.68184 · doi:10.1007/978-3-642-02959-2_23
[12] 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 · Zbl 0898.68039 · doi:10.1006/jsco.1996.0125
[13] 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) · Zbl 05587935 · doi:10.1007/978-3-642-02959-2_12
[14] 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) · Zbl 1350.68293 · doi:10.1007/978-3-319-10515-4_4
[15] Bradford, R., Davenport, J., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symbol. Comput. 76, 1–35 (2016) · Zbl 1351.68314 · doi:10.1016/j.jsc.2015.11.002
[16] 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) · Zbl 1432.68596 · doi:10.1007/978-3-319-21401-6_42
[17] Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003) · Zbl 1083.68148 · doi:10.1145/968708.968710
[18] Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings ISSAC 2007, pp. 54–60. ACM (2007) · Zbl 1190.68028 · doi:10.1145/1277548.1277557
[19] 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) · Zbl 05702237 · doi:10.1007/978-3-642-12002-2_12
[20] 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) · Zbl 1158.01307 · doi:10.1016/j.jsc.2005.09.007
[21] 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) · Zbl 1237.14068 · doi:10.1145/1576702.1576718
[22] 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) · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[23] 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)
[24] Collins, G.E.: The SAC-1 system: an introduction and survey. In: Proceedings SYMSAC 1971, pp. 144–152. ACM (1971) · doi:10.1145/800204.806279
[25] 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) · doi:10.1007/3-540-07407-4_17
[26] 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) · doi:10.1109/SYNASC.2013.29
[27] 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 · doi:10.1145/800157.805047
[28] 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) · Zbl 1471.68241 · doi:10.1007/978-3-319-24318-4_26
[29] Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symbol. Comput. 5, 29–35 (1988) · Zbl 0663.03015 · doi:10.1016/S0747-7171(88)80004-X
[30] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[31] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[32] 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
[33] Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997) · doi:10.1145/261320.261324
[34] 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) · Zbl 05187406 · doi:10.1007/11817963_11
[35] 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) · Zbl 1325.68276 · doi:10.1145/2608628.2608654
[36] 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) · Zbl 1144.68371
[37] Grayson, D.R., Stillman, M.E.: Macaulay2, a software system for research in algebraic geometry. http://www.math.uiuc.edu/Macaulay2/
[38] Hearn, A.C.: REDUCE: The first forty years. In: Proceedings A3L, pp. 19–24. Books on Demand GmbH (2005)
[39] Jenks, R.D., Sutor, R.S.: AXIOM: The Scientific Computation System. Springer, New York (1992) · Zbl 0758.68010
[40] 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) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27
[41] Kahrimanian, H.G.: Analytic differentiation by a digital computer. Master’s thesis, Temple University Philadelphia (1953)
[42] Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, New York (2008) · Zbl 1149.68071
[43] Maple. http://www.maplesoft.com/
[44] Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506–521 (1999) · Zbl 01935259 · doi:10.1109/12.769433
[45] Martin, W.A., Fateman, R.J.: The Macsyma system. In: Proceedings SYMSAC 1971, pp. 59–75. ACM (1971) · doi:10.1145/800204.806267
[46] Moses, J.: Symbolic integration. Ph.D. thesis, MIT & MAC TR-47 (1967) · Zbl 0228.68009
[47] 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) · Zbl 1383.68084 · doi:10.1007/978-3-642-36675-8_2
[48] 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) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[49] Nelson, G., Oppen, D.C.: Simplifications by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[50] Nolan, J.: Analytic differentiation on a digital computer. Master’s thesis, MIT (1953)
[51] 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) · Zbl 1250.68197 · doi:10.1007/978-3-642-02959-2_35
[52] Risch, R.H.: The problem of integration in finite terms. Trans. Am. Math. Soc. 139, 167–189 (1969) · Zbl 0184.06702 · doi:10.1090/S0002-9947-1969-0237477-8
[53] 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)
[54] Slagle, J.: A heuristic program that solves symbolic integration problems in freshman calculus. Ph.D. thesis, Harvard University (1961) · Zbl 0113.32801
[55] Strzeboński, A.: Solving polynomial systems over semialgebraic sets represented by cylindrical algebraic formulas. In: Proceedings ISSAC 2012, pp. 335–342. ACM (2012) · Zbl 1308.68191 · doi:10.1145/2442829.2442877
[56] Weispfenning, V.: Comprehensive Gröbner bases. J. Symbol. Comput. 14(1), 1–29 (1992) · Zbl 0784.13013 · doi:10.1016/0747-7171(92)90023-W
[57] Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997) · Zbl 0867.03003 · doi:10.1007/s002000050055
[58] Wolfram Research, Inc.: Mathematica, version 10.4. Wolfram Research, Inc., Champaign, Illinois (2016)
[59] 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) · Zbl 1310.68126 · doi:10.1007/978-3-642-17511-4_27
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.