This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No H2020-FETOPEN-2015-CSA 712689.
It is the start of the general push to create a real SC2 community. More details can be found on the SC2 announcement poster, which is popular on ResearchGate.
Objectives
The overall aim of this project is to create a new research community bridging the gap between Satisfiability Checking and Symbolic Computation, whose members will ultimately be well informed about both fields, and thus able to combine the knowledge and techniques of both fields to develop new research and to resolve problems (both academic and industrial) currently beyond the scope of either individual field.
- O1) Build a joint SC2 community:
Build a community of researchers interested in developing technologies at the boundary of the
traditionally separate areas of Satisfiability Checking and Symbolic Computation.
- O1.1) Create communication platforms:
Create platforms for scientific exchange, discussion and cooperation within and between the currently disjoint communities.
- O1.2) Initiate cooperations:
Support the initiation and the fostering of cooperations within and across the communities of
Satisfiability Checking and Symbolic Computation.
- O1.3) Strengthen research and technology transfer to industry:
Identify obstacles and enabling conditions for the application of SC2 software tools (SMT solvers and computer algebra systems) in industry, and support the initiation of collaborations between academia and industry.
- O1.4) Support scientific offspring:
Increase the involvement and support of young researchers and minorities, especially women, in the SC2 network.
- O2) Create a research roadmap:
Create a research roadmap of potentials and challenges, both to the two traditional silos of Satisfiability Checking and Symbolic Computation, but also challenges that only the new joined SC2 community can address.
- O2.1) Common research roadmap:
Identify in detail, the research challenges that cross community boundaries, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O2.2) Research roadmap for Satisfiability Checking:
Identify in detail, the research challenges for the Satisfiability Checking community: Identify established techniques in Symbolic Computation which are promising candidates to adapt and integrate to tackle problems arising in Satisfiability Checking, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O2.3) Research roadmap for Symbolic Computation:
Identify in detail, the research challenges for the Symbolic Computation community: Identify successful techniques in Satisfiability Checking and generalise them to become applicable also in the area of Symbolic Computation, and where appropriate construct prototype proof-of-concept implementations (sufficient for handling modest, but non-trivial examples).
- O3) Initiate SC2 standards:
Create standards and benchmark libraries such that the SC2 community can share challenges and measure its progress.
- O3.1) Propose input language standards:
Develop appropriate standards for the input language of SC2 tools, such that a problem specified in the standard input language can be input to several tools.
- O3.2) Create an SC2 benchmark library:
Create and disseminate a library of SC2 benchmarks in the standard input language, focussing on(linear and non-linear real and integer) arithmetic theories.
- O4) Increase the visibility of SC2:
Disseminate research topics and results to other related research areas and to the public, with a special focus on young researchers and aiming at gender and geographic balance (e.g., addressing eastern Europe, surprisingly not so active in these areas).
Consortium
