학습한 정보를 관리하기
SAT 탐색에서는 충돌에서 얻은 절을 이후 탐색에 활용한다. Glucose는 어떤 학습 절을 유지하고 어떤 절을 제거할지 평가하는 전략에 중점을 둔다. 학습 정보를 무조건 많이 보관하는 것과 효과적인 탐색은 같은 문제가 아니다.
실행 형태와 기능
순차 버전과 병렬 계열이 있으며 점진적 질의나 불만족 증명 기록은 버전 및 구성에 따라 확인해야 한다. 병렬 실행의 성능이나 재현성도 순차 실행과 같다고 가정하면 안 된다. 비교 실험에서는 같은 모드를 사용한다.
입력과 결과 해석
CNF로 표현한 논리식에서 만족하는 대입이 있는지 검사한다. SAT 결과의 모델과 UNSAT 결과의 증명 기록은 서로 다른 확인 수단이다. 원래 문제를 CNF로 옮기는 과정이 정확한지도 해결기 판정과 별도로 검토한다.