a1 Department of Computer Science, Ben-Gurion University, Be'er sheva, Israel (email: email@example.com)
a2 Department of Computer Science & Software Engineering, University of Melbourne, Melbourne, Australia (email: firstname.lastname@example.org)
a3 NICTA Victoria Laboratory and Department of Computer Science & Software Engineering, University of Melbourne, Melbourne, Australia (email: email@example.com)
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 that we propose here as a logic programming pearl. To illustrate logic programming with SAT solving, we give an example Prolog program that solves instances of Partial MAXSAT.
(Received May 10 2006)
(Revised January 30 2007)
(Accepted February 12 2007)