기술 요약: 탐색 공간의 길들이기 – Hitori 및 Binairo 퍼즐의 해결과 생성

문제 정의

본 논문은 두 가지 특정 논리 퍼즐인 Hitori와 Binairo(Takuzu로도 알려짐)를 해결하고 생성하는 과제를 다룹다. 이러한 퍼즐들은 레크리에이션용이지만, 제약 충족 문제(Constraint Satisfaction Problems, CSPs)로 정식 모델링할 수 있는 복잡한 조합 구조를 제시한다. 핵심적인 어려움은 로컬 제약 조건(예: 인접성, 3회 연속 금지)과 글로벌 제약 조건(예: 행/열의 고유성, Hitori의 흰색 셀 연결성)이 혼합된 거대한 탐색 공간을 탐색하는 데 있다.

저자들은 이 퍼즐들을 해결하기 위한 두 가지 주요 패러다임을 평가하고 비교하는 것을 목표로 한다:

1. 체계적 백트래킹 탐색 (Systematic Backtracking Search): 도메인 특화 휴리스틱 및 최적화가 강화된 방식.
2. SAT 기반 솔버 (SAT-based Solving): 퍼즐 규칙을 논리곱 표준형(CNF)으로 인코딩하고 현대적인 충돌 구동 절차 학습(CDCL) 솔버를 활용하는 방식.

또한, 본 논문은 해결 분석에 비해 종종 간과되는 작업인, 유효하고 유일한 해를 갖는 퍼즐 인스턴스를 알고리즘적으로 생성하는 문제를 다룬다.

방법론

솔버 접근 방식

본 연구는 두 가지 구별되는 솔버 제품군을 구현하고 비교한다:

1. SAT 기반 솔버:

• 인코딩: 퍼즐을 명제 논리로 변환한다.
  • Binairo: 로컬 제약 조건(동일한 값의 3회 연속 금지), 글로벌 균형(0과 1의 동일한 개수), 그리고 쌍별 부등식 제약을 통한 행/열 고유성을 인코딩한다.
  • Hitori: 중복 제약과 검은색 셀의 비인접성을 인코딩한다. 결정적으로, 연결성 제약(모든 흰색 셀이 하나의 컴포넌트를 형성해야 함)은 복잡성으로 인해 CNF에 직접 인코딩되지 않는다. 대신, 솔버는 후보 해를 생성하고, 외부에서 연결성을 확인한 뒤, 유효하지 않은 후보를 거부하기 위해 "차단 절(blocking clauses)"을 반복적으로 추가한다.
• 실행: 솔빙 작업을 최첨단 SAT 솔버(예: minisat22, minicard, cadical)에 위임한다.

2. 백트래킹 기반 솔버:

• 메커니즘: 부분 할당(partial assignments)에 대한 깊이 우선 탐색(DFS)을 수행한다.
• 최적화 및 휴리스틱: 다음의 다양한 조합을 평가한다:
  • 전파 (Propagation): 부분 할당으로부터의 결과를 결정론적으로 강제함 (예: 중복을 피하기 위해 값을 강제함).
  • FastDup (Hitori): 전체 그리드를 스캔하는 것을 피하기 위한 증분적 중복 카운팅.
  • CellScore: 제약이 많은 변수를 우선순위에 두는 스코어링 함수 (변수 순서 결정).
  • WhiteFirst (Hitori): 연결성 유연성을 유지하기 위해 "흰색" 값을 "검은색"보다 먼저 할당하도록 선호함.
  • SkipConnected / SufficientConnected / FastSufficientConnected (Hitori): 구조적 조건이 연결성을 보장하거나 위반이 불가능할 때 전체 그래프 분석을 피하는 최적화된 연결성 체크.
  • IncrementalCheck (Binairo): 가장 최근의 할당에 의해 영향을 받는 제약만을 평가함.
  • BalancedValueOrder (Binairo): 행/열의 균형을 유지하는 할당을 선호함.
  • EfficientPropagation (Binairo): 영향을 받는 영역으로 업데이트를 제한하는 제한된 전파 변형.

생성기 접근 방식

견고한 벤치마크를 확보하기 위해, 저자들은 두 퍼즐 유형 모두에 대해 유효하고 유일하게 해결 가능한 인스턴스를 생성하는 커스텀 생성기를 개발하였다:

• Hitori 생성기: 유효한 검은색/흰색 패턴을 먼저 구성한 후, 숫자를 흰색 셀에 할당하고(중복이 없도록 보장), 검은색 셀에 숫자를 할당한다(중복이 존재하도록 보장). 유일성을 검증하기 위해 수정된 백트래킹 솔버를 사용하며, 모호성(예: 플립 쌍)을 해결하기 위해 그리드를 수정한다.
• Binairo 생성기: 희소한 무작위 할당에서 시작하여, SAT 솔버를 사용하여 유효한 전체 그리드를 완성한 후, 백트래킹 솔버를 사용하여 유일성을 확인하면서 값을 반복적으로 제거한다.

실험 설정

• 데이터셋: 벤치마크에는 Binairo의 경우 8×8에서 26×26, Hitori의 경우 8×8에서 54×54 크기의 그리드가 포함된다.
• 지표: 실행 시간(벽시계 시간), 해결율(5초 타임아웃 내에 해결된 인스턴스의 백분율), 탐색된 총 노드 수, 분기 계수(branching factor), 재귀 깊이.
• 구성: 모든 솔버는 64GB RAM을 갖춘 AMD Ryzen 9 7950X에서 싱글 스레드로 실행되었다.

주요 기여

1. 포괄적인 솔버 평가: Hitori 및 Binairo에 대해 베이스라인 백트래킹, 최적화된 백트래킹(다양한 휴리스틱 포함), 그리고 SAT 기반 솔빙을 체계적으로 비교하였다.
2. 도메인 특화 최적화: 퍼즐의 고유한 제약 조건에 맞춤화된 특정 휴리스틱(예: WhiteFirst, CellScore, FastDup)을 구현하고 경험적으로 테스트하였다.
3. 퍼즐 생성 프레임워크: 두 퍼즐 유형 모두에 대해 유일하고 유효한 인스턴스를 생성할 수 있는 생성기를 개발하여 체계적인 벤치마킹을 용이하게 하였다.
4. 트레이드오프의 경험적 분석: 서로 다른 최적화가 탐색 트리 크기와 계산 오버헤드에 어떻게 영향을 미치는지에 대한 상세한 분석을 제공하였다.

결과

Binairo

• SAT 성능: SAT 기반 접근 방식(특히 minisat22 사용)이 우수하였으며, 모든 인스턴스의 **100%**를 해결하였고 중앙값 실행 시간은 0.0386초였다.
• 백트래킹 성능: 가장 잘 최적화된 백트래킹 구성(BalancedValueOrder + CellScore + Propagation)조차 타임아웃 내에 인스턴스의 **49.0%**만을 해결하였다.
• 핵심 통찰: Binairo의 경우, 제약 조건이 SAT로 직접 인코딩하기에 적합하다. 전파(Propagation)는 백트래킹의 탐색 트리 크기를 크게 줄였지만(5,803개 노드에서 약 51개로), 어려운 인스턴스에서 SAT의 원시적인 속도나 성공률을 따라잡을 수는 없었다.

Hitori

• 백트래킹 성능: 전파 기반 백트래킹이 가장 좋은 결과를 보였으며, **100%**의 인스턴스를 해결하였고 중앙값 실행 시간은 0.1500초였다.
• SAT 성능: SAT 기반 접근 방식(minicard 사용)은 인스턴스의 **23.3%**만을 해결하였다. 쉬운 인스턴스에서는 매우 빨랐으나(중앙값 0.0191초), 더 크고 어려운 퍼즐에서는 빈번하게 타임아웃을 초과했다.
• 핵심 통찰: SAT 접근 방식의 반복적인 연결성 체크가 병목 현상을 일으켰다. 더 큰 퍼즐(18×18 이상)의 경우, 연결되지 않은 후보를 거부하기 위해 수천 번의 반복이 필요했다. 결과적으로, 실행 시간의 **97.4%**가 솔빙 자체보다는 SAT 솔버 외부의 작업(연결성 체크 및 절 생성)에 소비되었다.

최적화 분석

• **전파(Propagation)**는 두 퍼즐 유형 모두에서 백트래킹을 위한 가장 효과적인 최적화로 식별되었으며, 탐색 노드 수를 획기적으로 줄였다.
• 오버헤드 경고: 논문은 탐색 노드를 줄이는 것이 항상 실행 시간을 줄이는 것은 아니라고 지적한다. Binairo의 경우, EfficientPropagation은 Standard Propagation보다 적은 노드를 방문했지만, 북킹(bookkeeping) 및 반복적인 체크의 오버헤드로 인해 더 높은 실행 시간을 기록했다.

의의 및 주장

본 논문은 솔버의 성능이 솔빙 패러다임과 퍼즐의 제약 조건 사이의 구조적 일치 여부에 크게 의존한다고 주장한다:

• Binairo: 그 제약 조건들(로컬 패턴, 균형, 고유성)은 SAT로 자연스럽게 표현 가능하므로, SAT 솔버가 최적의 선택이다.
• Hitori: 글로벌 연결성 제약은 CNF로 효율적으로 인코딩하기 어렵다. Hitori에 필요한 반복적 정제 루프는 SAT를 덜 효과적으로 만드는 반면, 최적화된 백트래킹은 탐색 중에 연결성 체크를 점진적이고 더 저렴하게 처리할 수 있다.

저자들은 현대적인 SAT 솔버가 강력하긴 하지만, 연결성과 같은 복잡한 글로벌 위상적 제약을 가진 모든 CSP에 대한 보편적인 해결책은 아니라고 결론짓는다. 또한, 백트래킹의 경우 제약 전파가 핵심적인 최적화이지만, "스마트한" 최적화의 오버헤드가 탐색 공간 감소의 이점보다 커지지 않도록 주의해야 함을 강조한다.