z3-solver 사용법 정리

z3-solver 설치

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

z3-solver는 많은 언어에서 사용할 수 있지만 이 글에선 python 기준으로 설명하도록 하겠다.

 

pip install z3-solver

pip를 이용하면 손쉽게 z3-solver를 설치할 수 있다.

 

z3-solver 불러오기

사용 전에, z3-solver는 모듈이기 때문에 import로 모듈을 불러와야한다.

 

from z3 import *

z3-solver 모듈은 이렇게 불러올 수 있다.

 

미지수 선언

 

정수형 미지수 선언

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

 

Bool형 미지수 선언

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

 

비트벡터 미지수 선언

x = BitVec('x')
y = BitVec('y')

사용법

예를들어 이 문제를 푼다고 하면, 코드는 아래와 같이 짜면 된다.

from z3 import *

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

solve(2*x + 3*y == 13, 4*x - y == 5)

먼저 z3-solver를 불러와주고 x와 y를 정수형 미지수로 선언해주고 solve() 함수를 사용해 식과 맞게 매개변수를 넣어주면

답이 나온다.

 

[x = 2, y = 3]

답은 이런 방식으로 나온다.

 

Solver

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

 

s = Solver()

선언은 이렇게 할 수 있다.

 

s.add로 아래와 같이 식을 추가할 수 있다.

from z3 import *

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

s = Solver()
s.add(x+y==5)
s.add(x-y==3)
print(s)

 

식이 잘 추가된 걸 볼 수 있다.

 

s.push()
s.pop()

push함수는 수식을 기억한다. push를 하고 식을 추가하다 pop을 하면 push했던 상태로 식이 되돌아간다.

 

s.check()

해의 존재 여부를 확인할 수 있는 함수 check이다. 주어진 식들을 모두 만족하는 해가 있으면 sat, 없으면 unsat, 해결할 수 없는 식이면 unknown을 반환한다

 

s.reason_unknown()

s.check()의 결과값이 unknown일 때, 이 함수를 사용 해 이유를 알 수 있다.

 

s.model()

s.check()의 결과값이 sat일 때, 이 함수를 사용 해 식을 만족하는 해 중 하나를 출력한다.

 

s.reset()

초기화 함수이다.