Computer Sciences Commons^™

Abstract Modular Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński

Yuliya Lierler

Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience and computational benefits. We introduce concepts of abstract modules and abstract modular systems to study general principles behind the design and analysis of modelfinding programs, or solvers, for integrated heterogeneous multi-logic systems. We show how abstract modules and abstract modular systems give rise to transition systems, which are a natural and convenient representation of solvers pioneered by the SAT community. We illustrate our approach by showing how it applies to answer set programming and propositional logic, and to multi-logic systems based on these two formalisms.

Asp-Based Problem Solving With Cutting-Edge Tools, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

In the development of practical applications of answer set programming (ASP), encodings that use well-established solvers such as CLASP and DLV are sometimes affected by scalability issues. In those situations, one can resort to more sophisticated ASP tools exploiting, for instance, incremental and constraint ASP. However, today there is no specific methodology for the selection or use of such tools. In this paper we describe how we used such cutting-edge ASP tools on challenging problems from the Third Answer Set Programming Competition, and outline the methodology we followed. We view this paper as a first step in the development of …

A Transition System For Ac Language Algorithms, Yuliya Lierler, Yaunlin Zhang

Yuliya Lierler

Recently a logic programming language AC was proposed by Mellarkod et al. (2008) to integrate answer set programming (ASP) and constraint logic programming. In a similar vein, Gebser et al. (2009) proposed a CLINGCON language integrating ASP and finite domain constraints. A distinguishing feature of these languages is their capacity to allow new efficient inference algorithms that combine traditional ASP procedures and other efficient methods in constraint programming. In this paper we show that a transition system introduced by Nieuwenhuis et al. (2006) can be extended to model the “hybrid” ACSOLVER algorithm, by Mellarkod et al., designed for processing a …

Hybrid Automated Reasoning Tools: From Black-Box To Clear-Box Integration, Marcello Balduccini, Yuliya Lierler

Yuliya Lierler

Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming (CASP). CASP languages and systems proved to be largely successful at providing efficient solutions to problems involving hybrid reasoning tasks, such as scheduling problems with elements of planning. Yet, the development of CASP systems is difficult, requiring non-trivial expertise in multiple areas. This suggests a need for a study identifying general development principles of hybrid systems. Once these principles …

Representing Synonymity In Causal Logic And In Logic Programming, Joohyung Lee, Yuliya Lierler, Vladimir Lifschitz, Fangkai Yang

Yuliya Lierler

We investigate the relationship between rules representing synonymity in nonmonotonic causal logic and in answer set programming. This question is of interest in connection with current work on modular languages for describing actions.

A Sat-Based Polynomial Space Algorithm For Answer Set Programming, Enrico Giunchiglia, Marco Maratea, Yuliya Lierler

Yuliya Lierler

The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-Based decision procedure for …

Fages' Theorem And Answer Set Programming, Yuliya Lierler, Esta Erdem, Vladimir Lifschitz

Yuliya Lierler

We generalize a theorem by François Fages that describes the relationship between the completion semantics and the answer set semantics for logic programs with negotiation as failure. The study of this relationship is important in connection with the emergence of answer set programming. Whenever the two semantics are equivalent, answer sets can be computed by a satisfiability solver, and the use of answer set solvers such as SMODELS and DLV is unnecessary. A logic programming representation of the blocks world due to Ilkka Niemelä is discussed as an example.

Research Challenges And Opportunities In Knowledge Representation, Section 2.3.2: Applications Based On Formal Models, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Yuliya Lierler

Final report edited by Natasha Noy and Deborah McGuinness. Report Section 2.3.2, Applications based on formal models, authored by Yuliya Lierer, UNO faculty member.

Research Challenges And Opportunities In Knowledge Representation, Section 2.4.2 Advances In Satisfiability And Answer Set Programming, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Yuliya Lierler

Final report edited by Natasha Noy and Deborah McGuinness. Report Section 2.4.2, Advances in satisfiability and answer set programming, authored by Yuliya Lierer, UNO faculty member.

Research Challenges And Opportunities In Knowledge Representation, Section 4.1.1 Hybrid Kr, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Yuliya Lierler

Final report edited by Natasha Noy and Deborah McGuinness. Report Section 4.1.1 Hybrid KR, co-authored by Yuliya Lierer, UNO faculty member.

Analyzing And Extending An Infeasibility Analysis Algorithm, Ammar Malik

Honors Projects

Constraint satisfaction problems (CSPs) involve finding assignments to a set of variables that satisfy some mathematical constraints. Unsatisfiable constraint problems are CSPs with no solution. However, useful characteristic subsets of these problems may be extracted with algorithms such as the MARCO algorithm, which outperforms the best known algorithms in the literature. A heuristic choice in the algorithm affects how it traverses the search space to output these subsets. This work analyzes the effect of this choice and introduces three improvements to the algorithm. The first of these improvements sacrifices completeness in terms of one type of subset in order to …

Research Challenges And Opportunities In Knowledge Representation, Section 2.4.2 Advances In Satisfiability And Answer Set Programming, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Final report edited by Natasha Noy and Deborah McGuinness.

Report Section 2.4.2, Advances in satisfiability and answer set programming, authored by Yuliya Lierer, UNO faculty member.

Research Challenges And Opportunities In Knowledge Representation, Section 4.1.1 Hybrid Kr, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Final report edited by Natasha Noy and Deborah McGuinness.

Report Section 4.1.1 Hybrid KR, co-authored by Yuliya Lierer, UNO faculty member.

Research Challenges And Opportunities In Knowledge Representation, Section 2.3.2: Applications Based On Formal Models, Natasha Noy, Deborah Mcguinness, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Final report edited by Natasha Noy and Deborah McGuinness.

Report Section 2.3.2, Applications based on formal models, authored by Yuliya Lierer, UNO faculty member.

Abstract Modular Systems And Solvers, Yuliya Lierler, Miroslaw Truszczyński

Computer Science Faculty Proceedings & Presentations

Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience and computational benefits. We introduce concepts of abstract modules and abstract modular systems to study general principles behind the design and analysis of modelfinding programs, or solvers, for integrated heterogeneous multi-logic systems. We show how abstract modules and abstract modular systems give rise to transition systems, which are a natural and convenient representation of solvers pioneered by the SAT community. We illustrate our approach by showing how it applies to answer set programming and propositional logic, and to multi-logic systems based on these two formalisms.

Hybrid Automated Reasoning Tools: From Black-Box To Clear-Box Integration, Marcello Balduccini, Yuliya Lierler

Computer Science Faculty Proceedings & Presentations

Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming (CASP). CASP languages and systems proved to be largely successful at providing efficient solutions to problems involving hybrid reasoning tasks, such as scheduling problems with elements of planning. Yet, the development of CASP systems is difficult, requiring non-trivial expertise in multiple areas. This suggests a need for a study identifying general development principles of hybrid systems. Once these principles …