Theory and Practice of Logic Programming

Programming Pearl

Logic programming with satisfiability

MICHAEL CODISHa1, VITALY LAGOONa2 and PETER J. STUCKEYa3

a1 Department of Computer Science, Ben-Gurion University, Be'er sheva, Israel (email: mcodish@cs.bgu.ac.il)

a2 Department of Computer Science & Software Engineering, University of Melbourne, Melbourne, Australia (email: vitaly.lagoon@gmail.com)

a3 NICTA Victoria Laboratory and Department of Computer Science & Software Engineering, University of Melbourne, Melbourne, Australia (email: pjs@csse.unimelb.edu.au)

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.

(Received May 10 2006)

(Revised January 30 2007)

(Accepted February 12 2007)

KEYWORDS:

  • Propositional logic;
  • Boolean satisfiability;
  • SAT solvers