Following the success of the first two SC2 workshops, and with the encouragement of the Editor-in-Chief, we are soliciting papers for a special issue of the Journal of Symbolic Computation on the theme of Satisfiability Checking and Symbolic Computation.
Submission is via EasyChair and the closing date for submissions is 31st March 2018. Papers should be prepared using the author information pack. There is no hard page limit: papers should be complete but not unnecessarily long.
Issue Scope
The field of Symbolic Computation, and its implementation in Computer Algebra Systems, is concerned with the algorithmic determination of exact solutions to mathematical problems. More recent developments in the field of Satisfiability Checking are starting to tackle similar problems, through the use of Satisfiability Modulo Theory (SMT) solvers which exploit technology built for the Boolean SAT problem to other domains. The two communities now share many central interests, but until recently there has been little interaction between them. Further, the lack of common or compatible interfaces is an obstacle to the fruitful combination of tools. Bridges between the communities in the form of common platforms and road-maps are needed to initiate exchange and support interaction. The aim of this special issue, along with the SC-square H2020 FETOPEN Coordination and Support Activity project, is to document progress, and share knowledge and experience across both communities.
The issue is open for submission and participation to everyone interested in the topics, whether they are members or associates of the SC-square project or not, and whether or not the contribution was discussed at the SC-square workshops.
We welcome extended versions of previously published workshop or conference papers, but would expect significant new material (this is hard to quantify, but "at least 25%" would be a good guideline).
The topics of interest include but are not limited to:
- Decision procedures and their embedding into SMT solvers and computer algebra systems
- Satisfiability Checking for Symbolic Computation
- Symbolic Computation for Satisfiability Checking
- Applications relying on both Symbolic Computation and Satisfiability Checking
- Combination of Symbolic Computation and Satisfiability Checking tools
- Theory and implementation of quantifier elimination techniques
The First International Workshop on Satisfiability Checking and Symbolic Computation was held on 24th September 2016 in Timisoara, Romania. It was affiliated to the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2016. The proceedings are at CEUR-WS volume 1804.
The Second International Workshop on Satisfiability Checking and Symbolic Computation was held on 29th July 2017 in Kaiserslautern, Germany. It was affiliated to the 42nd International Symposium on Symbolic and Algebraic Computation, ISSAC 2017. The proceedings will shortly appear in a CEUR-WS volume.
Editors
- James Davenport - University of Bath, UK
- Matthew England - Coventry University, UK
- Alberto Griggio - Fondazione Bruno Kessler (FBK), Italy
- Thomas Sturm - CNRS, France, and MPI Informatics, Germany
- Cesare Tinelli - The University of Iowa, USA
Click here for the plain text version of this call.