A pearl on SAT and SMT solving in Prolog

Howe, J. M. & King, A. (2012). A pearl on SAT and SMT solving in Prolog. Theoretical Computer Science, 435, pp. 43-55. doi: 10.1016/j.tcs.2012.02.024

[img]
Preview
Text - Accepted Version
Available under License : See the attached licence file.

Download (193kB) | Preview
[img]
Preview
Text (Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence) - Other
Download (201kB) | Preview

Abstract

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl. Furthermore, the SAT solver can be integrated into an SMT framework which exploits the constraint solvers that are available in many Prolog systems.

Item Type: Article
Additional Information: © 2012, Elsevier. Licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/
Uncontrolled Keywords: SAT solving; SMT solving; Prolog; Constraint logic programming
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: School of Informatics > Department of Computing
URI: http://openaccess.city.ac.uk/id/eprint/12501

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics