5_Z3 사용해보기

YUMMMM 2023. 4. 7. 02:50

이번주에는 Z3를 설치하고 간단하게 사용해보는 과제를 진행하였다! 진행과정을 간단히 적어보겠다.

1) Z3 Solver 설치

Z3-Solver는 수식이나 논리를 자동으로 증명하거나 값을 찾아주는 SMT Solver의 한 종류이다.

간단히 pip 명령어로 설치하거나, https://github.com/Z3Prover/z3 해당 주소를 이용하여 설치할 수 있다.

나는 pip를 사용하여 일단 계속 사용해보던 miasm 프로젝트의 가상환경에 설치해보았다.

pip install z3-solver

2) Z3 예제와 함께 코드 분석해보기

1. 모듈 불러오기

from z3 import *

2. 정수형 변수 선언과 조건에 따른 해 구하기

>>> x = Int('x')
>>> y = Int('y')
>>> solve(x > 2, y < 10, x + 2 * y == 7)
[y = 0, x = 7]

정수형 변수 x와 y를 선언한 후, 해당 조건들을 만족하는 x, y를 구해준다.

3. 여러 명령어 확인하기

>>> n = x + y >= 3
>>> print(n.num_args())
2
>>> print(n.children())
[x + y, 3]
>>> print(n.arg(0))
x + y
>>> print(n.decl())
>=

n에는 x 변수와 y 변수의 값을 더한 결과가 3 이상인지 여부를 나타내는 boolean 논리식이 들어가게 된다.

n.num_args()의 경우, n의 인자의 개수를 반환한다. 해당 코드에선 'x + y' 와 '3'으로 두 개이므로 2를 반환한다.

n.children()의 경우, n의 모든 인자들을 반환한다. 해당 코드에선 'x + y' 와 '3'을 리스트 형태로 반환한다.

n.arg(0)의 경우, 첫 번째 인자를 반환한다. 해당 코드에선 'x + y'가 첫 번째 인자이므로 해당값이 반환된다.

n.decl()의 경우, 연산자를 반환한다. 해당 코드에선 '>='가 반환된다.

4. 실수형 변수 선언과 조건에 따른 해 구하기

>>> x = Real('x')
>>> y = Real('y')
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[y = -1.1885280594?, x = 1.2599210498?]

>>> set_option(precision = 30)
>>> solve(x**2 + y**2 == 3, x**3 == 2)
[y = -1.188528059421316533710369365015?,
 x = 1.259921049894873164767210607278?]

실수형 변수 x와 y를 선언한 후, solve 함수를 이용하여 연립방정식을 푸는 코드이다.

'x**2 + y**2 = 3'과 'x**3 == 2'를 모두 만족하는 해를 찾고자 하는데,

두 번째 solve 함수를 호출하기 전 'set_option(precision = 30)' 해당 코드를 실행하여 소수점 이하 30짜리까지 표시되도록 했다.

5. 객체 생성 후 다양한 명령어 사용해보기

>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
>>> print(s)
[]

>>> s.add(x > 10, y == x + 2)
>>> print(s)
[x > 10, y == x + 2]

>>> s.check()
>>> print(s.check())
sat

>>> s.push()
>>> s.add(y < 11)
>>> print(s)
[x > 10, y == x + 2, y < 11]

>>> s.check()
>>> print(s.check())
unsat

>>> s.pop()
>>> s.check()
>>> print(s.check())
sat

Solver() 함수를 이용해 Solver 객체도 생성해줄 수 있다.

정수형 변수 x와 y를 선언한 후, Solver 객체 s를 생성해주고 add() 함수를 이용하여 'x가 10보다 크다'는 조건과 'y는 x + 2한 값과 같다'는 조건을 추가해준다.

처음 객체 s의 현재 상태를 출력했을 때는 빈 객체여서 '[]' 가 출력되지만, 조건을 추가해준 뒤에는 '[x > 10, y == x + 2]' 이 출력되는 것을 확인할 수 있다.

check() 함수로는 해당 조건들을 만족하는 해가 있는지 여부를 확인하는 함수이다. 따라서 s.check를 출력했을 때 'sat(만족)'이 출력됐다는 것은 해당 조건을 만족하는 변수 값이 존재한다는 것이다.

push() 함수는 객체 s의 현재 상태를 스택에 저장한다. 다시 add() 함수를 이용해 'y가 11보다 작다' 는 조건을 추가해주고, 객체 s의 현재 상태를 출력한다. 추가된 제약 조건까지 잘 출력되는 것을 확인할 수 있다.

다시 check() 함수를 이용해 확인하고 해당 여부를 출력했을 땐 'unsat(불만족)'이 출력되었다. 해당 조건들을 모두 만족하는 값이 없다는 것을 의미한다.

pop() 함수는 스택에 가장 최근에 저장된 값을 불러오고 스택에서 그 값을 삭제한다. 따라서 가장 최근에 저장된(추가된) 'y < 11' 조건이 삭제되고, 다시 check() 함수로 여부를 출력했을 때 'sat(만족)'이 출력되는 것을 확인할 수 있다.

6. Solver 객체의 모델을 얻고 각 변수값 출력하기

>>> x, y, z = Reals('x y z')
>>> s = Solver()
>>> s.add(x > 1, y > 1, x + y > 3, z - x < 10)
>>> s.check()
>>> print(s.check())
sat

>>> m = s.model()
>>> for data in m.decls():
>>>     print("%s = %s" %(data.name(), m[data]))
y = 2
x = 3/2
z = 0

model() 함수는 Solver 객체에서 check() 함수를 호출하여 모델을 찾은 경우, 해당 모델을 반환한다.

여기서 모델은 제약조건을 만족시키는 변수들의 값을 가지고 있다.

delcs() 함수는 모델의 모든 변수와 상수를 반환하는 함수이다.

해당 코드에선 add() 함수로 추가된 제약식을 만족하는 값이 있는지 확인 후 Solver 객체 s의 모델을 m에 넣어주고, decls() 함수를 이용해 모든 변수와 변수가 가지는 값을 출력한다. data.name은 변수 이름을, m[data]는 해당 변수의 값을 반환한다.

3) 간단한 함수 정리

Int('x') : 변수 x를 정수형으로 선언

Real('x') : 변수 x를 실수형으로 선언

Bool('b') : 변수 b를 boolean형으로 선언

solve() : 해 구하기

Solver() : Solver 객체 선언

add() : 조건 추가

check() : 해당 조건을 만족하는 값이 있는지 확인

decls() : 모델의 모든 변수와 상수값 반환