Analiza in primerjava reševalnikov tekmovanja SAT

Barbo, Janez (author), Čibej, Uroš (mentor)

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.

• Language: Slovenian
• Keywords: SAT, boolean, reševalnik, algoritmi, DPLL, CDCL
• Work type: Bachelor thesis/paper
• Organization: FRI - Faculty of Computer and Information Science
• Year: 2024
• PID: 20.500.12556/RUL-164793
• Publication date in RUL: 12.11.2024

Secondary language

• Language: English
• Title: Analysis and comparison of solvers from SAT competitions

Abstract

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.

• Keywords: Sat, boolean, solver, algorithms, DPLL, CDCL