# 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))