# Advanced Topics in Computational Social Choice 2021 # Code Presented in Lectures 1 and 2 # Ulle Endriss, October 2021 # http://www.illc.uva.nl/~ulle/teaching/advanced-comsoc-2021/ # Documentation: Please refer to the slide sets 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 # Unanimity def cnfUnanimous(): cnf = [] for x in allAlternatives(): for r in profiles(lambda r : all(top(i,x,r) for i in allVoters())): cnf.append([posLiteral(r,x)]) return cnf # Majoritarianism def most(bools): return sum(bools) > len(list(bools)) / 2 def cnfMajoritarian(): cnf = [] for x in allAlternatives(): for r in profiles(lambda r : most(list(top(i,x,r) for i in allVoters()))): cnf.append([posLiteral(r,x)]) return cnf # Saving CNF to Text File def saveCNF(cnf, filename): nvars = max([abs(lit) for clause in cnf for lit in clause]) nclauses = len(cnf) file = open(filename, 'w') file.write('p cnf ' + str(nvars) + ' ' + str(nclauses) + '\n') for clause in cnf: file.write(' '.join([str(lit) for lit in clause]) + ' 0\n') file.close() # Interpreting Variables def interpret(variable): r = (variable - 1) // m x = (variable - 1) % m print(str([preflist(i,r) for i in allVoters()]) + ' --> ' + str(x))