문제와 배정의 관계
불리언 변수에 값을 정해 모든 절이 성립하는지 판단한다. 입력 조건을 만족하는 배정이 있으면 이를 원래 문제의 변수로 다시 해석한다. 실제 요구를 CNF로 바꿀 때 조건을 빠뜨리거나 부정을 잘못 적용하면 원래 문제와 다른 결과를 얻게 된다. 풀이 전에 모델의 의미를 확인한다.
여러 인스턴스와 점진적 사용
재진입 가능한 API에서는 관리 객체를 통해 같은 프로세스 안의 여러 solver 인스턴스를 구분한다. 점진적 SAT 도구를 위한 IPASIR 인터페이스도 지원한다. 서로 다른 버전의 API를 섞지 않고 생성한 객체와 질의의 수명을 맞춘다. 별도의 Python이나 Go 바인딩을 사용할 때도 기반 라이브러리와 호환되는지 살핀다.
증명과 핵심 조건
증명 trace를 압축해 메모리에서 증명과 core를 다룰 수 있으며 TraceCheck 형식을 지원한다. 만족 불가능한 결과를 어떻게 확인할지와 필요한 자료를 얻는 설정을 함께 결정한다. core는 입력 전체와 같은 개념이 아니므로 실제로 어떤 조건을 대상으로 얻었는지 기록한다. 버전과 입력 및 옵션을 보존해 다른 환경에서도 결과를 비교한다.