Paracooba
1.0.0
Dies ist ein modulares Tool zur verteilten parallelen SAT- und QBF-Lösung. Es verwaltet automatisch den Lösungsprozess von Formeln mit bereitgestellten Würfeln über ein Netzwerk von Rechenknoten. Es verfügt außerdem über einen integrierten Cubing-Algorithmus. Cubes können diesem Tool im „iCNF“-Format bereitgestellt werden (normale DIMACS mit angehängten Cubes der Form a 1 2 3 0 ). Diese Würfel können beispielsweise bis März generiert werden.
Nachfolgend werden die beiden Nutzungsszenarien beschrieben. Es werden zusätzliche Befehlszeilenargumente bereitgestellt. Für weitere Informationen verwenden Sie --help . Einige Optionen haben noch keine Auswirkungen, da sie überarbeitet wurden. Die Binärdateien parac und paracs sind funktional identisch, paracs ist jedoch statisch mit allen Modulen verknüpft, während parac Module zur Laufzeit lädt. Wenn Sie Probleme beim Auffinden der erforderlichen Module haben, verwenden Sie paracs .
Das Ankündigungsintervall steuert die Häufigkeit von IPv4-UDP-Broadcasts in das lokale Subnetz, um andere Instanzen des Standardkommunikatormoduls zu finden. Alternativ können auch andere Fernbedienungen direkt angegeben werden.
Wenn dem Masterknoten zusätzliche Optionen für das Solver-Modul bereitgestellt werden, synchronisiert es die bereitgestellten Optionen automatisch mit allen anderen verbundenen Knoten. Beim Lösen von Formeln ohne vordefinierte Würfel ist die Option --resplit sehr nützlich, da sie CaDiCaL automatisch abbricht, wenn die Lösung zu lange dauert, und einen Lookahead-Löser anwendet, um einen neuen Würfel zu generieren.
Ein Beispiel für den Start eines neuen Masterknotens ist unten dargestellt.
parac <file.[i]cnf> [--cadical-cubes] [--resplit]
Zusätzlich zum SAT-Lösungsmodul ist mit dem Modul cpp_qbf_prefixexpander auch ein QBF-Solver integriert. Es analysiert eine QBF-Formel und gibt QBF-Löserwürfel basierend auf dem Präfix aus.
Der Standardaufruf verwendet den QBF-Solver DepQBF als Backend und funktioniert wie folgt (unter Verwendung der statischen Version ohne dynamisches Laden des Moduls):
paraqs <file.qdimacs> [--use-depqbf]
parac <file.[i]cnf> [--udp-announcement-interval 1000]
parac [--known-remote hostname]
Dieses Tool erfordert die folgenden externen Abhängigkeiten. Bitte stellen Sie sicher, dass deren Entwicklungsheader installiert sind, um die Software kompilieren zu können.
Mindestens getestete Boost-Version: 1.65.1
Alle anderen Abhängigkeiten sind in diesem Quellbaum (und den Submodulen) enthalten und müssen nicht speziell behandelt werden. Distrac kann auch vom Build ausgeschlossen werden, indem entweder das Submodul einfach nicht geklont wird oder indem -DENABLE_DISTRAC=OFF auf CMake gesetzt wird.
# 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
