sabe

Association:

University of Kentucky
University of Texas at Tyler
Microsoft

Description:

Our solver takes in as input a ground logic program that is obtained by grounding an encoding of the benchmark problem and the instance using lparse. The solver sabe is a variant of the solver pbmodels. It compiles weight atoms away and it is integrated into the SAT solver minisat. The solver can be downloaded from the following website http://www.cs.uky.edu/ai/

We provided encodings for some of the benchmark problems by modifying and reusing some of the exisiting gringo encodings that was made available to us through the asparagus website, and developing our own encodings for other problems.

Participants:

Lengning Liu, Microsoft

Artur Mikitiuk, University of Texas at Tyler

Gayathri Namasivayam, University of Kentucky

Miroslaw Truszczynski, University of Kentucky

Jianzhong Wang, University of Kentucky