http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7Smith2 2026-04-05T23:10:12Z Revision history for this page on the wiki MediaWiki 1.43.5 http://mw.hh.se/wg211/index.php?title=WG211/M7Smith2&diff=249&oldid=prev 2011-12-12T10:06:28Z

<p>1 revision</p> <p><b>New page</b></p><div>[[Category:WG211]]<br /> <br /> <br /> &lt;h1&gt;Automated Synthesis of Propositional Satisfiability Solvers&lt;/h1&gt;<br /> &lt;h3&gt;Doug Smith&lt;/h3&gt;<br /> <br /> Last year we carried out automated derivations of several<br /> SAT solvers using Kestrel&#039;s Specware system. We were able to<br /> recapitulate many of the key design features of modern DPLL SAT<br /> solvers using abstract and reusable design concepts: the Global Search<br /> and Constraint Propagation algorithm paradigms, expression<br /> simplification, finite differencing, and datatype refinement. I&#039;ll<br /> survey two forms of knowledge needed to derive these SAT solvers: (1)<br /> General and domain-specific laws needed to reason about the domain of<br /> propositional satisfiability; (2) Design knowledge, including abstract<br /> algorithmic, data structuring, and optimization concepts. From a<br /> formal specification of the SAT problem, these two forms of knowledge<br /> are combined via a metaprogram (or derivation script) that specifies<br /> how to calculate the code. Specware automatically carries out the<br /> derivation script, resulting in fast, correct executable code.</div>

Admin