Paracooba
1.0.0
이는 분산 병렬 SAT 및 QBF 해결을 위한 모듈식 도구입니다. 컴퓨팅 노드 네트워크를 통해 제공된 큐브를 사용하여 공식 해결 프로세스를 자동으로 관리합니다. 또한 통합된 큐빙 알고리즘도 있습니다. 큐브는 "iCNF" 형식( a 1 2 3 0 형식의 큐브가 추가된 일반 DIMACS)으로 이 도구에 제공될 수 있습니다. 예를 들어 이러한 큐브는 3월까지 생성될 수 있습니다.
두 가지 사용 시나리오는 아래에 설명되어 있습니다. 추가 명령줄 인수가 제공됩니다. 자세한 내용을 보려면 --help 사용하세요. 일부 옵션은 재작업되었기 때문에 아직 효과가 없습니다. 바이너리 parac 과 paracs 기능적으로 동일하지만 paracs 모든 모듈에 정적으로 연결되는 반면 parac 런타임에 모듈을 로드합니다. 필요한 모듈을 찾는 데 문제가 있으면 paracs 사용하세요.
알림 간격은 기본 커뮤니케이터 모듈의 다른 인스턴스를 찾기 위해 로컬 서브넷으로 IPv4 UDP 브로드캐스트의 빈도를 제어합니다. 또는 다른 리모컨을 직접 지정할 수도 있습니다.
솔버 모듈에 추가 옵션을 마스터 노드에 제공하면 제공된 옵션을 연결된 다른 모든 노드에 자동으로 동기화합니다. 사전 정의된 큐브 없이 수식을 해석할 때 --resplit 옵션은 해석이 너무 오래 걸리면 자동으로 CaDiCaL을 중단하고 예측 솔버를 적용하여 새 큐브를 생성하므로 매우 유용합니다.
새 마스터 노드를 시작하는 방법의 한 가지 예가 아래에 나와 있습니다.
parac <file.[i]cnf> [--cadical-cubes] [--resplit]
SAT 해석 모듈 외에도 QBF 해석기도 cpp_qbf_prefixexpander 모듈 형태로 통합됩니다. QBF 공식을 구문 분석하고 접두사를 기반으로 QBF 솔버 큐브를 제공합니다.
기본 호출은 QBF 솔버 DepQBF를 백엔드로 사용하고 다음과 같이 작동합니다(동적 모듈 로딩 없이 정적 버전 사용).
paraqs <file.qdimacs> [--use-depqbf]
parac <file.[i]cnf> [--udp-announcement-interval 1000]
parac [--known-remote hostname]
이 도구에는 다음과 같은 외부 종속성이 필요합니다. 소프트웨어를 컴파일하려면 개발 헤더가 설치되어 있는지 확인하십시오.
최소 테스트된 부스트 버전: 1.65.1
다른 모든 종속성은 이 소스 트리(및 하위 모듈)에 포함되어 있으므로 특별히 처리할 필요가 없습니다. 단순히 하위 모듈을 복제하지 않거나 CMake에 -DENABLE_DISTRAC=OFF 설정하여 Distrac을 빌드에서 제외할 수도 있습니다.
# 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
