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

DOI10.7561/SACS.2018.2.269MaRDI QIDQ4621226zbMATH OpenOpenAlexWikidataFDO

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

complexityPost correspondence problemSATSMTSMT-LibSMT-solversstring correction problemTowers of Hanoi

Mathematics Subject Classification ID

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

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)

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

Describes a project that uses

Uses Software

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

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)