Analiza in primerjava reševalnikov tekmovanja SAT

Barbo, Janez (avtor), Č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.

• Jezik: Slovenski jezik
• Ključne besede: SAT, boolean, reševalnik, algoritmi, DPLL, CDCL
• Vrsta gradiva: Diplomsko delo/naloga
• Organizacija: FRI - Fakulteta za računalništvo in informatiko
• Leto izida: 2024
• PID: 20.500.12556/RUL-159006
• Datum objave v RUL: 27.06.2024

Sekundarni jezik

• Jezik: Angleški jezik
• Naslov: Analysis and comparison of SAT competition solvers

Izvleček

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.

• Ključne besede: Sat, boolean, solver, algorithms, DPLL, CDCL