글쓴이 ·0개의 댓글

SMT solvers support stack-based incremental solving, but it only supports going back and forth at the end of the history chain and needs manual creation of checkpoints. I want an SMT solver with continuous learning that works out-of-the-box. If a solver previously checked conditions A and B independently, that information could be used later to make checking for A && B faster. I believe a solver with this optimization will significantly improve the performance of many research projects that rely on satisfiability checking.

To be more specific, symbolic execution engines will greatly benefit from this optimization. State-of-the-art symbolic execution engines are caching terms on the execution side to reduce the number of calls to SMT solvers. This optimization surely helps, but it is still pretty limited. Doing similar optimizations on the solver side is more promising to me since solvers have a better context to utilize that information. There is a report that nonoptimized stack-based incremental solving already gives 5x speedup, and I believe we can achieve greater speedup with an optimization based on continuous learning.

글쓴이 ·0개의 댓글

오랜만의 블로그 포스트가 알고리즘 대회 후기가 될 것이라고 예상하지 못했는데, 마지막 글이 올라온지도 꽤 됐고 이번 대회에서 하고 싶은 얘기도 있어서 포스팅을 하기로 했다. 현재 나는 작년 ICPC 이후로 공식적으로는 경쟁 프로그래밍을 은퇴한 상태다. 평소에 공부하고 시간 쓰는건 완전히 멈췄고, 대신 거기 쓰던 시간을 워게임 등 해킹 문제를 풀거나 졸업 후 진로 준비에 쓰고 있다. 이렇게 말하니까 알고리즘 공부에 계속 시간을 많이 쓰고 노력했던 것 같지만 은퇴 선언 이전에도 실질적으로 손을 놓은지는 꽤 됐다. 지금은 티셔츠나 상금 등 부상 주는 대회를 가끔 부담 없이 나가는 걸 목표로 하고 있다.

원래 이번 코드잼은 Rust로 알고리즘 라이브러리를 짜고 그걸 써서 대회를 치고, 대회와 대회 사이에 라이브러리를 보강한 뒤 대회 이후 프로젝트를 다듬어서 공개한다는 원대한 계획과 함께하고 있었다. 하지만 코드잼 플랫폼이 바뀌고 Rust가 지원 언어 목록에 없어서 라이브러리 작성에 대한 관심이 급격하게 식었고, 다익스트라 알고리즘 정도만 겨우 구현된 Rust 알고리즘 라이브러리는 지금까지 존재했던 나만 알고 있다가 비트의 저편으로 사라졌던 많은 개인 프로젝트와 마찬가지로 GitHub 개인 저장소에 조금 더 머무르다 영영 사라질 예정이다. Cargo 배포용으로 이름도 지어줬는데 불쌍한 친구…

올해 코드잼 연습 세션을 치고 나서 느꼈던 건 생각하는 능력 자체는 예상보다 덜 줄었고, 전통적인 테크닉을 떠올리거나 코드를 빠르게 짜는 능력은 예상보다 많이 줄었다는 거였다. 여기서 “생각하는 능력”은 연습 세션 3번 Steed 2 Cruise Control에서 여러 속도로 달리는 말들 사이의 불변조건을 구하는 능력을 말하고 “전통적인 테크닉”은 R1A 3번 Edgy Baking을 보고 냅색이니까 DP로 풀면 뚝딱 할 수 있겠다는 걸 떠올리는 능력을 말한다. 연습 세션부터 이번 R1A까지 예전에 비해 같은 코드를 짜는데 시간이 훨씬 오래 걸린다는게 느껴졌다.

이번 대회를 치면서 좀 놀랐던 점은 대회 중 오랜만에 초심을 되찾은 기분을 느꼈던 것이다. 내 풀이에서 놓친 점을 찾았을 때 예전 같았으면 쉬운 문제에서 실수했다고 자책했겠지만 이번 대회에서는 웬일로 풀이의 빠진 구멍을 채워 나가는 느낌이 즐겁게 느껴졌다. 알고리즘 대회에서 어려운 문제에 도전하는 지적 만족감을 느낀 적은 많았지만, 문제를 푸는 것이 아니라 시간 제한을 두고 대회를 치는 것을 즐겁다고 생각해 본지는 꽤 오래됐다. 평소에 연습을 많이 안 하니 예전만큼 잘하지 못하는 건 당연하다고 생각하면서도 무의식 속에서는 그래도 내가 경력이 얼마인데 못해도 어느 정도는 해야 한다는 부담을 느끼고 있었다고 생각한다. 나도 내가 무의식에서 어떤 생각을 하는지 완전히 모르지만, 공식적으로 은퇴했다고 선언했던게 그런 부담을 낮춰준 게 아닌가 추측하고 있다. 바뀐 플랫폼에서 스코어보드가 문제 페이지에 보이지 않는 것도 도움이 됐다.

원래 대회 후기는 문제 풀이도 함께 올리는게 전통이므로 간단한 풀이도 함께 첨부한다.

  • A: 전체 초콜릿 개수를 세고, \text{(number of H piece)}\times \text{(number of V piece)}로 나누어 떨어지는지 확인한다. 가로 분할선과 세로 분할선의 위치는 초콜릿 개수를 통해 독립적으로 판단 가능하며, 분할선들의 위치가 정해지면 분할된 각 칸에 초콜릿이 균등하게 들어가 있는지 확인한다.
  • B: 계산이 특정 시간 안에 끝날 수 있는지를 판단하는 판별 함수를 작성하고 파라메트릭 바이너리 서치를 수행한다. 판별 함수는 각 계산원이 그 시간까지 처리 가능한 비트의 수를 계산한 뒤 정렬해 큰 순서대로 R개를 뽑아 B 이상이면 처리 가능한 것이다.
  • C: 0-1 냅색. 2 \cdot w_i h_i를 미리 P에서 빼고, 물건의 크기가 min(w, h) 점수는 \sqrt{w^2 + h^2}인 냅색을 수행한다.

글쓴이 ·댓글 한 개

마지막으로 뻘글을 쓴지 꽤 된 것 같은데 새벽이고 우울하고 과제하기 싫어서 오랜만에 뻘글을 또 써야겠다.

공대생으로 살면서 의문을 가졌던 것 중 하나가 공대생에 대한 차별적 발언에 제제를 가하는 사람이 거의 없다는 사실이다. 우리 학교에는 문화콜로퀴움이라는 과목이 있다. 외부에서 연사를 초청해 강연 또는 공연을 듣고 보고서를 쓰는 유닛 과목인데, 지금까지 했던 모든 강연과 공연에서 공대생에 대한 고정관념을 언급하지 않은 사람이 없었다. 예를 들자면 다음과 같다. “공대생이라 안경 쓴 분들이 많은데 공교롭게도 우리 팀 멤버가 나 빼고 전부 안경을 썼다”, “공대생이라 문학에는 관심이 없을 줄 알았는데 생각보다 호응이 좋다”, “공대라 그런지 역시 관객에 남성분들이 많다”. 전부 틀린 말은 아니다. 실제로 안경 쓴 사람 많고, 인문학 싫어하는 사람들 쉽게 찾을 수 있고, 성비도 치우쳐 있다. 그렇지만 그게 통계적 사실을 나타내는 문장으로 사용되는 경우와, 공대생들을 일반화하기 위해 사용되는 경우는 의미가 다르다.

이런 말을 들었을 때 기분이 나쁘다고 표현하면 지나치게 강한 표현인 것 같고, 미묘한 불편함이 있다. 하지만 공대생에 대한 편견을 갖지 말라고 이야기하기도 애매한 부분이 있는게, 공대생에 대한 편견을 유머코드로 하는 공대생 개그의 주 생산자와 소비자가 공대생들이다. 자기들끼리 하는 공대생 개그가 일반 대중으로 퍼지면서 그 뒤에 숨어 있는 공대생에 대한 고정관념도 같이 무의식 속에 새겨지는 게 아닐까? 공대생 유우머를 하지 말자고 주장하고 싶은건 아닌데 그걸 외부 사람들한테 들으니까 거부감이 생기는 것 같다. 까도 우리가 깐다!

공대에 대한 고정관념이 공대생들의 미묘한 불편함보다 더 심각한 문제인 이유는, 대중이 가지는 고정관념은 그 고정관념을 강화하는 방향으로 작용하기 때문이다. 예전에 ‘컴퓨터 공학과에는 왜 여자가 적은가’를 분석한 기사를 본 적이 있다. 여성들이 학과를 선택할 때 자기가 생각하는 컴퓨터 공학도의 이미지-너드, 밤샘, 천재적 번뜩임, 기계같은 반응-와 자신을 비교하고는 자신이 컴퓨터 공학에 어울리지 않는다고 판단하고 다른 과를 선택한다는 것이다. 실제로 입학한 학생들의 성적에서 성별에 따른 차이는 관찰되지 않았음에도 불구하고 말이다. 수학과에는 여성이 적고 영문과에는 많은 것도 같은 이유라고 한다. 그래서 공대생에 대한 고정관념이 퍼지면 퍼질수록 공대생들의 다양성은 줄어들고 사람들이 ‘공대생’하면 떠올리는 이미지로 일반화 되어 갈 것 같아 걱정이 된다.

그래서 이 문제를 해결하기 위해서는 무엇을 해야 할까? 내가 이것까지 명쾌하게 제시할 수 있었으면 첫 문장에 뻘글이라는 용어를 쓰지 않았을 것이다. 고정관념을 해소하는 문제는 굉장히 어려운 문제 중 하나다. 아직까지도 자신의 고정관념을 근거로 인종차별, 성차별 발언을 하는 사람이 한참 남아 있는데, 공대생에 대한 고정관념을 고쳐야 한다고 강력하게 주장하기에는 중요도가 떨어지는 것 같아 어쩐지 부끄럽다. 이런 문제들을 해결하려면 결국 대중의 무의식 속에 숨어 있는 고정관념을 수정해야 하는데 다행히도 대중에 대한 효과적인 세뇌 수단이 발견되지 않았으니 꾸준한 문제제기가 해답이 아닐까? 뻘글로 시작했지만 쓰다보니 공대생에 대한 고정관념에 문제제기를 하는 글이 되어 버렸다. 그러니까 공대생 너무 놀리지 마시고, 이번 기회에 공대생에 대한 고정관념을 다시 한 번 되돌아보는 계기가 됐으면 좋겠습니다.

끝

글쓴이 ·댓글 한 개

1.

6개월 정도의 단기유학이 끝났다. 여름학기에 SBU에 있을 때는 주변에 놀 것도 먹을 것도 없는데 수업도 쉬워서 시간을 주체할 수 없는 기분이었는데, UCB는 주변에 먹을 것도 많고 수업 로드도 적절하고 방도 잘 얻어 걸려서 즐거운 생활을 했다. 한국에 비하면 많이 놀았다. Machine Structures랑 Linear Algebra를 제일 열심히 했고, Introduction to Neuroscience를 그 다음으로 열심히 했다. 수업들 질이 정말 좋았는데 괜히 명문대 소리 듣는게 아니구나 싶었다.

선형대수는 포스텍의 선형대수가 모든 학생이 다 듣는 기초필수과목인 것에 비해, 학점변환이 인정되는 버클리의 선형대수학 과목은 수학과 Upper Division 과목이었다. 처음에는 생소한 개념들이 많이 나와서 헤맸지만 그런 개념들을 하나 둘 이해하고 증명하는 과정이 정말 재미있었다. 포스텍에서 미적분학 들으면서도 느꼈던 거지만 나한테 프로그래밍이 워낙 잘 맞아서 그렇지 수학을 전공했어도 재밌게 했을 것 같다.

2.

학기가 끝나고 나서 내 룸메이트는 바로 한국으로 돌아갔고, 나는 좀 더 미국을 보고 가려고 미리 비행기표를 일주일 쯤 연장해 두었다. 하지만 게으른 나머지 계획을 세우지 않고 있다가, 학과 친구들의 LA 여행에 꼽사리로 놀러가게 되었다. 도시 구경도 하고 테마파크도 가고 아쿠아리움도 갔다. 내가 집을 좋아하긴 하지만 나가서 노는 것도 좋아하기는 한다. 하지만 물고기가 물 밖에 너무 오래 있으면 죽듯이, 집 밖에 너무 오래 있었는지 날짜가 지날수록 컨디션이 조금씩 나빠졌다. 다행히 많이 안 좋아지기 전에 버클리로 돌아가고 있다.

LA에서는 에어비엔비로 숙박했다. 집 주변에 한인타운이 있었는데, 화폐 단위가 달러라는 점을 빼면 한국과 다를 게 없었다. 한국인 주인이 한국어 간판을 달고 운영하는 식당, PC방, 노래방, 당구장, 카페 등이 있었다. LA 도착한 첫날에는 부대찌개랑 곱창전골을 먹으러 갔는데 반찬으로 나온 깍두기가 정말 맛있었다. 식당 사장님께서 공기밥하고 콜라도 서비스로 주시고 혹시 궁금한 거 있으면 전화하라고 명함도 주셨다. 한국에 있을 때였다면 이런 잘 모르는 사람의 과도한 관심은 별로 안 좋아했겠지만, 오랜만에 겪으니 이런 게 한국인의 장점인가 하는 생각이 들었다. 주변에 맛있어 보이는 한식집이 많았지만 어차피 한국 가면 많이 먹을 것들이란 생각에 많이 가지는 않기로 친구들과 합의를 보았다.

3.

미국은 해가 지고 나면 정말 무섭다. 다행히 우리 과 사람들이 직접 겪은 사례는 없었지만 질의응답 사이트에 노트북이 털렸는데 과제 제출마감을 연장해 줄 수 있냐고 물어보는 사람도 보았고, 친구의 룸메이트가 총 든 2인조 노상강도를 만나 가지고 있던 물건을 전부 털린 얘기도 한 다리 건너서 들었다. LA에서 버클리로 돌아갈 때는 새벽 급행 버스를 타는 일정이었는데, 메트로 첫 차가 막 다닐 때 쯤의 시간이었지만 멀쩡하게 역까지 갈 자신이 없어서 우버를 처음으로 타 봤다.

4.

우버 기사 분은 안타깝게도 내가 별로 좋아하지 않는 말이 많은 스타일이었다. 처음에는 내가 밤에 검은 옷을 입고 있어서 나를 못 봤다는 이야기부터 시작해서, 자기 애들이 머리를 분홍색이랑 초록색으로 염색했고 곧 피어싱을 할 거라는데 내기해도 좋다는 이야기, 할리우드에서 픽업해서 다운타운까지 내려다 주는데 한 시간은 걸렸는데 3 달러도 못 벌었다는 이야기를 했다.

나는 적당히 심드렁하게 맞장구를 쳐 주면서 버클리에 살다가 크리스마스 시즌에 LA로 놀러왔다는 얘기를 했다. 그랬더니 우버 기사 분이 나를 royalty라고 부르면서 신세한탄을 하셨다. Royalty들은 자식을 키우면서 “우리 애들은 스페인어를 공부했으면 좋겠어요.” 같은 얘기를 하지만, 자기 같은 사람들은 자식들이 변호사나 의사가 됐으면 정말 좋을 것 같다는 생각을 한다는 얘기를 하셨다. 처음에는 나를 공격하는 것 같아서 약간 당황스러웠는데 지금 생각해보면 그냥 자기 같은 사람들이 있다는걸 알아줬으면 했던 게 아닐까 싶다. 재미있게 읽었던 단편 카툰 ‘특권에 대한 짧은 이야기(On a Plate)’도 비슷한 내용을 다루고 있는데 혹시 시간 남으면 보길 바란다.

자본주의 사회에서 부의 불평등과 기울어진 운동장 문제는 아직도 뜨거운 감자인 채로 남아 있는데, 그렇기 때문에 이번 미국 대선에서 버니 샌더스 아재가 이겨서 미국이 사회주의 지상락원이 될 지 도날드 트럼프 아재가 이겨서 매드맥스 불지옥미국이 될 지 결과가 무척 기다려진다.

5.

터미널에 도착해서 의식의 흐름은 헬조센 담론으로 이어졌다. 나는 헬조센이라는 단어를 사용하는걸 꺼리는 편이다. 진지충, 선비 같은 단어들이 진지한 문제제기를 들을 가치가 없는 헛소리로 평가절하 해버리는 것처럼, 헬조센이라는 단어는 함께 풀어 나가야 할 사회문제들을 한국이 미개해서 어쩔 수 없이 생기는 문제들로 포장하기 때문이다.

이런 생각을 하며 페이스북 스크롤을 내리고 있는데 크로아티아에서 최초의 여성 대통령이 당선되었다는 기사가 보였다. 기사 썸네일에는 그 대통령이 비키니를 입고 해변에서 여가를 즐기는 사진이 있었고, 댓글에는 “ㅅㅂ 나보다 가슴 크네”가 3천개 가량의 좋아요를 받아 맨 위에 걸려 있었다. 기사 본문에는 미모의 대통령이 당선되어 SNS에서 화제가 되고 있다는 ‘최근 네티즌들의 반응’만이 자리를 차지하고 있었고, 어디에서도 그 사람이 어떤 사람인지를 알려주려는 노력의 흔적을 찾을 수 없었다. 그저 모두가 그 사람의 아름다운 외견을 소비하고 있을 뿐이었다. 비단 이 게시글 뿐 아니라 약자에 대한 폭력과 위협을 상남자라고 칭송하거나, 혐오표현을 할 수 있는 표현의 자유를 달라는 이해할 수 없는 주장에 공감을 표하는 사람들을 찾기란 그리 어렵지 않다.

눈에 보이는 가치만을 좇는 가벼움과 자신의 가치로 남을 멋대로 재단하는 행위는 어느새 솔직함과 쿨함이 되었다. 열심히 마음속에서 ‘대한민국이 고칠 점은 많아도 헬조센 까지는 아니지 않을까’ 하면서 실드를 쳐 주고 있었는데 이래서 헬조센 헬조센 하나 싶더라. 요새 생각을 하지 않고 살아가는 사람이 너무 많다고 느끼는 경우가 늘어났지만 어쩌면 이것도 그냥 내 중2병에 지나지 않을지도 모른다.

나는 게임을 할 때도 애니메이션을 볼 때도 음식을 먹을 때도 망작 헌터를 자처하며 남들이 망작이라고 평하는 걸 굳이 직접 체험해보면서 “음, 정말 듣던대로 망작이지만 이러저러한 점들은 나쁘지 않았어!” 같은 평을 즐기는 편인데, 이게 대한민국에도 적용되는건 아닐까 잠깐 생각했다. 최근에 했던 망작 헌팅으로는 트리오브세이비어와 코코넛 워터 ZICO가 있다. 다음 체험대상으로는 롯데리아의 모짜렐라 인 더 버거를 노리고 있다.

6.

사회 얘기에서 다시 좀 더 개인적인 얘기로 돌아와 보자. 터미널에서 읽었던 연애를 고양이 키우기에 비유한 대나무숲 게시글도 꽤 재미있었다. 그 글은 모든 사람이 고양이를 좋아하는 건 아니라는 얘기에서 시작해서, 고양이를 좋아하지만 고양이에게 쏟아야 하는 비용과 관심을 생각하면 키우지 않는게 좋을 것이라는 판단을 내린 사람에게 “왜 고양이를 좋아하면서 키우지 않느냐”고 묻지는 않는다는 이야기로 이어진다. 그리고 자기는 연애를 못 하는게 아니라 안 하는 거라고 주장하며 글이 끝난다. 물론 게시글 하단에는 울지 말고 천천히 얘기해 보라는 댓글이 달려 있었지만…

나는 안 하는게 아니라 못 하는 거긴 하지만 이 글을 쓴 사람과 연애에 관한 입장은 상당히 비슷하다고 느꼈다. 연애도 좋지만 나는 공부하는 것도 좋고 혼자 있는 시간도 중요하다. 그래서 일반적인 연인 관계에서 기대하는 ’10분에 한 번 카톡 확인’이나 ‘모든 일의 우선순위는 너’ 같은 걸 해 줄 자신이 없다. 평소에는 각자 자기 할 일 하면서 살다가 며칠에 한 번 정도의 빈도로 서로의 일상을 공유하면서 잘 살고 있는지 확인하고, 기념일에는 화려한 데이트코스보다는 편지나 주고 받으며 요리나 해 먹는, 딱 그 정도의 가볍지만 따뜻한 관계를 원하는 것 같다. 하지만 문제는 나랑 비슷한 연애를 추구하는 사람이 있다 치더라도 둘 모두 이 정도의 거리를 유지하고 있으면 연애를 시작할 수가 없다. 으앙 쥬금 ㅠㅠ

7.

기다리고 있던 버스에 드디어 탑승했는데 옆자리에 앉은 사람이 나랑 너무 비슷한 점이 많았다. 일단 나랑 똑같은 가방을 썼고, 복장도 둘 다 셔츠 안에 입은 티와 함께 청바지를 입었다. 심지어 그 사람도 프로그래머였다. 자세히 보지는 못했는데 Node로 웹개발 하고 있었던 듯. 나는 오클랜드까지 가고 그 분은 산호세에서 내렸다. 내가 열심히 글을 쓰는 동안 그 사람은 열심히 서브라임으로 코딩을 했다. 나중에 자다 일어나서 보니까 문명도 하더라. 나도 원래는 버스에서 코딩을 할 계획이었는데 버스 안에서 인터넷이 안 돼서 계획이 바뀌어서 오랜만에 일기를 쓰고 있다.

Greyhound사의 버스를 탔는데, 안에서 전기도 되고 와이파이도 된다는 걸 그렇게 광고했고 LA 갈 때는 유용하게 잘 사용했지만, 버클리로 돌아오는 버스에서는 되는게 없었다. 처음에는 전기도 안 됐는데 버스가 잠깐 휴게소에 멈췄을 때 옆자리에 앉은 그 분께서 기사님께 뭐라고 말을 하더니 전기가 들어오기 시작했다. 와이파이는 끝까지 되지 않았다. 서비스를 홍보한대로 제공하는데 실패했으니 티켓값 일부를 환불해 주면 좋겠지만 6개월 살아 본 결과 미국에는 원래 안 되는게 많아서 이 정도에 불만을 가지지 않는 사람이 대부분이고, 나머지 사람들은 환불요청이 아니라 고소를 한다.

8.

두서 없이 많은 이야기들을 했다. 평소대로 각 주제 하나하나를 하나의 완성된 글로써 다루고 싶은 마음도 있었지만 왠지 버스에서 다 쓰고 싶은 기분이 들어서 그냥 생각 나는 이야기들을 다 짧게 써 보았다. 인터넷이 없어서 글 쓰는 것 이외에 딱히 할 일이 없기도 했고. 글로 생각을 남기는 건 시간이 많이 드는 피곤한 작업이지만, 다 쓰고 났을 때의 성취감과 시간이 지나고 나서 예전에 어떤 생각들을 했었는지 돌아보는 재미 덕분에 종종 글을 쓰게 된다. 초등학교 때는 일기 쓰기를 별로 좋아하지 않았었는데 역시 누가 시켜서 하는 것보다는 알아서 할 때 작업 효율이 더 좋은 법이다.