Applying Modern SAT-solvers to Solving Hard Problems

• Autorzy: Niewiadomski Artur , Switalski Piotr , Sidoruk Teofil , Penczek Wojciech

Identyfikatory

DOI

10.3233/FI-2019-1788

• Języki publikacji: EN

Abstrakty

EN

We present nine SAT-solvers and compare their efficiency for several decision and combinatorial problems: three classical NP-complete problems of the graph theory, bounded Post correspondence problem (BPCP), extended string correction problem (ESCP), two popular chess problems, PSPACE-complete verification of UML systems, and the Towers of Hanoi (ToH) of exponential solutions. In addition to several known reductions to SAT for the problems of graph k-colouring, vertex k-cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, and ToH, SCP, and BPCP. Our extensive experimental results allow for drawing quite interesting conclusions on efficiency and applicability of SAT-solvers to different problems: they behave quite efficiently for NP-complete and harder problems but they are by far inferior to tailored algorithms for specific problems of lower complexity.

Słowa kluczowe

EN

NP-complete problems; hamiltonian graph theory; graph theory; statistical decision making; problem solving; chess

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 165, nr 3-4
• Strony: 321--344
• Opis fizyczny: Bibliogr. 42 poz., rys., tab., wykr.

Twórcy

autor

Niewiadomski Artur

• Siedlce University, Faculty of Science, Institute of Computer Science, 3-Maja 54, 08-110 Siedlce, Poland

autor

Switalski Piotr

• Siedlce University, Faculty of Science, Institute of Computer Science, 3-Maja 54, 08-110 Siedlce, Poland

autor

Sidoruk Teofil

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

autor

Penczek Wojciech

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

Bibliografia

• [1] Karp R. Reducibility among combinatorial problems. In: Complexity of Computer Computations, Plenum Press 1972 pp. 85-103. doi:10.1007/978-1-4684-2001-2_9.
• [2] Abdulla PA, Bjesse P, Eén 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. Springer-Verlag, 2000 pp. 411-425. doi:10.1007/3-540-46419-0_28.
• [3] Armando A, Compagna L. An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols. In: Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2005; 125(1):91-108. URL https://doi.org/10.1016/j.entcs.2004.05.021.
• [4] Biere A, et al. Symbolic Model Checking Using SAT Procedures Instead of BDDs. In: In Proc. of the ACM/IEEE Design Automation Conference (DAC). 1999 pp. 317-320. doi:10.1145/309847.309942.
• [5] Clarke E, Biere A, Raimi R, Zhu Y. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design, 2001;19(1):7-34. doi:10.1023/A:1011276507260.
• [6] Kacprzak M, Penczek W. Unbounded Model Checking for Alternating-Time Temporal Logic. In: 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), 19-23 August 2004, New York, NY, USA. 2004 pp. 646-653. doi:10.1109/AAMAS.2004.242515.
• [7] Knapik M, Penczek W. Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets and Other Models of Concurrency, 2012;5:141-159. doi:10.1007/978-3-642-29072-5_6.
• [8] Męski A, Penczek W, Szreter M, Woźna-Szcześniak B, Zbrzezny A. 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, 2014;28(4):558-604. doi:10.1007/s10458-013-9232-2.
• [9] Woźna B, Zbrzezny A, Penczek W. Checking Reachability Properties for Timed Automata via SAT. Fundamenta Informaticae, 2003;55(2):223-241.
• [10] Woźna-Szcześniak B. SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems. Fundamenta Informaticae, 2016;143(1-2):173-205. doi:10.3233/FI-2016-1310.
• [11] Kautz H, Selman B. Planning as satisfiability. In: In ECAI 92: Proceedings of the 10th European conference on Artificial intelligence. 1992 pp. 359-363. ISBN-0-471-93608-1.
• [12] Niewiadomski A, et al. Towards Automatic Composition of Web Services: SAT-Based Concretisation of Abstract Scenarios. Fundamenta Informaticae, 2012;120(2):181-203. doi:10.3233/FI-2012-756.
• [13] Davis M, Putnam H. A Computing Procedure for Quantification Theory. J. ACM, 1960;7(3):201-215. doi:10.1145/321033.321034.
• [14] Davis M, Logemann G, Loveland D. A Machine Program for Theorem-proving. Commun. ACM, 1962; 5(7):394-397. doi:10.1145/368273.368557.
• [15] Kaivola R, et al. Replacing Testing with Formal Verification in Intel Core I7 Processor Execution Engine Validation. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV’09. Springer-Verlag, Berlin, Heidelberg, 2009 pp. 414-429. ISBN-978-3-642-02657-7, doi:10.1007/978-3-642-02658-4_32.
• [16] de Moura L, Bjørner N. Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, pp. 400-411. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN-978-3-642-14203-1, 2010. doi:10.1007/978-3-642-14203-1_34.
• [17] Le Berre D, Rapicault P. Dependency Management for the Eclipse Ecosystem: Eclipse P2, Metadata and Resolution. In: Proceedings of the 1st International Workshop on Open Component Ecosystems, IWOCE ’09. ACM, New York, NY, USA, 2009 pp. 21-30. ISBN-978-1-60558-677-9, doi:10.1145/1595800.1595805.
• [18] Biere A. Lingeling and friends entering the SAT Challenge 2012. Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, volume B-2012-2, 2012 pp. 33-34. URL /pubpdf/Lingeling_and_Friends_Entering_the_SAT_Challenge_2012.pdf.
• [19] Audemard G, Simon L. Glucose and Syrup in the SAT Race 2015. SAT Race, 2015.
• [20] Gebser M, et al. clasp: A Conflict-Driven Answer Set Solver. In: Baral C., Brewka G., Schlipf J. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2007. volume 4483 of LNCS, Springer. 2007 pp. 260-265. doi:10.1007/978-3-540-72200-7_23.
• [21] Selman B, Levesque H, Mitchell D. A New Method for Solving Hard Satisfiability Problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence, AAAI’92. AAAI Press. 1992 pp. 440-446. ISBN-0-262-51063-4, URL http://dl.acm.org/citation.cfm?id=1867135.1867203.
• [22] Selman B, Kautz H, Cohen B. Local Search Strategies for Satisfiability Testing. In: Dimacs Series in Discrete Mathematics and Theoretical Computer Science. 1995 pp. 521-532.
• [23] Sorensson N, Een N. Minisat v1.13 - a SAT solver with conflict-clause minimization. SAT, 2005; 2005(53):1-2.
• [24] Hamadi Y, Jabbour S, Sais L. ManySAT: a Parallel SAT Solver. JSAT, 2009;6(4):245-262.
• [25] de Moura LM, Bjørner N. Z3: An Efficient SMT Solver. In: Proc. of TACAS’08, volume 4963 of LNCS. Springer-Verlag, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3_24.
• [26] Mahajan Y, Fu Z, Malik S. Zchaff2004: An efficient sat solver. In: Int. Conf. on Theory and Applications of Satisfiability Testing. volume 3542 of LNCS. Springer, 2004 pp. 360-375. doi:10.1007/11527695_27.
• [27] Stamm-Wilbrandt H. Programming in Propositional Logic or Reductions: Back to the Roots (Satisfiability), 1993.
• [28] Post EL. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 1946;52(4):264-268. URL https://projecteuclid.org/euclid.bams/1183507843.
• [29] Garey MR, Johnson DS. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. ISBN-0-7167-1044-7.
• [30] Kari L, Gloor G, Yu S. Using DNA to solve the Bounded Post Correspondence Problem. Theor. Comput. Sci., 2000;231(2):193-203. doi:10.1016/S0304-3975(99)00100-0.
• [31] Levenshtein VI. Binary codes capable of correcting deletions, insertions, and reversals. Soviet Physics Doklady, 1966;10(8):707-710. URL http://adsabs.harvard.edu/abs/1966SPhD...10..707L.
• [32] Wagner RA, Fischer MJ. The string-to-string correction problem. Journal of the ACM, 1974;21(1):168-173. doi:10.1145/321796.321811.
• [33] Damerau FJ. A technique for computer detection and correction of spelling errors. Commun. ACM, 1964;7(3):171-176. doi:10.1145/363958.363994.
• [34] Gent IP, Jefferson C, Nightingale P. Complexity of N-queens Completion. J. Artif. Int. Res., 2017;59(1):815-848. URL http://dl.acm.org/citation.cfm?id=3176788.3176807.
• [35] Bell J, Stevens B. A survey of known results and research areas for n-queens. Discrete Mathematics, 2009;309(1):1-31. doi:10.1016/j.disc.2007.12.043.
• [36] Lin SS, Wei CL. Optimal algorithms for constructing knight’s tours on arbitrary n x m chessboards. Discrete Applied Mathematics, 2005;146(3):219-232. doi:10.1016/j.dam.2004.11.002.
• [37] Martins R, Lynce I. Effective CNF Encodings for the Towers of Hanoi. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning. 2008.
• [38] UML O. Unified Modeling Language. Infrastructure Specification, 2007;2(1).
• [39] Niewiadomski A, Penczek W, Szreter M. A new approach to model checking of UML state machines. Fundamenta Informaticae, 2009;93(1-3):289-303. doi:10.3233/FI-2009-0103.
• [40] Niewiadomski A. Automatyczna weryfikacja systemow specyfikowanych w UML (in Polish). Ph.D. thesis, Polish Academy of Science, ICS, 2011.
• [41] De Smet G, et al. OptaPlanner user guide. http://www.optaplanner.org., 2017.
• [42] Parberry I. An Efficient Algorithm for the Knight’s Tour Problem. Discrete Appl. Math., 1997;73(3):251-260. doi:10.1016/S0166-218X(96)00010-8.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).