Advancing stochastic 3-SAT solvers by dissipating oversatisfied constraints.

Area of Science:

• Computer Science
• Artificial Intelligence
• Computational Complexity

Background:

• The 3-SAT problem is a fundamental Nondeterministic Polynomial Time (NP)-complete problem.
• Existing stochastic local search heuristics like WalkSAT can get trapped in local minima.
• Local minima in 3-SAT are often characterized by a high number of oversatisfied constraints.

Purpose of the Study:

• Introduce and benchmark a novel stochastic local search heuristic for 3-SAT.
• Address the limitation of existing solvers getting stuck in local minima.
• Improve performance on critically hard 3-SAT instances.

Main Methods:

• Developed a new algorithm, Dissipates Oversatisfied Constraints SAT (DOCSAT).
• DOCSAT focuses on reducing the abundance of oversatisfied constraints to escape local minima.
• Benchmarked DOCSAT against established solvers like WalkSAT and Kissat on randomly generated hard satisfiable 3-SAT instances up to N=15,000.

Main Results:

• DOCSAT significantly outperforms WalkSAT and other solvers on critically hard 3-SAT instances.
• DOCSAT demonstrates superior performance even when compared against the average performance of competitors on the hardest instances.
• The algorithm effectively avoids local minima by dissipating oversatisfied constraints.

Conclusions:

• DOCSAT represents a substantial improvement for solving difficult 3-SAT instances.
• The core mechanism of DOCSAT harnesses statistical structure to escape local minima.
• The approach offers potential for generalization to other complex combinatorial optimization problems.