×

Selection of search strategies for solving 3-SAT problems. (English) Zbl 1293.68253

Summary: 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.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C09 Boolean programming

Software:

Chaff
PDFBibTeX XMLCite
Full Text: DOI

References:

[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 Science21(4): 733-744, DOI: 10.2478/v10006-011-0058-2.; · Zbl 1288.90090
[3] Balduccini, M., Gelfond, M. and Nogueira, M. (2006). Answer set based design of knowledge systems, Annals of Mathematics and Artificial Intelligence47(1-2): 183-219.; · Zbl 1105.68105
[4] Brewka, G. (1991). Cumulative default logic: In defense of nonmonotonic inference rules, Artificial Intelligence50(2): 183-205.; · Zbl 0753.03011
[5] Davis, M., Logemann, G. and Loveland, D. (1962). A machine program for theorem proving, Communications of the ACM5(7): 394-397.; · Zbl 0217.54002
[6] Davis, M. and Putnam, H. (1960). A computing procedure for quantification theory, Journal of the ACM7(3): 201-215.; · Zbl 0212.34203
[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 semantics 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 Systems29(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 Systems27(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 Systems4(3): 68-89.;
[12] Marques-Silva, J. and Sakallah, K. (1999). GRASP: A search algorithm for propositional satisfiability, IEEE Transactions on Computers48(5): 506-521.; · Zbl 1392.68388
[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 Science20(2): 367-384, DOI: 10.2478/v10006-010-0027-1.; · Zbl 1194.94207
[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 Intelligence13(1): 81-132.; · Zbl 0435.68069
[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 Systems29(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 Science23(2): 473-483, DOI: 10.2478/amcs-2013-0036.; · Zbl 1282.93164
[21] Yin, L., He, F., Hung, W., Song, X. and Gu, M. (2012). Maxterm covering for satisfiability, IEEE Transactions on Computers61(3): 420-426.; · Zbl 1365.68293
[22] Zadeh, L.A. (2006). Generalized theory of uncertainty (GTU)—principal concepts and ideas, Computational Statistics and Data Analysis51(1): 15-46.; · Zbl 1157.62312
[23] Zadeh, L.A. (2008). Is there a need for fuzzy logic?, Information Sciences: An International Journal178(13): 2751-2779.; · Zbl 1148.68047
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.