# 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