The proof complexity of SMT solvers

DOI10.1007/978-3-319-96142-2_18MaRDI QIDQ6039408zbMATH OpenFDO

Authors Robert Robere, Antonina Kolokolova, Vijay Ganesh

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-96142-2_18

Mathematics Subject Classification ID

Complexity of proofs (03F20) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On the power of clause-learning SAT solvers as resolution engines
• SAT and SMT are still resolution: questions and challenges
• A (biased) proof complexity survey for SAT practitioners
• On CDCL-based proof systems with the ordered decision strategy
• Extended resolution simulates \({\mathsf{DRAT}}\)

Cited in

(5)

• Towards bit-width-independent proofs in SMT solvers
• Encoding first order proofs in SMT
• On the complexity of proof deskolemization
• The Smyth Completion
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

This page was built for publication: The proof complexity of SMT solvers

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