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...

• Type: Conference
• Year: 2010
• Where: SAT
• Authors: Dave A. D. Tompkins, Holger H. Hoos
• Keywords: Algorithm, Hardware, SAT 2010, Scoring Functions, Variable Expressions