SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩 = Optimized Encoding of Sudoku Puzzle for SAT Solvers

국문 초록 (Abstract)

SAT을 이용해서 수도쿠 퍼즐을 풀기 위해서는 수도쿠를 SAT 처리기의 표준 입력 언어인 CNF 논리식으로 인코딩 해야 한다. 기존에 제시된 인코딩 알고리즘으로 크기가 큰 수도쿠를 인코딩하면 현재 SAT 처리기의 처리 수준을 넘을 정도로 많은 논리식이 생성된다. 본 논문에서는 크기가 큰 수도쿠를 다루기 위해서 수도쿠의 고정 셀을 이용하여 최적화된 CNF 논리식을 생성하는 방법을 제시한다. 고정 셀에 배정된 숫자는 불변이기 때문에 이를 이용해서 일부 변수의 값을 인코딩 단계에서 미리 결정할 수 있고, 이들 변수의 값을 이용해서 SAT 처리에 영향을 주지 않는 절과 리터럴을 인코딩 단계에서 제거할 수 있다. 다양한 크기의 수도쿠 퍼즐에 적용한 결과 기존 인코딩 알고리즘에 비해서 우수한 성능을 보였다.

다국어 초록 (Multilingual Abstract)

Sudoku can be regarded as a SAT problem. Various encodings are known for encoding Sudoku as a Conjunctive Normal Form (CNF) formula, which is the standard input for most SAT solvers. Using these encodings for large Sudoku, however, generates too many clauses, which impede the performance of state-of-the-art SAT solvers. This paper presents an optimized CNF encodings of Sudoku to deal with large instances of the puzzle. We use fixed cells in Sudoku to remove redundant clauses during the encoding phase. This results in reducing the number of clauses and a significant speedup in the SAT solving time.

목차 (Table of Contents)

• 요약
• Abstract
• 1. 서론
• 2. 배경지식
• 3. 수도쿠 인코딩
• 4. 제안하는 인코딩
• 5. 실험 결과
• 6. 결론
• 참고문헌

참고문헌 (Reference)

1 "http://www.satlib.org/Benchmarks/SAT/satformat.ps"

2 "http://www.menneske.no/sudoku"

3 I. Lynce, "Sudoku as a SAT problem" 2006

4 L. Aaronson, "Sudoku Science: A popular puzzle helps researchers dig into deep math" 2006.02.

5 S. Subbarayan, "NiVER: Non increasing Variable Elimination Resolution for Preprocessing SAT Instances" 2004

6 H. A. Kautz, "Encoding Plans in Propositional Logic" 374-384, 1996

7 N. Een, "Effective Preprocessing in SAT through Variable and Clause Elimination" 2005

8 M.W. Moskewicz, "Chaff: Engineering an Efficient SAT Solver" 2001

9 A. Biere, "Bounded Model Checking" 58 : 2003

10 N. Een, "An Extensible SAT Solver" 2003

11 T. Weber, "A SAT-based Sudoku Solver" 11-15, 2005

12 M. Davis, "A Machine Program for Theorem Proving Communications of the ACM 5" 1962