Simple view
Full metadata view
Authors
Statistics
Coffe SAT solver - implementacja współczesnego SAT solvera.
Coffe SAT solver - modern SAT solver implementation
SAT, solver, NP-zupełny, GRASP, Chaff, MiniSAT, Glucose, VSIDS, propagacja
SAT, solver, NP-complete, GRASP, Chaff, MiniSAT, Glucose, VSIDS, propagation
Problem spełnialności boolowskiej (SAT) jest kluczowym problemem informatyki teoretycznej. W ostatnich dziesięcioleciach powstało wiele SAT solverów (np. GRASP, Chaff, MiniSAT, Glucose). Celem niniejszej pracy jest implementacja SAT solvera Coffee wyposażonego w najpopularniejsze heurystyki i struktury danych używane we współczesnych solverach (np. heurystykę VSIDS, propagację klauzul unarnych, strukturę Two Watched Literals).
Boolean satisfiability Problem (SAT) is a crucial problem in theoretical computer science. In recent years many SAT solvers have been described and implemented (eg. GRASP, Chaff, MiniSAT, Glucose). The aim of this work The aim of this work is to implement Coffee - modern SAT solver, which incorporates the most popular heuristics and data structures used in modern solvers (eg. VSIDS, unit clauses propagation, Two Watched Literals).
| dc.abstract.en | Boolean satisfiability Problem (SAT) is a crucial problem in theoretical computer science. In recent years many SAT solvers have been described and implemented (eg. GRASP, Chaff, MiniSAT, Glucose). The aim of this work The aim of this work is to implement Coffee - modern SAT solver, which incorporates the most popular heuristics and data structures used in modern solvers (eg. VSIDS, unit clauses propagation, Two Watched Literals). | pl |
| dc.abstract.pl | Problem spełnialności boolowskiej (SAT) jest kluczowym problemem informatyki teoretycznej. W ostatnich dziesięcioleciach powstało wiele SAT solverów (np. GRASP, Chaff, MiniSAT, Glucose). Celem niniejszej pracy jest implementacja SAT solvera Coffee wyposażonego w najpopularniejsze heurystyki i struktury danych używane we współczesnych solverach (np. heurystykę VSIDS, propagację klauzul unarnych, strukturę Two Watched Literals). | pl |
| dc.affiliation | Wydział Matematyki i Informatyki | pl |
| dc.area | obszar nauk ścisłych | pl |
| dc.contributor.advisor | Wrona, Michał | pl |
| dc.contributor.author | Woźniak, Maciej | pl |
| dc.contributor.departmentbycode | UJK/WMI2 | pl |
| dc.contributor.reviewer | Wrona, Michał | pl |
| dc.contributor.reviewer | Kozik, Marcin - 129358 | pl |
| dc.date.accessioned | 2020-07-27T14:05:53Z | |
| dc.date.available | 2020-07-27T14:05:53Z | |
| dc.date.submitted | 2018-10-10 | pl |
| dc.fieldofstudy | informatyka analityczna | pl |
| dc.identifier.apd | diploma-121473-178861 | pl |
| dc.identifier.project | APD / O | pl |
| dc.identifier.uri | https://ruj.uj.edu.pl/xmlui/handle/item/226015 | |
| dc.language | pol | pl |
| dc.subject.en | SAT, solver, NP-complete, GRASP, Chaff, MiniSAT, Glucose, VSIDS, propagation | pl |
| dc.subject.pl | SAT, solver, NP-zupełny, GRASP, Chaff, MiniSAT, Glucose, VSIDS, propagacja | pl |
| dc.title | Coffe SAT solver - implementacja współczesnego SAT solvera. | pl |
| dc.title.alternative | Coffe SAT solver - modern SAT solver implementation | pl |
| dc.type | master | pl |
| dspace.entity.type | Publication |