Journal article

Logic programming with satisfiability

Michael Codish, Vitaly Lagoon, Peter J Stuckey

THEORY AND PRACTICE OF LOGIC PROGRAMMING | CAMBRIDGE UNIV PRESS | Published : 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 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.