Transition systems for model generators-A unifying approach

Yuliya Lierler; Miroslaw Truszczynski

doi:10.1017/S1471068411000214

Transition systems for model generators-A unifying approach

Yuliya Lierler, Miroslaw Truszczynski

Computer Science

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

29 Scopus citations

Abstract

A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as "satisfiability modulo answer-set programming," where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).

Original language	English
Pages (from-to)	629-646
Number of pages	18
Journal	Theory and Practice of Logic Programming
Volume	11
Issue number	4-5
DOIs	https://doi.org/10.1017/S1471068411000214
State	Published - Jul 2011

Bibliographical note

Funding Information:
We are grateful to Marc Denecker and Vladimir Lifschitz for useful discussions. We are equally grateful to the reviewers who helped eliminate minor technical problems and improve the presentation. Yuliya Lierler was supported by a CRA/NSF 2010 Computing Innovation Fellowship. Miroslaw Truszczynski was supported by the NSF grant IIS-0913459.

Funding

We are grateful to Marc Denecker and Vladimir Lifschitz for useful discussions. We are equally grateful to the reviewers who helped eliminate minor technical problems and improve the presentation. Yuliya Lierler was supported by a CRA/NSF 2010 Computing Innovation Fellowship. Miroslaw Truszczynski was supported by the NSF grant IIS-0913459.

Funders	Funder number
NSF 2010 Computing Innovation
National Science Foundation (NSF)	IIS-0913459
Directorate for Computer and Information Science and Engineering	0913459
Computing Research Association

ASJC Scopus subject areas

Software
Theoretical Computer Science
Hardware and Architecture
Computational Theory and Mathematics
Artificial Intelligence

Access to Document

10.1017/S1471068411000214

Cite this

@article{7ab9b7db1f2f4a9a9f373b379d976442,

title = "Transition systems for model generators-A unifying approach",

abstract = "A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as {"}satisfiability modulo answer-set programming,{"} where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).",

author = "Yuliya Lierler and Miroslaw Truszczynski",

note = "Funding Information: We are grateful to Marc Denecker and Vladimir Lifschitz for useful discussions. We are equally grateful to the reviewers who helped eliminate minor technical problems and improve the presentation. Yuliya Lierler was supported by a CRA/NSF 2010 Computing Innovation Fellowship. Miroslaw Truszczynski was supported by the NSF grant IIS-0913459.",

year = "2011",

month = jul,

doi = "10.1017/S1471068411000214",

language = "English",

volume = "11",

pages = "629--646",

number = "4-5",

}

TY - JOUR

T1 - Transition systems for model generators-A unifying approach

AU - Lierler, Yuliya

AU - Truszczynski, Miroslaw

N1 - Funding Information: We are grateful to Marc Denecker and Vladimir Lifschitz for useful discussions. We are equally grateful to the reviewers who helped eliminate minor technical problems and improve the presentation. Yuliya Lierler was supported by a CRA/NSF 2010 Computing Innovation Fellowship. Miroslaw Truszczynski was supported by the NSF grant IIS-0913459.

PY - 2011/7

Y1 - 2011/7

N2 - A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as "satisfiability modulo answer-set programming," where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).

AB - A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other propositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as "satisfiability modulo answer-set programming," where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).

UR - http://www.scopus.com/inward/record.url?scp=80054912448&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80054912448&partnerID=8YFLogxK

U2 - 10.1017/S1471068411000214

DO - 10.1017/S1471068411000214

M3 - Article

AN - SCOPUS:80054912448

SN - 1471-0684

VL - 11

SP - 629

EP - 646

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

IS - 4-5

ER -

Transition systems for model generators-A unifying approach

Abstract

Bibliographical note

Funding

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this