A Topological Parallel Algorithm for the Pure Literal Rule in the Satisfiability Problem Solving Using a Matrix-Based Approach
Source abstract
Abstract
The Satisfiability Problem (SAT), a fundamental NP-complete problem, is widely applied in integrated circuit verification, artificial intelligence planning, and other fields, where the growing scale and complexity of practical problems demand higher solving efficiency. Due to redundant search paths, serialized reasoning steps, and inefficient pure literal detection, traditional serial SAT solvers require efficient parallelization of the pure literal rule. This paper adopts a parallel solving algorithm for the pure literal rule based on matrix representation. The algorithm can solve the shortcomings of poor universality, insufficient parallel collaborative mechanisms, and clause reduction. We first introduce a Clause-Numerical Incidence Matrix (CNIM) representation to provide a unified mathematical model for parallel operations. Second, we design a Column Vectors Pure Literal Parallel Topological Detection (CVPLPTD) algorithm that achieves pure literal detection with O(mn/p) time complexity (p being the number of parallel threads) within the coefficient range [1.0×mn/p, 1.2×mn/p]. Finally, we adopt a dynamic matrix reduction strategy that compresses the matrix scale through row and column deletion after each pure literal assignment to reduce computational load. These innovations integrate matrix algebra and parallel computing, effectively breaking through the efficiency limitations of solving large-scale SAT problems while ensuring good universality across different computing platforms.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Formal Methods in Verification · Constraint Satisfaction and Optimization · Embedded Systems Design Techniques
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
School of Mathematics, Hefei University of Technology, Hefei 230071, China
School of Computer and Artificial Intelligence, Hainan College of Software Technology, Qionghai 571400, China
Funding
Education Department of Hainan Province
References (25)
Show source-provided references
1. Cook, S.A. (1971, January 3–5). The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, OH, USA.
2. Biere, A., Cimatti, A., Clarke, E.M., and Zhu, Y. (1999, January 22–28). Symbolic Model Checking without BDDs. Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Lisbon, Portugal.10.1007/3-540-49059-0_14 ↗
3. Kautz, H.A., and Selman, B. (September, January 29). Planning as Satisfiability. Proceedings of the 10th European Conference on Artificial Intelligence, Vienna, Austria.
4. Using Bayesian Networks to Analyze Expression Data10.1089/106652700750050961 ↗
5. A Theory of Diagnosis from First Principles10.1016/0004-3702(87)90062-2 ↗
6. Lassez, J.-L., and Plotkin, G. (1991). Inductive Inference of Theories from Facts. Computational Logic: Essays in Honor of Alan Robinson, MIT Press.
7. Boneh, D., and Franklin, M. (2001, January 19–23). Identity-Based Encryption from the Weil Pairing. Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, Lecture Notes in Computer Science, Santa Barbara, CA, USA.10.1007/3-540-44647-8_13 ↗
8. van Harmelen, F., Lifschitz, V., and Porter, B. (2008). Satisfiability Solvers. Handbook of Knowledge Representation, Elsevier.
9. Eén, N., and Sörensson, N. (2003, January 5–8). An Extensible SAT-solver. Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, Santa Margherita Ligure, Italy.
10. Audemard, G., and Simon, L. (2009, January 11–17). Predicting Learnt Clauses Quality in Modern SAT Solvers. Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, CA, USA.
11. Zhang, L., Madigan, C.F., Moskewicz, M.W., and Malik, S. (2001, January 4–8). Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, San Jose, CA, USA.
12. GRASP: A Search Algorithm for Propositional Satisfiability10.1109/12.769433 ↗
13. Gogate, V., and Dechter, R. (2004, January 25–29). Distributed Constraints: A Survey. Proceedings of the 19th National Conference on Artificial Intelligence, San Jose, CA, USA.
14. Zulkoski, P., Burnette, D., and Ganesh, V. (2010, January 11–14). Accelerating SAT Solvers with Graphics Processors. Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, Edinburgh, UK.
15. Parallel Pure Literal Detection for SAT Solving Based on Bit Vector Operations
16. Wang, Z., Liu, J., and Li, S. (December, January 29). Clause Implication Detection Using Sparse Matrix Multiplication for SAT Solving. Proceedings of the 2020 IEEE 19th International Conference on Trust, Security and Privacy in Computing and Communications, Guangzhou, China.
17. Jain, S., Neoh, T.Y., and Stephan, F. (2024). An Improved Algorithm for Sparse Instances of SAT. arXiv.
18. Davey, B.A., and Priestley, H.A. (2002). Introduction to Lattices and Order, Cambridge University Press.10.1017/CBO9780511809088 ↗
19. Grätzer, G. (2011). Lattice Theory: Foundation, Birkhäuser.10.1007/978-3-0348-0018-1 ↗
20. Burris, S., and Sankappanavar, H.P. (1981). A Course in Universal Algebra, Springer.10.1007/978-1-4613-8130-3 ↗
21. Halmos, P.R. (1974). Boolean Algebras, Springer.10.1007/978-1-4612-9855-7_2 ↗
22. Sikorski, R. (1964). Boolean Algebras, Springer.
23. Hungerford, T.W. (1974). Algebra, Springer.10.1007/978-1-4612-6101-8 ↗
24. Dummit, D.S., and Foote, R.M. (2004). Abstract Algebra, John Wiley & Sons.
25. Kleine Büning, H., and Lettmann, T. (1999). Propositional Logic: Deduction and Algorithms, Cambridge University Press.