SMT 해결기를 이용하여 C 언어 프로그램을 검증하는 연구를 수행하는 중에...
이 녀석으로 수도쿠 퍼즐을 풀어보자는 생각이 들었습니다.
가장 많이 알려진 9 x 9 수도쿠 퍼즐을 푼다고 가정하면,
81 개의 정수 변수를 준비해서 수도쿠 규칙과 문제에 주어진 숫자를 SMT 식으로 표현하면 되겠지요.
Yices의 C 언어 API를 이용해서 간단히 프로그램을 하나 작성해 보았습니다.
다른 접근 방법과 자세히 비교해 보지는 못했지만, 그다지 만족할 만한 성능을 보여주지는 못합니다.
관련 자료를 찾아보니 SAT 해결기를 이용한 작업들이 논문으로 공개되어 있네요.
논문의 실험 결과를 보면 SAT 해결기 쪽이 더 빠른 것 같아요.
- T. Weber. A SAT-based Sudoku Solver. LPAR, 2005.
- I. Lynce & J. Ouaknine. Sudoku as a SAT Probem. AIMATH, 2006.
- 권기현. SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩. 정보과학회논문지, 2007.
첨부한 프로그램을 컴파일 하려면 환경에 맞는 Yices 라이브러리가 필요한데,
저는 리눅스 환경에서 Yices 1.0.23 (GMP Statically Linked) 버전을 사용했습니다.
첨부한 예제 파일은 T. Weber의 논문에 있는 수도쿠 문제를 입력 파일로 만든 것입니다.
sudoku-yices.zip$ make
gcc -o sudoku-yices -Iyices-1.0.23/include -Lyices-1.0.23/lib sudoku-yices.c -lyices
$ time ./sudoku-yices < problem-weber-hard.txt
Problem:
0 2 0 0 0 0 0 0 0
0 0 0 6 0 0 0 0 3
0 7 4 0 8 0 0 0 0
0 0 0 0 0 3 0 0 2
0 8 0 0 4 0 0 1 0
6 0 0 5 0 0 0 0 0
0 0 0 0 1 0 7 8 0
5 0 0 0 0 9 0 0 0
0 0 0 0 0 0 0 4 0
Solution:
1 2 6 4 3 7 9 5 8
8 9 5 6 2 1 4 7 3
3 7 4 9 8 5 1 2 6
4 5 7 1 9 3 8 6 2
9 8 3 2 4 6 5 1 7
6 1 2 5 7 8 3 9 4
2 6 9 3 1 4 7 8 5
5 4 8 7 6 9 2 3 1
7 3 1 8 5 2 6 4 9
gcc -o sudoku-yices -Iyices-1.0.23/include -Lyices-1.0.23/lib sudoku-yices.c -lyices
$ time ./sudoku-yices < problem-weber-hard.txt
Problem:
0 2 0 0 0 0 0 0 0
0 0 0 6 0 0 0 0 3
0 7 4 0 8 0 0 0 0
0 0 0 0 0 3 0 0 2
0 8 0 0 4 0 0 1 0
6 0 0 5 0 0 0 0 0
0 0 0 0 1 0 7 8 0
5 0 0 0 0 9 0 0 0
0 0 0 0 0 0 0 4 0
Solution:
1 2 6 4 3 7 9 5 8
8 9 5 6 2 1 4 7 3
3 7 4 9 8 5 1 2 6
4 5 7 1 9 3 8 6 2
9 8 3 2 4 6 5 1 7
6 1 2 5 7 8 3 9 4
2 6 9 3 1 4 7 8 5
5 4 8 7 6 9 2 3 1
7 3 1 8 5 2 6 4 9
real 0m0.582s
user 0m0.573s
sys 0m0.009s
Special thanks to
호아범 님께서 디버깅에 도움을 주셨습니다.
