여러 해결기 구성
같은 소스 배포에서 라이브러리와 여러 실행 도구를 빌드할 수 있다. 순차 해결과 병렬 해결, cube-and-conquer 계열은 실행 방식이 다르다. 도구 이름이 비슷하더라도 동일한 탐색 과정이나 옵션을 사용한다고 볼 수 없다.
선택적 구성 요소
AIGER 라이브러리가 연결되면 한정 모델 검사 도구를 추가로 빌드하는 경로가 있다. 증명 지원이나 지역 탐색 기능도 관련 라이브러리의 연결 여부에 영향을 받는다. 본체가 빌드되었다는 사실만으로 선택 기능이 전부 포함된 것은 아니다.
재현 가능한 실행
배포판과 실행 파일, 연결한 라이브러리 및 옵션을 함께 기록한다. SAT 질의가 끝나지 않았다는 사실과 만족 불가능 판정은 구분해야 한다. 다른 해결기와 비교할 때도 문제 표현과 시간 및 메모리 조건을 맞춘다.
관련 문서
Glucose SAT 해결기 / MiniSat / AIGER / CaDiCaL