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 metadatas

https://hal-amu.archives-ouvertes.fr/hal-01479538
Contributor : William Domingues Vinhas <>
Submitted on : Tuesday, February 28, 2017 - 8:38:47 PM
Last modification on : Wednesday, September 12, 2018 - 1:26:31 AM

Identifiers

  • HAL Id : hal-01479538, version 1

Citation

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⟩

Share

Metrics

Record views

149