Latest revision as of 11:06, 12 December 2011

Automated Synthesis of Propositional Satisfiability Solvers

Doug Smith

Last year we carried out automated derivations of several SAT solvers using Kestrel's Specware system. We were able to recapitulate many of the key design features of modern DPLL SAT solvers using abstract and reusable design concepts: the Global Search and Constraint Propagation algorithm paradigms, expression simplification, finite differencing, and datatype refinement. I'll survey two forms of knowledge needed to derive these SAT solvers: (1) General and domain-specific laws needed to reason about the domain of propositional satisfiability; (2) Design knowledge, including abstract algorithmic, data structuring, and optimization concepts. From a formal specification of the SAT problem, these two forms of knowledge are combined via a metaprogram (or derivation script) that specifies how to calculate the code. Specware automatically carries out the derivation script, resulting in fast, correct executable code.