Sciweavers

Share
SAT
2010
Springer

Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT

9 years 9 months ago
Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT
Abstract. We introduce a new conceptual model for representing and designing Stochastic Local Search (SLS) algorithms for the propositional satisfiability problem (SAT). Our model can be seen as a generalization of existing variable weighting, scoring and selection schemes; it is based upon the concept of Variable Expressions (VEs), which use properties of variables in dynamic scoring functions. Algorithms in our model are constructed from conceptually separated components: variable filters, scoring functions (VEs), variable selection mechanisms and algorithm controllers. To explore the potential of our model we introduce the Design Architecture for Variable Expressions (DAVE), a software framework that allows users to specify arbitrarily complex algorithms at runtime. Using DAVE, we can easily specify rich design spaces of SLS algorithms and subsequently explore these using an automated algorithm configuration tool. We demonstrate that by following this approach, we can achieve sig...
Dave A. D. Tompkins, Holger H. Hoos
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2010
Where SAT
Authors Dave A. D. Tompkins, Holger H. Hoos
Comments (0)
books