낭만 컴돌이 ::

Two Ways of Constructing a Software Design

분류없음 2009/11/17 14:15

There are two ways of constructing a software design:

One way is to make it so simple that there are obviously no deficiencies, and

the other way is to make it so complicated that there are no obvious deficiencies.

The first method is far more difficult.

It demands the same skill, devotion, insight, and even inspiration as the discovery of the simple physical laws which underlie the complex phenomena of nature.

-- C. A. R. Hoare, 1990

Posted by 김유일

트랙백 0개, 댓글 1개가 달렸습니다.

Sudoku with STP

분류없음 2009/10/09 10:42

STP라는 것도 사용해 봅시다.
역시 비트 벡터와 배열 타입의 변수만 지원합니다.

사실 처음에는 그냥 지나치려고 했습니다.
SMT-COMP'09의 비트 벡터 부문(QF_BV)에서 MathSAT과 Boolector가 더 좋은 점수를 받았거든요.

그런데 STP 홈페이지를 보니 STP를 사용하여 진행되고 있는 많은 프로젝트들이 있더군요.
많은 사람들이 사용하는 데에는 뭔가 이유가 있지 않을까요?
MIT 라이선스로 배포되기 때문에 회사에서 사용하는 데에도 별 문제가 없을 것 같구요.

그래서 STP 버전도 만들어 보았습니다. 시험에 사용한 버전은 stp-ver-0.1-11-18-2008 입니다.
역시 C API를 설명하는 문서는 찾을 수 없었지만,
배포폰에 포함된 c_interface.h 헤더 파일을 보면서 (절반은 추측으로) 작성했습니다.

sudoku-stp.zip

STP는 소스 코드 형태로 배포되고 있으니 라이브러리를 사용하기 전에 우선 빌드를 해야 합니다.
빌드를 하면 lib 디렉토리 아래에 libstp.a가 생성됩니다.

$ g++ -o sudoku-stp -Wall -Istp-ver-0.1-11-18-2008/c_interface -Lstp-ver-0.1-11-18-2008/lib sudoku-stp.c -lstp
$ time ./sudoku-stp < ../problems/problem-25x25-hard-448.txt
Problem:
16 0 0 0 0 5 13 17 1 0 0 0 0 0 6 0 3 0 0 21 12 0 20 7 0
0 0 0 0 0 0 0 0 0 0 0 0 7 12 9 0 0 2 0 17 0 4 0 13 0
6 0 11 5 0 0 0 0 0 0 0 2 0 20 23 0 4 0 12 0 0 0 24 0 10
21 4 20 0 12 0 7 0 11 2 16 22 0 0 0 24 0 13 10 25 0 18 0 8 0
24 13 0 7 0 0 16 0 12 4 0 8 5 0 3 0 0 0 0 0 0 22 0 0 14
0 0 18 21 5 17 23 11 0 12 0 1 16 0 0 10 0 0 15 20 0 0 8 6 4
4 0 8 3 20 9 2 0 10 0 7 0 21 14 0 0 12 0 1 0 5 19 22 0 0
19 0 0 11 0 7 21 0 0 0 20 12 3 2 17 0 5 4 9 14 10 25 0 0 0
0 10 17 0 0 1 0 19 4 0 0 0 0 0 15 0 0 0 0 13 7 0 0 0 0
2 0 0 0 9 0 24 0 6 5 0 0 23 25 0 21 19 0 0 8 0 0 0 1 20
0 8 0 18 15 0 17 5 20 0 0 0 0 0 0 0 0 0 0 0 6 7 13 0 0
0 0 0 9 0 0 0 6 3 0 0 17 0 0 13 4 0 23 0 16 14 0 15 0 1
0 16 0 0 6 0 10 0 0 0 0 3 0 8 0 0 0 0 21 0 4 0 0 18 0
12 0 10 0 4 25 0 18 0 7 15 0 0 21 0 0 13 5 0 0 0 11 0 0 0
0 0 14 22 1 0 0 0 0 0 0 0 0 0 0 0 17 8 7 0 25 5 0 24 0
9 21 0 0 0 22 0 0 19 18 0 15 8 0 0 3 6 0 5 0 13 0 0 0 23
0 0 0 0 19 6 0 0 0 0 4 0 0 0 0 0 11 20 0 1 0 0 18 17 0
0 0 0 15 23 13 3 10 25 0 11 6 20 19 16 0 0 0 2 7 0 24 0 0 12
0 0 24 10 22 0 20 0 16 0 0 25 14 0 2 0 8 0 13 19 3 1 11 0 6
1 3 12 0 0 14 5 0 0 23 0 0 24 7 0 17 0 9 25 4 20 10 2 0 0
20 0 0 19 0 0 0 0 0 0 17 0 2 10 0 15 14 0 22 0 0 3 0 11 25
0 11 0 8 0 19 22 14 0 24 0 0 0 13 12 9 25 0 18 0 16 0 7 21 2
5 0 9 0 0 0 1 0 23 0 22 11 0 16 0 0 0 0 0 0 0 20 12 0 19
0 22 0 4 0 2 0 25 0 0 6 9 18 0 0 0 0 0 0 0 0 0 0 0 0
0 12 13 0 10 16 0 0 9 0 14 0 0 0 0 0 1 21 11 2 0 0 0 0 18
Solution:
16 9 22 23 18 5 13 17 1 25 24 10 11 4 6 14 3 19 8 21 12 2 20 7 15
10 25 15 14 8 20 18 24 22 6 1 19 7 12 9 5 23 2 16 17 11 4 3 13 21
6 17 11 5 3 15 14 8 21 19 25 2 13 20 23 7 4 22 12 18 1 16 24 9 10
21 4 20 1 12 23 7 3 11 2 16 22 17 15 14 24 9 13 10 25 19 18 6 8 5
24 13 19 7 2 10 16 9 12 4 21 8 5 18 3 20 15 1 6 11 17 22 25 23 14
25 24 18 21 5 17 23 11 14 12 19 1 16 9 22 10 7 3 15 20 2 13 8 6 4
4 23 8 3 20 9 2 13 10 15 7 24 21 14 11 25 12 18 1 6 5 19 22 16 17
19 1 6 11 13 7 21 16 18 8 20 12 3 2 17 22 5 4 9 14 10 25 23 15 24
22 10 17 12 14 1 25 19 4 20 8 18 6 5 15 23 2 16 24 13 7 9 21 3 11
2 15 7 16 9 3 24 22 6 5 10 13 23 25 4 21 19 11 17 8 18 12 14 1 20
3 8 21 18 15 11 17 5 20 16 23 4 19 22 25 1 10 12 14 24 6 7 13 2 9
7 20 5 9 25 24 8 6 3 22 2 17 10 11 13 4 18 23 19 16 14 21 15 12 1
11 16 23 24 6 12 10 1 13 14 5 3 9 8 7 2 20 25 21 15 4 17 19 18 22
12 19 10 17 4 25 9 18 2 7 15 14 1 21 24 6 13 5 3 22 23 11 16 20 8
13 2 14 22 1 4 19 23 15 21 18 16 12 6 20 11 17 8 7 9 25 5 10 24 3
9 21 2 20 16 22 11 7 19 18 12 15 8 17 1 3 6 24 5 10 13 14 4 25 23
8 14 25 13 19 6 12 2 24 9 4 5 22 3 10 16 11 20 23 1 21 15 18 17 7
17 5 4 15 23 13 3 10 25 1 11 6 20 19 16 18 21 14 2 7 8 24 9 22 12
18 7 24 10 22 21 20 4 16 17 9 25 14 23 2 12 8 15 13 19 3 1 11 5 6
1 3 12 6 11 14 5 15 8 23 13 21 24 7 18 17 22 9 25 4 20 10 2 19 16
20 18 16 19 24 8 4 12 7 13 17 23 2 10 21 15 14 6 22 5 9 3 1 11 25
15 11 1 8 17 19 22 14 5 24 3 20 4 13 12 9 25 10 18 23 16 6 7 21 2
5 6 9 2 7 18 1 21 23 10 22 11 25 16 8 13 24 17 4 3 15 20 12 14 19
14 22 3 4 21 2 15 25 17 11 6 9 18 1 19 8 16 7 20 12 24 23 5 10 13
23 12 13 25 10 16 6 20 9 3 14 7 15 24 5 19 1 21 11 2 22 8 17 4 18

real 1m37.119s
user 1m37.023s
sys 0m0.080s
$

이건...! 결과가 기대 이상입니다. 25 x 25 수도쿠를 1 분대에 풀어 주는군요. -o-

일단 SMT 인코딩을 평이하게 했음에도 불구하고,
호아범 님께서 열심히 최적화하신 Yices 버전과 비교할 만한 성능을 보여주었습니다.
역시 많은 사람들이 사용하는 데에는 이유가 있었던 것입니다.
당분간 이 예쁜 녀석을 조금 더 살펴보려 합니다.

Posted by 김유일

TAG SMT solver, STP, sudoku, 수도쿠, 스도쿠

트랙백 0개, 댓글 0개가 달렸습니다.

Sudoku with Boolector

분류없음 2009/10/08 17:59

이번에는 Boolector입니다.
Boolector에는 정수 타입 변수가 없네요. 비트 벡터와 배열을 다루는 기능만 있더군요.
그래서 정수를 비트 벡터로 인코딩하는 방법을 사용했습니다.
예를 들어 9 이하의 정수는 4 비트로 이루어진 비트 벡터에 저장할 수 있겠지요.

sudoku-boolector.zip

역시 C API의 기본적인 틀은 다른 SMT 해결기들과 비슷합니다.
홈페이지에 관련 문서는 없지만 배포본에 들어있는 헤더 파일을 살펴보면 그럭저럭 이해할 수 있습니다.
나중에 모델을 얻기 위해서는 다음과 같이 모델 생성이 가능하도록 설정해 주어야 합니다.

SudokuContext = boolector_new();
boolector_enable_model_gen(SudokuContext);

실험에 사용한 버전은 boolector-1.1-IA-32입니다.
실험에 사용한 서버가 64 비트 머신이어서 다음과 같은 오류를 만났습니다.

$ gcc -o sudoku-boolector -Iboolector-1.1-IA-32/include -Lboolector-1.1-IA-32/lib sud
oku-boolector.c -lboolector
/usr/bin/ld: skipping incompatible boolector-1.1-IA-32/lib/libboolector.a when search
ing for -lboolector
/usr/bin/ld: cannot find -lboolector
collect2: ld returned 1 exit status
$

현재 64 비트 버전을 배포하지 않는군요.
일단 컴파일러에 옵션에 -m32 옵션을 추가하여 컴파일하면 실행해 볼 수는 있습니다.

자, 그럼 16 x 16 수도쿠 문제를 풀어볼까요?
참고로 첨부한 파일은 9 x 9 수도쿠 문제를 풀도록 설정되어 있습니다.
다른 크기의 퍼즐을 푸시려면 매크로의 숫자를 조정하시고 컴파일하셔야 합니다.
처음부터 퍼즐 크기를 입력할 수 있도록 작성하면 좋았겠지만 프로그램이 복잡해지고... (네네, 게을러서...)

$ make
gcc -o sudoku-boolector -m32 -Iboolector-1.1-IA-32/include -Lboolector-1.1-IA-32/lib sudoku-boolector.c -lboolector
$ time ./sudoku-boolector < ../problems/problem-16x16-hard-2068.txt
Problem:
12 3 5 4 10 0 1 15 0 6 11 0 0 0 7 0
0 15 0 0 0 3 7 12 0 0 1 0 0 0 0 0
7 0 8 0 11 9 0 0 0 10 0 0 0 0 0 0
11 0 0 10 0 2 0 0 0 0 0 14 6 0 3 0
0 8 0 2 0 0 0 7 0 11 0 0 10 0 13 0
5 1 9 0 0 13 0 0 0 0 0 12 0 7 0 11
0 0 3 0 4 10 12 0 0 0 2 0 16 0 5 0
0 6 0 0 0 5 0 1 0 0 0 0 3 0 0 0
0 0 0 16 0 0 0 0 15 0 3 0 0 0 1 0
0 11 0 5 0 15 0 0 0 12 16 7 0 14 0 0
15 0 2 0 1 0 0 0 0 0 5 0 0 11 16 3
0 9 0 1 0 0 10 0 11 0 0 0 15 0 4 0
0 10 0 6 7 0 0 0 0 0 14 0 8 0 0 5
0 0 0 0 0 0 16 0 0 0 10 9 0 6 0 1
0 0 0 0 0 14 0 0 4 1 7 0 0 0 15 0
0 13 0 0 0 6 8 0 12 5 0 2 4 10 9 14
Solution:
12 3 5 4 10 8 1 15 2 6 11 16 14 9 7 13
2 15 6 9 14 3 7 12 13 4 1 5 11 16 8 10
7 14 8 13 11 9 6 16 3 10 12 15 1 5 2 4
11 16 1 10 13 2 5 4 9 7 8 14 6 12 3 15
4 8 15 2 6 16 14 7 5 11 9 3 10 1 13 12
5 1 9 14 15 13 3 8 10 16 4 12 2 7 6 11
13 7 3 11 4 10 12 9 6 14 2 1 16 15 5 8
16 6 10 12 2 5 11 1 7 15 13 8 3 4 14 9
10 12 7 16 9 11 2 14 15 8 3 4 5 13 1 6
6 11 13 5 8 15 4 3 1 12 16 7 9 14 10 2
15 4 2 8 1 7 13 6 14 9 5 10 12 11 16 3
3 9 14 1 16 12 10 5 11 2 6 13 15 8 4 7
9 10 4 6 7 1 15 2 16 13 14 11 8 3 12 5
14 2 12 15 5 4 16 13 8 3 10 9 7 6 11 1
8 5 11 3 12 14 9 10 4 1 7 6 13 2 15 16
1 13 16 7 3 6 8 11 12 5 15 2 4 10 9 14

real 0m3.418s
user 0m3.411s
sys 0m0.007s

$

3 초! 이 녀석은 그래도 싹수가 보입니다. 조금 더 살펴볼 가치가 있겠네요.

하지만 25 x 25 수도쿠는 100 분 걸리더군요. 지난 Yices 버전은 11 분 걸렸는데... ㅠ_ㅠ
인코딩 방법이 달라서 그런 걸까요?

Posted by 김유일

TAG Boolector, SMT solver, sudoku, 수도쿠, 스도쿠

트랙백 0개, 댓글 0개가 달렸습니다.