Theory Propagation and Rational-Trees

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)

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)