Research on Abstraction-Based Search Space Partitioning and Solving Satisfiability Problems

Solving satisfiability problems is central to many areas of computer science, including artificial intelligence and optimization. Efficiently solving satisfiability problems requires exploring vast search spaces, where search space partitioning plays a key role in improving solving efficiency. This paper defines search spaces and their partitioning, focusing on the relationship between partitioning strategies and satisfiability problem solving. By introducing an abstraction method for partitioning the search space—distinct from traditional assignment-based approaches—the paper proposes sequential, parallel, and hybrid solving algorithms. Experimental results show that the hybrid approach, combining abstraction and assignment, significantly accelerates solving in most cases. Furthermore, a unified method for search space partitioning is presented, defining independent and complete partitions. This method offers a new direction for enhancing the efficiency of SAT problem solving and provides a foundation for future research in the field.