{
  "nbformat": 4,
  "nbformat_minor": 0,
  "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"
    },
    "toc": {
      "base_numbering": 1,
      "nav_menu": {},
      "number_sections": true,
      "sideBar": true,
      "skip_h1_title": false,
      "title_cell": "Table of Contents",
      "title_sidebar": "Contents",
      "toc_cell": false,
      "toc_position": {},
      "toc_section_display": true,
      "toc_window_display": false
    },
    "colab": {
      "name": "LabZ3.ipynb",
      "provenance": [],
      "collapsed_sections": [],
      "include_colab_link": true
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "view-in-github",
        "colab_type": "text"
      },
      "source": [
        "<a href=\"https://colab.research.google.com/github/lclem/logic_course/blob/master/docs/labs/LabZ3.ipynb\" target=\"_parent\"><img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open In Colab\"/></a>"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "3",
        "colab_type": "text"
      },
      "source": [
        "# SAT solving in Python with Z3\n",
        "\n",
        "We will be using Z3 programmatically in Python.\n",
        "Consider the following classical logic tautologies:\n",
        "\n",
        "\\begin{align}\n",
        "    \\varphi_1 &\\ \\equiv\\ p \\vee \\neg p & \\textrm{ (excluded middle)} \\\\\n",
        "    \\varphi_2 &\\ \\equiv\\ ((p \\to q) \\to p) \\to p & \\textrm{ (Pierce's law)}.\n",
        "\\end{align}\n",
        " \n",
        "The Z3 code below (via its convenient Python interface) checks that the formulas above are tautologies by trying to find a satisfying assignment to their negation."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "zWK4E7FDZJrg",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "%pip install z3-solver\n",
        "\n",
        "from z3 import *\n",
        "\n",
        "# create a fresh propositional variable uniquely identified by its name 'p'\n",
        "p = Bool('p')\n",
        "\n",
        "# excluded middle\n",
        "solve(Not(Or(p, Not(p))))\n",
        "\n",
        "# Pierce's law\n",
        "q = Bool('q')\n",
        "solve(Not(Implies(Implies(Implies(p, q), p), p)))\n",
        "\n",
        "#Other useful connectives:\n",
        "#And"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "yQ8vP3UCZJrl",
        "colab_type": "text"
      },
      "source": [
        "## Exercise (tautologies)\n",
        "\n",
        "Prove that the following propositional formula is a classical tautology\n",
        "by checking that its negation is unsatisfiable:\n",
        "\\begin{align}\n",
        "    (p \\land q \\to r) \\leftrightarrow (p \\to q \\to r) \\\\    \n",
        "\\end{align}\n",
        "What about the following Łukasiewicz's formula?\n",
        "\\begin{align}\n",
        "((p \\to q) \\to r) \\to (r \\to p) \\to s \\to p.\n",
        "\\end{align}"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "tags": [
          "solution"
        ],
        "id": "OJkfb2-oZJrm",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "r = Bool('r')\n",
        "s = Bool('s')"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "g3U5sn1fZJrq",
        "colab_type": "text"
      },
      "source": [
        "## Example (long conjunctions and disjunctions)\n",
        "\n",
        "We can conveniently use arrays to represent long conjunctions `And` and disjunctions `Or`.\n",
        "For instance the next cell implements the following formula:\n",
        "\\begin{align}\n",
        "    x_1 \\wedge x_2 \\wedge \\cdots \\wedge x_n.\n",
        "\\end{align}"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "4x6MESzWZJrr",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "n = 10\n",
        "x = [Bool('x' + str(k)) for k in range(n)]\n",
        "phi = And([x[k] for k in range(n)])\n",
        "print(phi)\n",
        "solve(phi)"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "FySYBmCbZJru",
        "colab_type": "text"
      },
      "source": [
        "## Exercise (The SCS problem)\n",
        "\n",
        "Let $\\Sigma = \\{0, 1\\}$ be a finite alphabet.\n",
        "The *shortest common substring* problem (SCS) has as input a set of finite strings\n",
        "$S = \\{w_1, \\dots, w_m\\}$ with $w_i \\in \\Sigma^*$\n",
        "and a bound $n$, and asks to determine whether there is a string $w \\in \\Sigma^n$ of length $n$\n",
        "s.t. every $w_i$ is a (*contiguous*) substring of $w$. The SCS problem is NP-complete.\n",
        "1. Encode the SCS problem as a SAT problem and use Z3 to solve it.\n",
        "2. Can you reconstruct a solution $w$ from the Z3 model?"
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "8_lOCfUtZJru",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# input example\n",
        "S = [\"001010011101\", \"1001010101011\", \"101101010101010\",\n",
        "     \"10111011001010101010\", \"10110101011010101010\", \"10110101101010101010\"]\n",
        "m = len(S)\n",
        "n = 75 # tight\n",
        "# 12 + 13 + 15 + 20 + 20 + 20 = 100\n",
        "# students reported 74 is a solution\n",
        "\n",
        "# how to declare a list of n variables x0, ..., x(n-1)\n",
        "x = [ Bool('x' + str(k)) for k in range(n) ]\n",
        "\n",
        "# Solution for S: 001010011101101011010101010100101010101110110010101010101101010110101010100\n",
        "\n",
        "# this procedure returns an assignment (as a dictionary) if any exists\n",
        "def model(phi):\n",
        "    \n",
        "    # create a SAT instance\n",
        "    s = Solver()\n",
        "    s.add(phi)\n",
        "\n",
        "    # return a satisfying assignment\n",
        "    return s.model() if s.check() == sat else []"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "Z1TvMIgGZJr0",
        "colab_type": "text"
      },
      "source": [
        "## Exercise (All satisfying assignments)\n",
        "The Z3 solver returns some satisfying assignment, just in case it exists. How can we use Z3 in order to construct all satisfying assignments? Write a Python program that returns all satisfying assignments of a given SAT instance and test it on the Pigeonhole formulas from the previous exercise."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "Vdx3zV-RZJr0",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "# this procedure returns an assignment (as a dictionary) if any exists\n",
        "def model(phi):\n",
        "    \n",
        "    # create a SAT instance\n",
        "    s = Solver()\n",
        "    s.add(phi)\n",
        "\n",
        "    # return a satisfying assignment as a dictionary\n",
        "    return s.model() if s.check() == sat else []\n",
        "\n",
        "p = Bool(\"p\")\n",
        "q = Bool(\"q\")\n",
        "r = Bool(\"r\")\n",
        "phi = Or(And(p, Not(q)), r)\n",
        "m = model(phi)\n",
        "print(m[p])\n",
        "print(m[q])\n",
        "print(m[r])\n",
        "\n",
        "# Pro tip 1: can enumerate all variables by looking at the keys of m\n",
        "# Pro tip 2: if x is a key of m,\n",
        "# the corresponding Z3 variable can be reconstructed with \"Bool(str(x))\"\n",
        "# (it should be just \"x\", but so is life)\n",
        "vars = [Bool(str(x)) for x in m]"
      ],
      "execution_count": 0,
      "outputs": []
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "qYiRu1FjZJr7",
        "colab_type": "text"
      },
      "source": [
        "## Exercise (Phase transition)\n",
        "\n",
        "In this exercise we explore the phenomenon of *phase transition* for the $k$-SAT problem, where $k$ is the size of each clause.\n",
        "Let $n$ be the number of variables $X = \\{x_1, \\dots, x_n\\}$ and let $m$ be the number of clauses.\n",
        "A random $k$-SAT instance is obtained by producing each of the $m$ clauses according to the following process:\n",
        "\n",
        "* Extract $k$ variables without replacement from $X$ and determine independently and uniformly whether each variable appears positively or negatively.\n",
        "\n",
        "Fix $k = 3$, $n = 10$,\n",
        "and let $p_{m/n}$ be the probability that a SAT instance randomly generated as above is satisfiable.\n",
        "1. For a fixed $m$, compute an estimate $\\hat p_{m / n}$ by sampling $N = 100$ instances as above.\n",
        "2. Plot the estimates $\\hat p_{m / n}$ as a function of $m \\in \\{1, \\dots, 10 * n \\}$.\n",
        "3. What is an \"interesting\" interval for $m$? Refine the interval above if necessary."
      ]
    },
    {
      "cell_type": "code",
      "metadata": {
        "id": "fmUxP9z0ZJr8",
        "colab_type": "code",
        "colab": {}
      },
      "source": [
        "import matplotlib.pyplot as plt\n",
        "import numpy as np\n",
        "import random\n",
        "\n",
        "# number of variables\n",
        "n = 10\n",
        "\n",
        "# size of a clause\n",
        "k = 3\n",
        "\n",
        "# number of samples per point\n",
        "N = 100\n",
        "\n",
        "variables = [Bool('x' + str(i)) for i in range(n)]\n",
        "\n",
        "# Hints:\n",
        "# np.random.choice(list) returns a random element from list\n",
        "# np.random.choice(list, k, replace=False) returns k random elements from list *without replacement*\n",
        "# np.mean(list) computes the average of the numbers in the list\n",
        "# plt.plot(list) generates a plot from a list of values\n",
        "# plt.show() displays the plot"
      ],
      "execution_count": 0,
      "outputs": []
    }
  ]
}