제약을 불리언 문제로
논리식에 포함한 변수들을 참이나 거짓으로 정해 모든 조건을 만족할 수 있는지 확인한다. 프로그램이나 하드웨어의 동작을 검증하려면 앞단 도구가 원래 요구를 이 형식으로 바꾸어야 한다. 제약이 누락되면 가능한 해가 실제 문제의 해와 달라질 수 있으므로 변환과 풀이를 구분해 검토한다.
구현과 전처리의 영향
CaDiCaL을 C로 옮기는 과정에서 자료 구조와 탐색 중 처리 일정 및 알고리즘을 조정했다. 특정 solver의 성능은 문제의 구조와 실행 환경에 따라 달라질 수 있다. 다른 도구의 이름이나 과거 경연 결과만으로 모든 입력에서 빠르다고 단정하지 않고 실제 대상 문제에서 비교한다.
API와 실행 관리
C API는 solver 생성과 절 추가 및 풀이와 모델 값 조회를 제공한다. 종료 요청이나 탐색 자원 제한도 연결할 수 있다. 풀이가 제한 때문에 끝났는지 실제 판정에 도달했는지를 구분한다. SAT API끼리도 지원 기능이 모두 같지는 않으므로 점진적 사용이나 가정이 필요한 도구에 연결할 때 정확한 인터페이스를 확인한다.