SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME

DOI10.7561/SACS.2018.2.269zbMATH Open1424.68151OpenAlexW2893472332WikidataQ129187869 ScholiaQ129187869MaRDI QIDQ4621226FDOQ4621226

Authors Artur Niewiadomski, Piotr Switalski, Teofil Sidoruk, Wojciech Penczek 

Publication date 8 February 2019

Published in Scientific Annals of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.7561/sacs.2018.2.269

zbMATH Keywords

complexitySATSMTPost correspondence problemTowers of Hanoistring correction problemSMT-LibSMT-solvers

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Using SMT for solving fragments of parameterised Boolean equation systems
• Parallelizing SMT solving: lazy decomposition and conciliation
• Extending Sledgehammer with SMT solvers
• Extending Sledgehammer with SMT solvers
• Induction for SMT solvers
• Symbolic optimization with SMT solvers
• Incomplete SMT techniques for solving non-linear formulas over the integers

Cited in

(3)

• Applying modern SAT-solvers to solving hard problems
• Lookahead-Based SMT Solving
• MedleySolver: online SMT algorithm selection

Describes a project that uses

Uses Software

• Boolector
• SMT-LIB
• z3
• SMTInterpol
• CVC4
• MathSAT5

This page was built for publication: SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME

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