본문 바로가기 주메뉴 바로가기
22대 대한민국 국회 국회정보길라잡이 국회의원검색
회원가입 로그인
HOME

정보검색

소장정보 검색

국회도서관 홈으로 정보검색 소장정보 검색
결과 내 검색 동의어 포함
결과 내 검색 동의어 포함

-

목차보기

표제지

요약

목차

1. 서론 6

2. 관련 연구 7

3. SAT Hard Instance를 풀기 위한 방법론 제안 11

4. Incremental Interpolation 알고리즘 12

4.1. Interpolation 13

4.2. Proof of Unsatisfiability 14

4.3. Interpolant 구하기 15

4.4. Incremental Interpolation 알고리즘 16

4.5. 예제 19

5. Model Accumulation 알고리즘 24

5.1. Model Accumulation 25

5.2. Model Accumulation 알고리즘 30

5.3. 예제 33

6. 결론 및 향후 과제 34

7. 참고 문헌 35

초록보기

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에 좋은 결과를 보일 것으로 예상된다.

추천서가 (다양한 추천 자료를 만나보세요)

권호기사보기

권호기사 목록 테이블로 기사명, 저자명, 페이지, 원문, 기사목차 순으로 되어있습니다.
기사명 저자명 페이지 원문 기사목차