Combining Adaptive and Dynamic Local Search for Satisfiability

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 G2 WSAT, 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: AdaptG2 WSAT0, G2 WSAT and AdaptNovelty+ , and two of the most representative DLS solvers: RSAPS and PAWS. Our new results augment the SAT competition results and show that gNo...

• Type: Journal
• Year: 2008
• Where: JSAT
• Authors: Duc Nghia Pham, John Thornton, Charles Gretton, Abdul Sattar
• Keywords: Algorithm, JSAT 2008, Local Search, SAT Competition