HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Improving Configuration Checking for Satisfiable Random k-SAT Instances

Abstract : Local search algorithms based on the Configuration Checking (CC) strategy have been shown to be efficient in solving satisfiable random k-SAT instances. The purpose of the CC strategy is to avoid the cycling problem, which corresponds to revisiting already flipped variables too soon. It is done by considering the neighborhood of the formula variables. In this paper, we propose to improve the CC strategy on the basis of an empirical study of a powerful algorithm using this strategy. The first improvement introduces a new and simple criterion, which refines the selection of the variables to flip for the 3-SAT instances. The second improvement is achieved by using the powerful local search algorithm Novelty with the adaptive noise setting. This algorithm enhances the efficiency of the intensification and diversification phases when solving k-SAT instances with k>= 4. We name the resulting local search algorithm \texttt{Ncca+} and show its effectiveness when treating satisfiable random k-SAT instances issued from the SAT Challenge 2012. Ncca+ won the bronze medal of the random SAT track of the SAT Competition 2013.
Complete list of metadata

Contributor : William Domingues Vinhas Connect in order to contact the contributor
Submitted on : Tuesday, February 28, 2017 - 8:38:47 PM
Last modification on : Wednesday, November 3, 2021 - 9:37:44 AM


  • HAL Id : hal-01479538, version 1


André Abrame, Djamal Habet, Donia Toumi Gatfaoui. Improving Configuration Checking for Satisfiable Random k-SAT Instances. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2017, 79 (1-3). ⟨hal-01479538⟩



Record views