{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# SAT Solving via Python\n",
    "To prepare for the part of the *Computational Social Choice* course where we are going to use SAT-solving technology to reason about voting rules, try to get this notebook to run on your machine. Prepared by [Ulle Endriss](https://staff.science.uva.nl/u.endriss/), ILLC, University of Amsterdam (November 2023)."
   ]
  },
  {
   "cell_type": "markdown",
   "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 the [PySAT](https://pysathq.github.io/) toolkit [installed](https://pysathq.github.io/installation/) on your machine. Download this notebook and run it locally (the copy on nbviewer.org is for non-interactive viewing only).\n",
    "\n",
    "To run the Python code in the cells below, click on a cell and then press *Shift* and *Enter* together. Note that in some cases there are dependencies between cells, and a given cell will only run successfully if (some of) the earlier cells have already been run. Alternatively, you can run *all* cells in order by pressing the \"fast forward\" button above (which will restart the kernel and run the entire notebook from scratch)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Basic Examples\n",
    "The first cell should print the string 'Hello world!' on the screen. The second one should calculate the product of 7 and 17<sup>2</sup>. The third one should return a list with the six possible permutations of the numbers 0, 1, and 2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print('Hello world!')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "7 * (17 ** 2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from itertools import permutations\n",
    "mylist = [0, 1, 2]\n",
    "list(permutations(mylist))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## SAT Solving\n",
    "During the course, we will want to use SAT-solving technology to reason about voting rules. 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 use PySAT to make available the functionality of one of the SAT solvers supported, in this case Glucose 3.0. But using any of the other solvers should work just as well."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "from pysat.solvers import Glucose3"
   ]
  },
  {
   "cell_type": "markdown",
   "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": null,
   "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",
   "metadata": {},
   "source": [
    "You do not need to understand the code in the previous cell. The point is that you can now use the method ```solve()``` without having to worry about the precise inner workings of PySAT.\n",
    "\n",
    "So let's try it. The first example below demonstrates that the formula $\\varphi = (\\neg p_1 \\lor p_2) \\land (p_1) \\land (\\neg p_2)$ is not satisfiable. Indeed, whatever truth values you assign to $p_1$ and $p_2$, the formula $\\varphi$ will always evaluate to *false*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "solve([[-1,2], [1], [-2]])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Our second example illustrates how you can obtain a model demonstrating the satisfiability of a given formula, in this case $\\varphi = (\\neg p_1 \\lor \\neg p_2 \\lor p_3) \\land (p_2) \\land(\\neg p_3 \\lor p_1)$. Note that $\\varphi$ has two satisfying models: we must set $p_2$ to *true* but can choose either truth value for $p_1$ and $p_3$, as long as those truth values are the same for both variables. The solver only reports one of those two models. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = [[-1,-2,3], [2], [-3,1]]\n",
    "model = solve(cnf)\n",
    "print(model)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The two models of our formula correspond to the lists ```[1,2,3]``` and ```[-1,2,-3]```. The output returned for the code in the previous cell should be one of those two terms. Let's assume it is the second (which one it actually is depends on the internals of the SAT solver used).\n",
    "\n",
    "Think about what we would need to do to get the solver to also compute the second model for us. We can do this in a systematic manner by adding a clause to our CNF that says that the model we already have found should not be considered a satisfactory solution anymore. To exclude the model that sets $p_2$ to true and $p_1$ and $p_3$ to false, we can add the clause $(p_1 \\lor \\neg p_2 \\lor p_3)$ to our CNF. At the code level, we can get from the *model* ```[-1,2,-3]``` to the *clause* ```[1,-2,3]``` by simply switching the signs of each of the numbers in the first list. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "clause = [-x for x in model] \n",
    "print(clause)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now let's append this additional clause to the end of our CNF and then run the solver again. This will produce the second model of the original formula."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf.append(clause)\n",
    "newmodel = solve(cnf)\n",
    "print(newmodel)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we repeat this process one more time, the solver will report ```UNSATISFIABLE```, meaning that the original formula indeed does not have a third model."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "newclause = [-x for x in newmodel]\n",
    "cnf.append(newclause)\n",
    "solve(cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In fact, PySAT also offers the possibility to directly compute all models of a given formula. The following cell provides access to this facility by implementing the method ```enumModels()```. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "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",
   "metadata": {},
   "source": [
    "Again, it is not important to understand the details of the implementation in the previous cell. Note that you can now compute the two models of the formula we considered earlier with a single call."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = [[-1,-2,3], [2], [-3,1]]\n",
    "models = enumModels(cnf)\n",
    "print(list(models))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "What do you expect will happen if you apply ```enumModels()``` to a formula that is unsatisfiable? You can always try."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "cnf = [[-1, 2], [1], [-2]]\n",
    "models = enumModels(cnf)\n",
    "print(list(models))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "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.7.7"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}