20.500.12556/RUL-164793 Analiza in primerjava reševalnikov tekmovanja SAT Analysis and comparison of solvers from SAT competitions Problem SAT je odločitveni problem, ki za dani logični izraz odloči, če je izpolnljiv ali ne. V nalogi problem SAT podrobno opišemo in na kratko predstavimo teoretično ozadje. Nato opišemo dva glavna algoritma za reševanje, DPLL in CDCL. Algoritma razložimo in prikažemo na primeru. \\ Od leta 2002 naprej se vsako leto odvijajo SAT tekmovanja. Na tekmovanjih tekmujejo najnovejši reševalniki -- programi, ki rešujejo SAT izraze. Opišemo zgodovino in obliko tekmovanj. Prav tako izberemo šest reševalnikov in množico tristotih testnih primerov iz tekmovanj. Reševalnike testiramo nad primeri in opravimo analizo rezultatov. Opazimo velik napredek v moči reševalnikov v zadnjih letih. Po kratki analizi testnih primerov ugotavljamo, da se le-ti prav tako spreminjajo v značilnostih, kot so število spremenljivk in klavzul ter povprečna stopnja in gostota grafa izpeljanega iz izrazov. The SAT problem is a decision problem that decides whether a given Boolean expression is satisfiable. In our thesis, we describe the SAT problem in detail and briefly present its theoretical background. We then describe the two main solving algorithms called DPLL and CDCL. We thoroughly explain them and demonstrate them with an example. \\ Since the year 2002, SAT competitions have been held annually. In these competitions, the newest solvers (programs that solve SAT expressions) compete with each other. We write about the history and structure of these competitions. Additionally, we select six solvers and three hundred benchmarks from the competitions. We test the solvers on the benchmarks and perform an analysis of the results. We observe a significant increase of the power of the solvers in recent years. After a short analysis of the benchmarks, where we compare the number of variables and clauses as well as the average degree and density of their graphs, we conclude that they as well have changed over the years. SAT boolean reševalnik algoritmi DPLL CDCL Sat boolean solver algorithms DPLL CDCL true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2024-11-12 12:00:01 2024-11-12 12:00:01 2024-12-30 09:05:11 0000-00-00 00:00:00 2024 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 37242 200618243 Barbo_Janez_-_Analiza_in_primerjava_resevalnikov_tekmovanja_SAT.pdf Barbo_Janez_-_Analiza_in_primerjava_resevalnikov_tekmovanja_SAT.pdf 1 FB8C17C41B8B549D4CABBC87CFFB39C6 46e7a3200fe372492f70cb519bc04a15294398ae3658e0284dd1def0faae343b e6999afc-a0e4-11ef-b232-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=195477 Fakulteta za računalništvo in informatiko 0 0 0