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 project is a joint effort between the University of Nebraska at Omaha and the University of Kentucky. The main component of the project is located at UNO (follow this link) with the UK component being a subcontract to UNO; the present page archives work performed at UK.

People (the UK component only)

Team Members

Collaborators

Alumni

  • Miroslaw Truszczynski (PI)
  • Liu Liu (PhD Student)
  • Giovanni Amendola
  • Francesco Ricca
  • Michael Dingess (REU Student)
  • Daniel Houston (REU Student)
  • Eamonn Magner (MS Student)
  • Shelby Stocker (REU Student)
  • Will Kimmerer (REU Student)

Publications

Presentations

Research Topics

Encoding Selection

We study machine learning approaches to encoding selection. Our focus so far has been on specific problems, including the Hamiltonian cycle problem, the wire routing problem and the snake puzzle. We obtained most promising results for the Hamiltonian cycle problem. We are seeking ways to generalize the approach we develped for the HC problem to other domains. We also seek to improve performance of solving by selecting some small number of encodings predicted to perform well for an instance and running them according to a time schedule computed for the instance.

Case studies

  • Hamiltonian Cycle Problem: The zip file contains
    1. Hamiltonian Cycle encodings instances and instances used, instance generators, and performance data
    2. Software for building performance prediction models, including the code for feature extractor, and software for encoding selection
    3. Experimental results.

  • Wire Routing Problem: The zip file contains wire routing encodings and an instance generator. One can set up experiments by generating instances, combining them with instances, and running clingo (or gringo/clasp). The work on performance prediction and encoding selection is still ongoing.

  • The Snake Puzzle The zip file contains snake puzzle encodings and an instance generator. One can set up experiments by generating instances, combining them with instances, and running clingo (or gringo/clasp). The work on performance prediction and encoding selection is still ongoing.

  • Graph Coloring The zip file contains graph coloring encodings and all instance generators. One can set up experiments by generating instances, combining them with instances, and running clingo (or gringo/clasp). The work on performance prediction and encoding selection is still ongoing.

Encoding selection platform

The encoding selection platform is an automated tool to generate, evaluate, and select encodings. Based on the instance set and enocodings provided by users, the system will rewrite and generate new encodings, evaluate the performance of all encodings to generate encoding candidates, and finally build machine learning models to predict the best encoding or encoding schedule on a per-instance basis.

Software

  • Encoding selection platform: The link contains code and explanation for our platform. The system involves encoding rewriting, performance data collection, encoding candidate generation, instance feature extraction, machine learning modeling, schedule generation, solution evaluation and solving.

Aggregator project

We study the problem of automating encoding rewriting by introducing, removing and rewriting aggregates. Our current focus is on the count aggregate. The goal is to show that aggregate intruduction and rewriting can be automated and can generate many alternative encodings of complementary strengths.

Software

  • Automated Aggregator - AAgg: This is our first version of the counting aggregate rewriting software. It is currently subject to limitations on the allowed syntax of rules considered for rewrting. The project to develop a more general version of the software is underway.

Case studies

  • AAgg case studies: We have experimented with several problems from the ASP Competitions to demonstrate capabilities AAgg. The link provides problem descriptions, encodings and the instances we used in experiments.

Papers and reports

  • A link to a paper summarizing our findings is provided above. Download additional related documents here: AAgg docs.

Optimizing the use of ASP - beyond the single call case

In many cases, problems are solved not by a single answer-set program and a single call to an ASP grounder/solver, but by several calls to a grounder/solver made on carefully designed answer-set programs. Computing maximin share allocations, a problem of importance in social choice (preference aggregation and fair division), of that type. We proposed alternative ASP based solutions to these problems and are interested in finding rewriting of answer-set programs involved that might improve the overall effectiveness of the software. key tasks of the We study the use and effectiveness of ASP encoding rewriting when ASP is used to solve hard problems requiring multiple calls to a solver. Our current focus is on the problem of fair division of indivisible goods.

Encodings

  • MaxiMin Share Encodings and Software: Here we provide encodings and tools for generating and solving instances of the Maximin Share fairness problem, and different search algorithms for comparison.

Comments

Fair division of indivisible goods on a graph is a computationallly hard problem. In the general case, no efficient algorithms are known for evaluating or allocating goods to satisfy the Maximin Share (MMS) fairness criterion or, in other words, to allocate to each agent goods worth at least the maximin share value for the agent. The maximin share is defined as the best value the agent can get when the agent propose the allocation to others, let all other agents pick bundles in the allocation first and takes the last remaining bundle.

In lieu of efficient algorithms we encode the evaluation, or calculation of the guarantees, and allocation, or final division of the resources, in the Answer Set Programming (ASP) paradigm of logic programming. Using an efficient ASP solver like Potassco Clingo we can solve instances of a significant size using a simple declarative encoding. The evaluation of guarantees is an iterative process, where the guarantee is increased until we reach the maximum guarantee the agent can expect to receive. We present several encodings which take advantage of two of Clingo's capabilities: optimization, and multi-shot solving. Clingo's optimization statements are executed by finding a valid solution with a particular value. Clingo then constrains subsequent solutions to be greater than or less than this value for maximization and minimization respectively. This is performed using Clingo's powerful multi-shot solving capabilities, but there is potential for domain specific improvement. We are experimenting with replacing this general optimization statement with different search algorithms.

 

 

Miroslaw Truszczynski, Ph.D.
Computer Science
University of Kentucky
309 Davis Marksbury Building
Lexington, KY 40508

E-mail: mirek@cs.uky.edu