Research and Investment

본 포스트는 아래 Youtube 링크에 해당하는 영상을 보고 정리하였습니다.

https://www.youtube.com/watch?v=56IIrBZy9Rc&list=PLlMMtlgw6qNiRlD_RaJMNbZj2kSUPrPtU&index=1 

강사의 github link는 아래와 같습니다.

https://github.com/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb

Z3 Variables

다른 종류(Sorts, z3의 type)의 z3 변수를 만듦

x = Bool("x")
x = Const("x" , BoolSort())
p, q, r = Bools("p q r") # convenience function for multiple definitions
x = Real("x")
x, y = Reals("x y")		# need space
y = Int("x") 
v = BitVec("n", 32) # 32 bit bitvector
f = FP("f", Float64()) #Floating point values
a = Array("a", IntSort(), BoolSort()) # arrays

Constraints / Operations

# Common numerical operations
print(x + x) # addition
print(x * x) # multiplication
print(x ** 4) # fourth power of x 

# Common boolean operations
print(And(p,q))
print(And(p,q,r)) # some can accept more than one argument for convenience.
print(Or(p,q))
print(Implies(p,q))
print(Xor(p,q))
print(Not(p))

# Constraints 
print(x == x) #equal
print(x != x) # not equal
print(x <= RealVal(3)) # inequality
print(Or( x < 3,  x == 3, x > 3  )) # Constraints are operations into booleans

# And many more! Look in the API docs for others https://z3prover.github.io/api/html/namespacez3py.html

Exercise

Get a root of the polynomial x**3 + 3*x**2 + 4*x + 2 == 0 using z3.

x = Real("x")
solve(x**3 + 3*x**2 + 4*x + 2)

증명 방법

x = Real("x")
solve(x**3 + 3*x**2+ 4*x + 2 ==0, x != -1)
# 또는
prove( Implies( x**3 + 3*x**2+ 4*x + 2 ==0, x == -1))

Exercise : Send More Money

    Send

+  More

----------

  Money

를 찾는 문제

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits
send = Sum([10**(3-i) * d for i,d in enumerate([s,e,n,d])]) # convert digits of number to number
more = Sum([10**(3-i) * d for i,d in enumerate([m,o,r,e])])
money = Sum([10**(4-i) * d for i,d in enumerate([m,o,n,e,y])])

print(type(digits))

solver = Solver()
solver.add([s > 0, m > 0]) # first digits are nonzero

# Constrain all digits constrained to be 0 through 9
# FILL IN
solver.add([ And(0 <= d, d <=9) for d in digits]) 

# Constrain all digits to be unique (Hint: Look at the 8-Queens constraints. Anything useful?)
# FILL IN
solver.add(Distinct(digits))

# Constrain send + more == money
# FILL IN
solver.add(send + more == money)

solver.check()
print(solver.check())
solver.model()

# see the value of send
print(solver.model().eval(send))

Proof = Exhaustively Not Finding Counterexamples

solver.check() may return

• sat - "I have found a solution. You may ask for it with solver.model()"
• unknown - This means "I give up". There may be a solution out there somewhere, there may not.
• unsat - "I KNOW there is no solution. I've tried EVERYTHING".

Z3 solver가 주어진 problem을 solve하기 위해 모든 것을 try해보기 때문에 실행 시간이 크다는 단점 존재

본 포스트는 Programming Z3를 읽고 정리한 내용입니다.

링크 : http://theory.stanford.edu/~nikolaj/programmingz3.html

1. Introduction

Z3는 background theories를 해결하기 위한 specialized 알고리즘들을 갖춘 SMT solver

  * SMT(Satisfiability Modulo Theories) : SMT problem은 고전적인 1차 논리로 표현되는 background theories(arithmetic, bit-vectors, arrays 등)의 조합과 관련된 logical formulas에 대한 decision problem

    SMT는 constraint satisfaction problem의 한 형태로 생각할 수 있으므로, constraint programming에 대한 공식화된 접근 방식

  출처 : https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

Tutorial의 목적

  1) Z3의 available한 feature는? 어떤 용도로 설계됐는가?

  2) Z3에서 사용되는 underlying 알고리즘은 무엇인가?

  3) Top of Z3에서 어떻게 어플리케이션을 프로그래밍할 수 있는가?

Z3 System Architecture

Z3는 2가지 interface를 제공

  SMT-LIB2 : 텍스트 파일 또는 pipe로 제공되는 스크립트

  C : C-based API를 통한 호출

Architecture 내 기능

  Formulas : draw from symbols whose meaning are defined by a set of Theories

  Solvers : provide services for deciding satisfiability of formula

  Tactics : provide means for pre-processing simplification and creating sub-goals

  Optimization : services allow users to solve satisfiability modulo objective functions to maximize or minimize values

Sort : Z3에서의 type

In