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

Abstract

We compare the efficiency of seven modern SMT-solvers for several decision and combinatorial problems: the bounded Post correspondence problem (BPCP), the extended string correction problem (ESCP), and the Towers of Hanoi (ToH) of exponential solutions. For this purpose, we define new original reductions to SMT for all the above problems, and show their complexity. Our extensive experimental results allow for drawing quite interesting conclusions on efficiency and applicability of SMT-solvers depending on the theory used in the encoding.