-
[BOJ] 1948 : 임계경로
1948 : 임계경로 풀이 문제를 다르게 생각해보자. 마지막에 도착하는 사람까지 도착을 하는 시간 이라는 문장은 결국 가장 먼 길을 선택하는 사람, 즉 최장 거리를 의미한다. 따라서 이 문제는 최장 거리와, 최장 경로들에 포함되는 모든 간선의 개수를 카운팅해서 출력하면 된다! 풀다보니까 이게 개수를 카운팅 할 때 뒤에서 부터 돌아야 할 것 같은데… 인접행렬이 아니라 백터를 써서 짰단 말이야 코드를 다시 짜긴 귀찮고 그래서 dp 배열을 아예 백트랙킹? 그런 느낌으로 구했다. get_max_len() 함수를 보면 일단 카운팅하기 전에...
-
[BOJ] 11758 : CCW
11758 : CCW 풀이 CCW 알고리즘의 연습문제이다. 식: S = (x2 - x1)(y3 - y1) - (y2 - y1)(x3 - x1) S > 0 : 반시계 방향 S = 0 : 일직선 S < 0 : 시계 방향 코드 #include <stdio.h> int main() { int x1, y1, x2, y2, x3, y3, S, ans = 0; scanf("%d %d %d %d %d %d", &x1, &y1, &x2, &y2, &x3, &y3); S = (x2 - x1) * (y3 -...
-
[BOJ] 머그컵 풀이
문제: https://www.acmicpc.net/contest/view/213 많은 도움 주신 스타트링크께 감사드립니다! A. 준오는 심술쟁이!! BOJ 백준 14437 준오는 심술쟁이!! 제한시간이 1초이기 때문에 단순히 3000 * 3000 * 25 dp를 돌렸다간 시간초과를 받는다. dp[문자열길이][s의 합] 일 때, 문자열 길이를 p, s 합을 q라고 하면 dp[p][q] = k가 0 ~ min(q, 25)일 때의 모든 dp[p-1][q-k]의 합 으로 점화식을 세워 해결할 수 있다. #include <iostream> #include <string> #define min(x, y) ((x)<(y)?(x):(y)) using namespace std; typedef long long ll; const int MOD =...
-
SIGPL Winter School 2017 3일차 정리
SIGPL Winter School 2017 3일차 정리 마지막 날 Type Check Val/Computation.Inductive/Fuction 4가지 룰이랑 Eval만 사용해서 체크함 logical한 step 4개의 룰만 있으면 거의 모든 증명을 할 수 있음 나머지 불가능한 것도 axiom? 추가하면 가능 프로그램 식을 그대로 읽으면 증명하는 거랑 똑같음 ->은 non dependent function forall은 dependent function ==forall, ->, =, P -> false, True, False, /|, |/, exists== 이것만 가지고 모든 set을 만들 수 있음 set이 바로 proposition (coq에서, m zigler set은 set prop는 prop)...
-
SIGPL Winter School 2017 2일차 정리
SIGPL Winter School 2017 2일차 정리 Martin Ziegler Logic 강의 tautology - always true satisfiability - true but not always inconsistency - false emptyset : false -> true 추후에 추가 예정 다시 Coq 강의 istrue = predicate type check 동시에 evaluate P -> Q P ------------ Q 증명 불가능한 함수는 짤 수 없다 1+(n:nat)를 짤 수는 없지만 1+(n:nat)->false 는 가능 evaluation은 증명을 단순화 시키는 것, simplify type checking 할 때 evaluation 해도 안전함 eval termination...
-
SIGPL Winter School 2017 1일차 정리
SIGPL Winter School 2017 1일차 정리 주어가 명시되지 않은 문장은 대부분 Coq가 그렇다는 의미로 받아들이면 대부분 알아들을 수 있을 것이다. Coq는 실제 계산할 때 퍼포먼스 때문에 nat에서 다른 타입으로 계산을 허용한다고 한다. Coq로 짠 코드를 실행하다가 오버플로우 등의 현실적인 에러가 발생할 수 있지만, 애초에 Coq는 Theorem을 증명하는 데에 목적을 두기 때문에 Coq에 대해 문제를 제기할 필요는 없다. 문제 없이 Type Check를 통과하면 안전하다고 보장된다. 이의를 제기할 필요는 없다. Type Check를 통과하면 안전하다는 사실이 이미 다...
-
SIGPL Winter School 2017
SIGPL Winter School 2017 SIGPL Winter School 2017에 참여하여 보고, 듣고, 배우고, 느낀점을 정리한 글입니다. 관련 자료가 여기(슬라이드)와 여기(책) 있으니 필요하신 분은 참고하시기 바랍니다!