Paper Info
Title
Symbolic Computation Techniques in Satisfiability Checking
Abstract
Satisfiability Checking is a relatively young research area, aiming at the development of efficient software technologies for checking the satisfiability of existentially quantified logical formulas. Besides the success story of SAT solving for propositional logic, SAT-modulo-theories (SMT) solvers offer sophisticated solutions for different theories. When targeting arithmetic theories, SMT solvers also make use of decision procedures rooted in Symbolic Computation. In this paper we give a brief introduction to SMT solving, discuss differences to Symbolic Computation, and illustrate the potentials and obstacles for embedding Symbolic Computation techniques in SMT solving on the example of the Cylindrical Algebraic Decomposition.
Year
DOI
Venue
2016
10.1109/SYNASC.2016.014
2016 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
Keywords
Field
DocType
Satisfiability Checking,SAT-Modulo-Theories Solving,Algebra
Discrete mathematics,Symbolic-numeric computation,Embedding,Model checking,Programming language,Computer science,Satisfiability,Symbolic computation,Propositional calculus,Theoretical computer science,Cylindrical algebraic decomposition,Symbolic trajectory evaluation
Conference
ISSN
ISBN
Citations 
2470-881X
978-1-5090-5708-5
0
PageRank 
References 
Authors
0.34
12
1
Name
Order
Citations
PageRank
Erika Ábrahám183063.17