Transition systems for model generators-A unifying approach

Yuliya Lierler, Miroslaw Truszczynski

Research output: Contribution to journalArticlepeer-review

27 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 languageEnglish
Pages (from-to)629-646
Number of pages18
JournalTheory and Practice of Logic Programming
Volume11
Issue number4-5
DOIs
StatePublished - 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.

ASJC Scopus subject areas

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

Fingerprint

Dive into the research topics of 'Transition systems for model generators-A unifying approach'. Together they form a unique fingerprint.

Cite this