×

zbMATH — the first resource for mathematics

Editorial: Symbolic computation and satisfiability checking. (English) Zbl 1444.68006
Summary: The two communities of Symbolic Computation and Satisfiability Checking have recently found themselves tackling similar problems and having a growing interest in each other’s technology. This special issue presents articles whose contribution is of interest to, and is influenced by, both communities. Given the context of this journal we start this editorial with a more thorough overview of Satisfiability Checking, and then turn to Symbolic Computation and the potentials and challenges for collaboration. The collection of articles in this issue is evidence of the already existing fruitful work at the intersection of these communities.

MSC:
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W30 Symbolic computation and algebraic computation
00B15 Collections of articles of miscellaneous specific interest
Software:
Lynx; Maple; QEPCAD; SMT-LIB; UCLID
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ábrahám, E., Building bridges between symbolic computation and satisfiability checking, (Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15 (2015), ACM), 1-6 · Zbl 1345.68279
[2] Ábrahám, E.; Abbott, J.; Becker, B.; Bigatti, A.; Brain, M.; Buchberger, B.; Cimatti, A.; Davenport, J.; England, M.; Fontaine, P.; Forrest, S.; Griggio, A.; Kroening, D.; Seiler, W.; Sturm, T., \( \mathsf{SC}^2\): Satisfiability checking meets symbolic computation, (Kohlhase, M.; Johansson, M.; Miller, B.; de Moura, L.; Tompa, F., Intelligent Computer Mathematics: Proceedings. Intelligent Computer Mathematics: Proceedings, CICM 2016. Intelligent Computer Mathematics: Proceedings. Intelligent Computer Mathematics: Proceedings, CICM 2016, Lecture Notes in Computer Science, vol. 9791 (2016), Springer International Publishing), 28-43 · Zbl 1344.68198
[3] (Ábrahám, E.; Fontaine, P., Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2016. Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2016, CEUR Workshop Proceedings, vol. 1804 (2016), Springer)
[4] Barrett, C.; Fontaine, P.; Tinelli, C., The Satisfiability Modulo Theories Library (SMT-LIB) (2016), Online Resource
[5] Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C., Satisfiability modulo theories, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOP Press), 825-885, Chapter 26
[6] Biere, A.; Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., (Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185 (2009), IOS Press: IOS Press Amsterdam, The Netherlands) · Zbl 1183.68568
[7] (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2018. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2018, CEUR Workshop Proceedings, vol. 2189 (2018), Springer)
[8] Brown, C., Open non-uniform cylindrical algebraic decompositions, (Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15 (2015), ACM), 85-92 · Zbl 1346.68273
[9] Brown, C., Bridging two communities to solve real problems, (18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’16 (2016), IEEE), 11-14
[10] Buchberger, B., Ein algorithmus zum auffinden der basiselemente des restklassenrings nach einem nulldimensionalen polynomideal. (An algorithm for finding the basis elements of the residue class ring of a zerodimensional polynomial ideal) (1965), Mathematical Institute, University of Innsbruck, See Buchberger (2006) for an English translation · Zbl 1245.13020
[11] Buchberger, B., Symbolic computation (an editorial), J. Symb. Comput., 1, 1, 1-6 (1985)
[12] Buchberger, B., Bruno Buchberger’s PhD thesis (1965): An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, J. Symb. Comput., 41, 3-4, 475-511 (2006) · Zbl 1158.01307
[13] Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation (1998), Springer-Verlag
[14] Collins, G., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages (1975), Springer-Verlag), 134-183, (Reprinted in the collection Caviness and Johnson, 1998)
[15] Collins, G.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 299-328 (1991) · Zbl 0754.68063
[16] Cook, S. A., The complexity of theorem-proving procedures, (Proceedings of the Third Annual ACM Symposium on Theory of Computing. Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71 (1971), ACM: ACM New York, NY, USA), 151-158
[17] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002
[18] de Moura, L.; Jovanović, D., A model-constructing satisfiability calculus, (Giacobazzi, R.; Berdine, J.; Mastroeni, I., Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation, Proc. VMCAI 2013 (2013), Springer: Springer Berlin, Heidelberg), 1-12 · Zbl 1426.68251
[19] (England, M.; Ganesh, V., Proceedings of the 2nd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 2nd Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2017. Proceedings of the 2nd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 2nd Workshop on Satisfiability Checking and Symbolic Computation, SC^2 2017, CEUR Workshop Proceedings, vol. 1974 (2017), Springer)
[20] Forrest, S., Integration of smt-lib support into Maple, (England, M.; Ganesh, V., Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, \( \mathsf{SC}^2 2017\). Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, \( \mathsf{SC}^2 2017\), CEUR Workshop Proceedings, vol. 1974 (2017)), 6
[21] Ganesh, V.; O’Donnell, C. W.; Soos, M.; Devadas, S.; Rinard, M. C.; Solar-Lezama, A., Lynx: a programmatic sat solver for the rna-folding problem, (Cimatti, A.; Sebastiani, R., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2012 (2012), Springer: Springer Berlin, Heidelberg), 143-156
[22] Huang, Z.; England, M.; Davenport, J.; Paulson, L., Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases, (18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’16 (2016), IEEE), 45-52
[23] Jovanovic, D.; de Moura, L., Solving non-linear arithmetic, (Gramlich, B.; Miller, D.; Sattler, U., Automated Reasoning: 6th International Joint Conference. Automated Reasoning: 6th International Joint Conference, IJCAR. Automated Reasoning: 6th International Joint Conference. Automated Reasoning: 6th International Joint Conference, IJCAR, Lecture Notes in Computer Science, vol. 7364 (2012), Springer), 339-354 · Zbl 1358.68257
[24] Kosta, M., New Concepts for Real Quantifier Elimination by Virtual Substitution (2016), Saarland University, Available at:
[25] Kroening, D.; Strichman, O., Decision Procedures: An Algorithmic Point of View (2013), Springer: Springer New York
[26] Lahiri, S. K.; Seshia, S. A., The UCLID decision procedure, (Alur, R.; Peled, D. A., Computer Aided Verification, 16th International Conference, Proceedings. Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, Boston, MA, USA, July 13-17, 2004. Computer Aided Verification, 16th International Conference, Proceedings. Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, Boston, MA, USA, July 13-17, 2004, Lecture Notes in Computer Science, vol. 3114 (2004), Springer), 475-478 · Zbl 1103.68628
[27] Marques-Silva, J.; Sakallah, K., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388
[28] Mulligan, C.; Bradford, R.; Davenport, J.; England, M.; Tonks, Z., Non-linear real arithmetic benchmarks derived from automated reasoning in economics, (Bigatti, A.; Brain, M., Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, \( \mathsf{SC}^2 2018\). Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation. Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation, \( \mathsf{SC}^2 2018\), CEUR Workshop Proceedings, vol. 2189 (2018)), 48-60
[29] Risch, R., The problem of integration in finite terms, Trans. Am. Math. Soc., 139, 167-189 (1969) · Zbl 0184.06702
[30] Sturm, T., A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications, Math. Comput. Sci., 11, 3, 483-502 (2017) · Zbl 1425.68380
[31] Tarski, A., A Decision Method For Elementary Algebra And Geometry (1948), RAND Corporation: RAND Corporation Santa Monica, CA, See Tarski (1998) for a readily available reprint · Zbl 0044.25102
[32] Tarski, A., A decision method for elementary algebra and geometry, (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation (1998), Springer-Verlag), 24-84 · Zbl 0900.03045
[33] Tseitin, G., On the complexity of derivation in propositional calculus, (Siekmann, J.; Wrightson, G., Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970 (1983), Springer: Springer Berlin, Heidelberg), 466-483
[34] 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
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.