Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Concurrency, Specification, and Programming: Special Issue of Selected Papers of CS&P 2017
Guest editors: Wojciech Penczek, Holger Schlingloff and Piotr Wasilewski
Article type: Research Article
Authors: Niewiadomski, Artura | Switalski, Piotra | Sidoruk, Teofilb | Penczek, Wojciechb; *
Affiliations: [a] Siedlce University, Faculty of Science, Institute of Computer Science, 3-Maja 54, 08-110 Siedlce, Poland. artur.niewiadomski@uph.edu.pl, piotr.switalski@uph.edu.pl | [b] Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland. t.sidoruk@ipipan.waw.pl, penczek@ipipan.waw.pl
Correspondence: [*] Address for correspondence: Institute of Computer Science, Siedlce University of Natural Sciences and Humanities, 3-Maja 54, 08-110 Siedlce, Poland. Also affiliated with: Institute of Computer Science, Siedlce University of Natural Sciences and Humanities
Abstract: 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.
DOI: 10.3233/FI-2019-1788
Journal: Fundamenta Informaticae, vol. 165, no. 3-4, pp. 321-344, 2019
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl