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
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.
| Publication 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/ |
| Publisher Keywords: | SAT solving; SMT solving; Prolog; Constraint logic programming |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Departments: | School of Science & Technology > Computer Science |
| SWORD Depositor: |
Preview
Available under License : See the attached licence file.
Download (193kB) | Preview
Preview
Download (201kB) | Preview
Export
Downloads
Downloads per month over past year
Metadata
Metadata
MetadataAltmetric
CORE (COnnecting REpositories)
Actions (login required)
Actions (login required)
Admin Login