Abstract
Many finite discrete problems can be modeled as satisfiability (SAT) problems. There are different types of SAT-problems. Most common are CD-SAT-formulas which consist of a conjunctions of disjunctions of Boolean variables and this expression is equal to 1. Such disjunctions are also called clauses. New CDC-SAT-formulas are conjunctions of disjunctions of conjunctions of Boolean variables and allow a more compact specification of the problem. Besides of special algorithms for SAT-problems (SAT-solvers) ternary vector lists are an appropriate data structure to express and solve all such problems. SAT-problems belong to the class of NP-complete problems. The modeling and solution of many SAT-problems will be explored. Studied problem classes are placement problems, covering problems, path problems, and coloring problems. Some of the selected examples have their root many centuries ago, but also very recent research results will be presented. Hints for efficient solutions using a single central processing unit (CPU), several CPU-cores of a multi-processor, or even the huge number of cores of a graphical processing unit (GPU) will be given.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Biere, A., et al. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009). ISBN: 978-1-58603-929-5
Cook, S.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing. STOC, pp. 151–158. ACM, Shaker Heights (1971). https://doi.org/10.1145/800157.805047
Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) Theory and Applications of Satisfiability Testing – SAT 2016, pp. 228–24. Springer, Cham (2016). ISBN: 978-3-319-40970-2. https://doi.org/10.1007/978-3-319-40970-2_15
Posthoff, C., Steinbach, B.: The solution of discrete constraint problems using Boolean models. In: Filipe, J., Fred, A., Sharp, B. (eds.) Proceedings of the 2nd International Conference on Agents and Artificial Intelligence. ICAART 2, Valencia, Feb. 2010, pp. 487–493. ISBN: 978-989-674-021-4
Schwarzkopf, B.: Without cover on a rectangular chessboard. In: Feenschach, pp. 272–275 (1990). Ohne Deckung auf dem Rechteck (in German)
Steinbach, B., Posthoff, C.: New results based on Boolean models. In: Steinbach, B. (ed.) Boolean Problems, Proceedings of the 9th International Workshops on Boolean Problems. IWSBP 9, Sept. 2010, pp. 29–36. Freiberg University of Mining and Technology, Freiberg (2010). ISBN: 978-3-86012-404-8
Steinbach, B., Posthoff, C.: Improvements in exact minimal waveform coverings of periodic binary signals. In: Quesada-Arencibia, A., et al. (eds.) Computer Aided System Theory, Extended Abstracts. 13th International Conference on Computer Aided System Theory Eurocast 13, Las Palmas, Feb. 2011, pp. 410–411. ISBN: 978-84-693-9560-8
Steinbach, B., Posthoff, C.: Parallel solution of covering problems super-linear speedup on a small set of cores. Int. J. Comput. Global Sci. Technol. Forum 1(2), 113–122 (2011). ISSN: 2010-2283
Steinbach, B., Posthoff, C.: Sources and obstacles for parallelization - a comprehensive exploration of the unate covering problem using both CPU and GPU. In: Astola, J., et al. (eds.) GPU Computing with Applications in Digital Logic. TICSP 62. Tampere International Center for Signal Processing, Tampere, pp. 63–96 (2012). ISBN: 978-952-15-2920-7. https://doi.org/10.13140/2.1.4266.4320
Steinbach, B., Posthoff, C.: Fast calculation of exact minimal unate coverings on both the CPU and the GPU. In: Quesada-Arencibia, A., et al. (eds.) 14th International Conference on Computer Aided Systems Theory – EUROCAST 2013 Part II, Feb. 2013. Lecture Notes in Computer Science, vol. 8112, pp. 234–241. Springer, Las Palmas (2013). ISBN: 978-0-9924518-0-6
Steinbach, B., Posthoff, C.: Multiple-valued problem solvers – comparison of several approaches. In: Proceedings of the IEEE 44th International Symposium on Multiple-Valued Logic. ISMVL 44, Bremen, May 2014, pp. 25–31. https://doi.org/10.1109/ISMVL.2014.13
Steinbach, B., Posthoff, C.: Evaluation and optimization of GPU based unate covering algorithms. In: Quesada-Arencibia, A., et al. (eds.) Computer Aided Systems Theory – EUROCAST 2015, Feb. 2015. Lecture Notes in Computer Science, vol. 9520, pp. 617–624. Springer, Las Palmas (2015). ISBN: 978-3-319-27340-2. https://doi.org/10.1007/978-3-319-27340-2_76
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer International Publishing AG
About this chapter
Cite this chapter
Posthoff, C., Steinbach, B. (2019). SAT-Problems. In: Logic Functions and Equations. Springer, Cham. https://doi.org/10.1007/978-3-030-02420-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-02420-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02419-2
Online ISBN: 978-3-030-02420-8
eBook Packages: Computer ScienceComputer Science (R0)