Logic programming with satisfiability

Michael Codish; Vitaly Lagoon; Peter J. Stuckey

doi:10.1017/S1471068407003146

Logic programming with satisfiability

Michael Codish, Vitaly Lagoon, Peter J. Stuckey

Research output: Contribution to journal › Article › Research › peer-review

30 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 language	English
Pages (from-to)	121-128
Number of pages	8
Journal	Theory and Practice of Logic Programming
Volume	8
Issue number	1
DOIs	https://doi.org/10.1017/S1471068407003146
Publication status	Published - 1 Jan 2008
Externally published	Yes

Keywords

Boolean satisfiability
Propositional logic
SAT solvers

Access to Document

10.1017/S1471068407003146

Cite this

@article{30a26b24e5ac4e15838d2689f0a5f070,

title = "Logic programming with satisfiability",

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.",

keywords = "Boolean satisfiability, Propositional logic, SAT solvers",

author = "Michael Codish and Vitaly Lagoon and Stuckey, \{Peter J.\}",

year = "2008",

month = jan,

day = "1",

doi = "10.1017/S1471068407003146",

language = "English",

volume = "8",

pages = "121--128",

journal = "Theory and Practice of Logic Programming",

issn = "1471-0684",

publisher = "Cambridge University Press",

number = "1",

}

TY - JOUR

T1 - Logic programming with satisfiability

AU - Codish, Michael

AU - Lagoon, Vitaly

AU - Stuckey, Peter J.

PY - 2008/1/1

Y1 - 2008/1/1

N2 - 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.

AB - 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.

KW - Boolean satisfiability

KW - Propositional logic

KW - SAT solvers

UR - https://www.scopus.com/pages/publications/36849050713

U2 - 10.1017/S1471068407003146

DO - 10.1017/S1471068407003146

M3 - Article

AN - SCOPUS:36849050713

SN - 1471-0684

VL - 8

SP - 121

EP - 128

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

IS - 1

ER -

Logic programming with satisfiability

Abstract

Keywords

Access to Document

Other files and links

Cite this