-
SMT Solver in CTF - z3 vs Boolector
서론 SMT (Satisfiability modulo theories) Solver는 CTF에서 빠질 수 없는 존재입니다. SMT Solver가 무엇인지 구체적으로 설명하기 보다는, 다음 z3py 예시를 보는 것이 더 직관적일 것입니다. (Link) x = Int('x') y = Int('y') s = Solver() print s s.add(x > 10, y == x + 2) print s print "Solving constraints in the solver s ..." print s.check() print "Create a new scope..." s.push() s.add(y < 11) print s print "Solving updated set of constraints..." print...
-
visualizing data
Visualizing data Contents 탐색적 자료 분석 Data to Image 다양한 툴과 차트 마치며 참고자료 탐색적 자료 분석 “the greatest value of picture is when it forces us to notice what we never expected to see” 위는 ‘존 튜키’ 라는 통계학자의 발언으로, 그림의 가장 위대한 가치는 우리가 예상하지 못한 것을 알려줄 때 라고 말하고 있습니다. 탐색적 자료 분석 (Exploratory Data Analysis) 는 ‘존 튜키’ 라는 통계학자가 창안한 자료 분석 방법으로, 시각적 방법으로 주요 특성들을 알아내기 위해,...
-
양자 컴퓨팅 입문 (2) - Grover's Algorithm
Grover’s Algorithm은 정렬되지 않은 데이터베이스에 있는 $N$개의 항목 중 특정한 조건을 만족하는 항목을 $O(\sqrt{N})$에 찾는 알고리즘입니다. 고전 컴퓨팅에서 이 문제를 해결하려면, 간단하지만 느리게 갈 수밖에 없습니다. 전수 조사(brute force)가 유일한 해결책입니다. 당연히 시간 복잡도는 $O(N)$이며, 랜덤하게 셔플해서 순서를 바꾼다 해도 마찬가지입니다. 그리고 이보다 더 나은 시간복잡도로 찾을 수는 없습니다. Grover’s Algorithm은 이 시간복잡도를 $O(\sqrt{N})$으로 낮추는데 성공하였고, 이 시간복잡도가 최적이라는 것이 알려져 있습니다. 또다른 유명한 양자 알고리즘인 Shor’s Algorithm과는 달리 알고리즘 자체가 간단하면서도 심도 있기 때문에...
-
부동소수점에 대한 이해 2
서론 지난 글에서는 부동소수점 자료형이 무엇이고, 이들의 대표적인 표준인 IEEE 754에서 규정한 이진법 16비트 자료형의 세부적인 구조 및 10진수와 서로 변환하는 법 등을 알아보았습니다. 이번 글에서는 지난 글에 이어, 부동소수점 자료형으로 나타낸 수들끼리의 사칙연산을 수행하는 과정을 알아보고, 실제 프로그래밍 언어에서의 수학 라이브러리 함수를 보며 비교적 간단한 연산들을 어떻게 구현하게 되는지에 대해 알아보도록 하겠습니다. 사칙연산 사칙연산과 같은 기본적인 연산은 CPU, 또는 FPU (floating-point unit)에 내장되어 있기 때문에 별도의 라이브러리 없이도 사용이 가능합니다. 이 문단에서는 부동소수점 자료형을...
-
Parametrized inapproximability for Steiner Orientation by Gap Amplification
Parametrized inapproximability for Steiner Orientation by Gap Amplification 이 글에서는 k-STEINER ORIENTATION 문제와 MAX (k, p)-DIRECTED MULTICUT 문제에 대한 FPT hardness result를 소개하는 논문을 정리한다. 먼저, k-STEINER ORIENTATION 문제는 다음과 같이 정의된다: 입력: mixed graph $G$ 와 $k$ 개의 terminal pair $T_G = {(s_1, t_1), (s_2, t_2), \ldots, (s_k, t_k)}$ (mixed graph 는 무방향 간선과 방향성 간선이 둘 다 존재할 수 있는 그래프를 뜻한다.) 출력: $G$ 의 모든 무방향 간선에 방향성을 주어서, $s_i \rightarrow t_i$...