생몰정보
소속
직위
직업
활동분야
주기
서지
국회도서관 서비스 이용에 대한 안내를 해드립니다.
검색결과 (전체 1건)
원문 있는 자료 (1) 열기
원문 아이콘이 없는 경우 국회도서관 방문 시 책자로 이용 가능
목차보기더보기
표제지
요약
목차
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에 좋은 결과를 보일 것으로 예상된다.
원문구축 및 2018년 이후 자료는 524호에서 직접 열람하십시요.
도서위치안내: / 서가번호:
우편복사 목록담기를 완료하였습니다.
* 표시는 필수사항 입니다.
* 주의: 국회도서관 이용자 모두에게 공유서재로 서비스 됩니다.
저장 되었습니다.
로그인을 하시려면 아이디와 비밀번호를 입력해주세요. 모바일 간편 열람증으로 입실한 경우 회원가입을 해야합니다.
공용 PC이므로 한번 더 로그인 해 주시기 바랍니다.
아이디 또는 비밀번호를 확인해주세요
