Automated Optimization of Programs and Processing Tools in Answer Set Programming

Members

University of Nebraska Omaha (UNO) Dr. Yuliya Lierler Daniel Bresnahan Zachary Hansen Eleuterio Juan Lillo Portero	University of Kentucky (UK) Dr. Miroslaw Truszczynski Liu Liu	Collaborators Giovanni Amendola Pedro Cabalar Marc Denecker Jorge Fandinno Francesco Ricca Joost Vennekens	Alumni Mohan Ambati Michael Dingess Nicholas Hippen Brian Hodges John Hare Da Shen Jacob Lee Shelby Stocker Daniel Houston Daniel Bresnahan Justin Robbins Will Kimmerer

1 Project Summary and link to the UK Component
2 Software (UNO Component)
3 Publications (UNO Component)
4 Presentations (UNO Component)

Project Summary

The project aims to address critical outstanding challenges in answer set programming, a leading knowledge representation/declarative constraint programming paradigm. Answer set programming has its roots in the need to support fast design of robust and reliable software solutions for complex knowledge-intensive applications. It reduces the programming task to modeling an application domain as a theory in a language of logic, and leaves all computational concerns to automated reasoning. Answer set programming has been successfully used in scientific and industrial applications.

The main goal of the project is to develop automated, integrated methods and algorithms to synergistically optimize answer set programs, select appropriate solvers, and optimally configure their parameters, each task mindful of and informed by the two others. The underlying objectives are to support a systematic and principled process for building fast, scalable answer set programming solutions, and to make the declarative answer set programming technology the method of choice in a broad range of complex knowledge-intensive practical applications.

The project is sponsored under NSF grant 1707371.

The results (software, data, publications) on the University of Kentucky Component of the project are hosted here.

Software (UNO Component)

Publications (UNO Component)

Axiomatization of Aggregates in Answer Set Programming - Jorge Fandinno, Zach Hansen and Yuliya Lierler - AAAI - 2022
A Machine Learning System to Improve the Performance of ASP Solving Based on Encoding Selection - Liu Liu, Miroslaw Truszczyński and Yuliya Lierler - LPNMR - 2022
Arguing Correctness of ASP Programs with Aggregates - Jorge Fandinno, Zachary Hansen and Yuliya Lierler - LPNMR - 2022
Semantics for Conditional Literals via the SM Operator - Zachary Hansen and Yuliya Lierler - LPNMR - 2022
System Predictor: Grounding Size Estimator for Logic Programs under Answer Set Semantics - Daniel Bresnahan, Nicholas Hippen and Yuliya Lierler - technical report - 2022
Unifying Framework for Optimizations in non-boolean Formalisms - Yuliya Lierler - TPLP - 2022
Strong Equivalence and Program's Structure in Arguing Essential Equivalence between Logic Programs - Yuliya Lierler - TPLP - 2022
An Abstract View on Optimizations in SAT and ASP - Yuliya Lierler - JELIA - 2021

DualGrounder: Lazy Instantiation via Clingo Multi-shot Framework - Justin Robbins and Yuliya Lierler - JELIA - 2021
Estimating Grounding Sizes of Logic Programs under Answer Set Semantics - Nicholas Hippen and Yuliya Lierler - JELIA - 2021
Constraint Answer Set Programming: Integrational and Translationa (or SMT-based) Approaches - Yuliya Lierler - TPLP - 2021
The Informal Semantics of Answer Set Programming: A Tarskian Perspective - Marc Denecker, Yuliya Lierler, Miroslaw Truszczynski, Joost Vennekens, arxiv 2020
Modular Answer Set Programming as a Formal Specification Language - Pedro Cabalar, Jorge Fandinno, Yuliya Lierler - ICLP/TPLP - 2020
Automatic Program Rewriting in Non-Ground Answer Set Programs - Nicholas Hippen, Yuliya Lierler - PADL - 2019
Strong Equivalence and Program's Structure in Arguing Essential Equivalence between First-Order Logic Programs - Yuliya Lierler - PADL - 2019
Strong Equivalence and Program's Structure in Arguing Essential Equivalence between Logic Programs - Yuliya Lierler - 2019
SMT-based Constraint Answer Set Solver EZSMT+ for Non-tight Programs - Da Shen, Yuliya Lierler - KR - 2018
SMT-based Answer Set Solver CMODELS-DIFF (System Description) - Da Shen, Yuliya Lierler - ICLP - 2018
Strong Equivalence and Conservative Extensions Hand in Hand for Arguing Correctness of New Action Language C Formalization - Yuliya Lierler - technical report - 2018

Presentations (UNO Component)

Semantics for Conditional Literals via the SM Operator - Zach Hansen - LPNMR - 2022
Arguing Correctness of ASP Programs with Aggregates - Zach Hansen - LPNMR - 2022
Axiomatization of Aggregates In Answer Set Programs - Zach Hansen - AAAI - 2022
SMT-based Constraint Answer Set Solver EZSMT - Yuliya Lierler - PADL conference, Invited talk, 2021
Grounding Size Predictions for Answer Set Programs - Nicholas Hippen - University of Nebraska Omaha, MS Thesis Defense - 2019
Answer Set Programming and Automatic Optimization Methods in its Realm - Yuliya Lierler - Iowa State University Presentation - 2019
System PROJECTOR: An Automatic Program Rewriting Tool for Non-Ground Answer Set Programs - Yuliya Lierler -
Invited Talk, 35th International Conference on Logic Programming - 2019
Dynamic Lazy Grounding in Answer Set Programming - Brian Hodges - UNO CS Graduate Research Workshop - 2019
Automatic Program Rewriting for Non-Ground Answer Set Programs - Nicholas Hippen - UNO CS Graduate Research Workshop - 2019
Automatic Program Rewriting in Non-Ground Answer Set Programs - Yuliya Lierler - La Coruna University Presentation - 2019
Automatic Program Rewriting in Non-Ground Answer Set Programs - Nicholas Hippen - PADL - 2019
Automatic Program Rewriting in Non-Ground Answer Set Programs - Nicholas Hippen - MVD - 2018
SMT-based Constraint Answer Set Solver EZSMT - Yuliya Lierler - MVD - 2018