An Effective Local Search Algorithm for SAT Solving with CNF-XOR Formulas
Xin Xu , Jieyu Wu , Quan Zhang , Yiyuan Wang , Minghao Yin
As a fundamental problem in theoretical computer science, the Boolean satisfiability (SAT) problem has a wide range of applications in diverse fields. While the SAT problem is traditionally expressed in Conjunctive Normal Form (CNF), the CNF-XOR Formulas (denoted XNF), which combine OR and XOR clauses, provide a more compact and expressive representation for numerous real-world applications. Despite the progress made in solving XNF, the performance of local search methods still exhibits notable limitations when handling challenging instances. In this work, we present an effective local search algorithm called LS-XNF for XNF, which incorporates three key innovations. First, a novel variable selection strategy with a dedicated weighting scheme and scoring function is designed to select high-quality flipping variables. Second, a two- level search framework that alternates between spaces that consider and ignore XOR clauses. Finally, a fast perturbation mechanism to escape local optima and ensure search diversification. We conducted experiments on two challenge benchmarks derived from matrix multiplication and the DIMACS 32-bit parity problem. Experimental results demonstrate that LS-XNF outperforms state-of-the-art algorithms on most instances.
Boolean satisfiability / CNF-XOR Formulas / Local Search / Variable Selection Strategy / Two-level Search Framework / Perturbation Mechanism
Higher Education Press 2025
/
| 〈 |
|
〉 |
PDF
(1752KB)
