GipSAT: IC3 알고리즘을 위한 혁신적인 SAT 솔버

중국과학원 연구진이 개발한 GipSAT은 IC3 알고리즘을 위한 경량화된 SAT 솔버로, 변수 결정 최소화, 효율적인 데이터 구조, 임시 절 관리 개선 등의 최적화 전략을 통해 Minisat 대비 평균 3.61배의 속도 향상을 달성했습니다.

GipSAT: IC3 알고리즘의 성능을 한 단계 끌어올리다

최근 몇 년간 모델 검증 분야에서 괄목할 만한 성과를 보인 IC3(또는 PDR) 알고리즘. 그 효율성과 확장성, 그리고 완전성 덕분에 많은 주목을 받고 있습니다. IC3 알고리즘은 상대적 귀납(relative induction)에 관련된 일련의 SAT 쿼리를 해결하기 위해 SAT 솔버를 활용합니다.

중국과학원 소속 수 연구진(Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang) 은 IC3 알고리즘 내 SAT 쿼리의 고유한 특징을 면밀히 분석하여, GipSAT이라는 경량화된 SAT 솔버를 개발했습니다. 기존의 SAT 솔버와는 달리 GipSAT은 다음과 같은 핵심적인 최적화 전략을 도입했습니다.

• 변수 결정 최소화: 모든 변수에 대한 결정이 항상 필요한 것은 아닙니다. GipSAT은 결과에 영향을 미치지 않는 범위 내에서 결정해야 할 변수의 하위 집합을 계산하여 불필요한 연산을 줄입니다. 이는 마치 퍼즐 조각을 맞추듯, 가장 중요한 조각부터 먼저 맞춰나가는 전략과 같습니다.

• 효율적인 데이터 구조: VSIDS 알고리즘에서 사용되는 이진 힙 연산의 오버헤드는 상당합니다. GipSAT은 이를 해결하기 위해 이진 힙 대신 버킷(bucket)을 사용하여 상수 시간 연산을 달성했습니다. 이는 데이터 접근 속도를 획기적으로 높이는 효과를 가져왔습니다.

• 임시 절(clause) 관리 개선: GipSAT은 임시 절을 생성할 때마다 새로운 활성화 변수를 할당할 필요가 없습니다. 이를 통해 솔버 재설정 과정을 간소화하고 추가적인 연산을 줄였습니다.

결과는 놀라웠습니다. Minisat과 비교한 결과, GipSAT은 평균 3.61배의 속도 향상을 보였습니다. 이는 IC3 알고리즘의 성능을 획기적으로 향상시킨 쾌거라 할 수 있습니다. GipSAT의 등장으로 모델 검증 분야는 한층 더 효율적이고 빠르게 발전할 것으로 기대됩니다. 향후 GipSAT의 발전 방향과 다른 알고리즘과의 연동 연구에도 귀추가 주목됩니다.