Robbins, Ed and King, Andy and Jacob, Howe (2013) Theory Propagation and Rational-Trees. In: Schrijvers, Tom, ed. Principles and Practice of Declarative Programming. ACM Press, New York, pp. 193-204. ISBN 978-1-4503-2154-9. (doi:https://doi.org/10.1145/2505879.2505901) (Full text available)
Download (256kB)
Preview
|
|
|
Official URL http://dx.doi.org/10.1145/2505879.2505901 |
Abstract
SAT Modulo Theories (SMT) is the problem of determining the satisfiability of a formula in which constraints, drawn from a given constraint theory $T$, are composed with logical connectives. The DPLL($T$) approach to SMT has risen to prominence as a technique for solving these quantifier-free problems. The key idea in DPLL($T$) is to closely couple unit propagation in the propositional part of the problem with theory propagation in the constraint component. In this paper it is demonstrated how reification provides a natural way for orchestrating this in the setting of logic programming. This allows an elegant implementation of DPLL($T$) solvers in Prolog. The work is motivated by a problem in reverse engineering, that of type recovery from binaries. The solution to this problem requires an SMT solver where the theory is that of rational-tree constraints, a theory not supported in off-the-shelf SMT solvers, but realised as unification in many Prolog systems. The solver is benchmarked against a number of type recovery problems, and compared against a lazy-basic SMT solver built on PicoSAT.
Item Type: | Book section |
---|---|
Subjects: | Q Science |
Divisions: | Faculties > Sciences > School of Computing > Programming Languages and Systems Group |
Depositing User: | Andy King |
Date Deposited: | 12 Dec 2013 13:41 UTC |
Last Modified: | 03 Dec 2018 14:40 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/37525 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):