An effective SAT-Solving mechanism with backtrack controlled by FDL

• Autorzy: Pułka A.

Warianty tytułu

PL

Efektywny mechanizm kontroli spełnialności formuł logicznych z nawrotem sterowanym logiką FDL

• Konferencja: Mixed Design of Integrated Circuits and Systems MIXDES 2011 (18 ; 16-18.06.2011 ; Gliwice, Poland)
• Języki publikacji: EN

Abstrakty

EN

This work presents a novel approach to SAT solving problem based on commonsense reasoning methodology. The methodology has been implemented and tested in PROLOG. Discussion of different modern approaches to the satisfiability that have been published recently is presented. A parallelism between the SAT solving problem and non-monotonic extensions verifying is given. The new algorithm of SAT solving based on fuzzy default reasoning (FDL) theory FUDASAT and cumulativity of CNF formulas is defined. Optimal backtracking search methodology is explained on examples. Some experiments on various benchmarks show the efficiency and advantages of the proposed methodology.

PL

Artykuł przedstawia nowe podejście do problemu badania spełnialności formuł logicznych oparte na metodzie wnioskowania zdroworozsądkowego. Zaproponowana metoda została zaimplementowana i przetestowana w środowisku języka PROLOG. Przeprowadzono szczegółową dyskusję dotyczącą istniejących nowoczesnych technik sprawdzania spełnialności formuł logicznych, które zostały opublikowane w ostatnich latach. Przedstawiono podobieństwa między problemem badania spełnialności formuł logicznych a weryfikacją rozszerzeń w logice niemonotonicznej. Sformułowano podstawowe założenia nowego algorytmu FUDASAT badania spełnialności formuł logicznych opartego na wnioskowaniu FDL oraz zdefiniowano problem kumulacyjności formuł w postaci normalnej CNF. Metoda optymalnego przeszukiwania podczas nawrotów została opisana na przykładach. Eksperymenty przeprowadzone na zestawach wzorcowych pokazują zalety proponowanej metody.

Słowa kluczowe

EN

SAT solving; formal verification; CNF; Boolean satisfiability

PL

badanie spełnialności logicznej; weryfikacja formalna; logiczne formuły w postaci CNF

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Elektronika : konstrukcje, technologie, zastosowania
• Rocznik: 2011
• Tom: Vol. 52, nr 12
• Strony: 21--25
• Opis fizyczny: Bibliogr. 15 poz., il., wykr., rys.

Twórcy

autor

Pułka A.

• Politechnika Śląska, Instytut Elektroniki, Gliwice

Bibliografia

• [1] Davis M., Putnam H.: A computing procedure for quantification theory. Journal of the ACM 7, 1960, pp. 201-215.
• [2] Davis M., Logemann G., Loveland D.: A machine program for theorem proving. Communications of the ACM 5, 1962, pp. 394-397.
• [3] Brewka. G.: Cumulative Default Logic: in defence of nonmonotonic inference rules. Artificial Intelligence 50 (1991), pp. 183-205.
• [4] Puika A., Pawlak A.: Experiences with VITAL Code Generator Controlled by a Nonmonotonic Inference Engine. Proceedings of 2nd WORKSHOP on Libraries Component Modelling and Quality Assurance with CHDL'97 and VHDL Forum.Toledo, Spain, April 20-25, 1997.
• [5] Solving satisfiability problems on FPGAs using experimental unit propagation heuristic. Parallel and Distributed Processing, Lecture Notes in Computer Science, Takayuki Suyama, Makoto Yokoo and Akira Nagoya (editors), Springer Berlin, Heidelberg, 1999.
• [6] Marques-Silva J. P., Sakallah K. A.: GRASP: a search algorithm for prepositional satisfiability. IEEE Transactions on Computers, vol.48, no.5, May 1999, pp. 506-521.
• [7] Moskewicz M. W., Madigan C. F., Zhao Y., Zhang L., Malik S.: Chaff: engineering an efficient SAT solver. Proceedings of Design Automation Conference 2001, pp. 530-535.
• [8] Aloul R. A., Mneimneh M. N., Sakallah K. A.: ZBDD-Based Backtrack Search SAT Solver. Proceedings of International Workshop on Logic Synthesis, Lake Tahoe, California, May 2002, pp. 131-136.
• [9] Balduccini M., Gelfond M., Nogueira M.: Answer Set Based Design of Knowledge Systems. Annals of Mathematics and Artificial Intelligence, vol. 47, no. 1-2, pp. 183-219.
• [10] Cong J. and Minkovich K.: Improved SAT-Based Boolean Matching Using Implicants for LUT-Based FPGAs. Proceedings of the 15th ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Monterey, CA, February 2007, pp. 139-147.
• [11] Yu Hu, Shih V., Majumdar R., Lei He: Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,, vol. 27, no.10, Oct. 2008, pp. 1751-1760.
• [12] Putka A., Milik A.: Hardware Implementation of Fuzzy Default Logic, in: Human-Computer Systems Interaction Backgrounds and Applications II, Series: Advances in Intelligent and Soft Computing, (accepted for publication), Hippe, Z S., Kulikowski, J. L. (Eds.), Springer Verlag 2011
• [13] Tille D., Eggersgluss S., Drechsler R.: Incremental Solving Techniques for SAT-based ATPG. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 29, no. 7, July 2010, pp. 1125-1130.
• [14] Hyojung Han, Somenzi F., Hoonsang Jin: Making Deduction More Effective in SAT Solvers. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 29, no. 8, Aug. 2010, pp.1271-1284.
• [15] Benchmarks database: from DIMACS implementation challenge available at: http://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf/