examples/sat.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# SAT solving in Python\n",
    "\n",
    "This is a small example to show how you use the [pysat](https://pysathq.github.io/) Python library to call SAT solvers.\n",
    "\n",
    "First, install pysat, e.g., using:\n",
    "`python -m pip install --upgrade --user python-sat`\n",
    "\n",
    "Let's start with importing some relevant things from the pysat library: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from pysat.formula import CNF\n",
    "from pysat.solvers import MinisatGH"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We will then create a CNF formula, and add some clauses to it.\n",
    "\n",
    "Let's take a simple example, representing the following formula:\n",
    "\n",
    "$(x_1 \\vee x_2) \\wedge\n",
    "(x_1 \\vee \\neg x_2) \\wedge\n",
    "(\\neg x_1 \\vee x_2) \\wedge\n",
    "(\\neg x_1 \\vee \\neg x_2 \\vee x_3) \\wedge\n",
    "(\\neg x_3 \\vee \\neg x_4)$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "formula = CNF();\n",
    "formula.append([1,2]);\n",
    "formula.append([1,-2]);\n",
    "formula.append([-1,2]);\n",
    "formula.append([-1,-2,3]);\n",
    "formula.append([-3,-4]);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We then create a solver object. Let's use the MinisatGH solver.\n",
    "\n",
    "And we load the CNF formula in the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "solver = MinisatGH();\n",
    "solver.append_formula(formula);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We then invoke the solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "answer = solver.solve();"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If `solver.solve()` found a model, we can access it as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Variable 1 is true\n",
      "Variable 2 is true\n",
      "Variable 3 is true\n",
      "Variable 4 is false\n"
     ]
    }
   ],
   "source": [
    "if answer == True:\n",
    "    for lit in solver.get_model():\n",
    "        if lit > 0:\n",
    "            print(\"Variable {} is true\".format(lit));\n",
    "        else:\n",
    "            print(\"Variable {} is false\".format(-1*lit));\n",
    "else:\n",
    "    print(\"Did not find a model!\");"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For more information, see the [pysat documentation](https://pysathq.github.io/docs/html/index.html)."
   ]
  }
 ],
 "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
}