A Topological Parallel Algorithm for the Pure Literal Rule in the Satisfiability Problem Solving Using a Matrix-Based Approach

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.