A study of local minimum avoidance heuristics for SAT

Thach Thao Duong, Duc Nghia Pham, Abdul Sattar

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Citations (Scopus)
11 Downloads (Pure)

Abstract

Stochastic local search for satisfiability (SAT) has successfully been applied to solve a wide range of problems. However, it still suffers from a major shortcoming, i.e. being trapped in local minima. In this study, we explore different heuristics to avoid local minima. The main idea is to proactively avoid local minima rather than reactively escape from them. This is worthwhile because it is time consuming to successfully escape from a local minimum in a deep and wide valley. In addition, revisiting an encountered local minimum several times makes it worse. Our new trap avoidance heuristics that operate in two phases: (i) learning of pseudo-conflict information at each local minimum, and (ii) using this information to avoid revisiting the same local minimum. We present a detailed empirical study of different strategies to collect pseudo-conflict information (using either static or dynamic heuristics) as well as to forget the outdated information (using naive or time window smoothing). We select a benchmark suite that includes all random and structured instances used in the 2011 SAT competition and three sets of hardware and software verification problems. Our results show that the new heuristics significantly outperform existing stochastic local search solvers (including Sparrow2011 - the best local search solver for random instances in the 2011 SAT competition) on all tested benchmarks.

Original languageEnglish
Title of host publicationECAI 2012 - 20th European Conference on Artificial Intelligence, 27-31 August 2012, Montpellier, France - Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstration
EditorsLuc De Raedt, Christian Bessiere, Didier Dubois, Patrick Doherty, Paolo Frasconi, Fredrik Heintz, Peter Lucas
Place of PublicationAmsterdam
PublisherIOS PRESS
Pages300-305
Number of pages6
ISBN (Electronic)9781614990987
ISBN (Print)9781614990970
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event20th European Conference on Artificial Intelligence, ECAI 2012 - Montpellier, France
Duration: 27 Aug 201231 Aug 2012

Publication series

NameFrontiers in Artificial Intelligence and Applications
Volume242
ISSN (Print)0922-6389

Conference

Conference20th European Conference on Artificial Intelligence, ECAI 2012
Country/TerritoryFrance
CityMontpellier
Period27/08/1231/08/12

Fingerprint

Dive into the research topics of 'A study of local minimum avoidance heuristics for SAT'. Together they form a unique fingerprint.

Cite this