Logic programming with satisfiability

Michael Codish, Vitaly Lagoon, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

25 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)121-128
Number of pages8
JournalTheory and Practice of Logic Programming
Volume8
Issue number1
DOIs
Publication statusPublished - 1 Jan 2008
Externally publishedYes

Keywords

  • Boolean satisfiability
  • Propositional logic
  • SAT solvers

Cite this