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

• Autorzy: Sobol Mariusz , Szpakowski Mateusz

Warianty tytułu

EN

Efficient solving of the SAT problem using the clause-learning algorithm

• Języki publikacji: PL

Abstrakty

PL

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.

EN

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.

• Wydawca: Oficyna Wydawnicza Politechniki Opolskiej
• Czasopismo: Zeszyty Naukowe. Informatyka / Politechnika Opolska
• Rocznik: 2015
• Tom: vol. 357, z. 3
• Strony: 167--181
• Opis fizyczny: Bibliogr. 16 poz., rys., tab.

Twórcy

autor

Sobol Mariusz

• Politechnika Opolska

autor

Szpakowski Mateusz

• Politechnika Opolska

Bibliografia

• [1] COOK S.A.: The complexity of theorem-proving procedures, Proceedings of the Third Annual ACM Symposium on the Theory of Computing, 1971, s. 151–158
• [2] DAVIS M., LOGEMANN G., LOVELAND D.: A machine program for theorem proving, Communications of the ACM, Vol. 5, 1962
• [3] MOSKEWICZ M.W., MADIGAN C.F., ZHAO Y., ZHANG L., MALIK S.: Chaff: Engineering an Efficient SAT Solver, Proc. of the 38th Design Automation Conference, 2001
• [4] PAPADIMITRIOU C.H.: Złożoność obliczeniowa, WNT, Warszawa 2007
• [5] SIPSER M.: Wprowadzenie do teorii obliczeń, WNT, Warszawa 2009
• [6] RYAN L.: Efficient algorithms for clause-learning sat solvers, Simon Fraser University, 2004 www.cs.sfu.ca/~mitchell/papers/ryan-thesis.ps
• [7] FINGER M.: SAT Solvers. A Brief Introduction, http://www.mat.unb.br/~ayala/MFingerSAT.pdf
• [8] LARROSA J., OLIVERAS A., RODRIGUEZ-CARBONELL E.: From DPLL to CDCL SAT solvers, http://www.lsi.upc.edu/~oliveras/RPAR/cdcl.pdf
• [9] PARAMESWARAN A., KUMAR L.: SAT Solvers, http://www.cfdvs.iitb.ac.in/download/Docs/verification/papers/sat/presentation.pdf
• [10] EEN N., SORENSSON N.: An Extensible SAT-solver, http://minisat.se/downloads/MiniSat.pdf
• [11] MITCHELL D. G.: A SAT Solver Primer http://www.cs.sfu.ca/~mitchell/papers/colLogCS85.pdf
• [12] BIERE A.: PicoSAT Essentials http://jsat.ewi.tudelft.nl/content/volume4/JSAT4_5_Biere.pdf
• [13] BEAME P., KAUTZ H., SABHARWAL A.: Understanding the Power of Clause Learning http://www.cs.washington.edu/homes/beame/papers/ijcai03.ps
• [14] SATLIB – Benchmark Problems, http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
• [15] SAT-Race 2008, http://baldur.iti.uka.de/sat-race-2008
• [16] The MiniSat Page http://minisat.se/