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 significant improvements over
previous state-of-the-art SLS-based SAT solvers on
software verification benchmark instances from the
literature.