[논문] 동적 파티셔닝·코어 기반 가지치기·온라인 백본 탐지로 병렬 SMT 해결

출처: arXiv - 2606.08852v1

개요

현대 CPU 아키텍처에서 병렬성을 활용하는 것은 SMT 솔버 최적화에서 오랜 과제로 남아 있습니다. 우리는 해결 과정에서 작업자들의 VSIDS 통계를 샘플링하여 탐색 공간의 이진 분할 트리를 동적으로 구축하는 새로운 병렬 프레임워크를 제시합니다. 코어 기반 CDCL 스타일 가지치기의 전체 힘을 활용해 분할 트리를 지속적으로 축소합니다. 또한 작업자 스레드에 온라인 백본 탐지를 통합하고, 가지치기된 하위 문제에 대한 작업을 신속히 제거하기 위한 요구 기반 종료 메커니즘을 도입해 아키텍처를 최적화했습니다. 결과 알고리즘은 높은 일반성을 가지며 사용 가능한 자원에 따라 효과적으로 확장됩니다. 우리는 이 접근법을 Z3 SMT 솔버에 구현했으며, SMT-COMP 2025 Parallel Track의 여섯 논리에서 도전적인 벤치마크에 대해 기존 순차 Z3 및 최신 병렬 프레임워크보다 뛰어난 성능을 보임을 입증했습니다.

주요 기여

이 논문은 다음 분야의 연구를 다룹니다:

• cs.LO
• cs.DC

방법론

자세한 방법론은 전체 논문을 참고하십시오.

실용적 함의

본 연구는 cs.LO 분야의 발전에 기여합니다.

저자

• Ilana Shapiro
• Sorin Lerner
• Nikolaj Bjørner

논문 정보

• arXiv ID: 2606.08852v1
• 분류: cs.LO, cs.DC
• 발표일: 2026년 6월 7일
• PDF: PDF 다운로드