diplomsko delo
Janez Barbo (Author), Uroš Čibej (Mentor)

Abstract

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.

Keywords

SAT;boolean;reševalnik;algoritmi;DPLI;CDCL;univerzitetni študij;diplomske naloge;

Data

Language: Slovenian
Year of publishing:
Typology: 2.11 - Undergraduate Thesis
Organization: UL FRI - Faculty of Computer and Information Science
Publisher: [J. Barbo]
UDC: 004(043.2)
COBISS: 200618243 Link will open in a new window
Views: 96
Downloads: 6
Average score: 0 (0 votes)
Metadata: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Other data

Secondary language: English
Secondary title: Analysis and comparison of solvers from SAT competitions
Secondary 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.
Secondary keywords: SAT;boolean;solver;algorithms;DPLI;CDCL;computer and information science;diploma;Univerzitetna in visokošolska dela;
Type (COBISS): Bachelor thesis/paper
Study programme: 1000468
Thesis comment: Univ. v Ljubljani, Fak. za računalništvo in informatiko
Pages: 62 str.
ID: 25390956