Search Results

The Boolean Satisfiability (SAT) problem is a fundamental NP-complete problem. Algorithms for SAT include complete ones, typically based on Conflict-Driven Clause Learning (CDCL) methods, and incomplete ones, mostly following local search frameworks. CDCL solvers perform very well on complex structured instances. Local search (LS) algorithms cannot compete with CDCL solvers on structured instances, but show good performance on random and crafted instances, and also serve as an important component in top CDCL solvers. This raises a natural question: can techniques from complete SAT solving be used to improve incomplete solvers? This paper proposes the PALSAT (Progressive Activation Local Search for SAT) incomplete solver to answer it, which integrates the core techniques from both sides, Unit Propagation (UP) and LS. PALSAT starts from a subproblem, which relaxes many variables, and uses UP to progressively activate the search space (i.e., expand the subproblem). When a conflict is encountered, LS is invoked to repair it by searching all variables induced in the subproblem and the conflict. PALSAT ensures that the subproblem size increases monotonically and that the search process gradually approaches the full formula. In PALSAT, UP can guide growth direction based on the structure, and LS can efficiently repair conflicts. Their cooperation leads to some promising results. After a decade of evolution in CCAnr and probSAT variants, PALSAT represents a new incomplete algorithm framework with significantly better performance across various benchmarks.