Z3 solver 정리

Z3 solver

z3 solver는 특정 값들을 찾아주는 SMT solver 모듈이라고 한다

쉽게 말하면 여러 수식을 풀어주는 모듈이라고 생각하면 된다

리버싱 할 때도 많이 필요하고 그게 아니더라도 유용히 쓸 수 있을 거 같아서 정리하기로 했다

설치

일단 Z3 solver 모듈의 링크는 이곳이다

github.com/Z3Prover/z3

들어가면 다양한 언어에서의 설치 과정이 자세히 나와있지만 나는 파이썬을 쓸 거라서 pip로 간단히 설치가 가능하다

pip install z3-solver

 or
 
pip3 install z3-solver

기본 문법

사용 전 모듈 불러오기

from z3 import *

정수형 미지수 선언

x = Int('x')
y = Int('y')

실수형 미지수 선언

x = Real('x')
y = Real('y')

불 형 미지수 선언

x = Bool('x')
y = Bool('y')

비트 벡터 미지수 선언

x = BitVec('x',16)
y = BitVec('y',16)

비트벡터는 모듈러 역수 같은걸 구할 때 쓰인다

미지수 뒤의 숫자는 몇 비트인지를 설정해주는 숫자이다

답 구하기

solve()

예시로 $\begin{cases}x+y=12\\x-y=6\end{cases}$라는 연립방정식의 해를 구하려고 하면 아래와 같이 쓸 수 있다

>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> solve(x+y==12,x-y==6)
[x = 9, y = 3]

Solver class

z3 solver는 Solver라는 객체를 지원하는데, 이를 사용하면 여러 수식을 원할때 추가하고 계산하는 식을 나누는 등 더욱 쉽게 코드를 짤 수 있다

선언

s = Solver()

식 추가

s.add()

아까 본 식을 Solver 객체로 추가해보자

>>> s = Solver()
>>> s.add(x+y==12)
>>> s.add(x-y==3)
>>> s
[x + y == 12, x - y == 3]

잘 들어간것을 알 수 있다

push & pop

s.push()
s.pop()

수식의 이전 상태를 기억해놓기 위한 함수 push와 push 했던 상태로 되돌리는 pop이 있다

push를 하고 수식을 추가하다가 pop을 하면 push를 했을때의 식 상황으로 돌아간다

해의 존재 여부

s.check()

주어진 식들을 모두 만족하는 해가 있으면 sat, 없으면 unsat, 해결할 수 없는 식이면 unknown을 반환한다

s.reason_unknown()

unkwown일 때는 위 함수를 통해 그 이유를 알 수 있다

답 구하기

s.model()

s.check()가 sat일 때 만족하는 해 중 하나를 반환한다

초기화

s.reset()

예제

>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
>>> s.add(x+y<12)
>>> s.add(x>8)
>>> s.push()
>>> s.add(y>9)
>>> s.check()
unsat
>>> s.pop()
>>> s
[x + y < 12, x > 8]
>>> s.check()
sat 
>>> s.model()
[y = 2, x = 9]
>>> s.reset()
>>> s
[]

push를 하고 식을 추가했더니 unsat이 떠서 pop으로 되돌려 답을 구하는 모습이다

답을 구한후 reset을 하니 식이 모두 사라지는 걸 볼 수 있다

답을 모두 구하기

문제를 풀다보면 답이 하나가 아닌 경우가 생긴다

그럴 때는 전에 구한 답이 중복되는지 비교하는 식을 넣어주면 된다

while s.check() == sat:
  print s.model()
  s.add(Or(x != s.model()[x], y != s.model()[y]))

그 외

나머지는 필요하면 추가하도록 하겠다