-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path4agents.sage.py
executable file
·141 lines (118 loc) · 7.08 KB
/
4agents.sage.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
# This file was *autogenerated* from the file 4agents.sage
from sage.all_cmdline import * # import sage library
_sage_const_3 = Integer(3); _sage_const_2 = Integer(2); _sage_const_1 = Integer(1); _sage_const_0 = Integer(0); _sage_const_7 = Integer(7); _sage_const_6 = Integer(6); _sage_const_5 = Integer(5); _sage_const_4 = Integer(4); _sage_const_8 = Integer(8)#
# This files generates a proof for the correctness of
# the following envy-free cake-cutting protocol for four agents:
#
# A:Equalize(4)
# One of:
# B:Equalize(2) C:Equalize(2)
# B:Equalize(3) C:Equalize(2)
# C:Equalize(2) B:Equalize(2)
# C:Equalize(3) B:Equalize(2)
#
def filter_by_equalize2_failure_4pieces(space, dict, cutter, observers, cycles):
"""
space: a string of spaces for display purposes.
dict: a dictionary matching agents (letters) to Prefs.
cutter: a lower-case letter representing the cutting agent, e.g. "b".
observers: a string representing the other agents, e.g. "c" or "cd".
cycles: a location to put the cycles, if found.
In Equalize(2), the cutter cuts his best piece (e.g, "4" becomes "4b"),
and equalizes it to his second best piece (e.g. "4b" and "3" become best).
If this fails, it means that the other agent prefers either "4b" or "3" over the other pieces.
"""
whole_pieces = dict[cutter].chain;
trimmed_pieces = list(whole_pieces); trimmed_pieces[-_sage_const_1 ]+=cutter
monotonicity_prefs = [ [trimmed_pieces[-_sage_const_1 ], whole_pieces[-_sage_const_1 ]] ]
whole_pieces_before_trimming = whole_pieces[-_sage_const_1 :]
trimmed_pieces_after_trimming = trimmed_pieces[-_sage_const_1 :]
equalized_pieces = trimmed_pieces[-_sage_const_2 :]
title = space+cutter+":Equalize(2) makes "+cutter+"'s best pieces: "+("=".join(equalized_pieces))
dict[cutter].equalities.append(equalized_pieces)
dict[cutter].calc_poset()
global_cover_relations = dict[cutter].global_cover_relations(trimmed_pieces_after_trimming)
if global_cover_relations:
title += ", so globally: "+Pref.repr_inequalities(global_cover_relations)
dict['*'].inequalities += monotonicity_prefs + global_cover_relations
title += ". This"
the_opts = [] # the conditions under which Equalize(2) failes.
for observer in observers:
observer_pref = dict[observer]
if observer_pref.is_best(whole_pieces[-_sage_const_2 ]):
return must_fail(title, [dict], observer) # since piece -2 is not cut
for i in [-_sage_const_1 ,-_sage_const_2 ]:
if observer_pref.may_be_best(whole_pieces[i], whole_pieces_before_trimming):
the_opts.append(dict_implied_by_best_piece({}, observer, trimmed_pieces, i))
return filter_opts(title, [dict], the_opts, cycles)
def filter_by_equalize3_failure_4pieces(space, dict, cutter, observers, cycles):
"""
space: a string of spaces for display purposes.
dict: a dictionary matching agents (letters) to Prefs.
cutter: a lower-case letter representing the cutting agent, e.g. "b".
observers: a string representing the other agents, e.g. "c" or "cd".
cycles: a location to put the cycles, if found.
In Equalize(3), the cutter cuts his two best pieces (e.g, "4" becomes "4bb" and "3" becomes "3bb"),
and equalizes it to his third best piece (e.g. "4bb", "3bb" and "2" become best).
If this fails, it means that the other agent prefers either "2" or "1" over the other pieces.
"""
whole_pieces = dict[cutter].chain;
trimmed_pieces = list(whole_pieces); trimmed_pieces[-_sage_const_1 ]+=cutter+cutter; trimmed_pieces[-_sage_const_2 ]+=cutter+cutter;
floor_piece = whole_pieces[-_sage_const_3 ]
monotonicity_prefs = [ [trimmed_pieces[-_sage_const_1 ], whole_pieces[-_sage_const_1 ]+cutter] ,
[trimmed_pieces[-_sage_const_2 ], whole_pieces[-_sage_const_2 ] ] ]
whole_pieces_before_trimming = whole_pieces[-_sage_const_2 :]
trimmed_pieces_after_trimming = trimmed_pieces[-_sage_const_2 :]
equalized_pieces = trimmed_pieces[-_sage_const_3 :]
title = space+cutter+":Equalize(3) makes "+cutter+"'s best pieces: "+("=".join(equalized_pieces))
dict[cutter].equalities.append(equalized_pieces)
dict[cutter].calc_poset()
global_cover_relations = dict[cutter].global_cover_relations(trimmed_pieces_after_trimming)
if global_cover_relations:
title += ", so globally: "+Pref.repr_inequalities(global_cover_relations)
dict['*'].inequalities += monotonicity_prefs + global_cover_relations
title += ". This"
the_opts = []
for observer in observers:
observer_pref = dict[observer]
for i in [_sage_const_0 ,_sage_const_1 ]:
if observer_pref.is_best(whole_pieces[i]):
return must_fail(title, [dict], observer) # since these two pieces are not cut
if observer_pref.may_be_best(whole_pieces[i], whole_pieces_before_trimming):
the_opts.append(dict_implied_by_best_piece({}, observer, trimmed_pieces, i))
return filter_opts(title, [dict], the_opts, cycles)
def prove_4pieces_for_given_orders(b_order, c_order):
dict_0 = {'b': Pref(chain=b_order), 'c':Pref(chain=c_order), '*':Pref()}
opts_1 = filter_by_equalize2_failure_4pieces(" "*_sage_const_2 , dict_0, cutter="b",observers="c",cycles=None)
if not opts_1: return None
for dict_1 in opts_1:
print_dict_explanation(dict_1, " "*_sage_const_3 )
opts_2 = filter_by_equalize2_failure_4pieces(" "*_sage_const_4 , dict_1, cutter="c",observers="b",cycles=None)
if not opts_2: continue
for dict_2 in opts_2:
print_dict_explanation(dict_2, " "*_sage_const_5 )
opts_3 = filter_by_equalize3_failure_4pieces(" "*_sage_const_6 , dict_2, cutter="b",observers="c", cycles=None)
if not opts_3: continue
for dict_3 in opts_3:
print_dict_explanation(dict_3, " "*_sage_const_7 )
opts_4 = filter_by_equalize3_failure_4pieces(" "*_sage_const_8 , dict_3, cutter="c",observers="b", cycles=None)
if not opts_4: continue
print "Failure!"
print dict_3
print opts_4
raise Exception("Not proved!")
def prove_4pieces():
a_pieces = ["1","2","3","4"]
print "Initially, agent a cuts four equal pieces: ", ",".join(a_pieces),"."
b_orders = [a_pieces]
c_orders = Poset([a_pieces,[]]).linear_extensions()
num_of_c_orders = len(c_orders)
for b_order in b_orders:
print "Assume w.l.o.g. that b's preferences are", Pref.repr_chain(b_order), "."
print "Consider the following",num_of_c_orders,"cases regarding the preferences of c:"
for index_c,c_order in enumerate(c_orders):
print "\nCASE",(index_c+_sage_const_1 ),"OF",num_of_c_orders, \
": c's order is", Pref.repr_chain(c_order),":"
prove_4pieces_for_given_orders(b_order, c_order)
print "\nQ.E.D!"
prove_4pieces();