Building bridges between symbolic computation and satisfiability checking

DOI10.1145/2755996.2756636MaRDI QIDQ2819729zbMATH OpenOpenAlexWikidataFDO

Authors Erika Ábrahám

Publication date 29 September 2016

Published in Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2755996.2756636

zbMATH Keywords

arithmeticsymbolic computationSMT solving

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Symbolic computation and algebraic computation (68W30)

Recommendations

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

Cited in

(16)

• Editorial: Symbolic computation and satisfiability checking
• Symbolic techniques in satisfiability solving
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• Satisfiability checking and symbolic computation
• Theory and Applications of Satisfiability Testing
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• SAT and lattice reduction for integer factorization
• Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• Satisfiability checking: theory and applications
• A nonexistence certificate for projective planes of order ten with weight 15 codewords
• The SAT+CAS method for combinatorial search with applications to best matrices
• What does ``without loss of generality mean, and how do we detect it
• Applying computer algebra systems with SAT solvers to the Williamson conjecture
• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Complex Golay pairs up to length 28: a search via computer algebra and programmatic SAT

Describes a project that uses

Uses Software

• iSAT
• SMT-RAT
• MathSAT5
• CVC4
• OpenSMT
• veriT
• REDLOG
• SMT-LIB
• QEPCAD

This page was built for publication: Building bridges between symbolic computation and satisfiability checking

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