Research and Investment

https://leggedrobotics.github.io/SimBenchmark/

본 포스트는 아래 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

WiFi CSI Survey

https://dl.acm.org/doi/abs/10.1145/3310194?casa_token=y1CEIPyF7O8AAAAA:uD8D4J1MrmCrpbocjHaZvUTO9hY6trVPM31G4gHMIgbHqMMX6hQ1YlFQ5UdnejC1KGhfEJCWPw 

5G CSI Estimation

https://ieeexplore.ieee.org/abstract/document/8395053?casa_token=hwTZVTZz9tgAAAAA:zYDuyPkTMgVfezRGo992x1jyYOWVUXtF4CczQfqN6lNxLsOm52or-THRcWzmviyV18XQVkc 

https://ieeexplore.ieee.org/abstract/document/9206084

* Positioning Method 정리

https://www.bitcraze.io/category/lighthouse/

Swarm positioning using lighthouse

https://www.youtube.com/watch?v=K1qmc8K3RUA 

https://www.dynsyslab.org/vision-news/

https://github.com/utiasDSL

실시간 음향 처리를 위한 python module 사용법

참조한 youtube link

https://www.youtube.com/watch?v=AShHJdSIxkY 

PyAudio는 cross-platform 오디오 I/O 라이브러리인 PortAudio에 대한 Python 바인딩을 제공한다.

PyAudio는 Python을 통해 Linux, Windows, Mac OS와 같은 다양한 플랫폼에서 오디오를 쉽게 재생/녹음할 수 있는 기능을 제공한다.

http://people.csail.mit.edu/hubert/pyaudio/

CHUNK : the (arbitrarily chosen) number of frames the (potentially very long) signals are split into in this example

rate : Sampling rate

Channels : number of channels

format : Sampling size and format

input : Specifies whether this is an input stream

output : Specifies whether this is an output stream 

PyAudio와 librosa 같이 설치하기

Anaconda install

conda env 생성 후,

pip install librosa

conda install pyaudio

https://stackoverflow.com/questions/33513522/when-installing-pyaudio-pip-cannot-find-portaudio-h-in-usr-local-include

본 과제에서 요구하는 기능은 풍물/사물놀이 음향 데이터(form 마이크)를 받았을 때 harmonic과 percussive를 나누어 이를 활용하여 드론을 제어하는 것

컴퓨터에 연결된 blue yeti 마이크를 input channel로 audio stream을 받아서 이를 실시간으로 처리함

관련 코드

class AudioHandler(object):


    def __init__(self):
        self.FORMAT = pyaudio.paFloat32
        self.CHANNELS = 1
        self.RATE = 44100
        self.CHUNK = 1024 * 2
        self.p = None
        self.stream = None
        self.WAVE_OUTPUT_FILENAME = "output.wave"
        self.RECORD_SECONDS = 5
        self.frames = []
        self.data = []
        self.arr = np.array([])
        self.recording = True


    def start(self):
        self.p = pyaudio.PyAudio()
        self.stream = self.p.open(format=self.FORMAT,
                                  channels=self.CHANNELS,
                                  rate=self.RATE,
                                  input=True,
                                  output=False,
                                  stream_callback=self.callback,
                                  frames_per_buffer=self.CHUNK)

audio stream을 실시간으로 처리하기 위하여 stream_callback 활용, callback 함수를 call함

    def callback(self, in_data, frame_count, time_info, flag):
        numpy_array = np.frombuffer(in_data, dtype=np.float32)
        y_harmonic, y_percussive = librosa.effects.hpss(numpy_array)
        self.arr = np.append(self.arr,y_percussive)
        print(sys.getsizeof(self.arr))

해당 callback 함수 내 librosa 라이브러리를 활용하여 percussive audio data 구분

librosa.effects.hpss의 input은 numpy array를 받으며, output 또한 numpy array(harmonic / percussive)

np.append는 numpy array의 append

현재는 mainloop에서 특정 key 입력을 받으면 append된 numpy array를 wav 파일로서 출력하는 형태로 개발함

이 때 사용한 라이브러리는 soundfile

sf.write('output_percussive.wav',self.arr,self.RATE)

--> 마이크로부터 실시간으로 들어오는 audio stream을 time window로 구분, 구분된 stream의 평균 audio 세기에 따라 드론이 움직이는 함수 추가 개발 예정

2021.06.30. 추가

Real-time audio segmentation 관련 참조

https://github.com/tyiannak/pyAudioAnalysis

참조 블로그

https://hyongdoc.tistory.com/400?category=884319 

https://dacon.io/competitions/official/235616/codeshare/1305?page=1&dtype=recent 

https://sanghyu.tistory.com/45

사물놀이 주파수 관련 논문

https://www.kci.go.kr/kciportal/ci/sereArticleSearch/ciSereArtiView.kci?sereArticleSearchBean.artiId=ART001315664 

https://www.dbpia.co.kr/Journal/articleDetail?nodeId=NODE00536716 

Matplot for display spectrum

https://stackoverflow.com/questions/19181165/matplotlib-figure-as-a-new-class-attribute-how-to-show-it-later-on-command

https://gist.github.com/sshh12/62c740b329229c7292f2a7b520b0b6f3

MFCC 관련 설명 블로그

* https://brightwon.tistory.com/11

http://keunwoochoi.blogspot.com/2016/03/2.html

https://hyunlee103.tistory.com/45