This is an extension of answer set programming (ASP) where rules and linear constraints over integers are used together for modelling.
gringo(v. 3.0.3) to ground the program,
lp2mip(v. 1.16) to translate it into mixed integer program, and an appropriate MIP solver (such as
cplex, v. 12.5) to compute answer sets.
int/1are reserved for declaring the required binary/integer variables.
mgt/*encode linear constraints over integers having the respective operator <=,<,>=, and >. These predicates can be renamed in the implementation if appropriate.
sorting.mingo, is run as follows
$ mingo.sh sorting.mingo
number(6) number(30) number(22) number(16) number(27) number(48) number(3) number(36)
Theory: mgeq(1,position(36),-1,position(3),0) ... (Relation predicates satisfied by the answer set)
Vars: position(36)=7 position(3)=1 position(48)=8 position(27)=5 position(16)=3 position(22)=4 position(30)=6 position(6)=2
G. Liu, T. Janhunen, and I. Niemelš: Answer Set Programming via Mixed Integer Programming. In T. Eiter and S. McIlraith, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the 13th International Conference (KR'12), 32—42, Rome, Italy, June 2012. AAAI Press.