z3-solver 사용법 정리해오기 (1000자 이상)
z3는 마이크로소프트에서 개발한 수식 해석 도구로, 방정식 같은 수학적인 식을 해결할 수 있게 해줍니다. 정확히는 특별하고 효율적인 알고리즘을 가진 SMT 솔버입니다.
pip install z3-solver
pip를 통해 z3-solver 을 설치해주면 됩니다.
z3-solver 모듈을 불러올 땐 아래의 코드로 불러올 수 있습니다.
from z3 import *
👾\정수인 미지수를 선언할 때에는 Int() 함수를 통해 선언할 수 있습니다. 예를 들어 변수명이 x인 정수인 미지수를 선언할 때에는 아래의 코드를 사용할 수 있습니다.
x = Int('x')
y = Int('y')
이 때 int() 와 Int() 대소문자를 구분해야 합니다. 소문자 int() 의 경우 파이썬에서 int형으로 자료형을 변환할 때 사용됩니다. 대문자 Int() 를 사용해야 z3에서 정수인 미지수를 선언할 수 있습니다.
실수형인 미지수를 선언할 때에는 Real() 함수를 통해 선언할 수 있습니다. 정수인 미지수를 선언할 때와 마찬가지로 아래의 코드를 사용할 수 있습니다.
x = Real('x')
y = Real('y')
논리형 미지수를 선언할 때에는 Bool() 함수를 통해 선언할 수 있습니다. 선언 코드는 아래와 같습니다.
x = Bool('x')
y = Bool('y')
Bool 은 Boolean을 줄인 말로, 0과 1을 저장합니다. 따라서 0과 1로 이루어진 미지수를 and, or, xor 등의 논리 게이트 형식으로 계산할 수 있습니다.