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

by Dave Tompkins

I will be presenting my recent work on developing a new model for representing Stochastic Local Search (SLS) algorithms for the satisfiability problem (SAT) that uses Variable Expressions (VEs) -- and the new software architecture we developed to design algorithms in this space.

This work corresponds to a chapter in my recently submitted PhD thesis, and will be presented at the upcoming 2010 SAT conference. The full paper is available here: http://people.cs.ubc.ca/~davet/papers/sat10-dave.pdf. The full abstract of my paper is as follows:
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.

Visit the LCI Forum page