Основные понятия
SAT 지역 탐색 알고리즘의 순차 실행 시간 분포 분석을 통해 병렬 실행 성능을 예측할 수 있다.
Аннотация
이 논문은 SAT 문제에 대한 지역 탐색 알고리즘의 확장성과 병렬화를 자세히 분석한다. 순차 버전의 실행 시간 행동을 통계적 방법으로 근사하여 병렬 프로세스의 실행 시간 행동을 예측하는 프레임워크를 제안한다.
이 접근법을 Sparrow와 CCASAT이라는 두 가지 SAT 지역 탐색 솔버에 적용하여 병렬 성능을 연구하고, 실제 실험 결과와 비교한다. 모델이 정확하며 경험적 데이터와 유사한 성능을 예측한다는 것을 보여준다. 또한 랜덤 및 수작업 인스턴스를 연구하면서 지역 탐색 솔버가 서로 다른 행동을 보이며, 실행 시간 분포가 지수 분포(이동 및 비이동)와 대수 정규 분포로 근사될 수 있음을 관찰한다.
Статистика
랜덤 인스턴스 rand-4에 대해 CCASAT은 16분 이내에 해결할 확률이 약 1.0이지만, Sparrow는 약 0.75이다.
384개의 코어를 사용할 때 Sparrow가 CCASAT보다 더 효과적이다.
위상 전이 영역의 인스턴스에 대해 Sparrow의 병렬 가속 요인은 최대 7.0이고, CCASAT은 3.4이다.
위상 전이 영역 외부의 인스턴스에 대해 Sparrow의 병렬 가속 요인은 최대 114.2이고, CCASAT은 50.5이다.
Цитаты
"이 논문은 SAT 문제에 대한 지역 탐색 알고리즘의 확장성과 병렬화를 자세히 분석한다."
"순차 버전의 실행 시간 행동을 통계적 방법으로 근사하여 병렬 프로세스의 실행 시간 행동을 예측하는 프레임워크를 제안한다."
"모델이 정확하며 경험적 데이터와 유사한 성능을 예측한다는 것을 보여준다."