Paracooba
=========

This is a modular tool for distributed parallel SAT & QBF solving. It
automatically manages the solving process of formulas with provided cubes over a
network of compute nodes. It also has an integrated cubing algorithm. Cubes can
be provided to this tool in "iCNF" format (normal DIMACS with appended cubes of
the form `a 1 2 3 0`). These cubes can for example be generated by
[March](https://github.com/marijnheule/CnC).

Usage [SAT]
-----------

The two usage scenarios are described below. Additional command line arguments
are provided, use `--help` for more information. Some options do not have any
effects yet, as they are reworked. The binaries `parac` and `paracs` are
functionally identical, but `paracs` is statically linked to all modules, while
`parac` loads modules at runtime. If you have issues with finding the required
modules, use `paracs`.

The announcement interval controls the frequency of IPv4 UDP broadcasts into the
local subnet to find other instances of the default communicator module.
Alternatively, other remotes can be specified directly.

When supplying additional options to the solver module to the master node, it
automatically syncs the provided options to all other connected nodes. When
solving formulas without predefined cubes, the `--resplit` option is very
useful, as it automatically aborts CaDiCaL when solving takes too long and
applies a lookahead solver to generate a new cube.

One example how to start a new master node is shown below.

    parac <file.[i]cnf> [--cadical-cubes] [--resplit]

Usage [QBF]
-----------

Additionally to the SAT solving module, a QBF solver is also integrated in the
form of the module `cpp_qbf_prefixexpander`. It parses a QBF formula and gives
QBF solvers cubes based on the prefix.

The default invocation uses the QBF solver DepQBF as backend and works as
follows (using the static version without dynamic module loading):

    paraqs <file.qdimacs> [--use-depqbf]

Networking
----------

### Master-Node ("solve this formula for me")

    parac <file.[i]cnf> [--udp-announcement-interval 1000]

### Daemon-Node ("provide compute node for other masters in the network")

    parac [--known-remote hostname]

External Dependencies
---------------------

This tool requires the following external dependencies. Please ensure that their
development headers are installed in order to be able to compile the software.

  - Boost Headers
  - Boost Log
  - Boost Program Options

Minimum tested boost version: 1.65.1

All other dependencies are included in this source-tree (and submodules) and do
not have to be handled specifically. [Distrac](https://github.com/maximaximal/Distrac)
can also be excluded from the build, either by simply not cloning the submodule or by
setting `-DENABLE_DISTRAC=OFF` to CMake.

Building
--------

    # Clone the repository
    git clone https://github.com/maximaximal/Paracooba.git
    git submodule update --init --recursive

    # Build directory
    mkdir build
    cd build

    # Building
    cmake ..
    make -j
