关键词: 配置检测, 重要邻居数组, 可满足性问题, SAT求解器, 变量决策策略

Abstract: In stochastic local search algorithms for SAT problems,mainstream variable decision strategies rely on probabilistic variable selection,such as the probSAT solver,which determines selection probabilities by calculating the break value of vari-ables.However,this approach is prone to falling into local optima,particularly underperforming in application-oriented problems.To address this,a variable decision method incorporating a configuration detection strategy is proposed,dynamically adjusting the variable selection probability function.When the environment remains unchanged,variables with lower break values are prioritized,enhancing global optimization capabilities.To tackle the high scanning overhead of long clauses,an important neighbor array strategy is introduced,incorporating highly active variables into the array to reduce computational complexity.Additionally,a restart mechanism is designed to leverage the advantage of probSAT in rapidly reducing the number of unsatisfied clauses during the initial phase,avoiding the global repeated flipping phenomenon in later stages,thereby improving solving efficiency.The improved probSAT_PCCR solver demonstrates significant performance enhancements in long-unsolved mathematical application problem tests,solving 142 more cases than the original probSAT,with a performance improvement of 546.1%.In practical application problem tests conducted by the FCC,it solves 1 596 more cases,with a performance improvement of 33.5%.In summary,the enhanced probSAT solver,through multiple strategic improvements,achieves substantial performance gains in solving application-oriented SAT problems,demonstrating significant application value.

Key words: Configuration detection, Important neighbor array, Satisfiability problem, SAT solver, Variable decision strategy