000K  utf8
1100  $c2017
1500  eng
2050  urn:nbn:de:gbv:8-diss-211795
2051  10.21941/kcss/2017/03
3000  Ehlers, Thorsten
4000  SAT and CP$dParallelisation and Applications$hChristian-Albrechts-Universität zu Kiel  [Ehlers, Thorsten]
4030  Kiel$nChristian-Albrechts-Universität zu Kiel
4209  In this thesis, we consider the parallelisation and application of SAT and CP solvers. In the first chapter, we consider SAT, the decision problem of propositional logic. We discuss details of the implementations of SAT solvers, and show how to improve upon existing sequential solvers. Furthermore, we discuss the parallelisation of these solvers with a focus on the communication of intermediate results within a parallel solver. The second chapter is concerned with Contraint Programing (CP) with learning. Contrary to classical Constraint Programming techniques, this incorporates learning mechanisms as they are used in the field of SAT solving. We present results from parallelising CHUFFED, a learning CP solver. In the final chapter, we discuss Sorting Networks, which are data oblivious sorting algorithms. Their independence of the input data lends them to parallel implementation. We consider the question how many parallel sorting steps are needed to sort some inputs, and present both lower and upper bounds for several cases.
4950  https://doi.org/10.21941/kcss/2017/03$xR$3Volltext$534
4950  https://nbn-resolving.org/urn:nbn:de:gbv:8-diss-211795$xR$3Volltext$534
4961  https://macau.uni-kiel.de/receive/diss_mods_00021179
5051  004
5550  CP
5550  Parallelisation
5550  SAT
5550  Sorting Networks