Satisfiability Checking meets Symbolic Computation (Project Paper)

TL;DR

This paper discusses a project aimed at integrating symbolic computation and satisfiability checking communities to develop shared platforms, foster collaboration, and address common challenges in decision procedures for arithmetic theories.

Contribution

It introduces the SC-square project, which seeks to unify two research communities through collaboration, shared platforms, and a common roadmap for advancing decision procedures.

Findings

Initial activities and aims of the SC-square project are outlined.

Formalization of key challenges for community integration.

Establishment of a foundation for future collaborative research.

Abstract

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-square 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-square community.