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.

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 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