Paracooba
1.0.0
これは、分散並列 SAT および QBF 解決のためのモジュール式ツールです。計算ノードのネットワーク上で、提供されたキューブを使用した数式の解決プロセスを自動的に管理します。また、統合された立方体アルゴリズムも備えています。キューブは、「iCNF」形式 ( a 1 2 3 0の形式のキューブが追加された通常の DIMACS) でこのツールに提供できます。これらのキューブは、たとえば 3 月までに生成できます。
以下に 2 つの使用シナリオについて説明します。追加のコマンドライン引数が提供されます。詳細については、 --helpを使用してください。一部のオプションは再加工されているため、まだ効果がありません。バイナリparacとparacs機能的には同じですが、 paracsすべてのモジュールに静的にリンクされ、 parac実行時にモジュールを読み込みます。必要なモジュールを見つけるのに問題がある場合は、 paracs使用してください。
アナウンス間隔は、デフォルト コミュニケータ モジュールの他のインスタンスを見つけるために、ローカル サブネットへの IPv4 UDP ブロードキャストの頻度を制御します。あるいは、他のリモコンを直接指定することもできます。
マスター ノードのソルバー モジュールに追加のオプションを提供すると、提供されたオプションが接続されている他のすべてのノードに自動的に同期されます。事前定義されたキューブを使用せずに数式を解く場合、 --resplitオプションは非常に便利です。これは、解決に時間がかかりすぎると自動的に CaDiCaL を中止し、先読みソルバーを適用して新しいキューブを生成するためです。
新しいマスターノードを起動する方法の一例を以下に示します。
parac <file.[i]cnf> [--cadical-cubes] [--resplit]
SAT 解決モジュールに加えて、QBF ソルバーもモジュールcpp_qbf_prefixexpanderの形式で統合されています。 QBF 式を解析し、プレフィックスに基づいて QBF ソルバーにキューブを与えます。
デフォルトの呼び出しは QBF ソルバー DepQBF をバックエンドとして使用し、次のように動作します (動的モジュールの読み込みなしで静的バージョンを使用)。
paraqs <file.qdimacs> [--use-depqbf]
parac <file.[i]cnf> [--udp-announcement-interval 1000]
parac [--known-remote hostname]
このツールには次の外部依存関係が必要です。ソフトウェアをコンパイルできるようにするために、開発ヘッダーがインストールされていることを確認してください。
テスト済みのブーストの最小バージョン: 1.65.1
他のすべての依存関係はこのソース ツリー (およびサブモジュール) に含まれており、特に処理する必要はありません。 Distrac は、サブモジュールのクローンを作成しないことによって、または CMake に-DENABLE_DISTRAC=OFFを設定することによって、ビルドから除外することもできます。
# 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
