N Queens 문제를 SMT solver 로 풀기

imyejin의 이미지

지는 번 SAT solver 에 이은 http://kldp.org/node/106607 두 번째 연재입니다. 지난 번에 Automated Theorem Proving(ATP)에 대해 다루겠다고 했는데요, 일단 이걸 다루기 전에 SMT solver 라는 것을 살펴보고 넘어가기로 하겠습니다.

SMT란 Satisfiability Modulo Theories의 약자로 자세한 내용은 위키피디아 http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories 항목을 참조하시기 바랍니다. SMT solver 를 SAT solver 와 비교해 아주 대강 설명하자면 SAT solver 는 참과 거짓값만을 갖는 명제 변수(predicate variable)만을 다룰 수 있는 데 반해 SMT solver 는 구현체가 제공하는 이론이 허락하는 영역으 다양한 타입의 변수를 다룰 수 있습니다. 위키피디아 항목에서 살펴보면 알 수 있겠지만 SMT solver 들은 대개 자연수, 정수, 실수 등을 기본적으로 사용할 수 있는 이론이 제공되며 비트 벡터, 리스트, 배열 등 다양한 데이타 구조를 다룰 수 있는 이론을 탑재한 SMT solver 들도 있습니다. 즉 SAT solver 가 가진 기능에다 방정식 및 부등식 등을 풀 수 있는 기능을 더했다고 할 수 있습니다. 주목할 점은 SAT 문제가 다루는 영역은 유한하지만 (명제변수가 n개일 때 모든 가능한 경우는 2^n으로 유한) SMT solver 가 다룰 수 있는 값들 중에는 자연수 정수 실수 등 무한한 영역의 것들이 있다는 점입니다. SMT solver 는 그런 무한한 영역에 대한 decidable theory, 즉 참인지 거짓인지를 유한 시간 안에 검사하여 결정할 수 있는 문제만을 다루는 것을 목표로 하기 때문에 정수나 실수 등을 다룬다고 해도 모든 종류의 방정식이나 부등식 등을 다 풀지는 않습니다. 현재 널리 쓰이고 있는 SMT solver 들은 linear arithmetic에 대한 decision procedure (decidable theory를 구현한 알고리듬) 만을 탑재하고 있습니다. 더 자세한 내용은 위키피디아 항목 http://en.wikipedia.org/wiki/Decision_problem 를 참조하시기 바랍니다. 간단히 말해서 보통 SMT solver 들은 일차 방정식이나 부등식만 풀 수 있고 이차 이상의 방정식은 지원하지 않으며, non-linear arithmetic에 대한 결정가능한 이론(decidable theory)들은 아직도 진행중인 연구 분야입니다.

이런 SMT solver 를 만드는 사람들은 매년 벤치마크 경쟁에 이기기 위해 시스템을 튜닝하느라 한가하게 매뉴얼이나 작성할 시간이 없다는 소문이 있는데, 그래서 대부분의 SMT solver는 문서화가 전혀 되어 있지 않다고 봐도 과장이 아닙니다 -_-;;; (혹시 Z3 라던가 다른 유명한 SMT solver에 대한 tutorial을 갖고 계신 분 있으면 여기다 좀 링크를 포스팅해 주시면 대단히 감사하겠습니다 ㅠ.ㅠ) 오픈소스 SMT solver 를 쓰고 싶었지만 현재 개발이 활발하게 진행되는 SMT solver 중에 오픈소스로 제공되는 것은 인텔에서 사용하는 DPT 라는 녀석이 OCaml 로 작성되어 있습니다만, 역시 문서화가 거의 되어 있지 않은데다 최신 버전은 내부적으로만 사용하고 아직 릴리즈를 하지 않았기 때문에 더 오래 전부터 개발되어 온 SMT solver 들에 아직은 범용적인 완성도가 떨어지는 것 같았습니다. 이 강좌에서는 SMT solver 중에서 유일하게 읽을만한 매뉴얼과 예제를 포함한 강좌까지 홈페이지에 올라와 있는 Yices 를 쓰도록 하겠습니다. Yices 홈페이지는 http://yices.csl.sri.com/ 입니다. 아쉽게도 소스를 제공하지는 않고 리눅스용 바이너리는 제공합니다. 홈페이지에서 tar.gz 파일을 받아서 아무 디렉토리에다 풀고 bin 디렉토리에 들어 있는 yices 를 실행하면 됩니다.

SMT 문제도 DIMACS SAT 형식과 같이 SMT-LIB 형식을 여러 SMT solver 의 표준적인 입력으로 사용하자고 제안하고 있으며 http://smtlib.org/ 이 형식으로 벤치마크 경쟁을 하기도 합니다만, SMT-LIB 역시 문서화가 별로 잘 안 되어 있기 때문에 (문법 BNF를 따라 설명만 해 놓고 막상 구할 수 있는 예제는 주로 벤치마크들 말고는 잘 없음) 저같이 처음 이런 툴을 써보려는 사람에게는 그다지 추천할 만하지 않습니다. 그래서 이 글에서는 그냥 SMT-LIB 형식이라는 게 있다는 것만 알아 두고 그냥 Yices에서 쓰는 자체적인 형식을 쓰겠습니다. 대개 SMT solver 에서 제공하는 자체적인 형식이 더 간결하고, 또 각 SMT solver 의 기능을 최대한 활용할 수 있습니다. 예를 들면 Yices의 경우는 자체적인 명령어 형식을 대화식 환경으로 구동하여 이용할 수 있다는 것이 특징입니다.

아래와 같이 yices에 -i 옵션을 주어 실행하면 대화식 환경으로 구동할 수 있습니다.

imyejin@vaio:~/yices-1.0.21$ ./bin/yices -i
Yices (version 1.0.21). Copyright 2005, 2006 SRI International.
GMP (version 4.3.1). Copyright Free Software Foundation, Inc.
Build date: Tue May  5 18:50:58 PDT 2009
Type `(exit)' with parentheses to exit.
Type `(help)' with parentheses for help.
yices > (help)
(assert [expr])           -- assert the formula [expr] into the current logical context.
(assert+ [expr])          -- similar to assert, but allows retraction and unsat core extraction.
(assert+ [expr] [weight]) -- similar to assert+, but the weight is used for max-sat.
(retract [idx])           -- retract the assertion with index idx from the logical context.
(check)                   -- check whether the logical context is satisfiable or not.
(max-sat)                 -- extract the maximal satisfying model.
(set-evidence! true)      -- enable the construction of evidence: models and unsatisfiable cores.
(set-evidence! false)     -- disable the construction of evidence: models and unsatisfiable cores.
(set-verbosity! [num])    -- set the verbosity level.
(set-arith-only! true)    -- tell yices that only boolean combinations of arithmetic constraints are going to be asserted.
(push)                    -- save the current logical context on the stack.
(pop)                     -- restore the context from the top of the stack, and pop it off the stack.
(echo [string])           -- print the string [string].
(reset)                   -- reset the logical context.
(include [file])          -- include the file [file].
(status)                  -- display the status of the logical context.
(exit)                    -- exit.
(help)                    -- display this message.
For more information, go to <a href="http://yices.csl.sri.com/language.shtml.
" rel="nofollow">http://yices.csl.sri.com/language.shtml.
</a>

(help) 라는 명령을 치면 도움말이 나옵니다. 괄호가 주르륵 보고 감을 잡으셨겠지만 리습과 유사한 문법을 쓰고 있습니다. 실제로 구현을 리습으로 한 것인지 아니면 문법 분석을 편리하게 하려고 한 것인지는 소스를 공개하지 않기 때문에 잘 모르겠습니다. 기본적인 사용법은 assert 명령어를 하나 이상 써서 조건을 명시한 후 그 조건을 모두 동시에 만족할 수 있는지를 check 명령어로 검사하는 것입니다. 대화식 환경이기 때문에 중간중간에 check 하면서 다시 assert 를 몇 개 더 하고 다시 check 하고 할 수도 있습니다. 우선 가장 간단한 것부터 해보겠습니다.
yices > (check)
sat
 
yices > (assert true)
 
yices > (check)
sat

일단 아무것도 없는 상태에서는 sat 즉 만족가능한 상태입니다. 그러므로 (assert true)를 하는 것은 아무 효과도 없겠죠. 그러니 당연히 만족한다는 결과가 또 나옵니다. 그럼 계속해서 절대로 만족할 수 없는 조건을 줘보겠습니다.
yices > (assert false)
unsat
 
yices > (check)
Logical context is inconsistent. Use (reset) to reset.

이렇게 모순을 발견하면 check로 물어보기도 전에 unsat 이 떠버리고 check를 하면 지금 모순된 상황이니 reset으로 다시 시작할 수 있다고 알려줍니다. reset을 하면 처음 아무것도 assert하지 않은 상황이 되므로 check를 해보면 다시 sat이 나옵니다.
yices > (reset)
 
yices > (check)
sat

이제 변수를 선언하고 정수를 다루는 아주 간단한 부등식 문제를 yices에게 풀어 보도록 하겠습니다.
yices > (define x::int)
 
yices > (assert (> x 0))
 
yices > (check)
sat

정수 x 에 대해 이 부등식을 만족하는 해가 당연히 존재하겠죠. 그러므로 sat 라는 답을 합니다. 그런데 구체적으로 어떤 해가 있는지 알고 싶을 때가 많기 때문에 만족하는 해(또는 model)를 하나 골라 보여주도록 설정할 수 있습니다.
yices > (set-evidence! true)
 
yices > (check)
sat
(= x 1)

다시 check하면 x가 1일 때 부등식을 만족함을 알려줍니다. yices 에 -e 옵션을 주어 실행하면 처음부터 이렇게 모델을 보여주도록 설정할 수 있습니다. 다음과 같이 yices를 일단 끝내고 다시 -e 옵션을 같이 주어 실행하면 set-evididence! 명령을 사용하지 않아도 바로 모델을 보여줍니다.
yices > (exit)
imyejin@vaio:~$ yices-1.0.21/bin/yices -i -e
Yices (version 1.0.21). Copyright 2005, 2006 SRI International.
GMP (version 4.3.1). Copyright Free Software Foundation, Inc.
Build date: Tue May  5 18:50:58 PDT 2009
Type `(exit)' with parentheses to exit.
Type `(help)' with parentheses for help.
yices > (define x::int)
 
yices > (assert (> x 0))
 
yices > (check)
sat
(= x 1)
 
 
yices > (assert (/= x 1))
 
yices > (check)
sat
(= x 2)
 
 
yices > (assert (/= x 2))
 
yices > (check)
sat
(= x 3)

계속해서 x가 1이 아니라는 조건을 준 다음 check를 하면 1말고 다른 해를 찾도록 할 수 있고 (그래서 2를 찾았죠) 또 x가 2가 아니라는 조건을 주면 다른 해 3을 찾습니다. 이렇게 조건에 맞는 값들을 계속해서 생성해 나갈 수 있다는 점을 응용해서 랜덤 테스팅을 보완하기 위한 특정 조건에 맞는 테스트를 생성하는 데 SMT solver 를 활용하는 시도가 활발히 이루어지고 있고, 특히 code coverage 를 만족하는 테스트를 자동화하는 데 응용하고 있는 것으로 압니다.

이번에는 reset한 다음 실수 변수를 하나 만들어 비슷한 일을 해보겠습니다.

yices > (reset)
 
yices > (define r::real)
 
yices > (assert (> r 0))
 
yices > (check)
sat
(= r 1)
 
 
yices > (assert (< r 1))
 
yices > (check)
sat
(= r 1/2)
 
 
yices > (assert (/= r 1/2))
 
yices > (check)
sat
(= r 3/4)
 
 
yices > (assert (/= r 3/4))
 
yices > (check)
sat
(= r 1/4)

실수라고는 하지만 실제로는 유리수 모델만을 찾습니다. (당연하죠, 디지털 컴퓨터로 랜덤한 무리수를 포함한 실수를 뚝딱 하고 만들어낼 방법....은 커녕 표현할 방법조차 제대로 없으니까요.)

N Queens 문제로 들어가기 전에 마지막으로 하나 더 살펴볼 것은 SMT solver 들은 아무 방정식이나 다 풀 수 없다는 보기입니다.

yices > (reset)
 
yices > (define n::int)
 
yices > (assert (= (* n n) 25))
Error: feature not supported: non linear problem.
 
yices > (exit)

이렇게 간단한 문제인 것 같아 보이지만 일차식이 아니므로 받아들이지 않습니다. SMT solver 의 목적은 복잡한 여러가지 종류의 문제를 푸는 것이 아니라 효율적인 decision procedure 있는 문제들을 빨리 푸는 데 있습니다.

이 문서는 당연히 Yices 홈페이지에 있는 강좌(tutorial)와 보기(example)들을 참조하여 작성하였습니다. 그러니까 더 자세한 내용은 Yices 홈페이지에 있는 친절한 강좌와 보기를 참고하시도록 하고, 우리는 다시 N Queens 문제로 돌아가서 yices와 같은 SMT solver로 N Queens 문제를 어떻게 표현할 수 있는지 알아보도록 하겠습니다.

이 글을 시작하면서 설명한 바와 같이 SMT solver는 SAT solver를 내장하고 있기 때문에 대부분의 SMT solver는 SAT 형식의 입력을 받을 수 있습니다. 그래서 지난 첫 연재에서 만들었던 q8.cnf 파일을 yices에 -d 옵션을 주어 실행시키면 yices를 단순한 SAT sovler로 이용할 수도 있습니다.

imyejin@vaio:~/yices-1.0.21$ cd examples/
imyejin@vaio:~/yices-1.0.21/examples$ ../bin/yices -d q8.cnf 
sat
imyejin@vaio:~/yices-1.0.21/examples$ ../bin/yices -d -e q8.cnf 
sat
-1 -2 -3 4 -5 -6 -7 -8 -9 10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 23 -24 -25 -26 27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 38 -39 -40 -41 -42 -43 -44 -45 -46 -47 48 -49 -50 -51 -52 53 -54 -55 -56 57 -58 -59 -60 -61 -62 -63 -64

하지만 이러면 SMT solver 로 N Queen 문제를 표현해 본다는 의미가 없기 때문에 Yices 형식으로 N Queen 문제를 표현한 다음 yices 에게 풀도록 해보겠습니다. Yices 형식은 앞서 살펴본 대화식 환경에서 썼던 명령어를 스크립트처럼 죽 적어 나가기만 하면 됩니다. 물론 위에서 사용하지 않은 다른 명령어 및 식들도 쓸 것입니다. 일단 4 queens 문제를 표현한 4queens.ys 를 살펴봅시다.
imyejin@vaio:~/yices-1.0.21/examples$ cat 4queens.ys 
; vim: syntax=lisp
(define-type nat4 (subtype (n::nat) (< n 4)))
 
(define abs::(-> int nat) (lambda (x::int) (if (>= x 0) x (- 0 x))))
 
(define q::(-> nat4 nat4))
 
; (assert (forall (y::nat4) (exists (x::nat4) (= y (q x)))))
(assert (exists (x::nat4) (= (q x) 0)))
(assert (exists (x::nat4) (= (q x) 1)))
(assert (exists (x::nat4) (= (q x) 2)))
(assert (exists (x::nat4) (= (q x) 3)))
 
(assert (/= (abs (- (q 0) (q 1))) 1))
(assert (/= (abs (- (q 0) (q 2))) 2))
(assert (/= (abs (- (q 0) (q 3))) 3))
 
(assert (/= (abs (- (q 1) (q 2))) 1))
(assert (/= (abs (- (q 1) (q 3))) 2))
 
(assert (/= (abs (- (q 2) (q 3))) 1))
 
(check)

주석도 리습 문법과 마찬가지로 세미콜론으로 시작합니다. Yices는 subtype 및 recursive datatype을 정의할 수 있다는 것이 특징입니다. nat4라는 타입은 자연수 중에서도 4보다 작은 자연수 즉 0,1,2,3 중 하나가 그 값이 될 수 있습니다. 그리고 람다식으로 함수를 정의할 수도 있습니다. abs 함수는 정수에서 자연수로 가는 함수로 이름에서 알 수 있듯이 절대값을 구하는 함수입니다. 대개의 SMT solver들은 함수에 대한 조건을 주면 그 함수가 만족하는 모델을 구해 주기도 합니다. 즉 abs처럼 처음부터 구체적으로 함수를 정의할 수도 있지만 q와 같이 함수의 타입만 정해 준 다음 assert로 q가 만족해야 할 조건을 주고 그러한 q 함수가 존재할 수 있는지를 알아볼 수 있다는 말입니다. q함수의 의미는 4x4를 x, y 축으로 표현했을 때 각각의 x값에 대해 퀸의 y값을 나타낸 함수입니다. 예를 들면 다음과 같이 퀸을 늘어놓는 것을 표한하는 q 함수를 그과 함께 표시하였습니다. (물론 이것은 4 qeeen 문제의 해가 아니죠. 대각선으로 퀸의 길이 겹치니까요.)
.+-+-+-+-+
3|o| | | |
.+-+-+-+-+
2| | |o| |
.+-+-+-+-+
1| |o| | |
.+-+-+-+-+
0| | | |o|
.+-+-+-+-+
..0 1 2 3
 
q(0) = 3
q(1) = 1
q(2) = 2
q(3) = 0

(위 그림에 표현한 방식은 보통 쓰는 수식 표현 방식입니다만, yices는 리습처럼 전위 표현을 쓰기 때문에 yices 형식으로 식을 표현할 경우 (= (q 0) 3) 이런 식으로 될 것입니다.) 또 한가지 4queens.ys 코드에서 특이한 사항은 exists 를 썼다는 것인데 exists 는 일일이 (define x0::nat4) (define x1::nat4) (define x2::nat4) (define x3::nat4) 이런 식으로 변수를 따로 정의하기 귀찮은 경우에 쓸 수 있습니다. (forall 도 제공하긴 하는데 forall 을 쓰기 시작하면 Yices가 undecidable 해져서 대략 난감하기 때문에 주의가 필요하고 골차아프므로 강좌에서는 그냥 넘어가기로 하겠습니다.) exists명령어들은 각 줄에 퀸이 하나씩 있어야 한다는 조건을 나타내고 (이 조건들에 의해 가로 세로 길은 서로 자동적으로 겹치지 않게 되죠) 그 아래 나머지 조건들은 대각선으로 퀸의 길이 겹치면 안된다는 것을 나타냅니다. yices를 -e 옵션으로 실행해서 풀라고 시키면 다음과 같이 4 queen 문제의 해를 하나 구해 줍니다.
imyejin@vaio:~/yices-1.0.21/examples$ ../bin/yices -e 4queens.ys 
sat
(= (q 1) 0)
(= (q 3) 1)
(= (q 0) 2)
(= (q 2) 3)

마찬가지 방법으로 8 Queens 문제도 다음과 같이 표현할 수 있으며

imyejin@vaio:~/yices-1.0.21/examples$ cat 8queens.ys 
; vim: syntax=lisp
(define-type nat8 (subtype (n::nat) (< n 8)))
 
(define abs::(-> int nat) (lambda (x::int) (if (>= x 0) x (- 0 x))))
 
(define q::(-> nat8 nat8))
 
; (assert (forall (y::nat8) (exists (x::nat8) (= y (q x)))))
(assert (exists (x::nat8) (= (q x) 0)))
(assert (exists (x::nat8) (= (q x) 1)))
(assert (exists (x::nat8) (= (q x) 2)))
(assert (exists (x::nat8) (= (q x) 3)))
(assert (exists (x::nat8) (= (q x) 4)))
(assert (exists (x::nat8) (= (q x) 5)))
(assert (exists (x::nat8) (= (q x) 6)))
(assert (exists (x::nat8) (= (q x) 7)))
 
(assert (/= (abs (- (q 0) (q 1))) 1))
(assert (/= (abs (- (q 0) (q 2))) 2))
(assert (/= (abs (- (q 0) (q 3))) 3))
(assert (/= (abs (- (q 0) (q 4))) 4))
(assert (/= (abs (- (q 0) (q 5))) 5))
(assert (/= (abs (- (q 0) (q 6))) 6))
(assert (/= (abs (- (q 0) (q 7))) 7))
 
(assert (/= (abs (- (q 1) (q 2))) 1))
(assert (/= (abs (- (q 1) (q 3))) 2))
(assert (/= (abs (- (q 1) (q 4))) 3))
(assert (/= (abs (- (q 1) (q 5))) 4))
(assert (/= (abs (- (q 1) (q 6))) 5))
(assert (/= (abs (- (q 1) (q 7))) 6))
 
(assert (/= (abs (- (q 2) (q 3))) 1))
(assert (/= (abs (- (q 2) (q 4))) 2))
(assert (/= (abs (- (q 2) (q 5))) 3))
(assert (/= (abs (- (q 2) (q 6))) 4))
(assert (/= (abs (- (q 2) (q 7))) 5))
 
(assert (/= (abs (- (q 3) (q 4))) 1))
(assert (/= (abs (- (q 3) (q 5))) 2))
(assert (/= (abs (- (q 3) (q 6))) 3))
(assert (/= (abs (- (q 3) (q 7))) 4))
 
(assert (/= (abs (- (q 4) (q 5))) 1))
(assert (/= (abs (- (q 4) (q 6))) 2))
(assert (/= (abs (- (q 4) (q 7))) 3))
 
(assert (/= (abs (- (q 5) (q 6))) 1))
(assert (/= (abs (- (q 5) (q 7))) 2))
 
(assert (/= (abs (- (q 6) (q 7))) 1))
 
(check)

yices로 풀면 다음과 같은 해를 얻습니다.
imyejin@vaio:~/yices-1.0.21/examples$ ../bin/yices -e 8queens.ys 
sat
(= (q 5) 0)
(= (q 2) 1)
(= (q 6) 2)
(= (q 3) 3)
(= (q 0) 4)
(= (q 7) 5)
(= (q 1) 6)
(= (q 4) 7)

8queens.ys 에 조건을 덧붙여서 q(0)=0 인 경우의 해가 있는지를 다음과 같이 알아볼 수 있습니다. 해가 있군요.
imyejin@vaio:~/yices-1.0.21/examples$ cat 8queens.ys - | ../bin/yices -e -i
Yices (version 1.0.21). Copyright 2005, 2006 SRI International.
GMP (version 4.3.1). Copyright Free Software Foundation, Inc.
Build date: Tue May  5 18:50:58 PDT 2009
Type `(exit)' with parentheses to exit.
Type `(help)' with parentheses for help.
yices > 
yices > 
yices > 
...
yices > 
yices > sat
(= (q 5) 0)
(= (q 2) 1)
(= (q 6) 2)
(= (q 3) 3)
(= (q 0) 4)
(= (q 7) 5)
(= (q 1) 6)
(= (q 4) 7)
 
 
yices > (assert (= (q 0) 0))
 
yices > (check)
sat
(= (q 0) 0)
(= (q 5) 1)
(= (q 7) 2)
(= (q 2) 3)
(= (q 6) 4)
(= (q 3) 5)
(= (q 1) 6)
(= (q 4) 7)
 
 
yices > 

SAT 형식으로 8 Queen 문제를 표현하면 700개가 넘는 CNF 절이 필요한 반면 SMT solver 의 경우에는 8 Queen 정도는 사람이 손으로 작성하기에도 무리가 없습니다. 이와 같이 SMT 형식을 사용하면 문제를 더 간결하고 자연스럽게 표시할 수 있습니다. 물론 이렇게 N Queens 문제를 풀면 SAT solver로 푸는 것보다 훨씬 (10~20배) 느립니다. SAT solver가 그만큼 빠르단 얘기죠. 그러니까 효율적인 풀이를 위해서는 SAT 문제로 바꿀 수 있는 문제라면 SAT 문제 형식으로 변환하여 푸는 것이 보통은 훨씬 효율적입니다. 특정 N에 대한 N Queen 문제는 SAT 형식으로 충분히 표현 가능한 유한한 영역의 문제이므로 SAT solver로 푸는 것이 더 적당하지만 이 강좌에서는 같은 문제를 놓고 표현 형식이 어떻게 다른지를 비교하기 위해 같은 문제를 SMT 형식으로 표현해 보고 풀어 본 것입니다. 하지만 일반적으로 정수나 실수에 대한 선형 방적식이나 부등식 등 유한하지 않은 영역에 대한 모델을 구해야 하는 경우에는 SAT solver의 영역을 넘어서는 문제이며 (어떻게든 인코딩이야 할 수 있겠지만 매우 부자연스럽거나 지나치게 많은 변수가 필요해지기 때문에) 이런 SAT 형식으로는 표현하거나 풀기 곤란한 문제들도 SMT solver가 해당 이론에 대한 decision procedure를 탑재하고 있다면 효율적으로 풀어낼 수 있는 것입니다. SMT solver는 Automated Theorem Prover들과 SAT solver의 중간쯤에 있는 둘 사이의 간격을 메워 주는 위치에 있으면서 static analysis와 dynamic analysis 기법을 연동하는 데 요긴하게 쓰이기도 한다고 들었습니다. 다음 연재에서는 정말로 Automated Theorem Prover 들을 살펴볼 수 있었으면 좋겠습니다만, 슬슬 바빠질 것 같아서 다음이 언제가 될 지 다음 연재를 기약하지는 못하겠군요 ㅠ.ㅠ;;

이상 맨땅에 해딩하면서 구른 SMT sovler 이야기였습니다. 얼마 전에 박사과정을 모집한다고 포스팅하신 홍콩과기대에 계시는 김성훈 교수님께서도 아미도 이런 툴들이 적용 가능한 분야를 연구하고 계시는 것 같은데요, (혹시 관련 내용이 없을까 해서 오랜만에 홈페이지를 방문해 보려고 했는데 홈페이지가 먹통이더군요 http://www.cse.ust.hk/~hunkim/ ) 하여간 관련 분야 전문가가 계시다면 더 정확한 설명이나 논평 그리고 다른 툴들과의 비교도 환영하고, 혹시 괜찮은 오픈소스 SMT solver면서 비교적 문서화가 잘 된 넘이 있다면 소개해 주셔도 감사하고요.

Forums: 
차리서의 이미지

언제나 좋은 글에 감사드립니다. 덕분에 잘 배웠습니다. 한 문장 한 문장 정확한 기술(description)과 예시여서, 정말 빠른 시간에 압축적으로—하지만 핵심은 충분히—브리핑받은 느낌이군요. 설명하시는 분의 능력이 느껴집니다. ^_^=b

imyejin wrote:
다음 연재에서는 정말로 Automated Theorem Prover 들을 살펴볼 수 있었으면 좋겠습니다만, 슬슬 바빠질 것 같아서 다음이 언제가 될 지 다음 연재를 기약하지는 못하겠군요 ㅠ.ㅠ;;
히이잉! ㅜㅜ

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

imyejin의 이미지

이번 SIGPL 여름학교에서 http://sigpl.or.kr/school/2009s/ 프로그래밍 언어에 관심 있는 사람들이 모여서 Coq 같은 증명 도우미에 대한 강의와 공부를 한다던데, 거기 가셔더 듣고 오시고 제가 바빠서 그때까지 아마 공부해서 정리가 안 될 것 같기 때문에 거기 가시면 거기서 여러 교수님들이나 강사님들께 잘 듣고 오셔서 저 대신 연재를 진행해 주셔도 됩니다.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

cocas의 이미지

오픈소스이면서 문서화도 잘 되어있고 성능도 좋은 SMT solver는 현재로서는 없습니다. 2009 smt competition 에서 그런 물건이 나올까 소망은 하고 있는데 잘 모르겠네요.

김성훈 교수님은 SMT solver를 어떤 쪽으로 활용하려고 하시나요? 제가 들었던 세미나들에서는 주로 debugging과 mining쪽 연구만 듣고 오늘 있었던 워크샵에서도 그쪽 얘기는 전혀 못 들어서요.

차리서의 이미지

cocas wrote:
제가 들었던 세미나들에서는 주로 debugging과 mining쪽 연구만 듣고 오늘 있었던 워크샵에서도 그쪽 얘기는 전혀 못 들어서요.
엇.. 지금 포천에 계신가요? 전 교수님이 안 보내주셔서(라고 쓰고 '전 귀찮아서'라고 읽습니다)...;;

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

cocas의 이미지

포천은 아니고 파주에 있었습니다. 원래 내일까진데 우리 연구실은 그냥 다 같이 오늘 내려왔지요. 고대에서 오신 분들(아 이름이 정확하게 기억이 안나네요) 보자마자 ATVA의 추억에 그만 눈물이.... ㅠㅠ

imyejin의 이미지

김성훈 교수님이 SMT solver를 쓰신다는 게 아니라 간혹 KLDP에 포스팅 하시는 분이라 분야를 살펴보니 테스팅이셔서 혹시나 하고 올려 본 글입니다. 혹시 국내에 SMT solver 많이 쓰는 연구실이나 회사가 있나요? cocas 님께서 잘 아시는 것 같은데, 제가 이렇게 맨땅에 구른 거 말고 좀 우리말로 정리된 강의자료라던가 세마나 자료랄까 그런 거 없을까요? 경기대 권교수님 홈페이지에서 예전에 비슷한 자료를 봤던 것 같기도 한데 다시 찾으려니 또 못찾겠네요 ㅠ.ㅠ

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

notpig의 이미지

안녕하세요

경기대학교 박사과정 이태훈입니다.

지금은 아니지만 예전에 SAT 하고 SMT 에 대해서 약간 해봤는데요
일단 문서화가 잘된 도구는 못본거 같습니다....
예전에 내부 세미나시 사용한 자료하고
몇가지 게임해결을 위해 SMT 와 SAT 를 사용한 사례가 있는데 시간이 되면 올려보도록 하겠습니다.

http://kuic.kyonggi.ac.kr/~khkwon/03-teaching/special-topics/se-2007.html

혹시 관심이 있으실진 모르지만 예전에 SAT 에 대한 강의자료입니다.

연구실은 아마도 Static Analysis쪽이나 Model Checking 쪽 하는 곳에서 사용해봤을꺼 같은데..몇군데는 안되는걸로 알고있고
회사에서 사용하는곳을 알고있긴 한데 많진 않은걸로 알고있습니다.

hunkim의 이미지

저희는 지금 자바 자동 testing에 SMT를 사용하고 있습니다. 즉 아래와 같은 함수가 있다고 합시다.

foo(T t) {
...
if (t.x * t.y == 123456) {
// error
}

} 인 코드가 있을 경우 error를 일으키는 입력값을 찾고 있습니다.

우선 이를 위해서는 자바의 조건문을 SMT 의 입력으로 바꾸어야 합니다. 이렇게 해서 입력 값들을 구할 수 있으면 testing 뿐만아니라 bug reproducing 등에도 사용될수 있고 여러가지 다양한 활용분야가 많습니다.

이런문제들을 저희와 같이 풀고자 하시는 분들은
http://www.se.or.kr/20 이나 http://www.se.or.kr/3 을 참고 하세요.

cocas의 이미지

저희도 C 자동 testing 에 SMT를 적용해서 코드 커버리지를 높이는 연구를 하고 있습니다.

홍콩에서 김성훈 교수님과 같이 문제를 풀어도 좋겠지만 군대 문제도 걸리고 이미 좋은 교수님을 만나서요 하하하..

나주엥 교수님과 같이 이 문제에 관해 논의해 보면 좋겠습니다. 저는 KAIST 김문주 교수님 연구실 학생 김윤호입니다.

imyejin의 이미지

위에 두 분께서는 어떤 SMT 툴이나 라이브러리를 쓰고 계시는지 궁금합니다.

특히 김성훈 교수님 올리신 코드 예제를 보면 t.x * t.y == 123456 이런 부분이 있는데 두 변수를 곱하는 형태가 나오면 일반적으로 linear constraint가 아닌데 저런 것을 잘 풀어 주는 (인수분해 같은 좀 복잡한(?) 이론도 동원하고 해서) SMT sovler가 있는지요?

하여간 연구하시면서 SMT solver들에 대한 팁이라던가 강좌라던가 혹시 정리되면 (특히나 우리말로 되어 있으면 더 좋고요) 연구실 홈페이지에다도 올리시고 이 글타래에다가도 링크 달아 주시면 대단히 감사하겠습니다.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

cocas의 이미지

저희는 주로 Z3, Yices, Boolector 등으로 사용하고 있습니다. 저런 경우는 Bitvector theory를 사용하면 됩니다. 이번 Z3 2.0 에는 non-linear support 가 추가되었다고 하는데 아직 확인은 못했고요. CPU 에서 수행하는 연산은 결국 adder와 같은 기본 게이트 로직으로 돌아가기 때문에 SMT solver 에서 BV theory를 사용하면 거의 동일한 semantics을 유지할 수 있습니다.

댓글 달기

Filtered HTML

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

BBCode

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param>
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

Textile

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • You can use Textile markup to format text.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Markdown

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • Quick Tips:
    • Two or more spaces at a line's end = Line break
    • Double returns = Paragraph
    • *Single asterisks* or _single underscores_ = Emphasis
    • **Double** or __double__ = Strong
    • This is [a link](http://the.link.example.com "The optional title text")
    For complete details on the Markdown syntax, see the Markdown documentation and Markdown Extra documentation for tables, footnotes, and more.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Plain text

  • HTML 태그를 사용할 수 없습니다.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 줄과 단락은 자동으로 분리됩니다.
댓글 첨부 파일
이 댓글에 이미지나 파일을 업로드 합니다.
파일 크기는 8 MB보다 작아야 합니다.
허용할 파일 형식: txt pdf doc xls gif jpg jpeg mp3 png rar zip.
CAPTCHA
이것은 자동으로 스팸을 올리는 것을 막기 위해서 제공됩니다.