Project for Automated Reasoning Exam

In the repository I propose to solve the instance problem given in the consegna.png file. It is required to implement the solution using both MiniZinc (known SAT-solver) and Answer Set Programming.

Problem constraints

The problem requires to divide total_money = 1mln between various italian universities (U1, U2, ... , Un) and four different topics (T1, T2, T3, T4).

Each topic has a reserved share of total_money, for example topics_perc = [40%, 30%, 10%, 20%].

Each topic is represented by num_hubs = 1 hub and by 0 <= num_spokes <= 5 spokes.

Each university has a list of topics on which is interested (from 1 to 3).

Each university, for each topic, can be:

• hub: receives hubs_perc = 70% of the topic share
• spoke: receives an equal part spoke_perc = 30% of the topic share, to be divided with the other spokes
• non-participating: do not receive anything

Clearly, non-interested universities will be non-participating, but the reverse is not true.

We define d(x,y) the distance in km between universities x and y.

Each university must gain a share quota between min_money = 50k and max_money = 150k

The constraints are the following:

• foreach U: U is hub for Ti ==> U is non-participating for all Tj, with j != i
• foreach U: U is spoke for Ti ==> d(U, hub(Ti)) <= 100 km
• foreach U: U is spoke for Ti, Tj ==> U is non-participating for all Tk, with k != i and k != j
• foreach U: min_money <= money_gained(U) <= max_money

Obtain Distances

The coordinates of italian cities can be downloaded here: https://github.com/MatteoHenryChinaski/Comuni-Italiani-2018-Sql-Json-excel

The file is available also in the repo: distances/italy_geo.xlsx.

In the python distances/distances.py I read the excel file and generate the matrixes accordingly to lp and mzn syntax.

Generate Interested Table

In the python interested/interested.py I generate randomly the interests for each university, accordingly to lp and mzn matrixes syntax.

Compilation

For the sake of simplicity for both Minizinc and ASP implementation the distances and interested matrixes are pasted directly in the source file.

Minizinc

Just open the progetto.mzn with MiniZinc and launch it from the IDE. At the end of the file is possible to define various techniques to apply for the tree exploration.

Answer Set Programming

ASP code can be launched from terminal, with the syntax: clingo [[-c own-param=value], ... ] [[--clingo-params=value], ...] source.lp

The parameters needed are:

• tot: total money to share
• min: minimum money to gain for each university
• max: maximum money to gain for each university
• n: number of universities
• s: number of topics

For example: clingo -c tot=1000 -c min=10 -c max=300 -c n=20 -c s=4 --time-limit=300 progetto.lp

Note that is not recommended to work with big integers like tot=1MLN, the grounding process will be very slow. I launched different instances always using tot=1000

Performance Analysis

The performances of both MiniZinc and ASP have been stored manually to the benchmarks.xlsx file.

Some consideration on timings are present in the report Relazione.pdf.

Check Correctness

The python check_solution.py can be used while developing to check the correctness of the solution.