  This paper presents a Prolog interface to the MiniSat satisfiability solver.
Logic program- ming 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.
