The Strategy Challenge in SMT Solving
From MaRDI portal
Publication:4913859
DOI10.1007/978-3-642-36675-8_2zbMath1383.68084OpenAlexW1533439771MaRDI QIDQ4913859
Leonardo de Moura, Grant Olney Passmore
Publication date: 16 April 2013
Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)
Full work available at URL: https://www.pure.ed.ac.uk/ws/files/17472511/Moura_Passmore_2013_The_strategy_challenge.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
An approximation framework for solvers and decision procedures ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Satisfiability Checking: Theory and Applications ⋮ Rewriting Strategies and Strategic Rewrite Programs ⋮ Improving complex SMT strategies with learning ⋮ Matching Multiplications in Bit-Vector Formulas ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- The proof monad
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Solution of the Robbins problem
- Solvable cases of the decision problem
- Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase
- Satisfiability of Non-linear (Ir)rational Arithmetic
- A Proof Method for Quantification Theory: Its Justification and Realization
- Toward Mechanical Mathematics
- An improved proof procedure1
- Solving SAT and SAT Modulo Theories
- Combined Decision Techniques for the Existential Theory of the Reals
- Logic and Computation
- Efficient projection orders for CAD
- The Matita Interactive Theorem Prover
- Cutting to the Chase Solving Linear Integer Arithmetic
- To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: The Strategy Challenge in SMT Solving
