Improving Configuration Checking for Satisfiable Random k-SAT Instances - Archive ouverte HAL Access content directly
Journal Articles Annals of Mathematics and Artificial Intelligence Year : 2017

Improving Configuration Checking for Satisfiable Random k-SAT Instances

, (1, 2) ,
1
2

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.
Not file

Dates and versions

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

Identifiers

  • HAL Id : hal-01479538 , version 1

Cite

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⟩
83 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More