본 논문은 효율성과 확장성, 완전성으로 인해 최근 몇 년 동안 큰 영향을 미친 SAT 기반 모델 검증 알고리즘인 IC3(또는 PDR) 알고리즘에 대한 최적화 기법들을 제시한다. IC3 알고리즘이 상대적 귀납과 관련된 일련의 SAT 질의를 풀기 위해 SAT 솔버를 사용하는 점에 착안하여, SAT 질의의 고유한 특성에 대한 관찰을 바탕으로 SAT 솔버에 대한 몇 가지 최적화 기법을 제안한다. 구체적으로, 모든 변수에 대한 결정이 항상 필요하지 않다는 점을 이용하여 각 풀이 과정 전에 결정해야 할 변수의 부분 집합을 계산하고, VSIDS에서 이진 힙 연산의 오버헤드가 무시할 수 없다는 점을 고려하여 이진 힙을 버킷으로 대체하여 상수 시간 연산을 달성하며, 각 풀이 과정마다 새로운 활성화 변수를 할당할 필요 없이 임시 절을 지원하여 솔버 재설정을 없앤다. 이러한 최적화 기법들을 통합한 새로운 경량화된 CDCL SAT 솔버인 GipSAT을 개발하고, GipSAT 기반 IC3가 MiniSat 기반 IC3에 비해 평균 3.61배의 속도 향상을 보이는 것을 종합적인 평가를 통해 보여준다.
