핵심 개념
SAT 지역 탐색 알고리즘의 순차 실행 시간 분포 분석을 통해 병렬 실행 성능을 예측할 수 있다.
초록
이 논문은 SAT(Satisfiability) 문제에 대한 지역 탐색 알고리즘의 확장성과 병렬화를 자세히 분석한다. 순차 버전의 실행 시간 행동을 통계적 방법으로 근사하여 병렬 프로세스의 실행 시간 행동을 예측하는 프레임워크를 제안한다. 이 접근법을 Sparrow와 CCASAT이라는 두 가지 SAT 지역 탐색 솔버에 적용하고, 최대 384개의 코어를 사용한 실제 실험 결과와 비교한다. 모델이 정확하며 경험적 데이터와 유사한 성능을 예측한다는 것을 보여준다. 또한 랜덤 및 수작업 인스턴스를 연구하면서 지역 탐색 솔버가 서로 다른 행동을 보이며 실행 시간 분포가 지수(shifted 및 non-shifted) 및 대수 정규 분포로 근사될 수 있음을 관찰한다.
통계
랜덤 인스턴스 rand-4에 대해 CCASAT은 16분 이내에 해결할 확률이 약 1.0이지만, Sparrow는 약 0.75이다.
랜덤 인스턴스 rand-7에 대해 Sparrow는 384개 코어를 사용할 때 약 67.8배의 가속 효과를 보이지만, CCASAT은 약 22.7배의 가속 효과를 보인다.
수작업 인스턴스 Crafted-1에 대해 Sparrow는 384개 코어를 사용할 때 약 349.8배의 가속 효과를 보인다.
인용구
"Indeed, by approximating the runtime distribution of the sequential process with statistical methods, the runtime behavior of the parallel process can be predicted by a model based on order statistics."
"We show that the model is accurate and predicts performance close to the empirical data."
"Moreover, as we study different types of instances (random and crafted), we observe that the local search solvers exhibit different behaviors and that their runtime distributions can be approximated by two types of distributions: exponential (shifted and non-shifted) and lognormal."