Implementing an Efficient SAT Solver for Structured Instances

摘要

As many problems can be solved by converting it into Boolean Satisfiability (SAT), building an efficient SAT solver is a big challenge. Different solvers are built to overcome the challenge and most of them compete on SAT competition. In this paper, we have proposed a stochastic local search (SLS) solver for SAT named CCAnrSim which performs well for structured benchmarks. A new metaheuristic named similarity checking (SC) is incorporated within the CCAnr framework to handle the cycling problem of SLS. Experimental results show that our proposed solver outperforms the state-of-the-art solvers in several aspects.