UTCS Artificial Intelligence
courses
talks/events
demos
people
projects
publications
software/data
labs
areas
admin
Transition Systems for Model Generators --- A Unifying Approach (2011)
Yuliya Lierler
and Miroslaw Truszczynski
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 Minisatid are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).
View:
PDF
Citation:
In
International Conference on Logic Programming (ICLP)
2011.
Bibtex:
@inproceedings{lier11d, title={Transition Systems for Model Generators --- A Unifying Approach}, author={Yuliya Lierler and Miroslaw Truszczynski}, booktitle={International Conference on Logic Programming (ICLP)}, url="http://www.cs.utexas.edu/users/ai-lab?lier11d", year={2011} }
People
Yuliya Lierler
Ph.D. Alumni
ylierler [at] unomaha edu
Areas of Interest
Answer Set Programming
Logic