Robert Aistleitner,
"An Evaluation of Bit-Parallelization applied to Failed Literal Probing"
, in TNF Technisch-Naturwissenschaftliche Fakultät, Johannes Kepler Universität, Linz, 2-2013
Original Titel:
An Evaluation of Bit-Parallelization applied to Failed Literal Probing
Sprache des Titels:
Englisch
Original Kurzfassung:
The satisfiability problem (SAT) can be used to encode many problems of other domains
since it is the first one to be proven NP-complete. Powerful SAT solvers have been developed
in the last years which can handle large real-world problems in a reasonable amount
of time. Today?s significant challenges on SAT solvers include the transition to parallel
computer architectures. Various techniques have been developed to utilize multiple cores,
but those are limited to multi-core CPU systems.
This thesis evaluates another concept of parallelism than what is state-of-the-art today.
An algorithm is developed that is based on a ?streaming? principle, like it is optimal for
massively parallel systems, including modern graphics cards. To take advantage of this
principle, major changes to existing algorithms are necessary, first of all to avoid branches
whenever possible. This also gives the opportunity to add parallelism in the sense of
bit-parallelism.
As the evaluation will show, there is a good chance that the implemented algorithm
will perform well on massively parallel systems. Even on regular computer systems further
optimization potential is conceivable.
Forschungs-