resources/SplitAndConquerGuide.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "contained-romance",
   "metadata": {},
   "source": [
    "# Marabou's Split & Conquer Guide\n",
    "\n",
    "This Notebook illustrates properties of the Split & Conquer (S&C) algorithm in Marabou, provides an overview of algorithm parameters, shows their impact on algorithm performance and offers some rules of thumb on how to choose parameter values for problems of unknown difficulty."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "interstate-trustee",
   "metadata": {},
   "source": [
    "## About Split & Conquer algorithm\n",
    "The algorithm is build on top of Marabou solver for neural network verification(NNV). Scalability is one of the chief hurdles for NNV. S&C algorithm is an effort-based algorithm, which dynamically decomposes queries which exceed the effort limit. \n",
    "\n",
    "Effort is inpractice specified in the form of timeout - initially *t_0*. Whenever a query exceeds its timeout, the S&C algorithm will split it into a number of new queries. The number of splits *n* is another parameter of the algorithm, and will result in *2^n* new queries created. This new generation of queries will be solved with an increased timeout, which is specified through the timeout factor *f*. Each of the queries will in turn be solved with the new timout and this process is repeated, until either:\n",
    "1. a subquery is shown to be **satisfiable**\n",
    "2. or **all** the generated sub-queries are **unsatisfiable**.\n",
    "\n",
    "Here is an illustration of the S&C algorithm execution with 4 parallel workers:\n",
    "![Execution of Split & Conquer algorithm](img/snc.png)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "sunset-detail",
   "metadata": {},
   "source": [
    "### How to split the query?\n",
    "Queries can be split in various way - the two that have shown the most success are:\n",
    "\n",
    "1. **input range splitting** for networks with few inputs and \n",
    "2. **early ReLU phase splitting** for perception networks.\n",
    "\n",
    "Both approaches still require to choose which particular input or ReLU to split on. Marabou implements several heuristics for this choice. The crucial property for parallelization is that the resulting queries are of similar difficulty, which in terms of search space means that the splits are *balanced*. The metric to estimate balance we call **polarity** and is the default choice for S&C.\n",
    "\n",
    "A crucial point is that the above splitting strategies generate queries whose disjucntion is equivalent to the original query. This is essential for completeness of the overall algorithm and trustworthiness of reported results."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "further-projection",
   "metadata": {},
   "source": [
    "## Getting a feel for S&C parameters\n",
    "\n",
    "In this section we will run a series of examples to show how different parameter values affect execution."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "hungarian-arrow",
   "metadata": {},
   "source": [
    "### First, run a sequential problem"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "substantial-saver",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Supress TF deprecation warnings\n",
    "import warnings\n",
    "warnings.filterwarnings('ignore')\n",
    "\n",
    "import sys\n",
    "\n",
    "# Path to Marabou folder if you did not export it\n",
    "# sys.path.append('/PATH/TO/Marabou')\n",
    "\n",
    "\n",
    "from maraboupy import Marabou\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "substantial-result",
   "metadata": {},
   "outputs": [],
   "source": [
    "# Choose an input file that takes about 30seconds to solve \n",
    "# Network files are sorted in increasing order of difficulty\n",
    "#nnetFile = \"nnet/acasxu/ACASXU_experimental_v2a_2_6.nnet\"\n",
    "#nnetFile = \"nnet/acasxu/ACASXU_experimental_v2a_2_5.nnet\"\n",
    "nnetFile = \"nnet/acasxu/ACASXU_experimental_v2a_5_2.nnet\"\n",
    "\n",
    "# Load the network from NNet file\n",
    "net = Marabou.read_nnet(nnetFile)\n",
    "\n",
    "# Encode property 3 - see properties/acas_property3.txt\n",
    "lower_bounds = [-0.3035311561, -0.0095492966, 0.4933803236, 0.3,  0.3]\n",
    "upper_bounds = [ -0.2985528119, 0.0095492966, 0.5, 0.5, 0.5]\n",
    "\n",
    "for idx in range(len(net.inputVars[0])):\n",
    "    net.setLowerBound(net.inputVars[0][idx], lower_bounds[idx])\n",
    "    net.setUpperBound(net.inputVars[0][idx], upper_bounds[idx])\n",
    "\n",
    "net.addInequality(net.outputVars[0], [+1.0,-1.0, 0.0, 0.0, 0.0], 0.0)\n",
    "net.addInequality(net.outputVars[0], [+1.0, 0.0,-1.0, 0.0, 0.0], 0.0)\n",
    "net.addInequality(net.outputVars[0], [+1.0, 0.0, 0.0,-1.0, 0.0], 0.0)\n",
    "net.addInequality(net.outputVars[0], [+1.0, 0.0, 0.0, 0.0,-1.0], 0.0)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "featured-nursing",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "defaultOpts = Marabou.createOptions()\n",
    "vals1, stats1 = net.solve(options=defaultOpts)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "contemporary-today",
   "metadata": {},
   "source": [
    "The query is reported unsat and we note the wall clock time as a baseline to solve this problem using Marabou. \n",
    "\n",
    "For the purposes of this demo choose a network among commented options that takes ~15 seconds on your machine.\n",
    "\n",
    "Run locally, solving Property 3 on ACASXU_experimental_v2a_5_2.nnet takes 14s."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "consolidated-combine",
   "metadata": {},
   "source": [
    "### Run a problem using S&C\n",
    "To run a problem in S&C mode, add *snc=True* to the Marabou.createOptions call. \n",
    "\n",
    "Since only S&C moded is enable and no other S&C parameters have been set, the algorithm is executed **sequentially**."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ordered-liquid",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "sequentialSnC = Marabou.createOptions(snc=True)\n",
    "vals1, stats1 = net.solve(options=sequentialSnC)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "temporal-doctrine",
   "metadata": {},
   "source": [
    "The query is again found unsat, which we know from the previous call to Marabou.\n",
    "\n",
    "Marabou in SnC mode outputs lines of the following format on the command line/Jypyter console:\n",
    "\n",
    "Worker ID : Query ID SOLVING_STATUS, number of remaining tasks.\n",
    "\n",
    "> Worker 0: Query 1 TIMEOUT, 1 tasks remaining\n",
    "\n",
    "The algorithm is executed sequentially so Worker 0 will feature on all the lines. \n",
    "\n",
    "Query 1 denotes the original query and SOLVING_STATUS can be sat/unsat/TIMEOUT. \n",
    "\n",
    "Here, Query 1 TIMEOUTS with default timeout. We refer to Query 1 as the intial query or the initial generation.\n",
    "\n",
    "The default number of splits is 2, so upon TIMEOUT S&C will generate 4 (2^2) subqueries. \n",
    "\n",
    "Each query has an ID that shows its location in the search space. Query 1-3 indicates that is the 3rd split of Query 1. We refer to Queries 1-X as first generation. Each dash in the name will indicate another generation.\n",
    "\n",
    "> Worker 0: Query 1-1 unsat, 4 tasks remaining  \n",
    "  Worker 0: Query 1-2 unsat, 3 tasks remaining  \n",
    "  Worker 0: Query 1-3 unsat, 2 tasks remaining  \n",
    "  Worker 0: Query 1-4 unsat, 1 tasks remaining  \n",
    "\n",
    "We can see that after splitting and timeout increase, all 4 subqueries are found to be unsat which which we expect since Query 1 is unsat.\n",
    "\n",
    "Run locally sequential S&C took 17s, which is a decrease in performance compared to 14s Marabou took to solve the same problem. This is expected as SnC introduces overhead with each intermediate subquery that times out.\n",
    "\n",
    "### Run a problem using S&C in parallel\n",
    "To execute SnC in parallel add *numWorkers = 4* in the Marabou.createOptions(). \n",
    "\n",
    "To make the number of splits explicit we will add *onlineSplits = 2* to the options. S&C will perform 2^onlineSplits after every TIMEOUT. Since the default value is also 2 there will be no change in the number of subqueries generated compared to the sequential execution. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "round-ridge",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions(snc=True,\n",
    "                                    numWorkers=4,\n",
    "                                    onlineSplits=2\n",
    "                                   )\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "editorial-minister",
   "metadata": {},
   "source": [
    "Running locally with 4 workers this call took 10s of wall clock time which less than both Marabou and sequential S&C call. The total CPU time is the same for sequential and parallel S&C calls, the CPU resources are utilized more effectively.\n",
    "\n",
    "If we look at the S&C output:\n",
    "\n",
    "> Worker 3: Query 1 TIMEOUT, 1 tasks remaining  \n",
    "  Worker 1: Query 1-2 unsat, 4 tasks remaining  \n",
    "  Worker 3: Query 1-1 unsat, 3 tasks remaining  \n",
    "  Worker 0: Query 1-4 unsat, 2 tasks remaining  \n",
    "  Worker 2: Query 1-3 unsat, 1 tasks remaining\n",
    "\n",
    "we can notice that now there are 4 different workers featuring in the output.\n",
    "\n",
    "If we think for a moment, we will realize that Workers 0,1 and 2 were idling while Query 1 was solved. We will address this in the next section\n",
    "\n",
    "### Run parallel S&C with initial splits\n",
    "Rather then letting workers idle during the first query, a query can be immediately split to match the number of workers, skipping Query 1 and jumping directly to generation 1 of the previous examples. To achieve this we add *initialSplits=2* to the options.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "given-witness",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=4,\n",
    "                                     onlineSplits=2,\n",
    "                                     initialSplits=2)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "enormous-apache",
   "metadata": {},
   "source": [
    "This took 4.75s of wall clock time on my local machine, beating all previous wall clock runtimes. \n",
    "\n",
    "Since S&C is not waiting on the initial query to timeout, the total time is 11s. This is less than total times of the baseline Marabou call and previous S&C calls.\n",
    "\n",
    "Looking at the output:\n",
    "> Worker 1: Query 2 unsat, 4 tasks remaining  \n",
    "  Worker 0: Query 1 unsat, 3 tasks remaining  \n",
    "  Worker 2: Query 4 unsat, 2 tasks remaining  \n",
    "  Worker 3: Query 3 unsat, 1 tasks remaining\n",
    "\n",
    "We can see that the queries are treated as initial generation, meaning that their IDs do not contain dashes. Implicitly, (Query) 0- is ommited. \n",
    "\n",
    "With these options we can solve the problem in one generation. Now, let's take a look at how timeout and timeout factor affect the behavior of S&C algorithm.\n",
    "\n",
    "### S7C: Choosing initial timeout\n",
    "\n",
    "To set the initial timeout add *initialTimeout=3* to the Marabou options. This will set the timeout to 3 seconds which is less than the default of 5 seconds."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "relevant-condition",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=4,\n",
    "                                     onlineSplits=2,\n",
    "                                     initialSplits=2,\n",
    "                                     initialTimeout=3)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "partial-preservation",
   "metadata": {},
   "source": [
    "This call took 5s on my machine, which is just slightly longer than the pervious call of 4.75s.\n",
    "\n",
    "Let's look at the output of S&C:\n",
    "> Worker 3: Query 2 unsat, 4 tasks remaining  \n",
    "  Worker 0: Query 1 unsat, 3 tasks remaining  \n",
    "  Worker 1: Query 4 unsat, 2 tasks remaining  \n",
    "  Worker 2: Query 3 TIMEOUT, 1 tasks remaining  \n",
    "  Worker 0: Query 3-3 unsat, 4 tasks remaining  \n",
    "  Worker 2: Query 3-1 unsat, 3 tasks remaining  \n",
    "  Worker 1: Query 3-4 unsat, 2 tasks remaining  \n",
    "  Worker 3: Query 3-2 unsat, 1 tasks remaining\n",
    "  \n",
    "We can see that Query 3 timed out resulting in a new generation of problems to be solved, however they were quickly solved. \n",
    "\n",
    "Let's take a look at what happens when we decrease the initial timeout further to 1s."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "decimal-softball",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=4,\n",
    "                                     onlineSplits=2,\n",
    "                                     initialSplits=2,\n",
    "                                     initialTimeout=1)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "convenient-religion",
   "metadata": {},
   "source": [
    "This call takes 4s which is faster than 4.75s obtained with the default timeout.\n",
    "\n",
    "Looking at the output of S&C:\n",
    "> Worker 0: Query 2 unsat, 4 tasks remaining  \n",
    "  Worker 2: Query 1 TIMEOUT, 3 tasks remaining  \n",
    "  Worker 1: Query 4 TIMEOUT, 6 tasks remaining  \n",
    "  Worker 3: Query 3 TIMEOUT, 9 tasks remaining  \n",
    "  Worker 1: Query 1-2 unsat, 12 tasks remaining  \n",
    "  Worker 1: Query 4-1 unsat, 11 tasks remaining  \n",
    "  Worker 3: Query 1-4 unsat, 10 tasks remaining  \n",
    "  Worker 0: Query 1-3 unsat, 9 tasks remaining  \n",
    "  Worker 1: Query 4-2 unsat, 8 tasks remaining  \n",
    "  Worker 0: Query 4-4 unsat, 7 tasks remaining  \n",
    "  Worker 2: Query 1-1 unsat, 6 tasks remaining  \n",
    "  Worker 2: Query 3-3 unsat, 5 tasks remaining  \n",
    "  Worker 1: Query 3-1 unsat, 4 tasks remaining  \n",
    "  Worker 3: Query 4-3 unsat, 3 tasks remaining  \n",
    "  Worker 2: Query 3-4 unsat, 2 tasks remaining  \n",
    "  Worker 0: Query 3-2 unsat, 1 tasks remaining\n",
    "  \n",
    "We can see that most of the initial generation times out, but that overall solving time improves. This suggests that **aggessive splitting might be a good strategy for this problem**. However, rather than wasting time by letting most of the initial generation time out, let's increase the number of initial splits to 4 (which results in 16 problems) and see what happens.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "intermediate-crawford",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=4,\n",
    "                                     onlineSplits=2,\n",
    "                                     initialSplits=4,\n",
    "                                     initialTimeout=5)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "roman-discrimination",
   "metadata": {},
   "source": [
    "This call took 1.95s of wall clock time and 5.81s of CPU time. Which reduces both wall-clock and total time by nearly 50%.\n",
    "\n",
    "So a rule of thumb is that if initial generations are timing out, either:\n",
    "1. **aggressively split using initialSplits** (regardless of the number of workers, they will be properly queued)\n",
    "2. **increase the timeout until some intial queries a solved effectively**, in particular when dealing with large networks (>1k nodes) this will be necessary. \n",
    "\n",
    "This is just one of the timeout parameters, the other is timeout factor which we will take a look at in the next section.\n",
    "\n",
    "### S&C: Choosing timeout factor\n",
    "The timeout factor indicates how much extra effort we want to spend on the next generation. For completeness purposes the factor needs to be strictly greater than 1, although with aggressive splitting that may be unnecessary.\n",
    "\n",
    "To simulate a more challenging query, let's reduce the number of workers to 2 and set initial and online divides and timeout to 1. We'll set the *timeoutFactor=1.25*, i.e. each generation gets 25% more time than the previous one."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "successful-publicity",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=2,\n",
    "                                     onlineSplits=1,\n",
    "                                     initialSplits=1,\n",
    "                                     initialTimeout=1,\n",
    "                                     timeoutFactor=1.25)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "catholic-conviction",
   "metadata": {},
   "source": [
    "This call takes 10s of wall clock time. \n",
    "\n",
    "Looking at the S&C ouput:\n",
    "\n",
    "> Worker 1: Query 2 TIMEOUT, 2 tasks remaining  \n",
    "  Worker 0: Query 1 TIMEOUT, 3 tasks remaining  \n",
    "  Worker 1: Query 2-1 TIMEOUT, 4 tasks remaining\n",
    "  Worker 0: Query 2-2 TIMEOUT, 5 tasks remaining\n",
    "  Worker 0: Query 1-2 unsat, 6 tasks remaining  \n",
    "  Worker 0: Query 2-1-1 unsat, 5 tasks remaining  \n",
    "  Worker 1: Query 1-1 TIMEOUT, 4 tasks remaining  \n",
    "  Worker 1: Query 2-2-1 unsat, 5 tasks remaining  \n",
    "  Worker 0: Query 2-1-2 unsat, 4 tasks remaining  \n",
    "  Worker 1: Query 2-2-2 unsat, 3 tasks remaining  \n",
    "  Worker 0: Query 1-1-1 unsat, 2 tasks remaining  \n",
    "  Worker 1: Query 1-1-2 unsat, 1 tasks remaining\n",
    "\n",
    "For the next attempt lets increase the timeoutFactor to 3, and observe the results."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "standard-nelson",
   "metadata": {},
   "outputs": [],
   "source": [
    "%%time\n",
    "SnC4workers = Marabou.createOptions( snc=True,\n",
    "                                     numWorkers=2,\n",
    "                                     onlineSplits=1,\n",
    "                                     initialSplits=1,\n",
    "                                     initialTimeout=1,\n",
    "                                     timeoutFactor=3)\n",
    "vals1, stats1 = net.solve(options=SnC4workers)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "communist-central",
   "metadata": {},
   "source": [
    "This call took 9.84s which is barely less than 10s of the previous call. \n",
    "\n",
    "We can see that it needed to solve fewer queries:\n",
    "> Worker 1: Query 1 TIMEOUT, 2 tasks remaining  \n",
    "  Worker 0: Query 2 TIMEOUT, 3 tasks remaining  \n",
    "  Worker 0: Query 1-2 unsat, 4 tasks remaining  \n",
    "  Worker 1: Query 1-1 unsat, 3 tasks remaining  \n",
    "  Worker 0: Query 2-1 TIMEOUT, 2 tasks remaining  \n",
    "  Worker 1: Query 2-2 unsat, 3 tasks remaining  \n",
    "  Worker 0: Query 2-1-1 unsat, 2 tasks remaining  \n",
    "  Worker 1: Query 2-1-2 unsat, 1 tasks remaining  \n",
    "\n",
    "But the time didn't improve much. What one needs to keep in mind when choosing the timeoutFactor is that wall clock solving time will be determined by the last generation generated. Each query in generation i takes T_0 * TimeoutFactor^i when it times out. \n",
    "\n",
    "One can look at a some initial set of solved queries of an incomplete solving run, use generation info to bucket them by solving time and use that information to choose intialSplits, timeout and timeoutFactor values in a way that will avoid unnecessary TIMEOUTs. \n",
    "\n",
    "\n",
    "This concludes this demo, and hopefully provides you with an idea on how to think about Split & Conquer parameters.\n",
    "  "
   ]
  }
 ],
 "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.6.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}