You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Combining Adaptive and Dynamic Local Search for Satisfiability

Issue title: 2007 Competitions

Guest editors: Ewald Speckenmeyer, Chu Min Li, Vasco Manquinho and Armando Tacchella

Article type: Research Article

Authors: Nghia Pham, Duca | Thornton, Johnb | Gretton, Charlesc | Sattar, Abduld

Affiliations: [a] SAFE Program, Queensland Research Laboratory, NICTA Ltd., Australia. E-mail: [email protected] | [b] Institute for Integrated and Intelligent Systems, Griffith University, Australia. E-mail: [email protected] | [c] SAFE Program, Queensland Research Laboratory, NICTA Ltd., Australia. E-mail: [email protected] | [d] Institute for Integrated and Intelligent Systems, Griffith University, Australia. E-mail: [email protected]

Keywords: SAT-solver, local search, clause weighting, adaptive heuristic

DOI: 10.3233/SAT190042

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 149-172, 2008

Received 1 October 2007
|
Revision received 1 January 2008
|
Published: 1 May 2008
Get PDF open access

Abstract

In this paper we describe a stochastic local search (SLS) procedure for finding models of satisfiable propositional formulae. This new algorithm, gNovelty+, draws on the features of two other WalkSAT family algorithms: AdaptNovelty+ and G2WSAT, while also successfully employing a hybrid clause weighting heuristic based on the features of two dynamic local search (DLS) algorithms: PAWS and (R)SAPS.

gNovelty+ was a Gold Medal winner in the random category of the 2007 SAT competition. In this paper we present a detailed description of the algorithm and extend the SAT competition results via an empirical study of the effects of problem structure, parameter tuning and resolution preprocessors on the performance of gNovelty+. The study compares gNovelty+ with three of the most representative WalkSAT-based solvers: AdaptG2WSAT0, G2WSAT and AdaptNovelty+, and two of the most representative DLS solvers: RSAPS and PAWS. Our new results augment the SAT competition results and show that gNovelty+ is also highly competitive in the domain of solving structured satisfiability problems in comparison with other SLS techniques.

Show more