Clause states based configuration checking in local search for satisfiability.

Area of Science:

• Computer Science
• Artificial Intelligence
• Algorithm Design

Background:

• Stochastic Local Search (SLS) and Focused Random Walk (FRW) are key paradigms for solving the propositional satisfiability (SAT) problem.
• Configuration Checking (CC) is a technique to address cycling issues in SLS algorithms, enhancing SAT solver performance.

Purpose of the Study:

• To introduce a novel Configuration Checking (CC) strategy based on clause states (CSCC) for SLS algorithms.
• To adapt and evaluate the CSCC strategy for both two-mode SLS and FRW paradigms in SAT solving.
• To improve the performance of FRW algorithms for SAT by integrating the CSCC strategy.

Main Methods:

• Developed a new Configuration Checking (CC) strategy utilizing clause states (CSCC).
• Applied the CSCC strategy to both two-mode SLS and FRW algorithms for SAT.
• Conducted extensive experiments to evaluate the effectiveness of CSCC on various SAT benchmarks.

Main Results:

• The CSCC strategy proved effective across both two-mode SLS and FRW algorithms.
• FRW algorithms enhanced with CSCC demonstrated state-of-the-art performance on random SAT benchmarks.
• The proposed CSCC strategy overcomes limitations of previous neighboring variable-based CC methods for FRW.

Conclusions:

• Clause states based Configuration Checking (CSCC) is a viable and effective enhancement for SLS algorithms in SAT solving.
• The CSCC strategy significantly improves FRW algorithms, leading to state-of-the-art performance.
• This research presents a novel approach to configuration checking applicable to diverse SLS paradigms for SAT.