Logic programming with satisfiability

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 give an example Prolog program which solves instances of Partial MAXSAT.

• Type: Journal
• Year: 2008
• Where: TPLP
• Authors: Michael Codish, Vitaly Lagoon, Peter J. Stuckey
• Keywords: Logic Programming, MiniSat Satisfiability, Satisfiability, TPLP 2008