Advertisement

SAT-Problems

  • Christian Posthoff
  • Bernd Steinbach
Chapter

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.

References

  1. 4.
    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-5Google Scholar
  2. 13.
    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
  3. 17.
    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 CrossRefGoogle Scholar
  4. 27.
    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-4Google Scholar
  5. 35.
    Schwarzkopf, B.: Without cover on a rectangular chessboard. In: Feenschach, pp. 272–275 (1990). Ohne Deckung auf dem Rechteck (in German)Google Scholar
  6. 50.
    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-8Google Scholar
  7. 53.
    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-8Google Scholar
  8. 54.
    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-2283Google Scholar
  9. 55.
    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
  10. 58.
    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-6Google Scholar
  11. 61.
    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
  12. 62.
    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 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2019

Authors and Affiliations

  • Christian Posthoff
    • 1
  • Bernd Steinbach
    • 2
  1. 1.Computing and Information TechnologyUniversity of the West Indies (retired)ChemnitzGermany
  2. 2.Computer ScienceTU Bergakademie Freiberg (retired)ChemnitzGermany

Personalised recommendations