Logic Programming with Satisfiability

Michael Codish, Vitaly Lagoon and Peter Stuckey   

Theory and Practice of Logic Programming; 8 (1): 121-128, 2008

Abstract:

This paper presents a Prolog interface to the MiniSat satisfiability solver. Logic programming with satisfiability combines the strengths of the two paradigms: logic programming for encoding search problems into satisfiability on the one hand and efficient SAT solving on the other. This synergy between these two exposes a programming paradigm which we propose here as a logic programming pearl. To illustrate logic programming with SAT solving we detail a Prolog program which solves instances of Partial MAXSAT and motivate the relation of this problem to termination analysis.

Available:    bibtex entry   pdf

Related sites:   SWI Interface to MiniSat

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il

© copyright notice