Paracooba
1.0.0
Esta es una herramienta modular para la resolución paralela distribuida de SAT y QBF. Gestiona automáticamente el proceso de resolución de fórmulas con los cubos proporcionados a través de una red de nodos informáticos. También tiene un algoritmo de cubing integrado. Se pueden proporcionar cubos a esta herramienta en formato "iCNF" (DIMACS normal con cubos adjuntos de la forma a 1 2 3 0 ). Estos cubos se pueden generar, por ejemplo, en marzo.
Los dos escenarios de uso se describen a continuación. Se proporcionan argumentos de línea de comando adicionales; use --help para obtener más información. Algunas opciones aún no tienen ningún efecto, ya que han sido reelaboradas. Los binarios parac y paracs son funcionalmente idénticos, pero paracs está vinculado estáticamente a todos los módulos, mientras que parac carga los módulos en tiempo de ejecución. Si tiene problemas para encontrar los módulos necesarios, utilice paracs .
El intervalo de anuncio controla la frecuencia de las transmisiones UDP IPv4 en la subred local para encontrar otras instancias del módulo comunicador predeterminado. Alternativamente, se pueden especificar otros controles remotos directamente.
Al proporcionar opciones adicionales al módulo de resolución del nodo maestro, sincroniza automáticamente las opciones proporcionadas con todos los demás nodos conectados. Al resolver fórmulas sin cubos predefinidos, la opción --resplit es muy útil, ya que cancela automáticamente CaDiCaL cuando la resolución tarda demasiado y aplica un solucionador anticipado para generar un nuevo cubo.
A continuación se muestra un ejemplo de cómo iniciar un nuevo nodo maestro.
parac <file.[i]cnf> [--cadical-cubes] [--resplit]
Además del módulo de resolución SAT, también se integra un solucionador QBF en forma de módulo cpp_qbf_prefixexpander . Analiza una fórmula QBF y proporciona cubos de resolución QBF según el prefijo.
La invocación predeterminada utiliza el solucionador QBF DepQBF como backend y funciona de la siguiente manera (usando la versión estática sin carga dinámica del módulo):
paraqs <file.qdimacs> [--use-depqbf]
parac <file.[i]cnf> [--udp-announcement-interval 1000]
parac [--known-remote hostname]
Esta herramienta requiere las siguientes dependencias externas. Asegúrese de que sus encabezados de desarrollo estén instalados para poder compilar el software.
Versión de refuerzo mínima probada: 1.65.1
Todas las demás dependencias están incluidas en este árbol fuente (y submódulos) y no es necesario manejarlas específicamente. Distrac también se puede excluir de la compilación, ya sea simplemente no clonando el submódulo o configurando -DENABLE_DISTRAC=OFF en CMake.
# 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
