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

Povzetek

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.

Ključne besede

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

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.11 - Diplomsko delo
Organizacija: UL FRI - Fakulteta za računalništvo in informatiko
Založnik: [J. Barbo]
UDK: 004(043.2)
COBISS: 200618243 Povezava se bo odprla v novem oknu
Št. ogledov: 96
Št. prenosov: 6
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: Analysis and comparison of solvers from SAT competitions
Sekundarni povzetek: 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.
Sekundarne ključne besede: SAT;boolean;solver;algorithms;DPLI;CDCL;computer and information science;diploma;Univerzitetna in visokošolska dela;
Vrsta dela (COBISS): Diplomsko delo/naloga
Študijski program: 1000468
Komentar na gradivo: Univ. v Ljubljani, Fak. za računalništvo in informatiko
Strani: 62 str.
ID: 25390956