Satisfiability Checking and Symbolic Computation

Bridging Two Communities to Solve Real Problems

The use of advanced methods to solve practical and industrially relevant problems by computers has a long history. Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; and more recent developments in the area of Satisfiability Checking are starting to tackle similar problems but with different algorithmic and technological solutions.

Though both communities have made remarkable progress in the last decades, they need to be further strengthened to tackle practical problems of ever increasing size and complexity. Their separate tools (computer algebra systems and SMT solvers) are urgently needed to address prevailing problems having a direct effect on our society. For example, Satisfiability Checking is an essential backend for assuring the security and the safety of computer systems. In various scientific areas, Symbolic Computation is able to deal with large mathematical problems far beyond the scope of pencil and paper solutions.

Currently the two communities are largely disjoint and unaware of the achievements of one another, despite there being strong reasons for them to discuss and collaborate, since they share many central interests. However, up to now, researchers from these two communities rarely interact, and also their tools lack common, mutual interfaces for unifying their strengths. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. These are the main objectives of this CSA. We will initiate a wide range of activities to bring the two communities together, identify common challenges, propose joint standards, offer global events and bilateral visits, and so on. Besides the partners in our EU Project, these people have expressed an interest in these activities.

We believe that these activities will initiate cross-fertilization of both fields and bring mutual benefits. Combining the knowledge, experience and the technologies in these communities will enable the development of radically improved software tools.

On February 28th, 2016, the European Commission anounced an intention to fund our first project: the SC-square CSA, which started on 1 July 2016 and ended on 31 August 2018.