Paracooba

帕拉库巴

这是一个用于分布式并行 SAT 和 QBF 求解的模块化工具。它通过计算节点网络自动管理使用提供的立方体的公式的求解过程。它还具有集成的立方算法。立方体可以“iCNF”格式提供给此工具（普通 DIMACS 附加形式为a 1 2 3 0的立方体）。例如，这些立方体可以在 March 之前生成。

用法 [SAT]

下面分别介绍两种使用场景。提供了其他命令行参数，使用--help获取更多信息。有些选项尚未产生任何效果，因为它们已被重新设计。二进制文件parac和paracs在功能上是相同的，但paracs静态链接到所有模块，而parac在运行时加载模块。如果您在查找所需模块时遇到问题，请使用paracs 。

公告间隔控制 IPv4 UDP 广播到本地子网的频率，以查找默认通信器模块的其他实例。或者，可以直接指定其他遥控器。

当向主节点的求解器模块提供附加选项时，它会自动将提供的选项同步到所有其他连接的节点。当求解没有预定义立方体的公式时， --resplit选项非常有用，因为当求解时间过长时它会自动中止 CaDiCaL，并应用前瞻求解器来生成新的立方体。

下面显示了如何启动新主节点的一个示例。

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

用法[QBF]

除了 SAT 求解模块之外，还以模块cpp_qbf_prefixexpander的形式集成了 QBF 求解器。它解析 QBF 公式并根据前缀给出 QBF 求解器立方体。

默认调用使用 QBF 求解器 DepQBF 作为后端，工作原理如下（使用静态版本，无需动态模块加载）：

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

联网

主节点（“帮我解决这个公式”）

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

Daemon-Node（“为网络中的其他主机提供计算节点”）

 parac [--known-remote hostname]

外部依赖

该工具需要以下外部依赖项。请确保安装了它们的开发头文件以便能够编译软件。

• 增强标头
• 升压日志
• 提升计划选项

最低测试的 boost 版本：1.65.1

所有其他依赖项都包含在此源代码树（和子模块）中，并且不必专门处理。也可以通过简单地不克隆子模块或通过为 CMake 设置-DENABLE_DISTRAC=OFF来从构建中排除 Distrac。

建筑

 # 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