Robbins, Ed, Howe, Jacob M., King, Andy (2015) Theory Propagation and Reification. Science of Computer Programming, 111 (1). pp. 3-22. ISSN 0167-6423. (doi:10.1016/j.scico.2014.05.013) (KAR id:37600)
PDF
Pre-print
Language: English |
|
Download this file (PDF/447kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.1016/j.scico.2014.05.013 |
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 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 Prolog systems. The approach is also illustrated with SMT solvers for linear constraints and integer difference constraints. The rational-tree solver is benchmarked against a number of type recovery problems, and compared against a lazy-basic SMT solver built on PicoSAT, while the integer difference logic solver is benchmarked against CVC3 and CVC4, both of which are implemented in C++.
Item Type: | Article |
---|---|
DOI/Identification number: | 10.1016/j.scico.2014.05.013 |
Subjects: |
A General Works Q Science Q Science > QA Mathematics (inc Computing science) Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Andy King |
Date Deposited: | 12 Dec 2013 23:01 UTC |
Last Modified: | 05 Nov 2024 10:21 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/37600 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):