Paracooba
1.0.0
Esta é uma ferramenta modular para solução distribuída paralela de SAT e QBF. Ele gerencia automaticamente o processo de resolução de fórmulas com cubos fornecidos em uma rede de nós de computação. Ele também possui um algoritmo de cubagem integrado. Os cubos podem ser fornecidos a esta ferramenta no formato "iCNF" (DIMACS normal com cubos anexados no formato a 1 2 3 0 ). Estes cubos podem, por exemplo, ser gerados até março.
Os dois cenários de uso são descritos abaixo. Argumentos adicionais de linha de comando são fornecidos, use --help para obter mais informações. Algumas opções ainda não têm efeitos, pois foram reformuladas. Os binários parac e paracs são funcionalmente idênticos, mas paracs está estaticamente vinculado a todos os módulos, enquanto parac carrega módulos em tempo de execução. Se você tiver problemas para encontrar os módulos necessários, use paracs .
O intervalo de anúncio controla a frequência de transmissões UDP IPv4 na sub-rede local para encontrar outras instâncias do módulo comunicador padrão. Alternativamente, outros controles remotos podem ser especificados diretamente.
Ao fornecer opções adicionais ao módulo solucionador para o nó mestre, ele sincroniza automaticamente as opções fornecidas para todos os outros nós conectados. Ao resolver fórmulas sem cubos predefinidos, a opção --resplit é muito útil, pois aborta automaticamente o CaDiCaL quando a resolução demora muito e aplica um solucionador antecipado para gerar um novo cubo.
Um exemplo de como iniciar um novo nó mestre é mostrado abaixo.
parac <file.[i]cnf> [--cadical-cubes] [--resplit]
Além do módulo de resolução SAT, um solucionador QBF também está integrado na forma do módulo cpp_qbf_prefixexpander . Ele analisa uma fórmula QBF e fornece cubos de resolução QBF com base no prefixo.
A invocação padrão usa o solucionador QBF DepQBF como backend e funciona da seguinte maneira (usando a versão estática sem carregamento dinâmico do módulo):
paraqs <file.qdimacs> [--use-depqbf]
parac <file.[i]cnf> [--udp-announcement-interval 1000]
parac [--known-remote hostname]
Esta ferramenta requer as seguintes dependências externas. Certifique-se de que seus cabeçalhos de desenvolvimento estejam instalados para poder compilar o software.
Versão mínima testada do boost: 1.65.1
Todas as outras dependências estão incluídas nesta árvore de origem (e submódulos) e não precisam ser tratadas especificamente. O Distrac também pode ser excluído da compilação, simplesmente não clonando o submódulo ou configurando -DENABLE_DISTRAC=OFF para 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
