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)
  • Depositors only (login required):

Downloads

Downloads per month over past year