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