pbmodels

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 pbmodels then translates ground logic programs with weight atoms into theories in propositional logic extended with weight atoms, and uses PB-solver minisat+ on them. A detailed descripton of the solver and the solver itself be obtained from the following website: http://www.cs.uky.edu/ai/pbmodels

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