수도쿠 퍼즐을 통해서 살펴본 SAT에서 전처리 효과

• 영문명: Effect on Preprocessing in SAT with Sudoku Puzzle
• 발행기관: 한국IT서비스학회
• 저자명: 권기현(Gihwon Kwon)
• 간행물 정보: 『한국IT서비스학회지』한국IT서비스학회지 제7권 제2호, 127~135쪽, 전체 9쪽
• 주제분류: 경제경영 > 경영학
• 파일형태: PDF
• 발행일자: 2008.06.30

영문 초록

  The concept of preprocessing is widely used in various computer science area such as compiler and software engineering for the purpose of macro processing and optimization. In addition, preprocessing is also used in SAT solvers in order to eliminate redundant literals and clauses to speed up its solving time before searching the state space. However, there is an unexpected run-time error such as stack-overflow during this step, in case the size of a given set of clauses is huge which impedes SAT solvers. In this case, the preprocessing should be applied at the encoding time to optimize its size. In this paper this idea is applied to several Sudoku problems. As a result, significant improvements are obtained with respect to the number of variables and clauses as well as the solving time compared to the previous works.

목차

Abstract
1. 서론
2. 배경 지식
3. 수도쿠 퍼즐 사례
4. 실험
5. 결론
참고문헌
저자소개

키워드

Satisfiability Clause Preprocessing Sudoku