{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Check your setup! \n",
"To prepare for the tutorial on *Automated Reasoning for Social Choice Theory*, and specifically the hands-on parts of the tutorial where we will use SAT-solving technology to reason about voting rules, try to get this notebook to run on your machine."
]
},
{
"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 [PySAT](https://pysathq.github.io/) [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^{2}. 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 tutorial, we 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)$.\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": [
"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": [
"solve([[-1,-2,3], [2], [-3,1]])"
]
},
{
"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
}