School of Computing

A Pearl on SAT Solving in Prolog

Jacob M. Howe and Andy King

In Matthias Blume and German Vidal, editors, Tenth International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, April 2010.

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.

Download publication 143 kbytes (PDF)

Bibtex Record

@inproceedings{2970,
author = {Jacob M. Howe and Andy King},
title = {A {P}earl on {SAT} {S}olving in {P}rolog},
month = {April},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/2970},
    publication_type = {inproceedings},
    submission_id = {22767_1262691039},
    booktitle = {Tenth International Symposium on Functional and Logic Programming},
    editor = {Matthias Blume and German Vidal},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014