전체보기

[Model Checking] 과제연구 주제 정리

지도교수님과 여러 가지 이야기를 나눴고, [특정 모델 체킹 언어를 사용해, 특정 시스템의 모델 체킹을 해 보기]를 주제로 과제연구를 진행하기로 했다. 대충 flow는 아래와 같다. 특정한 model checking 언어를 공부한다. 어떤 system을 체킹할 지 확인하기 distributed key-value store (cloud DB) RAFT consensus algorithm 위 2개를 추천받았는데, 모델링하기 위해서는 해당 system의 동작 방식을 알아야 한다. 일단 백엔드로 갈 거니까 분산 DB를 공부하는 게 좋아보인다. safety, fairness 등 어떤 property를 모델링할지 결정하기 Model Checking 언어 공부 model checking tool은 몇 가지가 있는데, ..

[Model Checking] Linear Time Properties

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. model checking의 주된 알고리즘은 transition system과 requirement를 model checker에 넣어, 해당 transition system이 requirement를 만족하는지 여부를 확인하는 방법이다. 그래서 지금까지 transition system을 모델링하는 방법을 살펴봤었고, 지금부터는 requirement를 모델링하는 방법을 살펴볼 것이다. 이 포스트에서는 크게 4가지를 살핀다. state-based and linear t..

23.09.17. 풀었던 문제들

Programmers Lv. 3 베스트앨범, 15분 그냥 풀면 되는 구현 문제. 장르별 재생회수의 순서 장르 내부에서 재생회수의 순서 위 2가지에 대해 정렬되어 있어야 하기 때문에 map을 2개 써야 한다. 그냥 뭐.. map에 genre를 key로 넣어 재생회수 합계와 해당 genre에 속한 노래들의 {재생회수, index}를 저장하면 된다. int len; struct Info{ int play, index; }; struct cmp{ // 조건 1. play가 큰 것. // 조건 2. index가 작은 것. bool operator()(Info &a, Info &b){ if(a.play == b.play) return a.index > b.index; return a.play < b.play; } ..

23.09.14. 풀었던 문제들

프로그래머스 Lv. 2 최댓값과 최솟값, 4분 30초 c++에서 delimiter를 사용해 string을 파싱할 줄 알면 바로 풀리는 문제. iss 쓰고 while getline으로 풀면 된다! string solution(string s) { int min_v = INT_MAX; int max_v = INT_MIN; istringstream iss(s); string buffer; while(getline(iss, buffer, ' ')){ int v; if(buffer[0] == '-'){ v = stoi(buffer.substr(1)); v *= -1; } else{ v = stoi(buffer); } min_v = min(min_v, v); max_v = max(max_v, v); } return..

[Model Checking] Modeling Concurrent System

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 지난 글에서는 Transition System과 Program Graph, 그리고 Program Graph를 Transition System으로 변환하는 방법을 살펴 봤다. 여기서 살폈었던 것들은 닫힌 계로써, 단 하나의 프로그램만 모델링하는 방법이었다. 이제 총 n개의 parallel system P$_1$, P$_2$, ... P$_n$ 이 있을 때를 모델링하고자 한다. 이 때 각 thread의 행동은 아래 3가지 중 하나이다. no communication ..

23.09.12. 풀었던 문제들

Leetcode 1647. Minimum Deletions to Make Character Frequencies Unique, 30분 첫 접근 그냥 주는 대로 풀었다. 일단 각 char이 몇 번 나오는지 알아둬야 하니까 map같은 걸 써야 하는데, 이 문제의 경우 알파벳 소문자만 나오기 때문에 vector(26, 0)을 map처럼 쓰면 된다. 이후, 내림차순으로 정렬한다. 정렬한 후, 만약 겹치는 값이 있는 경우에는 해당 값을 1 줄이고, 해당 문을 다시 반복한다. 이 접근이 문제될 때는, 2 2 2와 같은 예시를 보자. 2 2 2에서 index 1이 2 1 2로 바뀐다. index 1에서 같은 값의 비교는 앞의 값만 보기 때문에 pass. index 2에서 앞의 값만 보기 때문에 pass한다. 문제가 ..

23.09.11. 풀었던 문제들

Leetcode 1282. Group the People Given the Group Size They Belong To, 30분 문제 자체는 빨리 풀었는데, 여러 개선을 한다고 시간이 좀 걸렸다. 첫 번째 접근 최대한 생각나는 대로 구현했다. groupMap은 특정 size를 가지고 있는 모든 group의 정보를 가지고 있다. 때문에 구현은 단순하다. 입력으로 받은 size의 group이 없는 경우 생성한다. 입력으로 받은 size의 group이 있는 경우, 해당 group이 존재하지만 아직 size만큼 차지 못하는 경우 - 해당 group에 현재 인원을 넣어준다. 해당 group이 있고, size만큼 찬 경우 - 새로운 group을 넣어준다. 이렇게 푸니까 runtime 22ms, beats 8.5%..

[Model Checking] Transition System과 Program Graph

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 이 글에서는 model checking에서 사용하는 transition system이 대체 뭔지, 그리고 우리가 사용하는 일반적인 프로그램을 transition system으로 바꾸는 방법을 살펴본다. Transition System transition system은 directed graph로 나타낸다. 이 때 graph의 node는 state를, edge는 transition을 의미한다. Definition. Transition System transition..

23.09.10. 풀었던 문제들

오늘은 프로그래머스 데브코스 PCCP를 풀었다. 총 4문제였는데, 1번, 2번, 3번을 풀었다. 4번은 시간이 없더라. 구현이 너무 복잡했다. 4번 문제를 손을 대야 lv4를 받고, 올솔해야 lv5를 받는다... 음... lv5는 기대 안했지만, lv4는 받을 줄 알았는데. 아쉽다.

23.09.09. 풀었던 문제들

Programmers PCCP 모의고사 #1 외톨이 알파벳, 5분 프로그래머스 짝지어 제거하기를 풀어봤다면 바로 이어져 나오는 중복 char를 쉽게 줄일 수 있다. stack을 쓰든, string의 뒤에 중복을 빼고 붙여넣든. 이 방법을 사용하면 중복을 제거할 수 있고, 그러면 map으로 count만 하면 된다. 간단한 손풀기 문제. #include #include #include #include #include using namespace std; string solution(string str) { stack stk; for(char c : str){ if(!stk.empty() && stk.top() == c) continue; stk.push(c); } map m; while(!stk.empty(..

23.09.08. 풀었던 문제들

Programmers 자물쇠와 열쇠, 53분 자물쇠에 열쇠를 넣어서 맞는지 보면 되는 문제. 문제 접근 자체는, N과 M이 20으로 매우 작아서 brute-force로 다 돌릴 수 있었고, 결국 구현 문제였다. 열쇠를 특정 크기로 자르는 것은 매우 귀찮고 힘들기 때문에, 그렇게 하는 것보다는 아래와 같이 for문으로 돌리는 것이 편하다. 총 N + 2M - 2 크기의 배열을 만들고, 가운데에 자물쇠를 배치한다. 자물쇠에 해당하는 좌표는 [M-1, M-1]부터 [N+M-2, N+M-2]까지다. 이후 열쇠를 모든 위치에 두고, 자물쇠를 해제할 수 있는지 본다. 열쇠는 [0, 0]부터 [N+M-1, N+M-1]까지 가능하다. 열쇠 위치를 옮겨가면서, 자물쇠에 해당하는 모든 좌표들의 숫자가 1이면 OK이다. #..

23.09.07. 복학 후 계획 - 끝!

당분간 할 일들 Naver2Tistory 리팩토링 과정/선택/결과 블로그에 포스팅하기 - 23.09.05. 끝! large query vs small 2 query 실험하기 - 23.09.06. 끝! 위 2개 끝나면 포폴 다듬기 - 전역/복학한 내용 + resume만 고치고 업로드하면 됨. - 23.09.07. 끝! Naver2Tistory 부분 다듬기 + 포스팅 링크도 달기 - 끝! 다 끝나면 plan에 있는 포스팅 싹 읽으면서 정리하고, 당분간 또 할 일들 정리하기. - 23.09.07. 끝! 이후에 할 일들 하반기 채용 기업들 지원서 쓰기 - 끝! 지원서 쓴 이후 코테 공부하기 (하반기 공채가 시작했으니 다시 달려보자.) - 끝! 아마 프로그래머스 부계정 판 거로 풀어갈 것 같다. lv2 + lv3..

[N2T] 리팩토링 기록

리팩토링 하게 된 계기 개발 동기 Naver2Tistory는 사실 내가 사용하기 위해 만든 프로그램이다. 2022년 10월쯤에 개발 블로그를 네이버에서 티스토리로 옮기기로 결정하면서 안에 있는 포스팅들을 다 가져오고 싶었는데, 그동안 작성했던 포스팅이 약 300개 가량 되다 보니 수작업으로 일일히 옮길 수 없었다. 이를 위해 Naver2Tistory를 당시 내가 구현할 수 있는 수준으로 만들었었다. 만들다 보니 블로그를 나만 옮기는 게 아니니까 다른 사람들도 쓸 수 있겠다 싶어 리드미도 열심히 꾸몄고 형식을 맞춰서 오픈소스로 배포도 했다. 기존 Naver2Tistory의 문제점 이후에 Clean Code, Clean Architecture 같은 개발 서적을 읽고, 객체지향의 5대 원칙을 공부하면서 내가 ..

23.08.21. 풀었던 문제들 복기

Leetcode 459. Repeated Substring Pattern, 15분 주어진 대로 구현만 하면 되는 문제. 일단 substring으로 원 string을 표시하기 위해서는 substring의 길이가 s의 약수여야 한다. 만약 그렇다면, 해당 substring을 q개(s.length()/substr.length())만큼 만들어서 전체를 살펴보면 된다. // Runtime 19 ms Beats 64.17% // Memory 15.4 MB Beats 38.41% class Solution { public: bool repeatedSubstringPattern(string s) { int len = s.length(); for(int i = 0; i

23.08.17. 풀었던 문제들 복기

Leetcode 542. 01 Matrix, 20분 0과 1만 있는 matrix에서 0으로부터 거리를 리턴하면 되는 문제. 나는 BFS를 사용했다. 모든 0지점부터 BFS 탐색을 시작한다. 단, 갱신할 수 없는 위치라면(다른 0으로부터 더 가깝다면) 그곳은 탐색하지 않는다. 하나의 최적화를 추가하는데, 0에서 BFS를 각각 수행하는 것이 아니라(그렇게 하면 BFS가 10000번 수행될 수도 있다.) 모든 0을 queue에 넣고 한 칸씩 BFS 해 나가는 것이다. 그러면 0에 인접한 칸은 그 개수만큼 방문하지만, 다음 갱신할 칸은 1번씩만 방문한다. 그러면 worst case 최대 1만번 겹치는 탐색이 존재하고, 모든 칸을 1만번씩 방문하게 되므로 시간 내에 충분히 풀 수 있다. // Runtime 62 ..

23.08.16. 풀었던 문제들 복기

9646. 다이어그램과 태블로, 2시간 딱 보면 backtracking + purning으로 푸는 문제. 일단 아래로 내릴 수 있으면 내리고, 너무 많이 내려간 경우 다음 col로 넘어가는 형식으로 구현했다. 그러면 backtracking의 종료조건은 마지막 col을 탐색하고, 다음 칸을 탐색할 때 answer++를 해 주면 된다. 다음으로, backtracking 과정은 위/왼쪽에 있는 값을 보고 조건을 맞춘다. 여기서 하나 purning을 하는데, 아래 칸으로 내릴 수 있으면 바로 내리고, 그렇지 않으면 바로 다음 col을 탐색한다. 만약 이 과정을 recurse()에서 if문으로 걸면 call stack이 1번씩 더 쌓인다. worst case 모든 경우에 하나씩 더 쌓이게 되므로 이 과정을 여기로..

23.08.15. 풀었던 문제들 복기

Leetcode 86. Partition List, 25분 linked list에서 entry를 옮기는 방법을 알고 있으면 쉽게 풀리는 문제. 단, doubly linked list가 아니므로 head에 있는 값을 옮기기 위해 dummy head를 만들어야 했다. 접근 1. x보다 작은 것들만 옮기고, 기존 것들은 유지하는 방법. // Runtime 5 ms Beats 52.61% // Memory 10.3 MB Beats 21.22% /* x보다 작은 entry들은 다른 linked list로 옮기고, x보다 큰 entry들은 그대로 둠. - start pointer를 하나 두고, x보다 작은 것은 다 start로 옮김. x 이상인 것은 순서를 유지한 채로 head에 있을 것임. 이후 start와 원래..

23.08.11. 풀었던 문제들 복기

Leetcode 518. Coin Change II, 25분 백준 2293. 동전 1과 동일한 문제. 일단 2차원 dp로 푼다고 하면, dp[i][j] : coin i까지 봤을 때 j원을 표기할 수 있는 개수로 두자. i번째 coin을 안쓰는 경우 - dp[i][j] = dp[i-1][j] i번째 coin을 쓰는 경우 - dp[i][j] = dp[i][j-coin[i-1]] 위와 같이 되므로 이 점화식을 그대로 적용하기만 하면 된다. space complexity를 조금 개선할 수 있는데, dp[i][j] = dp[i-1][j]는 항상 고정이므로 dp를 1차원 배열로 만들수도 있다. // time O(nm), space O(nm) // Runtime 43 ms Beats 39.13% // Memory 1..

23.08.10. 풀었던 문제들 복기

Leetcode 53. Maximum Subarray, 25분 백준 1912 ,최대 연속 부분수열 합을 구하는 문제와 같은 문제. dp로 쉽게 풀 수 있다. 링크에 풀 수 있는 4가지 방법이 있다. // Runtime 76 ms Beats 96.56% // Memory 67.7 MB Beats 32.89% class Solution { public: int maxSubArray(vector& nums) { int n = nums.size(); int answer = -1e9, sum = 0; for(int i = 0; i>T; int x, y; for(int i = 0; i>x>>y; V[{x, y}] = 0; } queue q; // 좌표, dist q.push({0, 0, 0}); while(!q.e..

23.08.09. 풀었던 문제들 복기

BOJ 2224. 명제 증명, 30분 floyd warshall로 푸는 문제. floyd-warshall은 예전에 포스팅 한 적이 있다. floyd warshall의 특징은 모든 vertex에서 모든 vertex의 path weight를 최단거리로 만들고, 이를 위해 kij 순서로 for loop를 돌린다. typedef pair pcc; ////////////////////// write your code below // 모든 vertex에서 모든 vertex로의 path 여부를 알아야 하므로, floyd-warshall // directed임. int V = 52; int char2int(char c){ if(isupper(c)) return c - 'A'; if(islower(c)) return c..

23.08.08. 풀었던 문제들 복기

BOJ 7512. 연속하는 소수의 합 어떤 n1, n2, ... n$_m$이 주어졌을 때 연속된 n$_i$개의 소수의 합으로 나타낼 수 있는 가장 작은 소수를 찾는 문제. 처음에는 n개의 연속된 소수의 합을 빠르게 계산하기 위해 prefix sum을 사용했고, 메모리가 터졌다. 대체 왜..? 계산해 보면 그렇게 큰 값도 아닌데. ////////////////////// write your code below // 1000000000000 int INF = 1e7+1; //int INF = 312; vector primes; vector psum; void getPrime(){ vector isPrime(INF+1, true); isPrime[0] = isPrime[1] = false; for(int i ..

23.08.07. 풀었던 문제들 복기

Leetcode 74. Search a 2D Matrix, 25분 matrix가 정렬되어 있으므로 target이 있는 row를 찾고, 이후 col을 찾으면 된다. row를 찾을 때 binary search를 하고, col을 찾을 때 binary search를 하면 O(logm + logn)으로 해결할 수 있다. 이외에도, 모범답안은 전체를 하나의 array로 보고, index / m을 row index, index / n을 col index로 보고 O(log(m*n))만에 해결하는 방법도 있다. // Runtime 3 ms Beats 82.89% // Memory 9.6 MB Beats 19.73% class Solution { public: bool searchMatrix(vector& matrix, ..

23.08.05. 풀었던 문제들 복기

Leetcode 95. Unique Binary Search Trees II unique한 binary tree를 어떻게 만들지 ? ... 라고 생각하면. dp(start, end) = for all i in [start, end], dp[start, i-1] + dp[i+1, end] 로 풀면 된다. 이게 무슨 말이냐? start ~ end 사이에 있는 어떤 i를 root로 두고, 그 start ~ i-1은 왼쪽 subtree에, i+1 ~ right는 오른쪽 subtree에 넣는 DP라는 말이다. 그러면, left subtree와 right subtree의 cartesian product하면 모든 가능한 결과가 나온다. // Runtime 16 ms Beats 75.53% // Memory 16.1 ..

23.08.04. 풀었던 문제들 복기

Leetcode 139. Word Break, 1시간 첫 접근 처음에는 일단 brute-force로 접근했다. for문으로는 돌릴 수 없어서, dfs를 사용한 backtracking으로 접근했다. 코드는 뭐.. 간단하다. DFS(i)는 i부터 s.length()까지 만들 수 있는지 여부이다. 내부적인 구현은, i부터 모든 wordDict를 순회하면서 끝까지 도달할 수 있으면 true, 아니면 false인 식으로 class Solution { public: bool DFS(int i, string& s, vector& wordDict){ if(i == s.length()) return true; for(string word : wordDict){ int wordlen = word.length(); if(s..

23.08.02. 풀었던 문제들 복기

Leetcode 46. Permutations, 7분 어제와 마찬가지로 순열만 하면 되는 backtracking 문제. 마찬가지로 같은 포스팅에 작성해 두었다. 리트코드는 한 번 주제가 나오면 계속 그걸로 하는 느낌이라.. 뭔가 아쉽다. daily challenge가 분류 3개정도 나눠서 랜덤으로 하면 좋을 것 같다. // Runtime 3 ms Beats 67.29% // Memory 8 MB Beats 29.89% class Solution { public: vector answer; vector nums, result; vector isUsed; int N; void permutation(int cur_depth, int max_depth){ if(cur_depth == max_depth){ ans..

23.08.01. 풀었던 문제들 복기

Leetcode 77. Combinations, 8분 예전에 DFS로 순열/조합/중복순열/중복조합 코드를 썼었다. 코드야 그대로 쓰면 된다. 예전에 짰던 게 제일 깔끔하게 짜였던 걸로 기억했는데, 이번에 안 보고 짠 것도 비슷하게 짜진다. 다행이군. // Runtime 10 ms Beats 93.32% // Memory 9.9 MB Beats 56.99% class Solution { public: vector nums; vector answer; void combination(int cur_d, int max_d, int prev_idx, vector& result){ if(cur_d == max_d){ answer.push_back(result); return; } for(int i = prev_id..

23.07.31. 풀었던 문제들 복기

백준 2252. 줄 세우기 topological sort 문제. 처음에는 어떻게 풀지.. 생각했는데, 문제가 topological sort임을 깨달았다. 예전에 포스팅도 했었는데... 일단 topological sort의 핵심은, incoming edge가 0개인 vertex에서 연결된 모든 edge를 삭제하는 과정을 n번 반복하면 된다. 만약 n번 반복이 끝나기 전에 incoming edge가 0개인 vertex가 없다면, 어딘가에 cycle이 있다는 것이다. 또, edge를 직접 지우기에는 낭비가 심하니 incoming edge 개수 정보를 저장하고, edge를 삭제할 때 여기서 빼면 된다. vector edges; // edges[i] : src가 i인 edge array vector incomin..

[Network] 하향식 접근 네트워크 - 6. Mobile Networks

이 글은 이화여자대학교 이미정 교수님의 2014년 2학기 컴퓨터 네트워크 강의를 기반으로 재구성한 것입니다. 삽화는 링크를 출처로, 저작권은 J.F Kurose and K.W. Ross에게 있다는 것을 밝힙니다. 이 글에서는 다음과 같은 내용들을 살펴본다. wireless basics multiple access protocol CSMA/CA CDMA mobility - indirect routing wireless vs mobile 둘은 비슷하지만 엄밀하게는 다르다. wireless는 link가 wireless하게 연결된 경우를 말하고, mobile은 사용자가 움직이는 것을 의미한다. Wireless Basics Wireless Network Element wireless network는 아래 3개의 ..

[Network] 하향식 접근 네트워크 - 5. Link Layer

이 글은 이화여자대학교 이미정 교수님의 2014년 2학기 컴퓨터 네트워크 강의를 기반으로 재구성한 것입니다. 삽화는 링크를 출처로, 저작권은 J.F Kurose and K.W. Ross에게 있다는 것을 밝힙니다. link layer에서는 다음과 같은 내용들을 살펴본다. MAC addressing ARP web request senario MAC address network layer에 있는 IP까지는 32bit의 IP address를 사용해 destination을 표현했고, 이 정보를 사용해 forwarding table에 정보를 작성했다. network layer 아래에 있는 link layer는 datagram을 frame으로 encapsulate한다. internet의 경우 MAC layer가 en..

[Network] 하향식 접근 네트워크 - 4. Network Layer - (6) Broadcast, Multicast

이 글은 이화여자대학교 이미정 교수님의 2014년 2학기 컴퓨터 네트워크 강의를 기반으로 재구성한 것입니다. 삽화는 링크를 출처로, 저작권은 J.F Kurose and K.W. Ross에게 있다는 것을 밝힙니다. network layer principles virtual circuit, datagram network router의 내부 IP datagram format IPv4 addressing ICMP IPv6 routing algorithm link state distance vector hierarchical routing routing in the internet RIP OSPF BGP broadcast, multicast broadcast와 multicast는 간단하게 개념만 짚고 넘어간다. ..