Skip to main content

Theory Propagation and Rational-Trees

Robbins, Ed and Howe, Jacob M. and King, Andy (2013) Theory Propagation and Rational-Trees. In: Schrijvers, Tom, ed. Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming. PPDP Principles and Practice of Declarative Programming . ACM, New York, USA, pp. 193-204. ISBN 978-1-4503-2154-9. (doi:10.1145/2505879.2505901) (KAR id:37525)

Language: English
Download (261kB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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
DOI/Identification number: 10.1145/2505879.2505901
Subjects: Q Science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 13:41 UTC
Last Modified: 23 Apr 2022 22:07 UTC
Resource URI: (The current URI for this page, for reference purposes)
King, Andy:
  • Depositors only (login required):


Downloads per month over past year