#pip3 install z3-solverfrom z3 import*s =Solver()#The solver will be given the conditionsx =Bool("x")#Declare the symbos x, y and zy =Bool("y")z =Bool("z")# (x or y or !z) and ys.add(And(Or(x,y,Not(z)),y))s.check()#If response is "sat" then the model is satifable, if "unsat" something is wrongprint(s.model())#Print valid values to satisfy the model
정수/단순화/실수
SMT(Satisfiability Modulo Theories) 문제를 해결하기 위해 Z3는 정수, 단순화 및 실수와 관련된 다양한 기능을 제공합니다.
정수(Integers)
Z3는 정수 연산을 지원하며, 다음과 같은 연산자를 사용할 수 있습니다.
+: 덧셈
-: 뺄셈
*: 곱셈
/: 나눗셈
%: 나머지
div: 몫
mod: 나머지
abs: 절댓값
^: 거듭제곱
또한, 비교 연산자도 사용할 수 있습니다.
=: 같음
!=: 같지 않음
<: 작음
>: 큼
<=: 작거나 같음
>=: 크거나 같음
단순화(Simplification)
Z3는 식을 단순화하는 기능을 제공합니다. 이를 통해 복잡한 식을 간단하게 표현할 수 있습니다. 단순화는 simplify() 함수를 사용하여 수행할 수 있습니다.
실수(Reals)
Z3는 실수 연산을 지원하며, 다음과 같은 연산자를 사용할 수 있습니다.
+: 덧셈
-: 뺄셈
*: 곱셈
/: 나눗셈
^: 거듭제곱
또한, 비교 연산자도 사용할 수 있습니다.
=: 같음
!=: 같지 않음
<: 작음
>: 큼
<=: 작거나 같음
>=: 크거나 같음
Z3는 실수 연산에 대한 정확한 결과를 제공하지 않을 수 있으므로, 주의가 필요합니다.
from z3 import*x =Int('x')y =Int('y')#Simplify a "complex" ecuationprint(simplify(And(x +1>=3, x**2+ x**2+ y**2+2>=5)))#And(x >= 2, 2*x**2 + y**2 >= 3)#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solutionr1 =Real('r1')r2 =Real('r2')#Solve the ecuationprint(solve(r1**2+ r2**2==3, r1**3==2))#Solve the ecuation with 30 decimalsset_option(precision=30)print(solve(r1**2+ r2**2==3, r1**3==2))
모델 출력
To print the model, you can use the model object returned by the solver. The model object contains the assignments for each variable in the formula.
To print the assignments, you can iterate over the variables and use the eval method to get the assigned value.
Here is an example:
for variable in model: value = model.eval(variable)print(f"{variable} = {value}")
This will print each variable along with its assigned value.
from z3 import*x, y, z =Reals('x y z')s =Solver()s.add(x >1, y >1, x + y >3, z - x <10)s.check()m = s.model()print ("x = %s"% m[x])for d in m.decls():print("%s = %s"% (d.name(), m[d]))
기계 산술
현대의 CPU와 주류 프로그래밍 언어는 고정 크기 비트 벡터를 사용하여 산술 연산을 수행합니다. 기계 산술은 Z3Py에서 비트 벡터로 사용할 수 있습니다.
from z3 import*x =BitVec('x', 16)#Bit vector variable "x" of length 16 bity =BitVec('y', 16)e =BitVecVal(10, 16)#Bit vector with value 10 of length 16bitsa =BitVecVal(-1, 16)b =BitVecVal(65535, 16)print(simplify(a == b))#This is True!a =BitVecVal(-1, 32)b =BitVecVal(65535, 32)print(simplify(a == b))#This is False
부호 있는/부호 없는 숫자
Z3는 비트 벡터가 부호 있는지 없는지에 따라 다른 방식으로 처리되는 특수한 부호 있는 버전의 산술 연산을 제공합니다. Z3Py에서 <, <=, >, >=, /, % 및 >> 연산자는 부호 있는 버전에 해당합니다. 이에 대응하는 부호 없는 연산자는 ULT, ULE, UGT, UGE, UDiv, URem 및 LShR입니다.
from z3 import*# Create to bit-vectors of size 32x, y =BitVecs('x y', 32)solve(x + y ==2, x >0, y >0)# Bit-wise operators# & bit-wise and# | bit-wise or# ~ bit-wise notsolve(x & y ==~y)solve(x <0)# using unsigned version of <solve(ULT(x, 0))
함수
해석 함수는 **함수 +**가 고정된 표준 해석을 가지는 산술과 같은 함수입니다. 해석되지 않은 함수와 상수는 최대한 유연합니다. 이들은 함수나 상수에 대한 제약 조건과 일관성이 있는어떤 해석이든 허용합니다.
예시: x에 대해 f를 두 번 적용하면 다시 x가 되지만, x에 대해 f를 한 번 적용하면 x와 다릅니다.
from z3 import*x =Int('x')y =Int('y')f =Function('f', IntSort(), IntSort())s =Solver()s.add(f(f(x)) == x, f(x) == y, x != y)s.check()m = s.model()print("f(f(x)) =", m.evaluate(f(f(x))))print("f(x) =", m.evaluate(f(x)))print(m.evaluate(f(2)))s.add(f(x) ==4)#Find the value that generates 4 as responses.check()print(m.model())
예제
스도쿠 퍼즐 풀이기
from z3 import*defsolve_sudoku(grid):# Create a 9x9 grid of integer variables cells = [[Int(f"cell_{i}_{j}")for j inrange(9)] for i inrange(9)]# Each cell must contain a value between 1 and 9 cell_constraints = [And(1<= cells[i][j], cells[i][j] <=9)for i inrange(9)for j inrange(9)]# Each row must contain distinct values row_constraints = [Distinct(cells[i])for i inrange(9)]# Each column must contain distinct values col_constraints = [Distinct([cells[i][j] for i inrange(9)])for j inrange(9)]# Each 3x3 subgrid must contain distinct values subgrid_constraints = [Distinct([cells[i + 3 * (k // 3)][j + 3 * (k % 3)] for i in range(3) for j in range(3)]) for k in range(9)]
# Combine all constraints constraints = cell_constraints + row_constraints + col_constraints + subgrid_constraints# Create a solver and add the constraints solver =Solver() solver.add(constraints)# Add the initial values from the gridfor i inrange(9):for j inrange(9):if grid[i][j] !=0: solver.add(cells[i][j] == grid[i][j])# Check if there is a solutionif solver.check()== sat:# Get the solution model = solver.model()# Extract the values from the model solution = [[model.evaluate(cells[i][j]).as_long()for j inrange(9)] for i inrange(9)]return solutionreturnNone# Example Sudoku gridgrid = [ [5,3,0,0,7,0,0,0,0], [6,0,0,1,9,5,0,0,0], [0,9,8,0,0,0,0,6,0], [8,0,0,0,6,0,0,0,3], [4,0,0,8,0,3,0,0,1], [7,0,0,0,2,0,0,0,6], [0,6,0,0,0,0,2,8,0], [0,0,0,4,1,9,0,0,5], [0,0,0,0,8,0,0,7,9]]# Solve the Sudoku puzzlesolution =solve_sudoku(grid)# Print the solutionif solution:for row in solution:print(row)else:print("No solution found.")
from z3 import*defsolve_sudoku(grid):# 9x9 그리드의 정수 변수 생성 cells = [[Int(f"cell_{i}_{j}")for j inrange(9)] for i inrange(9)]# 각 셀은 1부터 9까지의 값을 가져야 함 cell_constraints = [And(1<= cells[i][j], cells[i][j] <=9)for i inrange(9)for j inrange(9)]# 각 행은 서로 다른 값을 가져야 함 row_constraints = [Distinct(cells[i])for i inrange(9)]# 각 열은 서로 다른 값을 가져야 함 col_constraints = [Distinct([cells[i][j] for i inrange(9)])for j inrange(9)]# 각 3x3 서브그리드는 서로 다른 값을 가져야 함 subgrid_constraints = [Distinct([cells[i + 3 * (k // 3)][j + 3 * (k % 3)] for i in range(3) for j in range(3)]) for k in range(9)]
# 모든 제약 조건을 결합 constraints = cell_constraints + row_constraints + col_constraints + subgrid_constraints# Solver 생성 및 제약 조건 추가 solver =Solver() solver.add(constraints)# 그리드에서 초기 값 추가for i inrange(9):for j inrange(9):if grid[i][j] !=0: solver.add(cells[i][j] == grid[i][j])# 해결책이 있는지 확인if solver.check()== sat:# 해결책 가져오기 model = solver.model()# 모델에서 값 추출 solution = [[model.evaluate(cells[i][j]).as_long()for j inrange(9)] for i inrange(9)]return solutionreturnNone# 예제 스도쿠 그리드grid = [ [5,3,0,0,7,0,0,0,0], [6,0,0,1,9,5,0,0,0], [0,9,8,0,0,0,0,6,0], [8,0,0,0,6,0,0,0,3], [4,0,0,8,0,3,0,0,1], [7,0,0,0,2,0,0,0,6], [0,6,0,0,0,0,2,8,0], [0,0,0,4,1,9,0,0,5], [0,0,0,0,8,0,0,7,9]]# 스도쿠 퍼즐 풀기solution =solve_sudoku(grid)# 해결책 출력if solution:for row in solution:print(row)else:print("해결책을 찾을 수 없습니다.")
# 9x9 matrix of integer variablesX = [ [ Int("x_%s_%s"% (i+1, j+1))for j inrange(9) ]for i inrange(9) ]# each cell contains a value in {1, ..., 9}cells_c = [ And(1<= X[i][j], X[i][j] <=9)for i inrange(9)for j inrange(9) ]# each row contains a digit at most oncerows_c = [ Distinct(X[i])for i inrange(9) ]# each column contains a digit at most oncecols_c = [ Distinct([ X[i][j] for i inrange(9) ])for j inrange(9) ]# each 3x3 square contains a digit at most oncesq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]for i inrange(3) for j inrange(3) ])for i0 inrange(3)for j0 inrange(3) ]sudoku_c = cells_c + rows_c + cols_c + sq_c# sudoku instance, we use '0' for empty cellsinstance = ((0,0,0,0,9,4,0,3,0),(0,0,0,5,1,0,0,0,7),(0,8,9,0,0,0,0,4,0),(0,0,0,0,0,0,2,0,8),(0,6,0,2,0,1,0,5,0),(1,0,2,0,0,0,0,0,0),(0,7,0,0,0,0,5,2,0),(9,0,0,0,6,5,0,0,0),(0,4,0,9,7,0,0,0,0))instance_c = [ If(instance[i][j] ==0,True,X[i][j] == instance[i][j])for i inrange(9)for j inrange(9) ]s =Solver()s.add(sudoku_c + instance_c)if s.check()== sat:m = s.model()r = [ [ m.evaluate(X[i][j])for j inrange(9) ]for i inrange(9) ]print_matrix(r)else:print"failed to solve"