Selection of search strategies for solving 3-SAT problems

Pułka, A.

International Journal of Applied Mathematics and Computer Science, Tome 24 (2014) no. 2, pp. 283-297.

Résumé

The paper concerns the problem of Boolean satisfiability checking, which is recognized as one of the most important issues in the field of modern digital electronic system verification and design. The paper analyzes different strategies and scenarios of the proving process, and presents a modified and extended version of the author’s FUDASAT algorithm. The original FUDASAT methodology is an intuitive approach that employs a commonsense reasoning methodology. The main objective of the work is to investigate the SAT-solving process and try to formulate a set of rules controlling the reasoning process of the FUDASAT inference engine. In comparison with the author’s previous works, the paper introduces new mechanisms: hypergraph analysis, multiple variable assignments and search space pruning algorithms. The approach considers only 3-SAT class functions, although a generalization of the method is discussed as well. The presented approach has been tested on various benchmarks and compared with the original pure FUDASAT algorithm as well as with other algorithms known from the literature. Finally, the benefits of the proposed SAT solving technique are summarized.

Détail

Keywords: SAT solving, formal verification, CNF, Boolean satisfiability
Mots-clés : badanie spełnialności logicznej, weryfikacja formalna, CNF

Bibliographie

[1] Aloul, F., Mneimneh, M. and Sakallah, K. (2002). ZBDD-based backtrack search SAT solver, Proceedings of the International Workshop on Logic Synthesis, Lake Tahoe, CA, USA, pp. 131–136.

[2] Arangú, M. and Salido, M.A. (2011). A fine-grained arc-consistency algorithm for non-normalized constraint satisfaction problems, International Journal of Applied Mathematics and Computer Science 21(4): 733–744, DOI: 10.2478/v10006-011-0058-2.

[3] Balduccini, M., Gelfond, M. and Nogueira, M. (2006). Answer set based design of knowledge systems, Annals of Mathematics and Artificial Intelligence 47(1–2): 183–219.

[4] Brewka, G. (1991). Cumulative default logic: In defense of nonmonotonic inference rules, Artificial Intelligence 50(2): 183–205.

[5] Davis, M., Logemann, G. and Loveland, D. (1962). A machine program for theorem proving, Communications of the ACM 5(7): 394–397.

[6] Davis, M. and Putnam, H. (1960). A computing procedure for quantification theory, Journal of the ACM 7(3): 201–215.

[7] DIMACS (1993). CNF benchmarks database, ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf/.

[8] Gelfond, M. and Lifschitz, V. (1988). The stable model emantics for logic programming, in R.A. Kowalski and K.A. Bowen (Eds.), Proceedings of the International Logic Programming Conference and Symposium, MIT Press, Cambridge, MA, pp. 1070–1080.

[9] Han, H., Somenzi, F. and Jin, H. (2010). Making deduction more effective in SAT solvers, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 29(8): 1271–1284.

[10] Hu, Y., Shih, V., Majumdar, R. and He, L. (2008). 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 27(10): 1751–1760.

[11] Lukasiewicz, T. and Straccia, U. (2008). Tightly coupled fuzzy description logic programs under the answer set semantics for the semantic web, International Journal on Semantic Web and Information Systems 4(3): 68–89.

[12] Marques-Silva, J. and Sakallah, K. (1999). GRASP: A search algorithm for propositional satisfiability, IEEE Transactions on Computers 48(5): 506–521.

[13] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L. and Malik, S. (2001). Chaff: Engineering an efficient SAT solver, Proceedings of the Design Automation Conference, Las Vegas, NV, USA, pp. 530–535.

[14] Opara, A. and Kania, D. (2010). Decomposition-based logic synthesis for PAL-based CPLDs, International Journal of Applied Mathematics and Computer Science 20(2): 367–384, DOI: 10.2478/v10006-010-0027-1.

[15] Pułka, A. (2009). Decision supporting system based on fuzzy default reasoning, Proceedings of the IEEE Human Systems Interaction Conference, HSI’09, Catania, Italy, pp. 32–39.

[16] Pułka, A. (2011). An effective SAT-solving mechanism with backtrack controlled by FDL, Proceedings of the 18th International Conference on Mixed Design of Integrated Circuits and Systems (MIXDES), Gliwice, Poland, pp. 252–257.

[17] Reiter, R. (1980). A logic for default reasoning, Artificial Intelligence 13(1): 81–132.

[18] Suyama, T., Yokoo, M. and Nagoya, A. (1999). Solving satisfiability problems on FPGAs using experimental unit propagation heuristic, parallel and distributed processing, in J. Rolim (Ed.), Parallel and Distributed Processing, Lecture Notes in Computer Science, Vol. 1586, Springer-Verlag, Berlin, pp. 709–711.

[19] Tille, D., Eggersgluss, S. and Drechsler, R. (2010). Incremental solving techniques for SAT-based ATPG, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 29(7): 1125–1130.

[20] Wyrwoł, B. and Hrynkiewicz, E. (2013). Decomposition of the fuzzy inference system for implementation in the FPGA structure, International Journal of Applied Mathematics and Computer Science 23(2): 473–483, DOI: 10.2478/amcs-2013-0036.

[21] Yin, L., He, F., Hung,W., Song, X. and Gu, M. (2012). Maxterm covering for satisfiability, IEEE Transactions on Computers 61(3): 420–426.

[22] Zadeh, L.A. (2006). Generalized theory of uncertainty (GTU)—principal concepts and ideas, Computational Statistics and Data Analysis 51(1): 15–46.

[23] Zadeh, L.A. (2008). Is there a need for fuzzy logic?, Information Sciences: An International Journal 178(13): 2751–2779.