Satisfiability Modulo Theories (SMT) solver Z3
SMT 란 ?
컴퓨터 과학 및 수학에서 SMT는 해당 mathematical formulation (수학적 공식)을 만족하는 지 결정하는 문제입니다. 기존의 Boolean satisfiability (SAT)는 Boolean formulation만 표현할 수 있지만, SMT는 추가적으로 실수, 정수, list, array, bit vector, 그리고 str과 같은 다양한 data를 사용한 보다 복합적인 formulation을 해결할 수 있습니다.
다음은 SAT의 예시입니다.
$$(A\lor \neg B)\land (B \lor C)$$
이 SAT 문제의 해결책은 A, B, C에 Boolean value를 할당하여, 표현식을 참으로 만드는 조합을 찾는 것입니다.
예로 A=1, B=0, C=1이면 표현식은 참이 됩니다.
SMT를 예로 생각해 보면,
$$(A\lor \neg B)\land (B \lor C) \land (y=x+2) \land (z=y-1)$$
여기서 A, B, C는 Boolean value이고, x, y, z는 integer입니다.
풀어보면, A=1, B=0, C=1, x=1, y=3, z=2일 경우 해당 표현식을 만족시킵니다.
예시를 통해서 보면, SMT는 더 복잡한 문제를 모델링하고 해결하는 데 사용되는 것을 짐작할 수 있습니다.
SMT Solver Z3
SMT solver는 입력 변수 집합에 대한 SMT 문제를 빠르게 해결하기 위한 tool입니다. 각 solver에 적합한 표현으로 수식을 변환해 주고 solver를 실행하면, 복잡한 문제에 대한 정답을 빠르게 찾을 수 있습니다.
Z3는 microsoft research에서 개발한 open source SMT solver이며 다음과 같은 특징이 있습니다.
- 다양한 문제에 적용: linear, non-linear, bit-vector, array, str., etc.
- 다양한 언어: Python, C#, C++, Java, etc.
저는 python3 환경에서 사용하므로 다음과 같은 code로 설치해 줍니다.
pip install z3-solver
위의 SAT 예시를 Z3로 작성해 보면 다음과 같이 작성할 수 있습니다.
from z3 import *
A, B, C = Bools('A B C')
s = Solver()
s.add(And(Or(A,Not(B)),Or(B,C)))
print(s.check())
print(s.model())
먼저 A, B, C를 Boolean 변수로 지정해 주고, Solver instance s에 위의 formula를 추가합니다.
이후에 해당 문제가 해결(만족) 가능한지 check()로 확인합니다.
check()는 sat (satisfiable), unsat (unsatisfiable), unknown 중 하나를 반환하며,
sat일 경우 model()를 사용해서 해당 문제의 구제적인 해를 반환할 수 있습니다.
따라서, 이에 대한 결과는 다음과 같이 출력됩니다.
sat
[A = True, B = True, C = False]
위의 예시에서 이야기한 해와는 다르지만, 이 또한 해가 될 수 있습니다.
이번 포스팅에서는 SMT와 SMT solver에 대해서 간단히 알아보았습니다.
다음은 실제 VLSI CAD 문제에 적용했을 경우에 대하여 이야기해보겠습니다.
참고
https://z3prover.github.io/papers/programmingz3.html
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories