Paracooba

Paracooba

Il s'agit d'un outil modulaire pour la résolution parallèle distribuée de SAT et QBF. Il gère automatiquement le processus de résolution de formules avec les cubes fournis sur un réseau de nœuds de calcul. Il dispose également d’un algorithme de cubage intégré. Des cubes peuvent être fournis à cet outil au format "iCNF" (DIMACS normal avec des cubes annexés de la forme a 1 2 3 0 ). Ces cubes peuvent par exemple être générés d'ici mars.

Utilisation [SAT]

Les deux scénarios d'utilisation sont décrits ci-dessous. Des arguments de ligne de commande supplémentaires sont fournis, utilisez --help pour plus d'informations. Certaines options n'ont pas encore d'effet, car elles ont été retravaillées. Les binaires parac et paracs sont fonctionnellement identiques, mais paracs est lié statiquement à tous les modules, tandis que parac charge les modules au moment de l'exécution. Si vous rencontrez des difficultés pour trouver les modules requis, utilisez paracs .

L'intervalle d'annonce contrôle la fréquence des diffusions IPv4 UDP dans le sous-réseau local pour trouver d'autres instances du module de communication par défaut. Alternativement, d'autres télécommandes peuvent être spécifiées directement.

Lorsque vous fournissez des options supplémentaires au module solveur au nœud maître, il synchronise automatiquement les options fournies avec tous les autres nœuds connectés. Lors de la résolution de formules sans cubes prédéfinis, l'option --resplit est très utile, car elle abandonne automatiquement CaDiCaL lorsque la résolution prend trop de temps et applique un solveur anticipé pour générer un nouveau cube.

Un exemple de démarrage d'un nouveau nœud maître est présenté ci-dessous.

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

Utilisation [QBF]

En plus du module de résolution SAT, un solveur QBF est également intégré sous la forme du module cpp_qbf_prefixexpander . Il analyse une formule QBF et donne des cubes de solveurs QBF basés sur le préfixe.

L'invocation par défaut utilise le solveur QBF DepQBF comme backend et fonctionne comme suit (en utilisant la version statique sans chargement de module dynamique) :

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

Réseautage

Master-Node ("résoudre cette formule pour moi")

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

Daemon-Node ("fournir un nœud de calcul pour les autres maîtres du réseau")

 parac [--known-remote hostname]

Dépendances externes

Cet outil nécessite les dépendances externes suivantes. Veuillez vous assurer que leurs en-têtes de développement sont installés afin de pouvoir compiler le logiciel.

• Boostez les en-têtes
• Journal de boost
• Options du programme Boost

Version boost minimale testée : 1.65.1

Toutes les autres dépendances sont incluses dans cette arborescence source (et sous-modules) et ne doivent pas être gérées spécifiquement. Distrac peut également être exclu de la construction, soit simplement en ne clonant pas le sous-module, soit en définissant -DENABLE_DISTRAC=OFF sur CMake.

Bâtiment

 # 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