Author ORCID Identifier

Year of Publication


Degree Name

Doctor of Philosophy (PhD)

Document Type

Doctoral Dissertation




Computer Science

First Advisor

Miroslaw Truszczynski


Answer set programming (ASP) has long been used for modeling and solving hard search problems. These problems are modeled in ASP as encodings, a collection of rules that declaratively describe the logic of the problem without explicitly listing how to solve it. It is common that the same problem has several different but equivalent encodings in ASP. Experience shows that the performance of these ASP encodings may vary greatly from instance to instance when processed by current state-of-the-art ASP grounder/solver systems. In particular, it is rarely the case that one encoding outperforms all others. Moreover, running an ASP system on one encoding for a specific instance may “take forever,” while running it on another encoding for this instance may yield a solution in a fraction of a second. The selection of a ”good” encoding for each instance is crucial to the performance of ASP solving. In this dissertation, I propose methods to improve the performance of ASP solving that exploit these observations. First, I designed and implemented methods that, given an encoding for a problem, rewrite it in several ways into new different but equivalent encodings. Second, I designed and implemented a system that given a set of input encodings of a problem, a set of problem instances, and an ASP grounder/solver system, automatically generates equivalent encodings and builds for each selected encoding its performance model. The model predicts for any instance the execution time that the grounder/solver system takes to process the instance under the corresponding encoding. These performance models are then used to improve solving efficiency: whenever a new instance arrives, the system selects the encoding predicted to perform the best on the instance and invokes the grounder/solver. The system also supports a scheduled execution and an interleaved execution of encodings, which are complementary to machine learning techniques. Third, I implemented algorithms that generate hard structured instances for several combinatorial problems I selected for our experimental study of the efficacy of the methods I developed. Hard instances can serve as the benchmark for evaluating the hardness of specific problems and contribute as training data to the platform I created to help build encoding selection models. The process can also provide meaningful insights into finding hard instances of other combinatorial problems.

Digital Object Identifier (DOI)

Funding Information

This study was supported by the University of Omaha Nebraska's Grant (no.: 3200001595) from 2018 to 2021