전달 루틴의 병렬화를 통한 SAT 알고리즘의 GPGPU 가속화 = GPGPU Acceleration of SAT Algorithm with Propagation Routine Parallelization

국문 초록 (Abstract)

대량의 데이터를 병렬적으로 처리할 수 있는 General-Purpose Graphics Processing Unit(GPGPU)가 최근 많은 분야에서 적용되고 있으며, 이는 전자 설계 자동화 분야에서도 예외가 아니다. SAT 알고리즘은 다양한 전자 설계 자동화 문제에 적용되는 대표적인 알고리즘 중 하나이다. GPGPU를 이용해서 SAT 알고리즘을 가속화하기 위해 노력이 이루어져 왔으나, SAT 알고리즘 자체의 특성으로 인해 병렬화에 어려움이 있어왔다. 이 논문에서는 SAT 알고리즘의 내부 과정 중 비교적 병렬화가 용이한 전달 루틴을 병렬화함으로써 GPGPU 가속화를 적용하였다. 전달 루틴이 희소 행렬의 곱셈과 유사한 점에 착안하여 데이터 구조를 구성하고 이에 맞추어서 병렬적인 전달 루틴을 작성하였다. 병렬적으로 동작하는 쓰레드들 사이의 데이터 손실을 방지하기 위해 아토믹(atomic) 연산을 이용하였다. 벤치마크 SAT 문제들에 대해 기존의 GPGPU 기반 SAT solver에 비해 성능이 10배 이상 향상되었음을 확인하였다.

다국어 초록 (Multilingual Abstract)

Because of the enormous processing ability, General-Purpose Graphics Processing Unit(GPGPU) has been applied to many fields including electronics design automation. The SAT algorithm is one of the core algorithm in many electronics design automation tools. There has been some efforts to apply GPGPU to the SAT algorithm, but it is difficult to parallelize the SAT algorithm because of its characteristics. In this paper, I applied GPGPU to the SAT algorithm by parallelizing the propagation routine that is relatively suitable to parallel processing. On the basis of the similarity of the propagation routine to the sparse matrix multiplication, the data structure for the SAT problem is constituted, and the parallel propagation routine is described. To prevent data loss between paralllel threads, atomic operations are exploited. The experimental results for some benchmark SAT problems show that the proposed algorithm is superior to the previous GPGPU-based SAT solver.

참고문헌 (Reference)

1 Y. Deng, "Taming irregular EDA applications on GPUs" 539-546, 2009

2 A. Biere, "Symbolic model checking using SAT procedures instead of BDDs" 317-320, 1999

3 M. Garland, "Sparse matrix computations on manycore GPU's" 2-6, 2008

4 H. H. Hoos, "Satlib: an online resource for research on SAT" 282-292, 2000

5 G. Audemard, "Predicting learnt clauses quality in modern SAT solvers" 399-404, 2009

6 A. Blum, "Noise-tolerant learning, the parity problem, and the statistical query model" 50 (50): 506-519, 2003

7 NVIDIA, "NVIDIA GeForce GTX 980"

8 Y. Hamadi, "ManySAT: a parallel SAT solver" 6 : 245-262, 2008

9 J. P. M.-Silva, "GRASP: A Search Algorithm for Propositional Satisfiability" 48 (48): 506-521, 1999

10 H. Fujii, "GPU acceleration of BCP procedure for SAT algorithms" 2012

11 Y. Deng, "GPU Accelerated VLSI Design Verification" 1213-1218, 2010

12 M. W. Moskewicz, "Chaff: Engineering an Efficient SAT Solver" 530-535, 2001

13 A. D. Palu, "CUD@SAT: SAT solving on GPUs" 27 (27): 293-316, 2015

14 N. Een, "An Extensible SAT-solver" 502-518, 2003

15 Q. Meyer, "3-SAT on CUDA: Towards a massively parallel SAT solver" 306-313, 2010