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

Scientific Annals of Computer Science

article

A. Niewiadomski¹  P. Switalski¹  T. Sidoruk²  W. Penczek¹ 

[1] Siedlce University, Faculty of Science, Institute of Computer Science;Institute of Computer Science, Polish Academy of Sciences

关键词: SAT;    SMT;    SMT-solvers;    SMT-Lib;    complexity;    post correspondence problem;    string correction problem;    Towers of Hanoi;   

DOI  :  10.7561/SACS.2018.2.269

来源: Alexandru Ioan Cuza University of Iasi

【 摘 要 】

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.

【 授权许可】

CC BY-ND