youil군이 포스팅으로 소개한 문제인데, 같이 몇마디 나눈 기억이 나서, youil군이 올려준 소스를 쪼끔 수정했습니다. 그랬더니 아주 재밌는 결과가 나왔네요.
우선 수정한 부분입니다.
/* Assertions for the Sudoku rule */
/* 변경전
for (row=0; row<(SIZE); ++row)
for (col=0; col<(SIZE); ++col)
{
yices_expr v = YicesVarExpr[row][col];
yices_expr min = yices_mk_ge(SudokuContext, v, YicesNum[1]);
yices_expr max = yices_mk_le(SudokuContext, v, YicesNum[SIZE]);
yices_assert(SudokuContext, min);
yices_assert(SudokuContext, max);
}
*/
/* 변경후 */
for (row=0; row<(SIZE); ++row)
for (col=0; col<(SIZE); ++col)
{
yices_expr v = YicesVarExpr[row][col];
yices_expr t[SIZE];
for(i=0; i<SIZE; i++)
{
t[i] = yices_mk_eq(SudokuContext, v, YicesNum[i+1]);
}
yices_expr or = yices_mk_or(SudokuContext, t, SIZE);
yices_assert(SudokuContext, or);
}
각 변수의 값이 가질 수 있는 값에 관한 조건입니다. 원본에서는 "변수는 1보다 크거나 작고, SIZE보다 작거나 같다"로 표현하고 있는데, 이것을 "변수는 1 또는 변수는 2 또는 ... 또는 변수는 SIZE" 형태로 변경하였습니다.
딴 이유는 없고 그냥 동물적인 감각으로 크기 비교와 and 연산 보다 or의 나열이 좀 싸보였습니다.
다음은 결과입니다.
1. problem-weber-easy
2. problem-weber-hard
각각에 대해 위가 원본이고 아래가 제가 수정한 결과입니다. 단지 연산 몇개 바꿨을뿐인데... 차이가 좀 나죠... easy는 약 1/3, hard는 약 1/7.5 로 수행시간이 줄었네요. 호호...
(추가내용) 그리고, Youil군으로부터 받은 25X25 문제에 대해선 원본에서 약 11분이 걸렸는데, 바뀐버젼에서 8분 30초 가량이 걸렸습니다.
이걸로 내릴 수 있는 결론은 바로, "Solver를 쓸때는 입력식에 따라 성능이 달라질 수 있다 정도가 되겠네요". 후후~
참고로, SMT solver 사용 등은 원문을 참조하세요.
'IT 이야기 > 프로그래밍' 카테고리의 다른 글
| LD_PRELOAD로 API hooking 하기 (0) | 2011/07/02 |
|---|---|
| Java에서 command line parameter parsing하기 (2) | 2010/07/07 |
| Sudoku as an SMT problem (upgrade?) (6) | 2009/10/06 |
| 나눔고딕 코딩체 적용해 보기 (2) | 2009/02/03 |
| OCaml: Objective Caml (2) | 2008/11/21 |
댓글을 달아 주세요
좋은 optimization 이야.
(1<x and x<SIZE) 보단 (x=1 or x=2 or ...) 가 CNF 의 기본형이네. 풀기도 더 쉬울 것 같고...첫째식이 둘째식과 같으려면 논리적으로 x 는 정수형 타입이어야 하고, SIZE 는 1보단 커야한다 등의 implicit 정보가 더 필요할테니, 기계(theorem prover)로썬 둘째식이 훨씬 풀기 쉬울꺼야.
칭찬 맞지? ㅋㅋ..
그나져나 왜 우리들은 이러고 놀까?
왠지 우울해... -_-;;..
우울할 것까지야.
즐기며 일을 한다는게 얼마나 즐거운 일인가 ㅎㅎㅎ
문제는 일과 놀이를 구분하는 법을 모른다는 거지...
놀이라고 생각하고 덤볐다가... 죽을똥 살똥 몰두해버리니.. ^^
권기현 교수님 수업 자료에 재밌는게 많은거 같아요.
http://kuic.kyonggi.ac.kr/~khkwon/03-teaching/special-topics/se-2007.html
이것들중에 "효율적인 CNF 인코딩" 보면 권교수님 연구실에서 한 것 같은 대표값 방식이나, linear하게 만드는 LTseq 같은게 소개되어 있어요.
웅.. Youil이랑 같이 이런저런 방식으로 돌려봤는데,
기본 방침은 SMT 스타일로 하자는 거지... 권기현 교수님 등이 이무 SAT 방식으로는 수없이 풀어놨더라구.. ㅋㅋ..
지금 Youil이는 마방진에 도전중... ^^