TL;DR

  • 옥수수 조각 퍼즐을 OR-Tools CP-SAT으로 모델링하면 조각 배치와 각 칸의 덮임을 제약 조건으로 표현해 해를 찾을 수 있음.
  • 퍼즐은 가능한 각 조각 배치를 나타내는 불리언 변수와 모든 조각·칸이 한 번씩 사용되도록 하는 정확 덮기(Exact Cover) 제약으로 표현됨.
  • 조각마다 가능한 배치 중 하나만 선택하고, 속대의 각 칸도 배치 하나에만 포함되도록 설정함.
  • 스도쿠는 칸마다 1~9의 정수 변수를 두고 각 행·열·상자에 서로 다른 값이 들어가도록 하는 방식으로 간단히 모델링됨.
  • 직접 역추적 알고리즘을 작성하기보다, 문제 형태에 맞는 기존 솔버를 사용하고 필요한 내용을 문서에서 찾아보는 교훈을 얻음.

예상했던 풀이

  • RC에서 어느 금요일, 3D 프린트된 퍼즐을 가지고 놀다가 지루해져 Claude에게 풀이를 요청함.
  • 퍼즐은 홈이 파인 흰색 ‘속대’와, 각각 3~10개의 알갱이가 특정 모양으로 붙은 ‘옥수수’ 조각으로 구성됨. 조각을 홈에 밀어 넣어 겹침이나 빈틈 없이 맞추는 것이 목표임.
  • 컴퓨터 비전이 조각 모양을 정확히 파악하지 못해 일부 모양을 직접 명확히 설명한 뒤, Claude가 풀이를 출력하는 파이썬 스크립트를 작성함. 직접 작성했을 법한 것보다 나은 코드여서 이를 통해 배움.
  • 직접 풀었다면 입문 컴퓨터 과학 수업에서 흔히 접하는 재귀적 역추적(recursive backtracking)을 먼저 떠올렸을 것임.
  • 역추적은 임의의 선택을 시도하고, 가능한 수가 남지 않으면 직전 선택을 되돌려 다른 선택을 시도하는 전수 탐색 방식임.
  • 문제 구조를 활용한 최적화도 가능함. 속대를 회전해도 해가 바뀌지 않는 대칭성을 활용하거나, 어떤 조각도 덮을 수 없도록 알갱이 칸 하나만 고립되는 순간 탐색을 중단할 수 있음.
  • 따라서 잘 설계한 역추적 풀이도 작동할 가능성이 높음.

이미 만들어진 바퀴

  • Claude 스크립트의 첫 줄은 ortools.sat.python에서 cp_model을 가져오는 코드였음. 문제에 맞는 기존 도구가 이미 있음을 보여주는 부분임.
  • Google의 OR-Tools CP-SAT은 제약 최적화 문제와 이 퍼즐 같은 만족 가능성 문제를 풀기 위한 라이브러리임.
  • 문제를 변수 집합과 변수들에 동시에 적용되는 제약 또는 단언으로 모델링함. 최적화 문제라면 목적 함수도 추가함.
  • 솔버는 수십 년간 축적된 연구를 활용해 모든 제약을 만족하는 변수 설정을 효율적으로 찾음.
  • 옥수수 퍼즐은 정확 덮기 문제의 변형임. 이를 처음 접한 관점에서 모델링 과정을 정리함.

제약 조건 1: 모든 조각을 정확히 한 번 배치

  • 변수는 참 또는 거짓인 불리언 값이며, 각각은 특정 조각을 특정 방식으로 배치한다는 뜻임.
  • 조각 i를 배치할 수 있는 방법이 N_i개라면 각 배치 방법을 변수 V_{i,n}으로 나타냄. 해당 위치에 조각을 두면 1, 두지 않으면 0임.
  • 각 조각에 대해 가능한 배치 변수의 합을 1로 제한함. 이에 따라 정확히 하나의 배치만 선택됨.

제약 조건 2: 모든 칸을 정확히 한 번 덮기

  • 각 조각 배치가 속대의 어느 칸을 덮는지 확인하고, 각 칸을 덮는 배치 변수 집합 C_s를 구성함.
  • 속대의 각 칸 s에 대해 C_s에 포함된 변수의 합을 1로 제한함. 따라서 모든 칸이 정확히 한 번 덮임.
  • 퍼즐이 올바르게 구성되어 조각의 전체 알갱이 수와 속대의 칸 수가 같다고 가정하면, 모든 조각을 한 번 사용하고 모든 칸을 한 번 덮는 제약만으로 충분함.
  • 파이썬 스크립트에서 솔버를 호출하는 부분은 간단하며, 실제로 복잡한 작업은 각 조각의 가능한 위치를 모두 열거하는 과정임.

장인이 직접 만든 CP-SAT 호출

  • 이 도구에 대해 더 배우고 같은 바퀴를 다시 발명하지 말라는 교훈을 익히기 위해, RC에서 Zaki, Tommy와 함께 CP-SAT의 대표적인 퍼즐 활용 사례인 스도쿠를 풀이함.
  • 스도쿠는 옥수수 퍼즐보다 적용하기 쉬운 입문 사례임. 각 칸에 1~9의 값을 갖는 변수 하나를 두고, 각 행·열·상자에 1~9가 하나씩 들어가도록 제약함.
  • 옥수수 퍼즐에서 조각 회전을 처리하기 위한 유틸리티 메서드가 필요했던 것과 달리, 스도쿠 모델 설정에는 그런 메서드가 필요하지 않음.
  • 빈칸에는 1~9 범위의 정수 변수를 만들고, 주어진 숫자에는 하한과 상한을 그 숫자로 고정한 변수를 만듦.
  • 각 행, 각 열, 그리고 3×3 상자마다 add_all_different 제약을 추가해 값이 모두 다르도록 함.
  • 이 방식으로 제공한 기준 스도쿠를 빠르게 풀었음.

다음에 기억할 점

  • 더 배울 내용은 많지만, 가장 중요한 교훈을 얻음. 앞으로 CP-SAT에 맞는 문제를 만나면 직접 구현하기보다 솔버를 시도하고, 필요한 내용은 해당 도구의 문서를 살펴볼 계획임.

링크

  • Claude와 옥수수 퍼즐 풀이에 관해 나눈 대화 및 Claude의 파이썬 스크립트
  • 스도쿠 솔버
  • RC에서 진행한 짧은 발표 자료