Simple view
Full metadata view
Authors
Statistics
Implementacja współczesnego SAT solvera.
The implementation of modern SAT solver.
SAT solver, propagacja jednostkowa, LBD, VSIDS, minimalizacja klauzul
SAT solver, unit propagation, LBD, VSIDS, clause minimalization
Celem pracy jest przegląd technik stosowanych współcześnie w celu szybszego rozwiązywania problemu spełnialności formuł logicznych, uproszczona implementacja tych technik oraz ich porównanie. Uproszczenia w implementacjach polegają głównie na pominięciu części niskopoziomowych usprawnień. Natomiast porównania uwzględniają również zmianę niektórych parametrów na inne niż te proponowane przez autorów metod.
The aim of this paper is to overview the modern techniques that are used to speed up the resolution of boolean satisfiability problem, simplified implementation of these techniques and their comparison. Simplifications within implementations are mainly based on skipping low-level parts of improvements. Comparisons, however, take into account the change of some parameters into different ones than those proposed by the author of the method.
| dc.abstract.en | The aim of this paper is to overview the modern techniques that are used to speed up the resolution of boolean satisfiability problem, simplified implementation of these techniques and their comparison. Simplifications within implementations are mainly based on skipping low-level parts of improvements. Comparisons, however, take into account the change of some parameters into different ones than those proposed by the author of the method. | pl |
| dc.abstract.pl | Celem pracy jest przegląd technik stosowanych współcześnie w celu szybszego rozwiązywania problemu spełnialności formuł logicznych, uproszczona implementacja tych technik oraz ich porównanie. Uproszczenia w implementacjach polegają głównie na pominięciu części niskopoziomowych usprawnień. Natomiast porównania uwzględniają również zmianę niektórych parametrów na inne niż te proponowane przez autorów metod. | pl |
| dc.affiliation | Wydział Matematyki i Informatyki | pl |
| dc.area | obszar nauk ścisłych | pl |
| dc.contributor.advisor | Wrona, Michał | pl |
| dc.contributor.author | Zawadzki, Jakub | pl |
| dc.contributor.departmentbycode | UJK/WMI2 | pl |
| dc.contributor.reviewer | Wrona, Michał | pl |
| dc.contributor.reviewer | Bendkowski, Maciej | pl |
| dc.date.accessioned | 2020-07-27T14:05:57Z | |
| dc.date.available | 2020-07-27T14:05:57Z | |
| dc.date.submitted | 2018-09-11 | pl |
| dc.fieldofstudy | informatyka analityczna | pl |
| dc.identifier.apd | diploma-121474-196539 | pl |
| dc.identifier.project | APD / O | pl |
| dc.identifier.uri | https://ruj.uj.edu.pl/xmlui/handle/item/226016 | |
| dc.language | pol | pl |
| dc.subject.en | SAT solver, unit propagation, LBD, VSIDS, clause minimalization | pl |
| dc.subject.pl | SAT solver, propagacja jednostkowa, LBD, VSIDS, minimalizacja klauzul | pl |
| dc.title | Implementacja współczesnego SAT solvera. | pl |
| dc.title.alternative | The implementation of modern SAT solver. | pl |
| dc.type | licenciate | pl |
| dspace.entity.type | Publication |