Paracooba

Paracooba

Ini adalah alat modular untuk penyelesaian SAT & QBF paralel terdistribusi. Secara otomatis mengelola proses penyelesaian rumus dengan kubus yang disediakan melalui jaringan node komputasi. Ia juga memiliki algoritma cubing terintegrasi. Kubus dapat diberikan ke alat ini dalam format "iCNF" (DIMACS normal dengan tambahan kubus berbentuk a 1 2 3 0 ). Kubus ini misalnya dapat dihasilkan pada bulan Maret.

Penggunaan [SAT]

Dua skenario penggunaan dijelaskan di bawah ini. Argumen baris perintah tambahan disediakan, gunakan --help untuk informasi lebih lanjut. Beberapa opsi belum memiliki efek apa pun karena sedang dikerjakan ulang. Biner parac dan paracs secara fungsional identik, tetapi paracs terhubung secara statis ke semua modul, sementara parac memuat modul saat runtime. Jika Anda mengalami masalah dalam menemukan modul yang diperlukan, gunakan paracs .

Interval pengumuman mengontrol frekuensi siaran UDP IPv4 ke subnet lokal untuk menemukan contoh lain dari modul komunikator default. Alternatifnya, remote lain dapat ditentukan secara langsung.

Saat memberikan opsi tambahan ke modul solver ke node master, modul tersebut secara otomatis menyinkronkan opsi yang disediakan ke semua node lain yang terhubung. Saat menyelesaikan rumus tanpa kubus yang telah ditentukan sebelumnya, opsi --resplit sangat berguna, karena secara otomatis membatalkan CaDiCaL ketika penyelesaian memakan waktu terlalu lama dan menerapkan pemecah masalah untuk menghasilkan kubus baru.

Salah satu contoh cara memulai node master baru ditunjukkan di bawah ini.

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

Penggunaan [QBF]

Selain modul penyelesaian SAT, pemecah QBF juga terintegrasi dalam bentuk modul cpp_qbf_prefixexpander . Ini mem-parsing rumus QBF dan memberikan kubus pemecah QBF berdasarkan awalan.

Pemanggilan default menggunakan pemecah QBF DepQBF sebagai backend dan berfungsi sebagai berikut (menggunakan versi statis tanpa memuat modul dinamis):

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

Jaringan

Master-Node ("pecahkan rumus ini untuk saya")

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

Daemon-Node ("menyediakan node komputasi untuk master lain di jaringan")

 parac [--known-remote hostname]

Ketergantungan Eksternal

Alat ini memerlukan dependensi eksternal berikut. Harap pastikan bahwa header pengembangannya telah diinstal agar dapat mengkompilasi perangkat lunak.

• Tingkatkan Header
• Tingkatkan Log
• Tingkatkan Opsi Program

Versi peningkatan minimum yang diuji: 1.65.1

Semua dependensi lainnya disertakan dalam pohon sumber ini (dan submodul) dan tidak harus ditangani secara khusus. Distrac juga dapat dikecualikan dari build, baik dengan tidak mengkloning submodul atau dengan menyetel -DENABLE_DISTRAC=OFF ke CMake.

Bangunan

 # 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