School of Computing

A Pearl on SAT and SMT Solving in Prolog

Jacob M. Howe and Andy King

Theoretical Computer Science, 435:43-55, June 2012 Special Issue for the Tenth International Symposium on Functional and Logic Programming, edited by Matthias Blume and German Vidal [doi].

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.

Download publication 178 kbytes (PDF)

Bibtex Record

@article{3136,
author = {Jacob M. Howe and Andy King},
title = {A {P}earl on {SAT} and {SMT} {S}olving in {P}rolog},
month = {June},
year = {2012},
pages = {43-55},
keywords = {determinacy analysis, Craig interpolants},
note = {Special Issue for the Tenth International Symposium on Functional and Logic Programming, edited by Matthias Blume and German Vidal},
doi = {j.tcs.2012.02.024},
url = {http://www.cs.kent.ac.uk/pubs/2012/3136},
    publication_type = {article},
    submission_id = {25260_1310715765},
    ISSN = {0304-3975},
    journal = {Theoretical Computer Science},
    publisher = {Elsevier},
    volume = {435},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014