| Abstrakt: | The boolean formula satisfiability problem (SAT) is interesting not only in theory as the canonical NP-complete
problem, but also for its importance in practice: Various problems from different areas of computing are
expressed in terms of SAT and then solved using SAT solving algorithms. In this thesis, we present a survey and comparison of such algorithms. We examine the complete algorithms, the incomplete but very fast heuristics
and even some special-case algorithms applicable only to formulae in a particular form. We also review the benchmarking
methods for SAT algorithms and compare the surveyed algorithms using these benchmarks. Our intention was to create a thorough overview that focuses not only on the algorithms' theoretical principles, but also their practical implementation. We therefore also discuss various implementation details and other practical aspects of SAT solvers, such as the parsing and representation of formulae.
|
|---|