Automatic Program Rewriting In Non-Ground Answer Set Programs, Nicholas Hippen, Yuliya Lierler
Dec 2018
Automatic Program Rewriting In Non-Ground Answer Set Programs, Nicholas Hippen, Yuliya Lierler
Yuliya Lierler
Answer set programming is a popular constraint programming paradigm that has seen wide use across various industry applications. However, logic programs under answer set semantics often require careful design and nontrivial expertise from a programmer to obtain satisfactory solving times. In order to reduce this burden on a software engineer we propose an automated rewriting technique for non-ground logic programs that we implement in a system Projector. We conduct rigorous experimental analysis, which shows that applying system Projector to a logic program can improve its performance, even after significant human-performed optimizations.
Strong Equivalence And Program's Structure In Arguing Essential Equivalence Between First-Order Logic Programs, Yuliya Lierler
Dec 2018
Strong Equivalence And Program's Structure In Arguing Essential Equivalence Between First-Order Logic Programs, Yuliya Lierler
Yuliya Lierler
Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper claims the correctness of a number of interesting program rewritings. Notably, they assume programs with variables and such important language features as choice, disjunction, and aggregates. We showcase the utility of some considered rewritings by using …
Smt-Based Constraint Answer Set Solver Ezsmt+ For Non-Tight Programs, Da Shen, Yuliya Lierler
Sep 2018
Smt-Based Constraint Answer Set Solver Ezsmt+ For Non-Tight Programs, Da Shen, Yuliya Lierler
Yuliya Lierler
Constraint answer set programming integrates answer set programming with constraint processing. System Ezsmt+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. The truly unique feature of ezsmt+ is its capability to process linear as well as nonlinear constraints simultaneously containing integer and real variables.
Strong Equivalence And Conservative Extensions Hand In Hand For Arguing Correctness Of New Action Language C Formalization, Yuliya Lierler
Aug 2018
Strong Equivalence And Conservative Extensions Hand In Hand For Arguing Correctness Of New Action Language C Formalization, Yuliya Lierler
Yuliya Lierler
Answer set programming is a declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation and reasoning formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Uncovering precise formal links between these programs is often of value. This paper develops a methodology for establishing such links. This methodology relies on the notions of strong equivalence and conservative extensions and a body of earlier theoretical work related to these concepts. We use distinct answer set programming formalizations of an action language C and a syntactically restricted action …
Smt-Based Answer Set Solver Cmodels-Diff (System Description), Da Shen, Yuliya Lierler
Jun 2018
Smt-Based Answer Set Solver Cmodels-Diff (System Description), Da Shen, Yuliya Lierler
Yuliya Lierler
Many answer set solvers utilize Satisfiability solvers for search. SMT solvers extend Satisfiability solvers. This paper presents the CMODELS-DIFF system that uses SMT solvers to find answer sets of a logic program. Its theoretical foundation is based on Niemala's characterization of answer sets of a logic program via so called level rankings. The comparative experimental analysis demonstrates that CMODELS-DIFF is a viable answer set solver.
First-Order Modular Logic Programs And Their Conservative Extensions (Extended Abstract), Amelia Harrison, Yuliya Lierler
Dec 2016
First-Order Modular Logic Programs And Their Conservative Extensions (Extended Abstract), Amelia Harrison, Yuliya Lierler
Yuliya Lierler
This paper introduces first-order modular logic programs, which provide a way of viewing answer set programs as consisting of many independent, meaningful modules. We also present conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. For example, we illustrate how the notion of a conservative extension can be used to justify the common projection rewriting. This is a short version of a paper that appeared at the 32nd International Conference on Logic Programming.
Iclp Tutorial: Relating Constraint Answer Set Programming And Satisfiability Modulo Theories, Yuliya Lierler
Dec 2015
Iclp Tutorial: Relating Constraint Answer Set Programming And Satisfiability Modulo Theories, Yuliya Lierler
Yuliya Lierler
No abstract provided.
Disjunctive Answer Set Solvers Via Templates, Remi Brochenin, Yuliya Lierler, Marco Maratea
Nov 2015
Disjunctive Answer Set Solvers Via Templates, Remi Brochenin, Yuliya Lierler, Marco Maratea
Yuliya Lierler
Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is ΣP2-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely dlv, gnt, cmodels, clasp and wasp. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze …
Constraint Answer Set Programming Versus Satisfiability Modulo Theories Or Constraints Versus Theories, Yuliya Lierler, Benjamin Susman
Dec 2014
Constraint Answer Set Programming Versus Satisfiability Modulo Theories Or Constraints Versus Theories, Yuliya Lierler, Benjamin Susman
Yuliya Lierler
Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. This research direction often informally relates itself to the field of Satisfiability Modulo Theory. Yet the exact formal link is obscured as the terminology and concepts used in these two research fields differ. The goal of this paper to make the link between these two fields precise.
