Názov:SAT Solving Algorithms
Vedúci:RNDr. Tomáą Kulich, PhD.
Kµúčové slová:SAT, SAT algorithms, SAT benchmarking
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.

Súbory bakalárskej práce: