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

Published in Volume XXVIII, Issue 2, 2018, pages 269–288, doi: 10.7561/SACS.2018.2.269

Authors: A. Niewiadomski, P. Switalski, T. Sidoruk, W. Penczek

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.

Full Text (PDF)

References

[1] P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic Reachability Analysis Based on SAT-Solvers. In Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), volume 1785 of LNCS, pages 411–425. Springer-Verlag, 2000. doi:10.1007/3-540-46419-0_28.

[2] A. Armando and L. Compagna. An Optimized Intruder Model for SAT-Based Model-Checking of Security Protocols. In Electronic Notes in Theoretical Computer Science, volume 125, pages 91–108. Elsevier Science Publishers, March 2005. doi:10.1016/j.entcs.2004.05.021.

[3] A. Armando, J. Mantovani, and L. Platania. Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. Int. Journal on Software Tools for Technology Transfer, 11(1):69–83, 2009. doi:10.1007/11691617_9.

[4] C. Barrett, L. de Moura, and A. Stump. SMT-COMP: Satisfiability Modulo Theories Competition. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, pages 20–23, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. doi:10.1007/11513988_4.

[5] C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. Technical Report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.

[6] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Handbook of Satisfiability: volume 185 Frontiers in Artificial Intelligence and Applications, chapter Satisfiability Modulo Theories. IOS Press, pages 825–885, 2009. doi:10.3233/978-1-58603-929-5-825.

[7] C. Barrett and C. Tinelli. Satisfiability Modulo Theories. In E.M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors, Handbook of Model Checking, pages 305–343, Cham, 2018. Springer International Publishing. doi:10.1007/978-3-319-10575-8_11.

[8] M. Berglund. Analyzing Edit Distance on Trees: Tree Swap Distance is Intractable. In Stringology, pages 59–72, 2011.

[9] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using SAT Procedures Instead of BDDs. In Proc. of the ACM/IEEE Design Automation Conference (DAC), pages 317–320, 1999. doi:10.1109/dac.1999.781333.

[10] R. Brummayer and A. Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 174–177. Springer, 2009. doi:10.1007/978-3-642-00768-2_16.

[11] J. Christ, J. Hoenicke, and A. Nutz. SMTInterpol: An Interpolating SMT Solver. In International SPIN Workshop on Model Checking of Software, pages 248–254. Springer, 2012. doi:10.1007/978-3-642-31759-0_19.

[12] A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 93–107. Springer, 2013. doi:10.1007/978-3-642-36742-7_7.

[13] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design, 19(1):7–34, 2001. doi:10.1023/A:1011276507260.

[14] F. J. Damerau. A Technique for Computer Detection and Correction of Spelling Errors. Commun. ACM, 7(3):171-176, 1964. doi:10.1145/363958.363994.

[15] L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Proc. Of the Theory and Practice of Software, 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, 2008. Springer-Verlag. doi:10.1007/978-3-540-78800-3_24.

[16] M. Deters, A. Reynolds, T. King, C. W. Barrett, and C. Tinelli. A Tour of CVC4: How It Works, and How to Use It. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, page 7. IEEE, 2014. doi:10.1109/fmcad.2014.6987586.

[17] B. Dutertre. Yices 2.2. In International Conference on Computer Aided Verification, pages 737–744. Springer, 2014. doi:10.1007/978-3-319-08867-9_49.

[18] V. Ganesh and D. L. Dill. A Decision Procedure for Bit-Vectors and Arrays. In International Conference on Computer-Aided Verification, pages 519–531. Springer, 2007. doi:10.1007/978-3-540-73368-3_52.

[19] M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979.

[20] M. Kacprzak and W. Penczek. Unbounded Model Checking for Alternating-Time Temporal Logic. In 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pages 646–653, 2004.

[21] L. Kari, G. Gloor, and S. Yu. Using DNA to Solve the Bounded Post Correspondence Problem. Theor. Comput. Sci., 231(2):193–203, 2000. doi:10.1016/s0304-3975(99)00100-0.

[22] R. Karp. Reducibility Among Combinatorial Problems. In Complexity of Computer Computations, pages 85–103. Plenum Press, 1972. doi:10.1007/978-1-4684-2001-2_9.

[23] H. Kautz and B. Selman. Planning as Satisfiability. In ECAI 92: Proceedings of the 10th European Conference on Artificial Intelligence, pages 359–363, 1992.

[24] T. King. Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. PhD Thesis, New York University, 2014.

[25] V. I. Levenshtein. Binary Codes Capable of Correcting Deletions, Insertions, and Reversals. Soviet Physics Doklady, 10(8):707-710, 1966.

[26] R. Martins and I. Lynce. Effective CNF Encodings for the Towers of Hanoi. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2008.

[27] A. Męski, W. Penczek, M. Szreter, B. Woźna-Szcześniak, and A. Zbrzezny. BDD-Versus SAT-Based Bounded Model Checking for the Existential Fragment of Linear Temporal Logic with Knowledge: Algorithms and Their Performance. Autonomous Agents and Multi-Agent Systems, 28(4):558–604, 2014. doi:10.1007/s10458-013-9232-2.

[28] A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, and A. Zbrzezny. Towards Automatic Composition of Web Services: SAT-Based Concretisation of Abstract Scenarios. Fundam. Inform., 120(2):181–203, 2012. doi:10.3233/FI-2012-756.

[29] A. Niewiadomski, W. Penczek, and T. Sidoruk. Comparing Efficiency of Modern SAT-Solvers for Selected Problems in P, NP, PSPACE, and EXPTIME. In Proceedings of the 26th International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, September 25-27, 2017, pages 1–12, 2017.

[30] A. Niewiadomski, P. Switalski,W. Penczek, and T. Sidoruk. Applying Modern SAT-Solvers to Solving Hard Problems. submitted to Fundamenta Informaticae, 2018.

[31] W. Penczek, A. Półrola, and A. Zbrzezny. Towards Automatic Composition of Web Services: A SAT-Based Phase. In Proc. of the 2nd Int. Workshop on Abstractions for Petri Nets and Other Models of Concurrency and of the Int. Workshop on Scalable and Usable Model Checking (APNOC’10 + SUMO’10), pages 76–96, 2010.

[32] E. L. Post. A Variant of a Recursively Unsolvable Problem. Bulletin of the American Mathematical Society, 52(4):264–268, 1946. doi:10.1090/s0002-9904-1946-08555-9.

[33] R. A. Wagner and M. J. Fischer. The String-to-String Correction Problem. Journal of the ACM, 21(1):168-173, 1974. doi:10.1145/321796.321811.

[34] B. Woźna, A. Zbrzezny, and W. Penczek. Checking Reachability Properties for Timed Automata Via SAT. Fundamenta Informaticae, 55(2):223–241, 2003.

[35] B. Woźna-Szcześniak. SAT-Based Bounded Model Checking for Weighted Deontic Interpreted Systems. Fundam. Inform., 143(1-2):173–205, 2016. doi:10.3233/fi-2016-1310.

[36] A. Zbrzezny. SAT-Based Reachability Checking for Timed Automata with Diagonal Constraints. Fundamenta Informaticae, 67(1-3):303–322, 2005.

Bibtex

@article{sacscuza:niewiadomski2018siaeasspinae,
  title={SMT-Solvers in Action: Encoding and Solving  Selected Problems in NP and EXPTIME},
  author={A. Niewiadomski, P. Switalski, T. Sidoruk, W. Penczek},
  journal={Scientific Annals of Computer Science},
  volume={28},
  number={2},
  organization={``A.I. Cuza'' University, Ia\c si, Rom\^ania},
  year={2018},
  pages={269–288},
  publisher={``A.I. Cuza'' University Press, Ia\c si}
}