# Advanced Topics in Computational Social Choice 2021 # Case Study: Base Case of the Gibbard-Satterthwaite Theorem # Ulle Endriss, September 2021 # http://www.illc.uva.nl/~ulle/teaching/advanced-comsoc-2021/ # Documentation: Please refer to the first slide set on the course website. from pylgl import solve, itersolve from math import factorial from itertools import permutations # Basics: Voters, Alternatives, Profiles n = 2 m = 3 def allVoters(): return range(n) def allAlternatives(): return range(m) def allProfiles(): return range(factorial(m) ** n) # Preferences def preference(i, r): base = factorial(m) return ( r % (base ** (i+1)) ) // (base ** i) def preflist(i, r): preflists = list(permutations(allAlternatives())) return preflists[preference(i,r)] def prefers(i, x, y, r): mylist = preflist(i, r) return mylist.index(x) < mylist.index(y) def top(i, x, r): mylist = preflist(i, r) return mylist.index(x) == 0 # Restricting the Range of Quantification def alternatives(condition): return [x for x in allAlternatives() if condition(x)] def voters(condition): return [i for i in allVoters() if condition(i)] def profiles(condition): return [r for r in allProfiles() if condition(r)] # Literals def posLiteral(r, x): return r * m + x + 1 def negLiteral(r,x): return (-1) * posLiteral(r, x) # Modelling Social Choice Functions def cnfAtLeastOne(): cnf = [] for r in allProfiles(): cnf.append([posLiteral(r,x) for x in allAlternatives()]) return cnf # Resoluteness def cnfResolute(): cnf = [] for r in allProfiles(): for x in allAlternatives(): for y in alternatives(lambda y : x < y): cnf.append([negLiteral(r,x), negLiteral(r,y)]) return cnf # Surjectivity def cnfSurjective(): cnf = [] for x in allAlternatives(): cnf.append([posLiteral(r,x) for r in allProfiles()]) return cnf # Strategyproofness def iVariants(i, r1, r2): return all(preference(j,r1) == preference(j,r2) for j in voters(lambda j : j!=i)) def cnfStrategyProof(): cnf = [] for i in allVoters(): for r1 in allProfiles(): for r2 in profiles(lambda r2 : iVariants(i,r1,r2)): for x in allAlternatives(): for y in alternatives(lambda y : prefers(i,x,y,r1)): cnf.append([negLiteral(r1,y), negLiteral(r2,x)]) return cnf # Nondictatorship def cnfNondictatorial(): cnf = [] for i in allVoters(): clause = [] for r in allProfiles(): for x in alternatives(lambda x : top(i,x,r)): clause.append(negLiteral(r,x)) cnf.append(clause) return cnf