Griductive 퍼즐이 만들어지는 과정

모든 Griductive 퍼즐은 대담한 약속을 합니다: 추측할 필요가 절대 없습니다. 모든 셀은 논리만으로 결정할 수 있으며, 모든 퍼즐에는 정확히 하나의 정답이 있습니다.

이것은 설계 목표가 아닙니다 — 운영 연구와 칩 검증에 사용되는 것과 같은 부류의 솔버에 의해 보장되는 수학적 보증입니다. 이 글에서 그 방법을 설명합니다.

유일성이 중요한 이유

퍼즐에 두 가지 유효한 해답이 있다면, 용의자와 무고한 사람 모두 모든 단서를 만족시키는 셀이 최소 하나 존재해야 합니다. 그 셀에서는 아무리 추론해도 어느 쪽이 맞는지 알 수 없습니다 — 추측해야 합니다. 추측은 연역 퍼즐의 핵심 계약을 위반합니다.

따라서 생성기는 해답이 하나인 퍼즐을 우연히 만들어내는 것이 아닙니다. 퍼즐이 공개되기 전에 두 번째 해답이 존재하지 않음을 증명합니다.

5단계 파이프라인

각 Griductive 퍼즐은 5단계 파이프라인을 통해 만들어집니다. 각 단계에서 일어나는 일은 다음과 같습니다.

1단계: 무작위 해답 생성

생성기는 유효한 해답 그리드를 만드는 것으로 시작합니다 — 모든 셀에 용의자와 무고한 사람을 무작위로 배정합니다. 이것이 플레이어가 최종적으로 연역할 기본 진실(ground truth)입니다.

이 시점에서는 아직 단서가 없습니다. 보드는 기본적인 구조적 제약 조건(그리드 크기, 유효 범위 내의 용의자 수)을 만족하는 무작위 구성일 뿐입니다.

2단계: 단서 풀 구축

다음으로, 생성기는 해답 보드에서 참인 모든 가능한 단서를 철저하게 나열합니다.

Griductive에는 26가지 이상의 고유한 단서 유형이 있습니다 — 세기, 비교, 공간적, 존재적, 유일성, 연결성 등. 각 유형에 대해, 생성기는 보드에 대해 모든 유효한 매개변수화를 테스트합니다. 4x4 그리드는 수천 개의 후보 단서를 생성할 수 있습니다. 해답에서 참으로 평가되는 단서만 유지됩니다.

이것이 생성기가 작업하는 원재료입니다: 대부분 중복되는 참인 명제들의 방대한 풀입니다.

3단계: 최소 단서 세트 선택 (핵심 단계)

여기서 진짜 작업이 이루어집니다. 생성기는 풀에서 다음 조건을 만족하는 작은 단서 부분집합을 선택해야 합니다:

1. 단서가 충분해야 합니다 — 함께, 해답 공간을 정확히 하나의 유효한 보드로 제한해야 합니다.
2. 중복 단서가 없어야 합니다 — 어떤 단서 하나를 제거해도 여러 해답이 가능해져야 합니다.

생성기는 탐욕적 제약 조건 충족 접근법을 사용합니다:

1. 선택된 단서 없이 시작합니다. 해답 공간은 완전히 열려 있습니다 — 많은 보드가 유효할 수 있습니다.
2. 모든 후보 단서를 해답 공간을 얼마나 좁히는지 기준으로 점수를 매깁니다. 나머지 가능성의 80%를 제거하는 단서가 10%를 제거하는 단서보다 높은 점수를 받습니다.
3. 가장 높은 점수의 단서를 선택하여 세트에 추가합니다.
4. 업데이트된 단서 세트로 제약 조건 모델을 다시 풉니다.
5. 솔버가 하나의 해답만 남아 있음을 확인할 때까지 반복합니다.
6. 가지치기: 최종 세트를 순회하며 유일성에 필요하지 않은 단서를 제거합니다. 이것은 퍼즐을 깔끔하게 유지하고 플레이어에게 공짜 정보를 주는 것을 방지합니다.

결과는 빈틈없고 공정한 단서 세트입니다 — 퍼즐을 완전히 풀기에 충분하면서, 낭비되는 단서가 없습니다.

4단계: 난이도 점수 매기기

단서 세트가 확정되면, 생성기는 0~100 척도로 퍼즐의 난이도를 점수 매깁니다. 네 가지 요소가 기여합니다:

• 단순 단서 비율 (35%) — 직접 세기 또는 정체 명시 단서가 얼마나 많은지. 단순 단서가 많을수록 쉬운 퍼즐입니다.
• 복잡 단서 비율 (30%) — 다단계 또는 공간적 추론이 필요한 단서가 얼마나 많은지. 이들은 더 깊은 연역 사슬을 요구합니다.
• 정보 희소성 (20%) — 그리드 크기 대비 단서가 얼마나 적게 주어지는지. 단서가 적을수록 작업할 것이 줄어듭니다.
• 그리드 규모 (15%) — 큰 그리드는 본질적으로 추적하기 더 어렵습니다. 5x5 퍼즐은 3x3의 거의 세 배에 달하는 셀을 가지고 있습니다.

각 단서 유형에는 요구하는 추론에 기반한 고유 복잡도 등급도 있습니다. "Julia는 용의자입니다"와 같은 단서는 가장 단순한 수준입니다. "Julia는 3행에서 정확히 1명의 용의자 이웃을 가진 유일한 사람입니다"와 같은 단서는 여러 셀을 교차 참조해야 하며 훨씬 높은 점수를 받습니다.

5단계: 힌트 생성 및 출력 포맷팅

마지막으로, 생성기는 힌트 시퀀스를 구축합니다 — 막힌 플레이어를 한 번에 하나의 논리적 단계씩 퍼즐을 통해 안내하는 권장 풀이 순서입니다. 힌트는 의존성 깊이 순으로 정렬됩니다: 즉시 연역할 수 있는 셀이 먼저 오고, 긴 사전 연역 사슬이 필요한 셀이 마지막에 옵니다.

최종 퍼즐은 게임에 필요한 모든 데이터와 함께 패키징됩니다: 메타데이터, 단서 세트, 힌트 시퀀스, 그리고 난이도 점수.

솔버: 유일성이 증명되는 방법

파이프라인의 핵심에는 Google OR-Tools CP-SAT이 있습니다 — 제약 조건 전파, 정수 프로그래밍, SAT 풀이를 결합한 제약 조건 프로그래밍 솔버입니다.

퍼즐이 수학 문제가 되는 과정

그리드의 각 셀은 부울 변수로 모델링됩니다: 용의자(1) 또는 무고한 사람(0). 각 단서는 해당 변수들에 대한 하나 이상의 수학적 제약 조건이 됩니다.

예를 들어:

• **"3행에 정확히 2명의 용의자가 있습니다"**는 다음이 됩니다: cell[3,0] + cell[3,1] + cell[3,2] + cell[3,3] = 2
• **"A열의 모든 용의자는 연결되어 있습니다"**는 다음이 됩니다: A열의 용의자 셀이 빈틈 없는 연속 체인을 형성하도록 보장하는 연결성 제약 조건.
• **"1행이 B열보다 용의자가 더 많습니다"**는 다음이 됩니다: sum(row_1) > sum(col_B)

유일성이 검증되는 방법

단서 세트를 조립한 후, 생성기는 CP-SAT에 정확한 질문을 합니다: "이 제약 조건들이 주어졌을 때, 유효한 배정이 둘 이상 존재합니까?"

CP-SAT은 해답 _하나_를 찾는 것에 그치지 않습니다 — 모든 해답을 열거할 수 있습니다. 솔버가 정확히 하나를 찾으면, 퍼즐은 유효합니다. 둘 이상을 찾으면, 생성기는 3단계로 돌아가 단서를 추가합니다.

이것은 경험적 방법이 아닌 형식적 증명입니다. CP-SAT은 전체 해답 공간을 철저히 탐색합니다. 해답이 하나라고 말하면, 정확히 하나입니다 — 마침표.

왜 무차별 대입이 아닌가?

5x5 그리드에는 25개의 셀이 있고, 각각 2개의 가능한 값을 가집니다. 이는 2의 25승 = 3,300만 개의 가능한 보드입니다. 모든 것을 무차별 대입하는 것은 느리고 확장성이 없습니다.

CP-SAT은 제약 조건 전파 덕분에 극적으로 더 빠릅니다: 단서가 "3행에 정확히 2명의 용의자가 있다"고 하면, 솔버는 각 조합을 개별적으로 확인하지 않고도 3행의 모든 셀에 대한 탐색 공간을 즉시 줄입니다. 복잡한 단서들은 이 효과를 복합적으로 증가시킵니다. 실제로 CP-SAT은 5x5 퍼즐의 유일성을 밀리초 단위로 증명합니다.

발생할 수 있는 문제 (그리고 방지하는 방법)

"단서가 모호하면 어떻게 됩니까?"

모든 단서 유형에는 형식적인 수학적 정의가 있습니다. "이웃"은 항상 대각선을 포함한 최대 8개의 주변 셀을 의미합니다. "연결된"은 항상 인접 셀의 연속 체인을 의미합니다. "사이"는 항상 같은 행이나 열에 있는 셀로, 끝점은 제외합니다.

이러한 정의는 제약 조건 모델에 직접 내장되어 있습니다 — 모호성이 스며들 수 있는 자연어 해석 단계가 없습니다. 게임 내 명확한 세부 사항 참조 문서는 플레이어에게 각 공간 키워드가 정확히 무엇을 의미하는지 보여줍니다.

"솔버에 버그가 있으면 어떻게 됩니까?"

CP-SAT 솔버는 Google 최적화 팀이 유지 관리하는 잘 테스트되고 널리 사용되는 도구입니다. 하지만 신뢰만에 의존하지 않습니다. 생성된 모든 퍼즐은 독립적으로 검증됩니다:

1. 자동화된 솔버가 인간 플레이어를 시뮬레이션하며 모든 퍼즐을 단계별로 풀려고 시도합니다. 논리적 연역만으로 완전한 해답에 도달할 수 없으면, 퍼즐은 거부됩니다.
2. 힌트 건전성 검사는 시퀀스의 각 힌트가 논리적으로 유효한지 — 즉, 힌트의 셀이 숨겨진 정보가 아닌 단서와 이전에 밝혀진 셀로부터 진정으로 연역 가능한지 검증합니다.

"단서 생성이 엣지 케이스를 놓치면 어떻게 됩니까?"

각 단서 유형에는 알려진 퍼즐 구성에 대해 테스트된 형식적 평가 함수가 있습니다. 단서 풀 생성 단계는 실제 해답에서 참으로 평가되는 단서만 포함합니다 — 해답에서 거짓인 단서는 퍼즐에 나타날 수 없습니다.

결과

Griductive 퍼즐을 열면, 이미 다음과 같은 과정이 완료된 것입니다:

1. 무작위 해답이 생성되었습니다.
2. 수천 개의 후보 단서가 그에 대해 평가되었습니다.
3. 최소한의 비중복 부분집합이 선택되었습니다.
4. 형식적 솔버가 정확히 하나의 해답만이 해당 단서들을 만족한다고 증명했습니다.
5. 자동화된 솔버가 퍼즐이 순수 연역으로 풀 수 있음을 독립적으로 검증했습니다.
6. 난이도 점수가 산출되고 힌트 시퀀스가 생성되었습니다.

모든 퍼즐, 매일, 네 가지 그리드 크기 전부에 걸쳐. 예외 없이.

약속은 유지됩니다: 만약 막혔다면, 아직 충분히 활용하지 못한 단서가 있습니다. 만약 두 가지 답이 가능하다고 생각한다면, 단서를 다시 읽으십시오 — 논리가 해결해 줄 것입니다. 그리고 증명을 원한다면, 로직 그래프가 단서에서 해답까지의 정확한 연역 사슬을 보여줄 것입니다.

다음 단계: 이야기를 들려주는 단서

현재 Griductive의 단서는 정밀한 논리적 명제처럼 읽힙니다 — 명확하고 모호하지 않지만, 다소 딱딱한 면이 있습니다. "3행에 정확히 2명의 용의자가 있습니다"는 역할을 하지만, 사건을 수사하는 형사가 된 기분을 정확히 주지는 않습니다.

저희는 이를 바꾸기 위해 적극적으로 노력하고 있습니다. 목표는 동일한 기본 논리적 정밀성을 유지하면서 단서가 표현되는 방식을 다양화하는 것입니다. 휴일 이벤트와 연결된 단서나, 특정 범죄 현장의 목격자 증언으로 구성된 단서를 상상해 보십시오. 무미건조한 공식 대신, 실제 수사의 증거 조각처럼 느껴지는 것을 읽게 될 것입니다.

핵심 제약 조건은 변하지 않았습니다: 모든 단서는 일관되고, 모호하지 않으며, 형식적으로 검증 가능해야 합니다. 솔버는 단서가 수학 교과서처럼 들리든 느와르 탐정 소설처럼 들리든 상관하지 않습니다 — 논리적 내용만 신경 씁니다. 이러한 분리가 정확성을 손상시키지 않으면서 더 풍부한 표현을 가능하게 합니다.

동일한 보장. 동일한 엄밀함. 하지만 방정식이 아니라 풀 가치가 있는 사건처럼 느껴지는 퍼즐.

추측 없음. 운 없음. 수학적으로 보장됨.

오늘의 퍼즐 플레이하기 →