Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Zeszyty Naukowe. Informatyka / Politechnika Opolska

1 2015

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Efektywne rozwiązywanie problemu SAT z wykorzystaniem algorytmu uczącego się klauzul

Sobol Mariusz, Szpakowski Mateusz

Zeszyty Naukowe. Informatyka / Politechnika Opolska

2015

vol. 357, z. 3

167--181

W artykule przedstawiono jedną z nowszych metod rozwiązywania problemu SAT jaką jest algorytm CDCL polegający na nauce klauzul w oparciu o konflikty. W algorytmie zaimplementowano strategie: wyboru zmiennych logicznych, minimalizacji klauzul uczących i restartów. Porównano skuteczność metody CDCL w stosunku do klasycznego algorytm DPLL. Porównanie metod przeprowadzono dla formuł o różnej liczbie zmiennych logicznych. Wykazano dużą przewagę algorytmu CDCL nad algorytmem DPLL.

This paper presents a novel method for solving the SAT problem, that is the CDCL algorithm relying on learning the clauses on the basis of conflicts. The algorithm implements the following strategies: selection of logic variables, minimization of learning clauses and restarts. Efficacy of the CDCL method and the classical DPLL algorithm is compared. Comparison of the two methods is performed for formulas with different numbers of logical variables. The great advantage of the CDCL algorithm over the DPLL one is shown.