Improving Configuration Checking for Satisfiable Random k-SAT Instances - Aix-Marseille Université Accéder directement au contenu
Article Dans Une Revue Annals of Mathematics and Artificial Intelligence Année : 2017

Improving Configuration Checking for Satisfiable Random k-SAT Instances

Résumé

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.
Fichier non déposé

Dates et versions

hal-01479538 , version 1 (28-02-2017)

Identifiants

  • HAL Id : hal-01479538 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More