Update README.md

README.md

@@ -40,6 +40,15 @@ The Python interface currently supports Python 3.8, 3.9, 3.10 and 3.11.
 
 ### Building from source
 
+#### Build dependencies
+
+The build process uses CMake version 3.16 (or later).
+You can get CMake [here](https://cmake.org/download/).
+
+Marabou depends on the Boost and the OpenBLAS libraries, which is automatically 
+downloaded and built when you run make. Library CXXTEST comes included in the 
+repository.
+
 The current version of Marabou can be built for Linux or MacOS machines using CMake:
 ```bash
 git clone https://github.com/NeuralNetworkVerification/Marabou/
@@ -159,6 +168,42 @@ The `maraboupy/examples` folder contains a list of examples. Please also see our
 [documentation](https://neuralnetworkverification.github.io/Marabou/) for the python interface, 
 which contains examples, API documentation, and a developer's guide.
 
+### Advanced configuration
+
+#### Choice of solver configurations
+
+Currently the default configuration of Marabou is a *single-threaded* one that
+uses DeepPoly analysis for bound tightening, and the DeepSoI procedure during the complete search.
+For optimal runtime performance, you need to build Marabou with Gurobi enabled (See sub-section below for Gurobi installation),
+so that LPs are solved by Gurobi instead of the open-source native simplex engine.  
+
+You could also leverage *parallelism* by setting the num-workers option to N. This will spawn N threads, each solving
+the original verification query using the single-threaded configuration with
+a different random seed. This is the preferred parallelization strategy for low level of parallelism (e.g. N < 30).
+For example to solve a query using this mode with 4 threads spawned:
+```
+./resources/runMarabou.py resources/nnet/mnist/mnist10x10.nnet resources/properties/mnist/image3_target6_epsilon0.05.txt --num-workers=4
+```
+
+If you have access to a large number of threads, you could also consider the Split-and-Conquer mode (see below).
+
+#### Using the Split and Conquer (SNC) mode
+
+In the SNC mode, activated by *--snc* Marabou decomposes the problem into *2^n0*
+sub-problems, specified by *--initial-divides=n0*. Each sub-problem will be
+solved with initial timeout of *t0*, supplied by *--initial-timeout=t0*. Every
+sub-problem that times out will be divided into *2^n* additional sub-problems,
+*--num-online-divides=n*, and the timeout is multiplied by a factor of *f*,
+*--timeout-factor=f*. Number of parallel threads *t* is specified by
+*--num-workers=t*.
+
+So to solve a problem in SNC mode with 4 initial splits and initial timeout of 5s, 4 splits on each timeout and a timeout factor of 1.5:
+```
+build/Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/properties/acas_property_3.txt --snc --initial-divides=4 --initial-timeout=5 --num-online-divides=4 --timeout-factor=1.5 --num-workers=4
+```
+
+A guide to Split and Conquer is available as a Jupyter Notebook in [resources/SplitAndConquerGuide.ipynb](resources/SplitAndConquerGuide.ipynb).
+
 ## Developing Marabou
 
 ### Setting up your development environment