SC-square - Satisfiability Checking and Symbolic Computation: uniting two communities to solve real problems

Project: EU Commission

Project Details


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

Though both communities have made remarkable progress in the last decades, they still need to be strengthened to tackle practical problems of rapidly increasing size and complexity. Their separate tools (computer algebra systems and SMT solvers) are urgently needed to examine prevailing problems with a direct effect to 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 enables dealing with large mathematical problems out of reach of pencil and paper developments.

Currently the two communities are largely disjoint and unaware of the achievements of each other, despite strong reasons for them to discuss and collaborate, as they share many central interests. However, 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 roadmaps are necessary to initiate an exchange, and to support and to 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, offer global events and bilateral visits, propose standards, and so on.

We believe that these activities will initiate cross-fertilisation of both fields and bring mutual improvements. Combining the knowledge, experience and the technologies in these communities will enable the development of radically improved software tools.
Effective start/end date1/07/1631/08/18


  • EU - Horizon 2020


Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.
  • The Role of Benchmarking in Symbolic Computation: (Position Paper)

    Davenport, J., 2018, Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018. IEEE

    Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

    Open Access
    81 Downloads (Pure)
  • A case study on the parametric occurrence of multiple steady states

    Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., Hoyt, C., Košta, M., Radulescu, O., Sturm, T. & Weber, A., 23 Jul 2017, ISSAC 2017 - Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation: Part F129312. Association for Computing Machinery, p. 45-52 8 p.

    Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

    23 Citations (SciVal)
  • The potential and challenges of CAD with equational constraints for SC-square

    Davenport, J. H. & England, M., 2017, Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings. Germany: Springer Verlag, p. 280-285 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10693 ).

    Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

    2 Citations (SciVal)