Old Resolution Meets Modern SLS

A. Anbulagan, Duc Nghia Pham, John Slaney, Abdul Sattar

Recent work on Stochastic Local Search (SLS) for the SAT and CSP domains has shown the importance of a dynamic (non-markovian) strategy for weighting clauses in order to escape from local minima. In this paper, we improve the performance of two best contemprorary clause weighting solvers, PAWS and SAPS, by integrating a propositional resolution procedure. We also extend the work to AdaptNovelty+, the best non-weighting SLS solver in the GSAT/WalkSAT series. One outcome is that our systems can solve some highly structured problems such as quasigroup existence and parity learning problems which were previously thought unsuitable for local search and which are completely out of reach of traditional solvers such as GSAT. Here we present empirical results showing that for a range of random and real-world benchmark problems, resolution-enhanced SLS solvers clearly outperform the alternatives.

Content Area: 6. Constraint Satisfaction and Satisfiability

Subjects: 15.2 Constraint Satisfaction; 15.7 Search

Submitted: May 9, 2005

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.