Satisfiability checking and symbolic computation

DOI10.1145/3055282.3055285MaRDI QIDQ5268815zbMATH OpenOpenAlexDBLPWikidataFDO

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

Publication date 21 June 2017

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

Full work available at URL https://arxiv.org/abs/1607.06945, http://opus.bath.ac.uk/54991/1/Abrahametal2017a_authors.pdf

Mathematics Subject Classification ID

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

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.

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

Cites work

• Building bridges between symbolic computation and satisfiability checking
• Real World Verification
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)

Cited in

(10)

• Editorial: Symbolic computation and satisfiability checking
• Symbolic techniques in satisfiability solving
• Building bridges between symbolic computation and satisfiability checking
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• Theory and Applications of Satisfiability Testing
• SAT and lattice reduction for integer factorization
• scientific article; zbMATH DE number 6528599 (Why is no real title available?)
• Testing satisfiability
• scientific article; zbMATH DE number 5917352 (Why is no real title available?)
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)

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)