Configuration Checking with Aspiration in Local Search for SAT
Author(s)
Su, Kaile
Cai, Shaowei
Griffith University Author(s)
Year published
2012
Metadata
Show full item recordAbstract
An interesting strategy called configuration checking (CC) was recently proposed to handle the cycling problem in local search for Minimum Vertex Cover. A natural question is whether this CC strategy also works for SAT. The direct application of CC did not result in stochastic local search (SLS) algorithms that can compete with the current best SLS algorithms for SAT. In this paper, we propose a new heuristic based on CC for SLS algorithms for SAT, which is called configuration checking with aspiration (CCA). It is used to develop a new SLS algorithm called Swcca. The experiments on random 3-SAT instances show that Swcca ...
View more >An interesting strategy called configuration checking (CC) was recently proposed to handle the cycling problem in local search for Minimum Vertex Cover. A natural question is whether this CC strategy also works for SAT. The direct application of CC did not result in stochastic local search (SLS) algorithms that can compete with the current best SLS algorithms for SAT. In this paper, we propose a new heuristic based on CC for SLS algorithms for SAT, which is called configuration checking with aspiration (CCA). It is used to develop a new SLS algorithm called Swcca. The experiments on random 3-SAT instances show that Swcca significantly outperforms Sparrow2011, the winner of the random satisfiable category of the SAT Competition 2011, which is considered to be the best local search solver for random 3-SAT instances. Moreover, the experiments on structured instances show that Swcca is competitive with Sattime, the best local search solver for the crafted benchmark in the SAT Competition 2011.
View less >
View more >An interesting strategy called configuration checking (CC) was recently proposed to handle the cycling problem in local search for Minimum Vertex Cover. A natural question is whether this CC strategy also works for SAT. The direct application of CC did not result in stochastic local search (SLS) algorithms that can compete with the current best SLS algorithms for SAT. In this paper, we propose a new heuristic based on CC for SLS algorithms for SAT, which is called configuration checking with aspiration (CCA). It is used to develop a new SLS algorithm called Swcca. The experiments on random 3-SAT instances show that Swcca significantly outperforms Sparrow2011, the winner of the random satisfiable category of the SAT Competition 2011, which is considered to be the best local search solver for random 3-SAT instances. Moreover, the experiments on structured instances show that Swcca is competitive with Sattime, the best local search solver for the crafted benchmark in the SAT Competition 2011.
View less >
Conference Title
Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence
Publisher URI
Subject
Artificial intelligence not elsewhere classified