SAT Hard Instance를 해결하기 위한 방법론 연구

국문 초록 (Abstract)

SAT 문제는 propositional formula를 참으로 만드는 truth assignment의 존재 여부를 알아보는 것으로. 이는 하드웨어/소프트웨어 검증, 보딜 체킹 등 다양한 분야에 응용되고 있다. SAT 문제는 시간 복잡도가 NP complete이기 때문에 풀기 어려우나, 많은 알고리즘. 도구. 휴리스틱이 개발되어 성능이 많이 개선되었다. 그러나 성능의 개선으로 적용할 수 있는 대상이 많아지고 있음에도 불구하고 여전히 풀리지 않는 문제 instance들이 존재한다. 이러한 것을 hard instance라 한다. 이 논문에서는 SAT 문제를 푸는 두 가지 방법론을 제시하는데, 이들이 hard instance를 해결하는데 사용될 수 있을 것이라 예상된다.
첫 번째는 interpolation 정리를 이용한 incremental interpolation 알고리즘이다. 이는 입력formula의 일부variable에 값을 할당하여 검색 공간을 줄여서 satisfiable/unsatisfiable 여부를 알아 본 다음, 차츰 검색공간을 늘려가는 방법이다. 값을 할당한 variable의 수를 하나씩 줄여가면서 반복하는데, 이때 intcrpolation을 이용하여 정보를 추가한다. 그러면 값을 할당한 variable이 줄어들면서 검색 공간이 늘어나는 대신, interpolation을 이용하여 추가한 정보로 검색공간이 줄어들게 된다.
두 번째 방법은 formula의 모든 모델을 구하는 model accumulation을 이용하는 것이다. 이는 입력 formula를 두 부분으로 나누어서 우선 한쪽의 모든 모델을 구한 다음, 이 모델들을 다른 부분에 적용해보는 방식이다.
Incremental interpolation 알고리즘과 model accumulation 알고리즘은 모두기존의 SAT 알고리즘을 사용하는 새로운 알고리즘이다. 따라서 모든 SAT instance에 적용할 수 있는데, 주어진 formula를 분리하여 단계적으로 접근하므로 특히 잘 풀리지 않는 hard instance에 좋은 결과를 보일 것으로 예상된다.

목차 (Table of Contents)

• 목차
• 요약
• 1. 서론 = 1
• 2. 관련 연구 = 2
• 3. SAT Hard Instance를 풀기 위한 방법론 제안 = 6
• 4. Incremental Interpolation 알고리즘 = 7
• 4.1. Interpolation = 8
• 4.2. Proof of Unsatisfiability = 9
• 4.3. Interpolant 구하기 = 10
• 4.4. Incremental Interpolation 알고리즘 = 11
• 4.5. 예제 = 14
• 5. Model Accumulation 알고리즘 = 19
• 5.1. Model Accumulation = 20
• 5.2. Model Accumulation 알고리즘 = 25
• 5.3. 예제 = 28
• 6. 결론 및 향후 과제 = 29
• 7. 참고 문헌 = 30