{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "80ac7da5",
   "metadata": {},
   "source": [
    "# SAT Solving for Social Choice Theory\n",
    "Notebook for the tutorial on *Automated Reasoning for Social Choice Theory*, demonstrating how to use SAT-solving technology to reason about voting rules. Prepared by [Ulle Endriss](https://staff.science.uva.nl/u.endriss/), ILLC, University of Amsterdam (May 2023)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5a22751b",
   "metadata": {},
   "source": [
    "## System Requirements\n",
    "You need to be able to run [Jupyter Notebooks](https://realpython.com/jupyter-notebook-introduction/) for Python 3 and you need to have [PySAT](https://pysathq.github.io/) [installed](https://pysathq.github.io/installation/) on your machine. If you are new to working with notebooks, I recommend first having a look at [setup.ipynb](https://nbviewer.org/urls/staff.science.uva.nl/u.endriss/teaching/aamas-2023/setup.ipynb) and using it to check your setup is working as required."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2600e4d3",
   "metadata": {},
   "source": [
    "## Using this Notebook\n",
    "The recommended way of using this notebook is to first restart the kernel and run the entire notebook cell by cell. With the exception of two cells near the end of the notebook, this should not generate any error messages. Then go to any of the cells labelled **\"Try it!\"** and see what happens when you make changes to those cells and run them again.\n",
    "\n",
    "To fully understand what is happening, you probably will have to work through the accompanying slide deck in parallel to going through the notebook step by step. Note that I followed to a 'minimalist' coding philosophy for this notebook: trying to write as little code as possible and trying to make that code as easy to understand as possible. So this is neither maximally efficient (but easily fast enough for our present needs) nor maximally robust (but it works fine when used as intended)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bec378b9",
   "metadata": {},
   "source": [
    "## Imports\n",
    "We first import some extra functionality from standard Python modules, so we can easily (a) compute the factorial of a given number, (b) work with the list of all permutations of a given list, and (c) randomly shuffle a given list."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "4c12677a",
   "metadata": {},
   "outputs": [],
   "source": [
    "from math import factorial\n",
    "from itertools import permutations\n",
    "from random import shuffle"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "25f910f6",
   "metadata": {},
   "source": [
    "## SAT Solving\n",
    "During the tutorial, we want to use SAT-solving technology to reason about voting rules. In this section, we provide the methods required to make this technology available to us. Specifically, we define methods to check whether a given formula is satisfiable, to enumerate all models of a satisfiable formula, and to compute a minimally unsatisfiable subset (MUS) of an unsatisfiable set of clauses. Our methods are simple wrappers around more sophisticated versions of the same methods provided by PySAT. Note that none of this is specific to our intended application to social choice theory. \n",
    "\n",
    "A *SAT solver* is a program that can determine whether a given formula of propositional logic is *satisfiable*. Recall that a formula $\\varphi$ is satisfiable if there exists an assignment of truth values to the propositional variables occurring in $\\varphi$ for which $\\varphi$ evaluates to *true*. Formulas must be provided in *conjunctive normal form* (CNF). Recall that a formula in CNF is a conjunction ('and') of *clauses*, with a clause being a disjunction ('or') of *literals*. A literal, in turn, is either a propositional variable or the negation of a propositional variable. \n",
    "\n",
    "In our code, we use positive integers to represent positive literals (i.e., propositional variables), negative integers to represent negative literals (i.e., negations of propositional variables), lists of integers to represent clauses, and lists of such lists to represent formulas in CNF. Thus, for example, the list `[[1,-3,2],[-2]]` represents the formula $(p_1 \\lor \\neg p_3 \\lor p_2) \\land (\\neg p_2)$. This is known as the DIMACS format.\n",
    "\n",
    "We first import the required functionality from PySAT. The first import makes available the solver Glucose 3.0 (any of the other solvers should work just as well). The second makes available a module for working with weighted formulas in CNF, which is required for the implementation of the MUS extractor provided by means of the third import."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "056e87e7",
   "metadata": {},
   "outputs": [],
   "source": [
    "from pysat.solvers import Glucose3\n",
    "from pysat.formula import WCNF\n",
    "from pysat.examples.musx import MUSX"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e7a8b11b",
   "metadata": {},
   "source": [
    "The method `solve()` implemented below offers easy access to the corresponding method of our chosen SAT solver. If you apply this method to a formula $\\varphi$ in CNF, it will return the string `UNSATISFIABLE` in case $\\varphi$ is unsatisfiable, and otherwise a *model* that satisfies $\\varphi$. Any such a model is presented in the form of a list of positive and negative integers, indicating which propositional variables must be set to *true* and which must be set to *false*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "5eed3957",
   "metadata": {},
   "outputs": [],
   "source": [
    "def solve(cnf):\n",
    "    solver = Glucose3()\n",
    "    for clause in cnf: solver.add_clause(clause)\n",
    "    if solver.solve():\n",
    "        return solver.get_model()\n",
    "    else:\n",
    "        return('UNSATISFIABLE')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9f849c15",
   "metadata": {},
   "source": [
    "**Try it!** You can change the CNF formula (i.e., the list of lists of integers) in the example below to test different formulas for their satisfiability."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "bc66a365",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'UNSATISFIABLE'"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "solve([[1,2], [1,-2], [-1,2], [-1,-2]])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "91c6b650",
   "metadata": {},
   "source": [
    "The method `enumModels()` can be used to enumerate all satisfying models of a given formula in CNF. Keep in mind that this is a demanding operation and that the number of models can be huge. Note that the object returned by `enumModels()` is an iterator (not a list). A simple way of inspecting it is to use the `list()` method on the object returned by `enumModels()`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "0461c9cd",
   "metadata": {},
   "outputs": [],
   "source": [
    "def enumModels(cnf):\n",
    "    solver = Glucose3()\n",
    "    for clause in cnf: solver.add_clause(clause)\n",
    "    return solver.enum_models()    "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3cd5f4a4",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "05757078",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[[-1, 2, -3], [1, 2, 3]]"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "models = enumModels([[-1,-2,3], [2], [-3,1]])\n",
    "list(models)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ffd42a8",
   "metadata": {},
   "source": [
    "The method `getMUS()` can be used to compute an MUS for a given formula in CNF (which should be unsatisfiable). Note that a given formula might have more than one MUS, and `getMUS()` does not necessarily return the smallest MUS (because computing a cardinality-minimal MUS is a much more demanding operation)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "8563c734",
   "metadata": {},
   "outputs": [],
   "source": [
    "def getMUS(cnf):\n",
    "    wcnf = WCNF()\n",
    "    for clause in cnf: wcnf.append(clause, 1)\n",
    "    mus = MUSX(wcnf,verbosity=0).compute()\n",
    "    return list(cnf[i-1] for i in mus)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3f41c20b",
   "metadata": {},
   "source": [
    "**Try it!** The list we obtain represents an unsatisfiable set of clauses that becomes satisfiable as soon as we remove even a single clause from it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "95abca35",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[[-1, 2], [1], [-2]]"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "getMUS([[-1,2], [1], [-3,4], [-2], [3,-4]])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ca5e1fc9",
   "metadata": {},
   "source": [
    "## Preferences and Profiles\n",
    "In this section, we set up everything we need to represent (a) voters, (b) alternatives, (c) preferences of a single voter over the alternatives, and (d) profiles bundling the preferences of all voters. Observe that $n$ voters and $m$ alternatives, there are $m!$ possible preferences and $m!^n$ possible profiles.\n",
    "\n",
    "We first fix `n`, the number of voters, and `m`, the number of alternatives. For much of what we are going to do, we shall assume `n = 2` and `m = 3`. Keep in mind that the number of objects we are dealing with grows exponentially in `n` and superexponentially in `m`, so things are unlikely to work well (or at all) for even moderately larger numbers."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "8e0bd2b7",
   "metadata": {},
   "outputs": [],
   "source": [
    "n = 2\n",
    "m = 3"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cf09422f",
   "metadata": {},
   "source": [
    "The set of voters is simply the set of integers from `0` to `n-1`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "76de5ec8",
   "metadata": {},
   "outputs": [],
   "source": [
    "def allVoters():\n",
    "    return range(n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "13967251",
   "metadata": {},
   "source": [
    "Similarly, the set of alternatives is simply the set of integers from `0` to `m-1`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "be68ea55",
   "metadata": {},
   "outputs": [],
   "source": [
    "def allAlternatives():\n",
    "    return range(m)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "93ebbd7f",
   "metadata": {},
   "source": [
    "It will be convenient to also represent preferences and profiles as integers (just think of some enumeration of all preferences and assign integers to them, starting with `0`, and similarly for profiles). The method below can be used to return the set of all such integers representing profiles (we happen to not require a corresponding method for preferences)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "bebf13d1",
   "metadata": {},
   "outputs": [],
   "source": [
    "def allProfiles():\n",
    "    return range(factorial(m) ** n)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e02c3d16",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "98708908",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0, 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]\n"
     ]
    }
   ],
   "source": [
    "ps = allProfiles()\n",
    "print(list(ps))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "63dd104e",
   "metadata": {},
   "source": [
    "The next three methods allow us to retrieve lists of voters, alternatives, and profiles, respectively, that meet a certain condition. Such a condition can be any function mapping objects of the appropriate types to a boolean value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "6f402785",
   "metadata": {},
   "outputs": [],
   "source": [
    "def voters(condition):\n",
    "    return [i for i in allVoters() if condition(i)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "9878a275",
   "metadata": {},
   "outputs": [],
   "source": [
    "def alternatives(condition):\n",
    "    return [x for x in allAlternatives() if condition(x)]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "ae3dff39",
   "metadata": {},
   "outputs": [],
   "source": [
    "def profiles(condition):\n",
    "    return [r for r in allProfiles() if condition(r)]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0d1d41e8",
   "metadata": {},
   "source": [
    "**Try it!** For example, using [lambda expressions](https://realpython.com/python-lambda/) in Python to define suitable (boolean) conditions, we can retrieve the list of all alternatives that are different from alternative ``1``."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "5eed6bd5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[0, 2]"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "alternatives(lambda x : x!=1)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "60f3cea4",
   "metadata": {},
   "source": [
    "Method `preference()` can be used to retrieve the number representing the preference order reported by a given voter `i` in a given profile `r`. The way I have chosen to implement this is to think of the numbers representing profiles as being written down in an `m!`-ary number system in which each digit represents the preference order of one voter. For example, for `n=2` and `m=3`, profiles are 2-digit numbers with digits ranging from `0` to `5`. In this case, profile `50` (representing the number $5 \\cdot 3!^1 + 0\\cdot 3!^0 = 30$ in the decimal system) is the profile in which the first agent has the last possible preference order (say, `2>1>0`) and the second agent has the first possible preference order (say, `0>1>2`)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "fde6399b",
   "metadata": {},
   "outputs": [],
   "source": [
    "def preference(i, r):\n",
    "    base = factorial(m)\n",
    "    return ( r % (base ** (i+1)) ) // (base ** i)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6409ac58",
   "metadata": {},
   "source": [
    "Method `iVariants()` can be used to check whether profiles `r1` and `r2` are `i`-variants, i.e., to check whether in the two profiles all voters, except possibly voter `i`, report the same preferences."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "c2ba8ac1",
   "metadata": {},
   "outputs": [],
   "source": [
    "def iVariants(i, r1, r2):\n",
    "    return all(preference(j,r1) == preference(j,r2)\n",
    "               for j in voters(lambda j : j!=i))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4045a186",
   "metadata": {},
   "source": [
    "Method `preflist()` can be used to retrieve a list-representation of the preference order of a given voter `i` in a given profile `r`. This is implemented by generating the list of all permutations of the alternatives and then picking the $k$th element of that big list, where $k$ is obtained using `preference(i,r)`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "985adb9f",
   "metadata": {},
   "outputs": [],
   "source": [
    "def preflist(i, r):\n",
    "    preflists = list(permutations(allAlternatives()))\n",
    "    return preflists[preference(i,r)]"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "22b82b74",
   "metadata": {},
   "source": [
    "We now have everything in place to implement the top-level methods we will actually need to reason about preferences and profiles. First among them is `prefers()`, which we can use to check whether voter `i` prefers alternative `x` to alternative `y` in profile `r`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "224d5ee5",
   "metadata": {},
   "outputs": [],
   "source": [
    "def prefers(i, x, y, r):\n",
    "    mylist =  preflist(i, r) \n",
    "    return mylist.index(x) < mylist.index(y)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7e2da0f8",
   "metadata": {},
   "source": [
    "**Try it!** Let's check, for example, whether the second voter (`1`) prefers the first alternative (`0`) to the third alternative (`2`) in profile number `30`. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "4ca12c1b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "prefers(1,0,2,30)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "a92d48f3",
   "metadata": {},
   "source": [
    "Method `top()` can be used to check whether voter `i` has alternative `x` at the top of her preference order in profile `r`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "f5d26275",
   "metadata": {},
   "outputs": [],
   "source": [
    "def top(i, x, r):\n",
    "    mylist =  preflist(i, r) \n",
    "    return mylist.index(x) == 0"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ed3272cf",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "c9e7fab9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "top(1,2,30)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2a6abd51",
   "metadata": {},
   "source": [
    "The next two methods are simple *pretty-print* methods for preferences and profiles, respectively."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "9a7d065d",
   "metadata": {},
   "outputs": [],
   "source": [
    "def strPref(i, r):\n",
    "    return ''.join(str(x) for x in preflist(i,r))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "a0156901",
   "metadata": {},
   "outputs": [],
   "source": [
    "def strProf(r):\n",
    "    return '(' + ','.join(strPref(i,r) for i in allVoters()) + ')'"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1cd52418",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "1d6b1943",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'(012,210)'"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "strProf(30)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1cdfecfd",
   "metadata": {},
   "source": [
    "## Encoding Voting Rules"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6e3bd4a1",
   "metadata": {},
   "source": [
    "Method `posLiteral()` can be used to return the positive literal corresponding to the statement that in profile `r` it is the case that alternative `x` is a winner (but not necessarily the only one). Method `negLiteral()` returns the corresponding negative literal."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "e451e8c9",
   "metadata": {},
   "outputs": [],
   "source": [
    "def posLiteral(r, x):\n",
    "    return r * m + x + 1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "3eef8350",
   "metadata": {},
   "outputs": [],
   "source": [
    "def negLiteral(r, x):\n",
    "    return (-1) * posLiteral(r, x)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3549185e",
   "metadata": {},
   "source": [
    "Method `strLiteral()` provide a simple *pretty-print* method for literals, and `strClause()` extends this to clauses (i.e., to lists of literals)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "aa74ca28",
   "metadata": {},
   "outputs": [],
   "source": [
    "def strLiteral(lit):\n",
    "    r = (abs(lit) - 1) // m\n",
    "    x = (abs(lit) - 1) % m\n",
    "    return ('not ' if lit<0 else '') + strProf(r) + '->' + str(x)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "99eb924d",
   "metadata": {},
   "outputs": [],
   "source": [
    "def strClause(clause):\n",
    "    return ' or '.join(strLiteral(lit) for lit in clause)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9a55e425",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "8caa9642",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'not (210,210)->2'"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "strLiteral(-108)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b495ffbc",
   "metadata": {},
   "source": [
    "Method `cnfAtLeastOne()` returns the CNF encoding the statement that a voting rule must always return at least one winner."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "c274f0bf",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfAtLeastOne():\n",
    "    cnf = []\n",
    "    for r in allProfiles():\n",
    "        cnf.append([posLiteral(r,x) for x in allAlternatives()])\n",
    "    return cnf    "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8ee9478f",
   "metadata": {},
   "source": [
    "**Try it!**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "aa6b0b2a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[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]]\n"
     ]
    }
   ],
   "source": [
    "print(cnfAtLeastOne())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4b38e8f7",
   "metadata": {},
   "source": [
    "Method `cnfResolute()` returns the CNF encoding the requirement that our voting rule must be resolute."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "e78ebab0",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfResolute():\n",
    "    cnf = []\n",
    "    for r in allProfiles():\n",
    "        for x in allAlternatives():\n",
    "            for y in alternatives(lambda y : x < y):\n",
    "                cnf.append([negLiteral(r,x), negLiteral(r,y)])\n",
    "    return cnf            "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "854893c1",
   "metadata": {},
   "source": [
    "## Axioms\n",
    "The following axioms encode various axioms we might want our voting rule to satisfy. Refer to the slide deck for explanation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "3bb6fc44",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfStrategyProof():\n",
    "    cnf = []\n",
    "    for i in allVoters():\n",
    "        for r1 in allProfiles():\n",
    "            for r2 in profiles(lambda r2 : iVariants(i,r1,r2)):\n",
    "                for x in allAlternatives():\n",
    "                    for y in alternatives(lambda y : prefers(i,x,y,r1)):\n",
    "                        cnf.append([negLiteral(r1,y), negLiteral(r2,x)])\n",
    "    return cnf                    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "9dfa2cca",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfSurjective():\n",
    "    cnf = []\n",
    "    for x in allAlternatives():\n",
    "        cnf.append([posLiteral(r,x) for r in allProfiles()])\n",
    "    return cnf    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "35e98a64",
   "metadata": {},
   "outputs": [],
   "source": [
    "def cnfNonDictatorial():\n",
    "    cnf = []\n",
    "    for i in allVoters():\n",
    "        clause = []\n",
    "        for r in allProfiles():\n",
    "            for x in alternatives(lambda x : top(i,x,r)):\n",
    "                clause.append(negLiteral(r,x))\n",
    "        cnf.append(clause)\n",
    "    return cnf    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "3f134e79",
   "metadata": {},
   "outputs": [],
   "source": [
    "def most(bools):\n",
    "    return sum(bools) > len(list(bools)) / 2\n",
    "\n",
    "def cnfMajoritarian():\n",
    "    cnf = []\n",
    "    for x in allAlternatives():\n",
    "        for r in profiles(lambda r : most(list(top(i,x,r) for i in allVoters()))):\n",
    "            cnf.append([posLiteral(r,x)])\n",
    "    return cnf"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b180cafa",
   "metadata": {},
   "source": [
    "The dictionary `axiom` associates names of axioms (i.e., strings) with methods generating the formulas encoding those axioms. This will be useful later on when we want to determine which axiom was responsible for a given clause to have been generated. (For convenience and by a slight abuse of terminology, we are including the requirements of always returning at least one winner and to be resolute in our list of axioms here.) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "42f1d530",
   "metadata": {},
   "outputs": [],
   "source": [
    "axiom = {\n",
    "    'AtLeastOne' : cnfAtLeastOne(),\n",
    "    'Resolute' : cnfResolute(),\n",
    "    'StrategyProof' : cnfStrategyProof(),\n",
    "    'Surjective' : cnfSurjective(),\n",
    "    'NonDictatorial' : cnfNonDictatorial(),\n",
    "    'Majoritarian' : cnfMajoritarian()\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ab136f1f",
   "metadata": {},
   "source": [
    "## Explaining Formulas\n",
    "For a given clause or CNF, respectively, the next two methods allow us to display a simple explanation for how this formula has been generated. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "722af968",
   "metadata": {},
   "outputs": [],
   "source": [
    "def explainClause(clause):\n",
    "    reason = next((k for k in axiom if clause in axiom[k]), 'None')\n",
    "    print(reason + ': ' + strClause(clause))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "4a69c863",
   "metadata": {},
   "outputs": [],
   "source": [
    "def explainCNF(cnf):\n",
    "    for clause in cnf: explainClause(clause)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "325e12e0",
   "metadata": {},
   "source": [
    "**Try it!** "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "6b89494c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "StrategyProof: not (120,012)->0 or not (210,012)->1\n"
     ]
    }
   ],
   "source": [
    "explainClause([-10,-17])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5bf3ec11",
   "metadata": {},
   "source": [
    "## Proving the Gibbard Satterthwaite Theorem\n",
    "**Try it!** We are now ready to generate the CNF corresponding to the Gibbard-Satterthwaite Theorem."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "id": "4f205168",
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = ( cnfAtLeastOne() + cnfResolute() + cnfStrategyProof() + cnfSurjective() + cnfNonDictatorial() )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "id": "70886954",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1445"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "134356d7",
   "metadata": {},
   "source": [
    "**Try it!** Let's ask the SAT solver to check whether the CNF we just generated is satisfiable. If it is not, we have found (an instance of) an impossibility theorem."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "id": "f106457a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'UNSATISFIABLE'"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "solve(cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "281f73f8",
   "metadata": {},
   "source": [
    "**Try it!** If our CNF indeed is unsatisfiable, then we can try to compute an MUS for it."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "id": "d658b938",
   "metadata": {},
   "outputs": [],
   "source": [
    "mus = getMUS(cnf)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "8b3ef8f5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "199"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(mus)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39f831d9",
   "metadata": {},
   "source": [
    "## Number of Strategyproof Voting Rules\n",
    "**Try it!** How many resolute voting rules are there (for the current values of `n` and `m`) that are stratgeyproof? We can easily find out by first generating the appropriate CNF and then counting the number of models for that formula."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "id": "0b2fb3bb",
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = cnfAtLeastOne() + cnfResolute() + cnfStrategyProof()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "id": "11d0ffd0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "17"
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "rules = enumModels(cnf)\n",
    "len(list(rules))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "886d69d2",
   "metadata": {},
   "source": [
    "## Incompatilbility of Strategyproofness and Majoritarianism\n",
    "**Try it!** The CNF below corresponds to the theorem by Geist and Peters on the incompatibility of strategyproofness and majoritarianism (which you can think of as a weakened version of the Gibbard-Satterthwaite Theorem). Recall that here the impossibility only kicks in once we set `n = 3`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "91f55d41",
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = ( cnfAtLeastOne() + cnfResolute() + cnfStrategyProof() + cnfMajoritarian() )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "id": "0e554b5a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[1,\n",
       " -2,\n",
       " -3,\n",
       " 4,\n",
       " -5,\n",
       " -6,\n",
       " -7,\n",
       " 8,\n",
       " -9,\n",
       " -10,\n",
       " 11,\n",
       " -12,\n",
       " -13,\n",
       " -14,\n",
       " 15,\n",
       " -16,\n",
       " -17,\n",
       " 18,\n",
       " 19,\n",
       " -20,\n",
       " -21,\n",
       " 22,\n",
       " -23,\n",
       " -24,\n",
       " -25,\n",
       " 26,\n",
       " -27,\n",
       " -28,\n",
       " 29,\n",
       " -30,\n",
       " -31,\n",
       " -32,\n",
       " 33,\n",
       " -34,\n",
       " -35,\n",
       " 36,\n",
       " 37,\n",
       " -38,\n",
       " -39,\n",
       " 40,\n",
       " -41,\n",
       " -42,\n",
       " -43,\n",
       " 44,\n",
       " -45,\n",
       " -46,\n",
       " 47,\n",
       " -48,\n",
       " -49,\n",
       " -50,\n",
       " 51,\n",
       " -52,\n",
       " -53,\n",
       " 54,\n",
       " 55,\n",
       " -56,\n",
       " -57,\n",
       " 58,\n",
       " -59,\n",
       " -60,\n",
       " -61,\n",
       " 62,\n",
       " -63,\n",
       " -64,\n",
       " 65,\n",
       " -66,\n",
       " -67,\n",
       " -68,\n",
       " 69,\n",
       " -70,\n",
       " -71,\n",
       " 72,\n",
       " 73,\n",
       " -74,\n",
       " -75,\n",
       " 76,\n",
       " -77,\n",
       " -78,\n",
       " -79,\n",
       " 80,\n",
       " -81,\n",
       " -82,\n",
       " 83,\n",
       " -84,\n",
       " -85,\n",
       " -86,\n",
       " 87,\n",
       " -88,\n",
       " -89,\n",
       " 90,\n",
       " 91,\n",
       " -92,\n",
       " -93,\n",
       " 94,\n",
       " -95,\n",
       " -96,\n",
       " -97,\n",
       " 98,\n",
       " -99,\n",
       " -100,\n",
       " 101,\n",
       " -102,\n",
       " -103,\n",
       " -104,\n",
       " 105,\n",
       " -106,\n",
       " -107,\n",
       " 108]"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "solve(cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bb622ba9",
   "metadata": {},
   "source": [
    "**Try it!** For `n=2` and `m=3`, the next cell will produce an error message, given that for these parameters the CNF we generated earlier in fact is satisfiable (so does not have an MUS). The intended use is for `n=3` and `m=3`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "id": "27938038",
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "'NoneType' object is not iterable",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "Cell \u001b[0;32mIn[53], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m mus \u001b[38;5;241m=\u001b[39m \u001b[43mgetMUS\u001b[49m\u001b[43m(\u001b[49m\u001b[43mcnf\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m      2\u001b[0m \u001b[38;5;28mlen\u001b[39m(mus)\n",
      "Cell \u001b[0;32mIn[7], line 5\u001b[0m, in \u001b[0;36mgetMUS\u001b[0;34m(cnf)\u001b[0m\n\u001b[1;32m      3\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m clause \u001b[38;5;129;01min\u001b[39;00m cnf: wcnf\u001b[38;5;241m.\u001b[39mappend(clause, \u001b[38;5;241m1\u001b[39m)\n\u001b[1;32m      4\u001b[0m mus \u001b[38;5;241m=\u001b[39m MUSX(wcnf,verbosity\u001b[38;5;241m=\u001b[39m\u001b[38;5;241m0\u001b[39m)\u001b[38;5;241m.\u001b[39mcompute()\n\u001b[0;32m----> 5\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28mlist\u001b[39m(cnf[i\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m] \u001b[38;5;28;01mfor\u001b[39;00m i \u001b[38;5;129;01min\u001b[39;00m mus)\n",
      "\u001b[0;31mTypeError\u001b[0m: 'NoneType' object is not iterable"
     ]
    }
   ],
   "source": [
    "mus = getMUS(cnf)\n",
    "len(mus)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bbbca0c2",
   "metadata": {},
   "source": [
    "**Try it!** Sometimes we can find a smaller MUS by first suffling our CNF."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "id": "433acbb1",
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "'NoneType' object is not iterable",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "Cell \u001b[0;32mIn[54], line 2\u001b[0m\n\u001b[1;32m      1\u001b[0m shuffle(cnf)\n\u001b[0;32m----> 2\u001b[0m mus \u001b[38;5;241m=\u001b[39m \u001b[43mgetMUS\u001b[49m\u001b[43m(\u001b[49m\u001b[43mcnf\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m      3\u001b[0m \u001b[38;5;28mlen\u001b[39m(mus)\n",
      "Cell \u001b[0;32mIn[7], line 5\u001b[0m, in \u001b[0;36mgetMUS\u001b[0;34m(cnf)\u001b[0m\n\u001b[1;32m      3\u001b[0m \u001b[38;5;28;01mfor\u001b[39;00m clause \u001b[38;5;129;01min\u001b[39;00m cnf: wcnf\u001b[38;5;241m.\u001b[39mappend(clause, \u001b[38;5;241m1\u001b[39m)\n\u001b[1;32m      4\u001b[0m mus \u001b[38;5;241m=\u001b[39m MUSX(wcnf,verbosity\u001b[38;5;241m=\u001b[39m\u001b[38;5;241m0\u001b[39m)\u001b[38;5;241m.\u001b[39mcompute()\n\u001b[0;32m----> 5\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[38;5;28mlist\u001b[39m(cnf[i\u001b[38;5;241m-\u001b[39m\u001b[38;5;241m1\u001b[39m] \u001b[38;5;28;01mfor\u001b[39;00m i \u001b[38;5;129;01min\u001b[39;00m mus)\n",
      "\u001b[0;31mTypeError\u001b[0m: 'NoneType' object is not iterable"
     ]
    }
   ],
   "source": [
    "shuffle(cnf)\n",
    "mus = getMUS(cnf)\n",
    "len(mus)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c59ffd21",
   "metadata": {},
   "source": [
    "**Try it!** Let's print the last MUS we generated."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "id": "9db4f665",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[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], [-2, -4], [-3, -7], [-3, -8], [-5, -1], [-5, -9], [-5, -13], [-9, -4], [-7, -11], [-7, -14], [-10, -8], [-10, -18], [-14, -4], [-16, -8], [-16, -12], [-17, -15], [-24, -19], [-24, -25], [-24, -28], [-27, -22], [-31, -36], [-38, -52], [-42, -37], [-42, -43], [-41, -52], [-41, -54], [-43, -53], [-48, -38], [-50, -52], [-52, -47], [-53, -51], [-57, -62], [-60, -55], [-60, -61], [-66, -62], [-68, -55], [-68, -58], [-71, -60], [-71, -69], [-75, -79], [-75, -80], [-78, -73], [-77, -90], [-82, -87], [-89, -87], [-92, -94], [-96, -97], [-95, -106], [-95, -108], [-99, -91], [-99, -106], [-99, -107], [-102, -92], [-102, -98], [-100, -108], [-104, -106], [-103, -108], [-104, -108], [-107, -96], [-106, -98], [-2, -19], [-2, -55], [-2, -73], [-5, -22], [-6, -22], [-6, -23], [-5, -40], [-6, -40], [-5, -58], [-6, -58], [-6, -59], [-5, -76], [-5, -94], [-6, -94], [-8, -25], [-8, -79], [-9, -98], [-11, -28], [-12, -46], [-11, -64], [-12, -64], [-12, -65], [-11, -82], [-12, -83], [-14, -31], [-15, -49], [-15, -50], [-14, -67], [-15, -68], [-14, -85], [-17, -34], [-18, -34], [-17, -52], [-18, -52], [-17, -88], [-18, -107], [-20, -1], [-21, -1], [-23, -4], [-26, -97], [-26, -99], [-30, -10], [-29, -100], [-29, -102], [-33, -13], [-33, -49], [-32, -103], [-32, -105], [-35, -106], [-35, -108], [-39, -1], [-37, -56], [-42, -4], [-40, -59], [-45, -7], [-45, -8], [-43, -98], [-48, -10], [-48, -11], [-46, -65], [-51, -13], [-49, -68], [-54, -16], [-52, -107], [-54, -107], [-61, -44], [-63, -44], [-66, -11], [-66, -47], [-64, -84], [-64, -101], [-66, -101], [-67, -105], [-72, -53], [-70, -107], [-70, -108], [-74, -1], [-73, -93], [-77, -94], [-76, -96], [-80, -97], [-79, -99], [-83, -10], [-86, -103], [-85, -105], [-86, -105], [-89, -106], [-88, -108], [-91, -38], [-91, -56], [-94, -59], [-97, -62], [-98, -81], [-101, -30], [-100, -65], [-101, -84], [-107, -36], [-106, -71], [-107, -90], [1, 4, 7, 10, 13, 16, 19, 22, 25, 28, 31, 34, 37, 40, 43, 46, 49, 52, 55, 58, 61, 64, 67, 70, 73, 76, 79, 82, 85, 88, 91, 94, 97, 100, 103, 106], [2, 5, 8, 11, 14, 17, 20, 23, 26, 29, 32, 35, 38, 41, 44, 47, 50, 53, 56, 59, 62, 65, 68, 71, 74, 77, 80, 83, 86, 89, 92, 95, 98, 101, 104, 107], [3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 42, 45, 48, 51, 54, 57, 60, 63, 66, 69, 72, 75, 78, 81, 84, 87, 90, 93, 96, 99, 102, 105, 108], [-1, -4, -8, -11, -15, -18, -19, -22, -26, -29, -33, -36, -37, -40, -44, -47, -51, -54, -55, -58, -62, -65, -69, -72, -73, -76, -80, -83, -87, -90, -91, -94, -98, -101, -105, -108], [-1, -4, -7, -10, -13, -16, -19, -22, -25, -28, -31, -34, -38, -41, -44, -47, -50, -53, -56, -59, -62, -65, -68, -71, -75, -78, -81, -84, -87, -90, -93, -96, -99, -102, -105, -108]]\n"
     ]
    }
   ],
   "source": [
    "print(mus)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "75687e27",
   "metadata": {},
   "source": [
    "**Try it!** Now let's retrieve explanations for how the clauses in our MUS have been generated in the first place. Provided the MUS is reasonably short, it should be easy to transform this into a human-readable proof."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "id": "8c8e07e9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "AtLeastOne: (012,012)->0 or (012,012)->1 or (012,012)->2\n",
      "AtLeastOne: (021,012)->0 or (021,012)->1 or (021,012)->2\n",
      "AtLeastOne: (102,012)->0 or (102,012)->1 or (102,012)->2\n",
      "AtLeastOne: (120,012)->0 or (120,012)->1 or (120,012)->2\n",
      "AtLeastOne: (201,012)->0 or (201,012)->1 or (201,012)->2\n",
      "AtLeastOne: (210,012)->0 or (210,012)->1 or (210,012)->2\n",
      "AtLeastOne: (012,021)->0 or (012,021)->1 or (012,021)->2\n",
      "AtLeastOne: (021,021)->0 or (021,021)->1 or (021,021)->2\n",
      "AtLeastOne: (102,021)->0 or (102,021)->1 or (102,021)->2\n",
      "AtLeastOne: (120,021)->0 or (120,021)->1 or (120,021)->2\n",
      "AtLeastOne: (201,021)->0 or (201,021)->1 or (201,021)->2\n",
      "AtLeastOne: (210,021)->0 or (210,021)->1 or (210,021)->2\n",
      "AtLeastOne: (012,102)->0 or (012,102)->1 or (012,102)->2\n",
      "AtLeastOne: (021,102)->0 or (021,102)->1 or (021,102)->2\n",
      "AtLeastOne: (102,102)->0 or (102,102)->1 or (102,102)->2\n",
      "AtLeastOne: (120,102)->0 or (120,102)->1 or (120,102)->2\n",
      "AtLeastOne: (201,102)->0 or (201,102)->1 or (201,102)->2\n",
      "AtLeastOne: (210,102)->0 or (210,102)->1 or (210,102)->2\n",
      "AtLeastOne: (012,120)->0 or (012,120)->1 or (012,120)->2\n",
      "AtLeastOne: (021,120)->0 or (021,120)->1 or (021,120)->2\n",
      "AtLeastOne: (102,120)->0 or (102,120)->1 or (102,120)->2\n",
      "AtLeastOne: (120,120)->0 or (120,120)->1 or (120,120)->2\n",
      "AtLeastOne: (201,120)->0 or (201,120)->1 or (201,120)->2\n",
      "AtLeastOne: (210,120)->0 or (210,120)->1 or (210,120)->2\n",
      "AtLeastOne: (012,201)->0 or (012,201)->1 or (012,201)->2\n",
      "AtLeastOne: (021,201)->0 or (021,201)->1 or (021,201)->2\n",
      "AtLeastOne: (102,201)->0 or (102,201)->1 or (102,201)->2\n",
      "AtLeastOne: (120,201)->0 or (120,201)->1 or (120,201)->2\n",
      "AtLeastOne: (201,201)->0 or (201,201)->1 or (201,201)->2\n",
      "AtLeastOne: (210,201)->0 or (210,201)->1 or (210,201)->2\n",
      "AtLeastOne: (012,210)->0 or (012,210)->1 or (012,210)->2\n",
      "AtLeastOne: (021,210)->0 or (021,210)->1 or (021,210)->2\n",
      "AtLeastOne: (102,210)->0 or (102,210)->1 or (102,210)->2\n",
      "AtLeastOne: (120,210)->0 or (120,210)->1 or (120,210)->2\n",
      "AtLeastOne: (201,210)->0 or (201,210)->1 or (201,210)->2\n",
      "AtLeastOne: (210,210)->0 or (210,210)->1 or (210,210)->2\n",
      "StrategyProof: not (012,012)->1 or not (021,012)->0\n",
      "StrategyProof: not (012,012)->2 or not (102,012)->0\n",
      "StrategyProof: not (012,012)->2 or not (102,012)->1\n",
      "StrategyProof: not (021,012)->1 or not (012,012)->0\n",
      "StrategyProof: not (021,012)->1 or not (102,012)->2\n",
      "StrategyProof: not (021,012)->1 or not (201,012)->0\n",
      "StrategyProof: not (102,012)->2 or not (021,012)->0\n",
      "StrategyProof: not (102,012)->0 or not (120,012)->1\n",
      "StrategyProof: not (102,012)->0 or not (201,012)->1\n",
      "StrategyProof: not (120,012)->0 or not (102,012)->1\n",
      "StrategyProof: not (120,012)->0 or not (210,012)->2\n",
      "StrategyProof: not (201,012)->1 or not (021,012)->0\n",
      "StrategyProof: not (210,012)->0 or not (102,012)->1\n",
      "StrategyProof: not (210,012)->0 or not (120,012)->2\n",
      "StrategyProof: not (210,012)->1 or not (201,012)->2\n",
      "StrategyProof: not (021,021)->2 or not (012,021)->0\n",
      "StrategyProof: not (021,021)->2 or not (102,021)->0\n",
      "StrategyProof: not (021,021)->2 or not (120,021)->0\n",
      "StrategyProof: not (102,021)->2 or not (021,021)->0\n",
      "StrategyProof: not (201,021)->0 or not (210,021)->2\n",
      "StrategyProof: not (012,102)->1 or not (210,102)->0\n",
      "StrategyProof: not (021,102)->2 or not (012,102)->0\n",
      "StrategyProof: not (021,102)->2 or not (102,102)->0\n",
      "StrategyProof: not (021,102)->1 or not (210,102)->0\n",
      "StrategyProof: not (021,102)->1 or not (210,102)->2\n",
      "StrategyProof: not (102,102)->0 or not (210,102)->1\n",
      "StrategyProof: not (120,102)->2 or not (012,102)->1\n",
      "StrategyProof: not (201,102)->1 or not (210,102)->0\n",
      "StrategyProof: not (210,102)->0 or not (120,102)->1\n",
      "StrategyProof: not (210,102)->1 or not (201,102)->2\n",
      "StrategyProof: not (012,120)->2 or not (102,120)->1\n",
      "StrategyProof: not (021,120)->2 or not (012,120)->0\n",
      "StrategyProof: not (021,120)->2 or not (102,120)->0\n",
      "StrategyProof: not (120,120)->2 or not (102,120)->1\n",
      "StrategyProof: not (201,120)->1 or not (012,120)->0\n",
      "StrategyProof: not (201,120)->1 or not (021,120)->0\n",
      "StrategyProof: not (210,120)->1 or not (021,120)->2\n",
      "StrategyProof: not (210,120)->1 or not (201,120)->2\n",
      "StrategyProof: not (012,201)->2 or not (102,201)->0\n",
      "StrategyProof: not (012,201)->2 or not (102,201)->1\n",
      "StrategyProof: not (021,201)->2 or not (012,201)->0\n",
      "StrategyProof: not (021,201)->1 or not (210,201)->2\n",
      "StrategyProof: not (120,201)->0 or not (201,201)->2\n",
      "StrategyProof: not (210,201)->1 or not (201,201)->2\n",
      "StrategyProof: not (012,210)->1 or not (021,210)->0\n",
      "StrategyProof: not (021,210)->2 or not (102,210)->0\n",
      "StrategyProof: not (021,210)->1 or not (210,210)->0\n",
      "StrategyProof: not (021,210)->1 or not (210,210)->2\n",
      "StrategyProof: not (102,210)->2 or not (012,210)->0\n",
      "StrategyProof: not (102,210)->2 or not (210,210)->0\n",
      "StrategyProof: not (102,210)->2 or not (210,210)->1\n",
      "StrategyProof: not (120,210)->2 or not (012,210)->1\n",
      "StrategyProof: not (120,210)->2 or not (102,210)->1\n",
      "StrategyProof: not (120,210)->0 or not (210,210)->2\n",
      "StrategyProof: not (201,210)->1 or not (210,210)->0\n",
      "StrategyProof: not (201,210)->0 or not (210,210)->2\n",
      "StrategyProof: not (201,210)->1 or not (210,210)->2\n",
      "StrategyProof: not (210,210)->1 or not (021,210)->2\n",
      "StrategyProof: not (210,210)->0 or not (102,210)->1\n",
      "StrategyProof: not (012,012)->1 or not (012,021)->0\n",
      "StrategyProof: not (012,012)->1 or not (012,120)->0\n",
      "StrategyProof: not (012,012)->1 or not (012,201)->0\n",
      "StrategyProof: not (021,012)->1 or not (021,021)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,021)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,021)->1\n",
      "StrategyProof: not (021,012)->1 or not (021,102)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,102)->0\n",
      "StrategyProof: not (021,012)->1 or not (021,120)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,120)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,120)->1\n",
      "StrategyProof: not (021,012)->1 or not (021,201)->0\n",
      "StrategyProof: not (021,012)->1 or not (021,210)->0\n",
      "StrategyProof: not (021,012)->2 or not (021,210)->0\n",
      "StrategyProof: not (102,012)->1 or not (102,021)->0\n",
      "StrategyProof: not (102,012)->1 or not (102,201)->0\n",
      "StrategyProof: not (102,012)->2 or not (102,210)->1\n",
      "StrategyProof: not (120,012)->1 or not (120,021)->0\n",
      "StrategyProof: not (120,012)->2 or not (120,102)->0\n",
      "StrategyProof: not (120,012)->1 or not (120,120)->0\n",
      "StrategyProof: not (120,012)->2 or not (120,120)->0\n",
      "StrategyProof: not (120,012)->2 or not (120,120)->1\n",
      "StrategyProof: not (120,012)->1 or not (120,201)->0\n",
      "StrategyProof: not (120,012)->2 or not (120,201)->1\n",
      "StrategyProof: not (201,012)->1 or not (201,021)->0\n",
      "StrategyProof: not (201,012)->2 or not (201,102)->0\n",
      "StrategyProof: not (201,012)->2 or not (201,102)->1\n",
      "StrategyProof: not (201,012)->1 or not (201,120)->0\n",
      "StrategyProof: not (201,012)->2 or not (201,120)->1\n",
      "StrategyProof: not (201,012)->1 or not (201,201)->0\n",
      "StrategyProof: not (210,012)->1 or not (210,021)->0\n",
      "StrategyProof: not (210,012)->2 or not (210,021)->0\n",
      "StrategyProof: not (210,012)->1 or not (210,102)->0\n",
      "StrategyProof: not (210,012)->2 or not (210,102)->0\n",
      "StrategyProof: not (210,012)->1 or not (210,201)->0\n",
      "StrategyProof: not (210,012)->2 or not (210,210)->1\n",
      "StrategyProof: not (012,021)->1 or not (012,012)->0\n",
      "StrategyProof: not (012,021)->2 or not (012,012)->0\n",
      "StrategyProof: not (021,021)->1 or not (021,012)->0\n",
      "StrategyProof: not (102,021)->1 or not (102,210)->0\n",
      "StrategyProof: not (102,021)->1 or not (102,210)->2\n",
      "StrategyProof: not (120,021)->2 or not (120,012)->0\n",
      "StrategyProof: not (120,021)->1 or not (120,210)->0\n",
      "StrategyProof: not (120,021)->1 or not (120,210)->2\n",
      "StrategyProof: not (201,021)->2 or not (201,012)->0\n",
      "StrategyProof: not (201,021)->2 or not (201,102)->0\n",
      "StrategyProof: not (201,021)->1 or not (201,210)->0\n",
      "StrategyProof: not (201,021)->1 or not (201,210)->2\n",
      "StrategyProof: not (210,021)->1 or not (210,210)->0\n",
      "StrategyProof: not (210,021)->1 or not (210,210)->2\n",
      "StrategyProof: not (012,102)->2 or not (012,012)->0\n",
      "StrategyProof: not (012,102)->0 or not (012,120)->1\n",
      "StrategyProof: not (021,102)->2 or not (021,012)->0\n",
      "StrategyProof: not (021,102)->0 or not (021,120)->1\n",
      "StrategyProof: not (102,102)->2 or not (102,012)->0\n",
      "StrategyProof: not (102,102)->2 or not (102,012)->1\n",
      "StrategyProof: not (102,102)->0 or not (102,210)->1\n",
      "StrategyProof: not (120,102)->2 or not (120,012)->0\n",
      "StrategyProof: not (120,102)->2 or not (120,012)->1\n",
      "StrategyProof: not (120,102)->0 or not (120,120)->1\n",
      "StrategyProof: not (201,102)->2 or not (201,012)->0\n",
      "StrategyProof: not (201,102)->0 or not (201,120)->1\n",
      "StrategyProof: not (210,102)->2 or not (210,012)->0\n",
      "StrategyProof: not (210,102)->0 or not (210,210)->1\n",
      "StrategyProof: not (210,102)->2 or not (210,210)->1\n",
      "StrategyProof: not (102,120)->0 or not (102,102)->1\n",
      "StrategyProof: not (102,120)->2 or not (102,102)->1\n",
      "StrategyProof: not (120,120)->2 or not (120,012)->1\n",
      "StrategyProof: not (120,120)->2 or not (120,102)->1\n",
      "StrategyProof: not (120,120)->0 or not (120,201)->2\n",
      "StrategyProof: not (120,120)->0 or not (120,210)->1\n",
      "StrategyProof: not (120,120)->2 or not (120,210)->1\n",
      "StrategyProof: not (201,120)->0 or not (201,210)->2\n",
      "StrategyProof: not (210,120)->2 or not (210,102)->1\n",
      "StrategyProof: not (210,120)->0 or not (210,210)->1\n",
      "StrategyProof: not (210,120)->0 or not (210,210)->2\n",
      "StrategyProof: not (012,201)->1 or not (012,012)->0\n",
      "StrategyProof: not (012,201)->0 or not (012,210)->2\n",
      "StrategyProof: not (021,201)->1 or not (021,210)->0\n",
      "StrategyProof: not (021,201)->0 or not (021,210)->2\n",
      "StrategyProof: not (102,201)->1 or not (102,210)->0\n",
      "StrategyProof: not (102,201)->0 or not (102,210)->2\n",
      "StrategyProof: not (120,201)->1 or not (120,012)->0\n",
      "StrategyProof: not (201,201)->1 or not (201,210)->0\n",
      "StrategyProof: not (201,201)->0 or not (201,210)->2\n",
      "StrategyProof: not (201,201)->1 or not (201,210)->2\n",
      "StrategyProof: not (210,201)->1 or not (210,210)->0\n",
      "StrategyProof: not (210,201)->0 or not (210,210)->2\n",
      "StrategyProof: not (012,210)->0 or not (012,102)->1\n",
      "StrategyProof: not (012,210)->0 or not (012,120)->1\n",
      "StrategyProof: not (021,210)->0 or not (021,120)->1\n",
      "StrategyProof: not (102,210)->0 or not (102,120)->1\n",
      "StrategyProof: not (102,210)->1 or not (102,201)->2\n",
      "StrategyProof: not (120,210)->1 or not (120,021)->2\n",
      "StrategyProof: not (120,210)->0 or not (120,120)->1\n",
      "StrategyProof: not (120,210)->1 or not (120,201)->2\n",
      "StrategyProof: not (210,210)->1 or not (210,021)->2\n",
      "StrategyProof: not (210,210)->0 or not (210,120)->1\n",
      "StrategyProof: not (210,210)->1 or not (210,201)->2\n",
      "Surjective: (012,012)->0 or (021,012)->0 or (102,012)->0 or (120,012)->0 or (201,012)->0 or (210,012)->0 or (012,021)->0 or (021,021)->0 or (102,021)->0 or (120,021)->0 or (201,021)->0 or (210,021)->0 or (012,102)->0 or (021,102)->0 or (102,102)->0 or (120,102)->0 or (201,102)->0 or (210,102)->0 or (012,120)->0 or (021,120)->0 or (102,120)->0 or (120,120)->0 or (201,120)->0 or (210,120)->0 or (012,201)->0 or (021,201)->0 or (102,201)->0 or (120,201)->0 or (201,201)->0 or (210,201)->0 or (012,210)->0 or (021,210)->0 or (102,210)->0 or (120,210)->0 or (201,210)->0 or (210,210)->0\n",
      "Surjective: (012,012)->1 or (021,012)->1 or (102,012)->1 or (120,012)->1 or (201,012)->1 or (210,012)->1 or (012,021)->1 or (021,021)->1 or (102,021)->1 or (120,021)->1 or (201,021)->1 or (210,021)->1 or (012,102)->1 or (021,102)->1 or (102,102)->1 or (120,102)->1 or (201,102)->1 or (210,102)->1 or (012,120)->1 or (021,120)->1 or (102,120)->1 or (120,120)->1 or (201,120)->1 or (210,120)->1 or (012,201)->1 or (021,201)->1 or (102,201)->1 or (120,201)->1 or (201,201)->1 or (210,201)->1 or (012,210)->1 or (021,210)->1 or (102,210)->1 or (120,210)->1 or (201,210)->1 or (210,210)->1\n",
      "Surjective: (012,012)->2 or (021,012)->2 or (102,012)->2 or (120,012)->2 or (201,012)->2 or (210,012)->2 or (012,021)->2 or (021,021)->2 or (102,021)->2 or (120,021)->2 or (201,021)->2 or (210,021)->2 or (012,102)->2 or (021,102)->2 or (102,102)->2 or (120,102)->2 or (201,102)->2 or (210,102)->2 or (012,120)->2 or (021,120)->2 or (102,120)->2 or (120,120)->2 or (201,120)->2 or (210,120)->2 or (012,201)->2 or (021,201)->2 or (102,201)->2 or (120,201)->2 or (201,201)->2 or (210,201)->2 or (012,210)->2 or (021,210)->2 or (102,210)->2 or (120,210)->2 or (201,210)->2 or (210,210)->2\n",
      "NonDictatorial: not (012,012)->0 or not (021,012)->0 or not (102,012)->1 or not (120,012)->1 or not (201,012)->2 or not (210,012)->2 or not (012,021)->0 or not (021,021)->0 or not (102,021)->1 or not (120,021)->1 or not (201,021)->2 or not (210,021)->2 or not (012,102)->0 or not (021,102)->0 or not (102,102)->1 or not (120,102)->1 or not (201,102)->2 or not (210,102)->2 or not (012,120)->0 or not (021,120)->0 or not (102,120)->1 or not (120,120)->1 or not (201,120)->2 or not (210,120)->2 or not (012,201)->0 or not (021,201)->0 or not (102,201)->1 or not (120,201)->1 or not (201,201)->2 or not (210,201)->2 or not (012,210)->0 or not (021,210)->0 or not (102,210)->1 or not (120,210)->1 or not (201,210)->2 or not (210,210)->2\n",
      "NonDictatorial: not (012,012)->0 or not (021,012)->0 or not (102,012)->0 or not (120,012)->0 or not (201,012)->0 or not (210,012)->0 or not (012,021)->0 or not (021,021)->0 or not (102,021)->0 or not (120,021)->0 or not (201,021)->0 or not (210,021)->0 or not (012,102)->1 or not (021,102)->1 or not (102,102)->1 or not (120,102)->1 or not (201,102)->1 or not (210,102)->1 or not (012,120)->1 or not (021,120)->1 or not (102,120)->1 or not (120,120)->1 or not (201,120)->1 or not (210,120)->1 or not (012,201)->2 or not (021,201)->2 or not (102,201)->2 or not (120,201)->2 or not (201,201)->2 or not (210,201)->2 or not (012,210)->2 or not (021,210)->2 or not (102,210)->2 or not (120,210)->2 or not (201,210)->2 or not (210,210)->2\n"
     ]
    }
   ],
   "source": [
    "explainCNF(mus)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "609a6300",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.11"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}