Satisfiability checking and symbolic computation

DOI10.1145/3055282.3055285zbMATH Open1365.68478DBLPjournals/cca/AbrahamA0BBBCDE16arXiv1607.06945OpenAlexW3123916761WikidataQ59590563 ScholiaQ59590563MaRDI QIDQ5268815FDOQ5268815

Bernd Becker, James H. Davenport, Stephen Forrest, Alessandro Cimatti, Alberto Griggio, Matthew England, Bruno Buchberger, Anna M. Bigatti, Erika Ábrahám, Werner M. Seiler, John Abbott, Martin Brain, Thomas Sturm, Daniel Kroening, Pascal Fontaine

Publication date: 21 June 2017

Published in: ACM Communications in Computer Algebra (Search for Journal in Brave)

Abstract: Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities.

Full work available at URL: https://arxiv.org/abs/1607.06945

Recommendations

• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Editorial: Symbolic computation and satisfiability checking
• Building bridges between symbolic computation and satisfiability checking
• Satisfiability checking: theory and applications
• Satisfiability modulo theories: an appetizer

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Symbolic computation and algebraic computation (68W30)

Cites Work

• Real World Verification
• Building bridges between symbolic computation and satisfiability checking
• $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation

Cited In (6)

• Symbolic techniques in satisfiability solving
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• Testing satisfiability
• Title not available (Why is that?)

This page was built for publication: Satisfiability checking and symbolic computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5268815)