Logic Programming with Satisfiability
Theory and Practice of Logic Programming;
8 (1): 121-128,
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.
Related sites: SWI Interface to MiniSat
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel