beginners_guide_example_SAT.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "56f0b47e",
   "metadata": {},
   "source": [
    "# Example: Computing on the Dynex Platform with Python - SAT"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ed479bbd",
   "metadata": {},
   "source": [
    "Dynex is the world’s first neuromorphic supercomputing blockchain based on the DynexSolve chip algorithm,\n",
    "a Proof-of-Useful-Work (PoUW) approach to solving real-world problems. This example demonstrates how to use the Dynex SDK to use Pyton to compute on the Dynex Platform with Python."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "4c52a895",
   "metadata": {},
   "outputs": [],
   "source": [
    "import dynex\n",
    "import dimod"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "afd0e043",
   "metadata": {},
   "source": [
    "## Building a SAT Problem "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "499a2526",
   "metadata": {},
   "source": [
    "In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula \"a AND NOT b\" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, \"a AND NOT a\" is unsatisfiable."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cc67c3a1",
   "metadata": {},
   "source": [
    "We need to define a SAT model that represents our problem. The simplest way to build such a model is by defining the clauses:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "931cfac2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[1, -2, 3], [-1, 4, 5], [6, 7, -8], [-9, -10, 11], [12, 13, -14], [-1, 15, -16], [17, -18, 19], [-20, 2, 3], [4, -5, 6], [-7, 8, 9], [10, 11, -12], [-13, -14, 15], [16, 17, -18], [-19, 20, 1], [2, -3, 4], [-5, 6, 7], [8, 9, -10], [-11, -12, 13], [14, 15, -16], [-17, 18, 19]]\n"
     ]
    }
   ],
   "source": [
    "# Example: SAT problem:\n",
    "clauses = [[1, -2, 3], [-1, 4, 5], [6, 7, -8], [-9, -10, 11], [12, 13, -14],\n",
    "           [-1, 15, -16], [17, -18, 19], [-20, 2, 3], [4, -5, 6], [-7, 8, 9],\n",
    "           [10, 11, -12], [-13, -14, 15], [16, 17, -18], [-19, 20, 1], [2, -3, 4],\n",
    "           [-5, 6, 7], [8, 9, -10], [-11, -12, 13], [14, 15, -16], [-17, 18, 19]]\n",
    "\n",
    "model = dynex.SAT(clauses);\n",
    "\n",
    "print(clauses);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4122925b",
   "metadata": {},
   "source": [
    "## Interacting with the Dynex Sampler "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9e3c77de",
   "metadata": {},
   "source": [
    "To find the minimum energy state for a SAT model (the assignment of variable values that gives us the\n",
    "minimum energy value for our model), the Dynex SDK provides samplers and solvers. A solver is\n",
    "a resource that runs a problem. Samplers are processes that run a problem many times to obtain\n",
    "a collection of samples, each of which is a possible solution to our problem. For convenience, we\n",
    "will generally refer to Dynex’s samplers as a whole, to include solvers as well."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "0cbcad35",
   "metadata": {},
   "outputs": [],
   "source": [
    "sampler = dynex.DynexSampler(model);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1548a123",
   "metadata": {},
   "source": [
    "Once we have established our sampler in our program, we can call it for our model. Each type of\n",
    "model has its own method for interacting with the sampler, whether it be QUBO, BinaryQuadrticModel, or any other type. We call the sampler to sample our SAT model using one of Dynex’s sample functions, depending on what type of model we are using. For example, the code snippet below demonstrates how we can sample a SAT object using the Dynex Platform."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "ade2765b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 0.00s #workers: 1 #chips: 32 #steps: 1 global loc: 0 global energy: 1.5\n",
      "FINISHED READ AFTER 0.01 SECONDS\n",
      "SAMPLESET LOADED\n"
     ]
    }
   ],
   "source": [
    "sampleset = sampler.sample(num_reads=32, annealing_time = 100);"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6db670b2",
   "metadata": {},
   "source": [
    "After we have sampled our SAT model, the sampler returns a SampleSet object. This object contains all\n",
    "of the samples returned along with their corresponding energy value, number of chips, number of integration steps, and more. The additional information varies depending on which sampler is used. As users get more\n",
    "comfortable with the Dynex SDK and the variety of samplers available, it is often useful to take\n",
    "some time to explore the wealth of information provided in the SampleSet object. Some of the key properties and methods of a SampleSet that we access are the following:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "1975c33e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'sample': ['1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000', '1.000000'], 'chips': 32, 'steps': 1, 'loc': 0, 'energy': 1.5}\n"
     ]
    }
   ],
   "source": [
    "print(sampleset[-1]) # sample with the lowest energy"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ba609414",
   "metadata": {},
   "source": [
    "The sample shows the corresponding energy values for our QM and additional information like total energy, number of chips or number of integration steps."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "92cecdda",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[{'sample': ['1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000'],\n",
       "  'chips': 32,\n",
       "  'steps': 1,\n",
       "  'loc': 0,\n",
       "  'energy': 1.5},\n",
       " {'sample': ['1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000',\n",
       "   '1.000000'],\n",
       "  'chips': 32,\n",
       "  'steps': 1,\n",
       "  'loc': 0,\n",
       "  'energy': 1.5}]"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sampleset # the full set of samples"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "01232e54",
   "metadata": {},
   "source": [
    "Each line shows a sample (solution) that was returned, along with the corresponding energy value,\n",
    "number of chips used (each Dynex chip provides one read), and number of integration steps (=annealing_time). Note that the effecitve number of integration steps can be lower then the specified annealing_time, because the ODE integration ends when a solution has been found."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "11d4820e",
   "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.8.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}