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

DOI10.7561/SACS.2018.2.269zbMath1424.68151OpenAlexW2893472332WikidataQ129187869 ScholiaQ129187869MaRDI QIDQ4621226

Piotr Switalski, Wojciech Penczek, Teofil Sidoruk, Artur Niewiadomski

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

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

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