North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

기술 요약: 만족 가능성(Satisfiability)을 이용한 $k$개의 공선점(Collinear Points)을 피하는 북동쪽 격자 경로 연구

문제 정의
본 논문은 북동쪽 격자 경로(단계가 $\{(1,0), (0,1)\}$인 경로)가 $k$개의 공선점을 포함하지 않도록 하는 최대 길이를 결정하고자 하는 Gerver–Ramsey 공선성 문제를 조사한다. $a(k)$를 모든 북동쪽 격자 경로가 $k$개의 공선점을 포함하게 되는 최소 정수라고 할 때, $a(k)-1$은 $k$개의 공선점을 피하는 가장 긴 경로의 길이이다. Montgomery(1972)는 모든 $k$에 대해 이러한 상계(upper bound)가 존재함을 증명했고, Gerver와 Ramsey(1979)는 명시적이지만 매우 느슨한 상계를 제공했으나, 작은 $k$에 대한 $a(k)$의 정확한 값은 여전히 미지수로 남아 있거나 계산적으로 검증하기 어려웠다. 본 연구 이전에 J. Shallit(2013)은 $a(4)=9$, $a(5)=29$, $a(6)=97$임을 계산적으로 결정하였으며, $a(7) \ge 261$이라는 하한선을 찾는 경로(길이 260)를 발견하였다.

방법론
저자들은 이러한 격자 경로를 열거하고 검증하기 위해 불리언 만족 가능성(Boolean Satisfiability, SAT) 솔버를 활용한다. 핵심 접근 방식은 $k$개의 공선점을 피하는 길이 $m$인 경로의 존재를 조합 정규형(Conjunctive Normal Form, CNF) 공식으로 인코딩하는 것이다.

1. SAT 인코딩:

   • 변수: 불리언 변수 $v_{x,y}$는 점 $(x,y)$가 경로 위에 있는지 여부를 나타낸다.
   • 경로 제약 조건: 경로는 $(0,0)$에서 시작하고, 북쪽 또는 동쪽으로만 이동하며, 경로가 갈라지지 않음(즉, 임의의 점에서 경로는 가능한 두 개의 다음 지점 중 정확히 하나로 진행함)을 보장하는 절(clauses)을 포함한다.
   • 비공선성 제약 조건: 저자들은 어떤 직선도 $k$개의 점을 포함하지 않도록 하기 위해 카디널리티 제약 조건(at-most-$k$)을 사용한다. 이는 순차적 카운터 인코딩(sequential counter encodings)을 사용하여 CNF로 인코딩되거나, klauses를 사용하는 "at-least-$k$ 조합 정규형(KNF)"을 통해 처리된다.
   • 최적화:
     • 대칭성 깨기(Symmetry Breaking): 첫 번째 단계를 북쪽으로 강제함으로써 보수(complementation) 대칭성을 제거하여 탐색 공간을 줄인다. 역전 대칭성(reversal symmetries)은 인코딩 오버헤드를 피하기 위해 탐색 중에 대부분 무시되었으며, 동형 검사(isomorphism checks)는 사후 열거 과정에서 수행되었다.
     • 도달 가능성 범위(Reachability Bounds): 도달 불가능하다고 증명된 점들(예: 한 방향으로 $k-1$번 연속된 단계가 필요한 점들)은 단위 절(unit clauses)을 통해 차단된다.
     • 제약 조건 제거 휴리스틱: 솔버의 효율성을 높이기 위해, 해당 영역 내에 점이 매우 적은 직선에 해당하는 비공선성 제약 조건을 제거한다. 솔루션이 발견되면, $k$개의 공선점이 존재하지 않음을 보장하기 위해 명시적으로 검증한다.
     • 병렬화: 대규모 인스턴스의 경우 "큐브 앤 컨커(cube-and-conquer)" 기술이 사용된다. 룩어헤드 솔버(lookahead solver, march)가 탐색 공간을 서로 소인 하위 문제(cubes)로 분할한 뒤, 이를 병렬로 해결한다.

2. 솔버 선택:

   • 저자들은 표준 CNF 인코딩(CaDiCaL에 의해 해결됨)을 KNF 인코딩(Cardinality-CaDiCaL에 의해 해결됨)과 비교 벤치마킹하였다.
   • 결과에 따르면, 만족 가능한 인스턴스(긴 경로를 찾는 경우)에서는 KNF가 훨씬 더 우수한 성능을 보였고, 불만족스러운 인스턴스(더 긴 경로의 부존재를 증명하는 경우)에서는 CNF가 더 우수했다. 방법론은 목표가 경로를 찾는 것인지 혹은 부존재를 증명하는 것인지에 따라 인코딩 유형을 적응시킨다.

주요 결과
본 논문은 다음과 같은 계산 결과를 제시한다:

• $k \le 6$에 대한 열거: 저자들은 $k \le 6$에 대해 동형성을 고려하여 모든 극대 GR($k$) 워크(길이가 $a(k)-1$인 경로)를 전수 열거하였다.

  • 이전 결과 확인: $a(4)=9$, $a(5)=29$, $a(6)=97$.
  • 두 개의 서로 다른 극대 GR(4) 워크, 하나의 고유한 극대 GR(5) 워크, 그리고 두 개의 서로 다른 극대 GR(6) 워크가 존재함을 발견하였다.
  • 더 긴 경로의 부존재를 입증하기 위해 DRAT 증명 인증서(proof certificates)를 생성하여, SAT 솔버 자체를 신뢰하지 않고도 결과를 독립적으로 검증할 수 있도록 하였다.

• $k = 7$에 대한 진전:

  • 하한선 개선: 저자들은 길이 327 단계의 GR(7) 워크를 발견하였으며, 이는 Shallit이 발견한 기존의 최장 경로인 260 단계를 크게 개선한 것이다.
  • 도달 가능성 분석: GR(7) 워크에 대해 267단계까지의 상한 및 하한 도달 가능성을 결정하였으며, 직선 $y=x+1$ 상의 첫 번째 도달 불가능한 점인 $(146, 147)$을 식별하였다.
  • 탐색 전략: 가장 긴 워크는 랜덤 시드 병렬화와 큐브 앤 컨커를 결합한 하이브리드 접근 방식을 사용하여 발견되었다. 주목할 점은, 발견된 가장 긴 워크들이 $y=x+1$ 선 근처에 집중되어 있었다는 것이다.

의의 및 주장
본 논문은 SAT 솔버가 거대한 탐색 공간을 가진 이산 기하학 문제를 해결하는 데 효과적일 뿐만 아니라, 증명 인증서(DRAT 형식)를 생성하고 검증할 수 있는 능력 덕분에 직접 작성한 탐색 코드보다 더 높은 수준의 신뢰성을 제공할 수 있다고 주장한다.

주요 기여는 다음과 같다:

1. 긴 GR($k$) 워크를 찾고 그 극대성을 증명하기 위한 SAT 기반 방법론.
2. $k \le 6$에 대한 극대 GR($k$) 워크의 완전한 열거 및 이전 계산 결과의 확인 및 확장.
3. $a(7)$에 대한 새로운 하한선 제시 (기존 최장 경로 260에서 327 단계로 확장).
4. $a(7)$의 정확한 값은 여전히 미지수이지만, SAT 솔법이 이전보다 훨씬 더 긴 경로를 찾는 데 효과적이며, 부존재 주장에 대한 증명 인증서를 생성할 수 있음을 보여주는 실험적 연구.

저자들은 $a(7)$의 결정에 대해 겸허한 태도를 유지하며, 정확한 값은 여전히 알 수 없으나, 이 문제에 SAT 솔빙을 도입한 것이 향후 추가적인 진전을 촉진하기를 희망한다고 언급하였다.