Exploring Z3 for the Fair Allocation Domain

Abstract

Denne masteroppgaven utforsker hvordan Z3, en "satisfiability modulo theories solver" (SMT-løser), kan brukes innenfor feltet rettferdig fordeling. Z3 ble testet for tilfeller der varene som skal fordeles er udelelige, og der agentene som skal motta varene bruker additive verdivurderinger på varene. Fokuset var rettet mot rettferdighetskravene "envy-freeness up to one good" (EF1), "envy-freeness up to any good" (EFX), og "maximin share fairness" (MMS). Flere ulike tilfeller ble utforsket: tilfeller uten noen begrensninger, tilfeller der noen varer kan ha konflikter mellom seg og tilfeller der det er krevd at varene som deles ut må henge sammen. Det ble utviklet programmer for å finne fordelinger som oppfyller de ulike rettferdighetskravene, og kjøretidene ble sammenlignet med eksisterende blandet heltalls-programmer (MIP-er) laget for å løse de samme oppgavene. Sammenlikningen viste at MIP-er ser ut til å være raskere på disse problemene, og dermed et bedre hjelpemiddel for å finne rettferdige fordelinger enn programmer laget med Z3. Det ble også utviklet programmer for å utforske åpne problemer i feltet. De åpne problemene som ble utforsket var karakterisering av konflikt-grafer som ikke garanterer EF1-fordelinger, eksistensen av EF1-fordelinger når konflikt-grafen er en sti, eksistensen av EF1-fordelinger når varene har binære verdier og konflikter mellom seg, og eksistensen av EFX-fordelinger når det ikke er noen begrensinger på de mulige fordelingene. Programmene viste at når det er konflikter mellom varene og antall varer er mindre enn eller lik syv, eksisterer alltid EF1-fordelinger i tilfellene der konflikt-grafen danner en sti og i tilfellene der varene har binære verdier. Dessuten ble det oppdaget at EFX-fordelinger alltid eksisterer når det ikke er noen begrensninger på fordelingene og antallet varer er seks eller mindre. Det ble også demonstrert at programmer laget med Z3 kan fungere som verktøy for å utforske ideer for og oppdage mønstre i probleminstanser der EF1-fordelinger ikke er garantert når varene har konflikter mellom seg.

This master thesis explores how the SMT-solver Z3 can be used, and how well it is suited, for the problem of allocating indivisible goods to agents under the fairness notions envy-freeness up to one good (EF1), envy-freeness up to any good (EFX), and maximin share fairness (MMS), when the valuations are additive. This was explored in the unconstrained case, as well as under conflict and connectivity constraints. Programs for finding allocations of different fairness notions were developed, and their runtimes were compared to existing mixed integer programs (MIPs) programmed to achieve the same task. The experiments showed that MIPs appear to be faster, and thus a better aid for finding allocations than programs made with Z3. Programs for exploring open problems in the field were also developed. The open problems explored were the characterization of conflict graphs that do not guarantee EF1 allocations, the existence of EF1 allocations when the conflict graph is a path, the existence of EF1 allocations under conflict constraints when the valuations are binary, and the existence of EFX allocations in the unconstrained case. The programs found that when there are conflict constraints and the number of items is less than or equal to seven, EF1 allocations always exist when the conflict graph forms a path, and they always exist when the valuations are binary. Moreover, it was found that in the unconstrained case, EFX allocations always exist when the number of items is six or less. Finally, it was demonstrated that programs made with Z3 could work as a tool for exploring ideas for and discovering patterns of problem instances that do not admit EF1 allocations under conflict constraints.