Paracooba

Паракуба

Это модульный инструмент для распределенного параллельного решения SAT и QBF. Он автоматически управляет процессом решения формул с помощью предоставленных кубов по сети вычислительных узлов. Он также имеет встроенный алгоритм кубирования. Кубы могут быть предоставлены этому инструменту в формате «iCNF» (обычный DIMACS с добавленными кубами в форме a 1 2 3 0 ). Эти кубы могут быть созданы, например, к марту.

Использование [СБ]

Ниже описаны два сценария использования. Предоставляются дополнительные аргументы командной строки. Для получения дополнительной информации используйте --help . Некоторые опции пока не имеют никаких эффектов, так как они переработаны. Двоичные файлы parac и paracs функционально идентичны, но paracs статически связан со всеми модулями, а parac загружает модули во время выполнения. Если у вас возникли проблемы с поиском необходимых модулей, используйте paracs .

Интервал объявления контролирует частоту широковещательных рассылок IPv4 UDP в локальную подсеть для поиска других экземпляров модуля коммуникатора по умолчанию. Альтернативно, другие пульты можно указать напрямую.

При передаче дополнительных опций решающему модулю на главный узел он автоматически синхронизирует предоставленные опции со всеми другими подключенными узлами. При решении формул без предопределенных кубов опция --resplit очень полезна, поскольку она автоматически прерывает CaDiCaL, если решение занимает слишком много времени, и применяет упреждающий решатель для создания нового куба.

Один из примеров запуска нового главного узла показан ниже.

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

Использование [QBF]

В дополнение к решающему модулю SAT также интегрирован решатель QBF в виде модуля cpp_qbf_prefixexpander . Он анализирует формулу QBF и выдает кубы решателей QBF на основе префикса.

Вызов по умолчанию использует решатель QBF DepQBF в качестве бэкэнда и работает следующим образом (с использованием статической версии без динамической загрузки модуля):

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

сеть

Мастер-узел («решите эту формулу для меня»)

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

Daemon-Node («предоставить вычислительный узел другим мастерам в сети»)

 parac [--known-remote hostname]

Внешние зависимости

Этот инструмент требует следующих внешних зависимостей. Пожалуйста, убедитесь, что их заголовки разработки установлены, чтобы можно было скомпилировать программное обеспечение.

• Повышение заголовков
• Журнал повышения
• Опции программы повышения

Минимальная протестированная версия Boost: 1.65.1.

Все остальные зависимости включены в это дерево исходного кода (и подмодули) и не требуют специальной обработки. Distrac также можно исключить из сборки, либо просто не клонируя подмодуль, либо установив -DENABLE_DISTRAC=OFF для 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