WANCE: Learnt Clause Evaluation Method for SAT Solver Using Graph Structure
摘要
Effective evaluation of learnt clauses is crucial for the performance of conflict-driven clause learning SAT solvers. We propose a novel learnt clause evaluation method using the information of the graph structure of SAT problem, called weight to adjacent node-based clause evaluation (WANCE). The graph representation of SAT problems is recognized as useful for understanding the structure of the problems, and it is known that the efficiency of SAT solvers is related to this structure. WANCE utilizes the problem structure of the input CNF, which can identify valuable clauses independently of their search, contrary to existing methods (e.g., literal block distance, LBD) reliant on a search tree state for their evaluation values. First, to reveal the relationship between learnt clauses and graph structure in more detail, we investigated the impact of a learnt clause on the graph structure through correlation analysis with its quality measured by LBD. Findings indicated that high-quality clauses had heavy edges to their adjacent variables on the graph, enhancing their propagation potential. Second, assuming that that feature implied clause quality, we implemented WANCE using the feature as the primary metric for clause management. The results of performance evaluation experiments demonstrated that a solver equipped with WANCE outperformed those using LBD-based methods. Our findings underscore the potential of utilizing the graph-structural properties of SAT problems for clause evaluation.