기술 요약: 대역폭 채색(Bandwidth Coloring)을 위한 SAT 인코딩

문제 정의

**대역폭 채색 문제(Bandwidth Coloring Problem, BCP)**는 에지에 양의 정수 가중치 $d(u, v)$가 부여된 그래프 채색 문제(Graph Coloring Problem, GCP)의 일반화된 형태이다. 목표는 각 정점 $v$에 색상 $c(v) \in \mathbb{N}$를 할당하여, 모든 에지 $\{u, v\} \in E$에 대해 거리 제약 조건 $|c(u) - c(v)| \ge d(u, v)$를 만족시키는 것이다. 목표는 할당된 색상의 최댓값인 **스팬(span)**을 최소화하는 것이다.

BCP는 무선 및 셀룰러 네트워크의 **주파수 할당 문제(Frequency Assignment Problems, FAP)**에서 자연스럽게 발생하며, 여기서 정점은 송신기를 나타내고 에지 가중치는 전자기 간섭을 피하기 위해 필요한 최소 주파수 분리량을 나타낸다. 메타휴리스틱 방법들이 존재하지만, 이들은 최적성 보장을 결여하고 있다. 정수 선형 계획법(ILP) 및 제약 프로그래밍(CP)에 기반한 정확한 방법들이 연구되어 왔으나, ILP 정식화는 에지 가중치에 따라 제약 조건의 수가 증가하는 문제점이 있다. 최근에는 SAT 기반 접근 방식이 최첨단 기법으로 부상했으나, BCP에 특화된 SAT 인코딩 설계 공간은 여전히 미개척 영역으로 남아 있다.

방법론

본 논문은 세 가지 범주로 구성된 6가지의 뚜렷한 인코딩 방법을 탐색하는 통합 프레임워크를 통해 BCP를 위한 SAT 인코딩의 체계적인 설계 연구를 제시한다. 이 프레임워크는 증분형 풀이(incremental solving), 대칭성 파괴(symmetry breaking), **블록 너비 전략(block width strategies)**의 세 가지 구성 가능한 기능의 영향을 평가한다.

1. 인코딩 범주

프레임웨크는 다음의 인코딩 방법들을 구현하고 비교한다:

• 단일 변수 인코딩 (1G, 1L): 순서 변수를 사용하여 색상 할당을 암시적으로 정의한다.
  • 1G (Greater-than): $y_{u,j} = \text{true} \iff c(u) \ge j$를 만족하는 변수 $y_{u,j}$를 사용한다.
  • 1L (Less-than): $y_{u,j} = \text{true} \iff c(u) \le j$를 만족하는 변수 $y_{u,j}$를 사용한다.
  • 이러한 방법들은 에지 가중치와 무관하게 $O(k(n+m))$의 점근적 절(clause) 수를 갖는다.
• 이중 변수 인코딩 (2G, 2L): 할당 변수($x_{u,j}$)와 순서 변수($y_{u,j}$)를 모두 명시적으로 유지하여 보다 직접적인 거리 제약을 허용한다.
  • 2G/2L: 1G/1L과 유사한 의미론을 가지나, $x$와 $y$ 변수를 연결하는 채널링 제약(channeling constraints)을 포함한다.
• 블록 인코딩 (X, Xa): 색상 범위를 고정 너비 블록으로 분할하고, 블록 내 할당 변수의 합을 나타내기 위해 보조 범위 변수($R_{u,a,b}$)를 사용한다.
  • X: 보조 변수 없이 뺄셈 연산(블록 내 범위 합에 필요)을 직접 인코딩한다.
  • Xa: 뺄셈 항을 나타내는 보조 변수를 도입하여 절(clause) 재사용을 가능하게 한다.
  • 블록 인코딩은 특히 에지 가중치가 클 때 거리 제약에 대한 절의 수를 줄이는 것을 목표로 한다.

2. 구성 가능한 기능

• 증분형 풀이 (Incremental Solving): (스팬의 상한이 감소함에 따라) 학습된 절을 재사용하는 것이 성능을 개선하는지 테스트한다. 이는 SAT 가정(assumptions)을 사용하여 구현된다.
• 대칭성 파괴 (Symmetry Breaking): 최고 차수 정점에 대해 반사 기반 기술을 적용하여, 해당 정점의 색상을 스팬 범위의 하위 절반($c(h) \le \lfloor k/2 \rfloor$)으로 제한한다. 이는 $c$가 유효한 채색이면 $c'(v) = k+1-c(v)$ 또한 유효하다는 성질을 이용한다.
• 블록 너비 전략 (Block Width Strategies): 블록 인코딩의 경우, 고정 너비 블록(기본값 $w=8$)과 가변 너비 블록(정점의 최대 인접 에지 가중치에 의해 결정됨)을 비교한다.

3. 실험 설정

연구는 51개의 벤치마크 인스턴스에 대해 36개의 뚜렷한 구성(6가지 방법과 기능의 조합)을 평가한다:

• GEOM 세트: 33개의 기하학적 랜덤 그래프 (GEOM20 ~ GEOM120).
• MS-CAP 세트: 셀룰러 네트워크 주파수 할당 문제에서 유도된 18개의 인스턴스.
• 솔버: CaDiCaL 1.9.5, 인스턴스당 3600초의 시간 제한.
• 베이스라인: 기존의 최첨단 SAT 인코딩인 POP-S-B 및 POPH-S-B (Faber et al., 2024)와 비교한다.

주요 결과

전반적인 성능

제안된 프레임워크는 최첨단 성능을 달면한다. 가장 우수한 성능을 보인 구성은 블록 인코딩 Xa(고정 너비, 증분형 풀이, 대칭성 파괴 적용)로, 51개 인스턴스를 모두 해결하였으며 총 소요 시간은 2721.3초였다. 이는 이전의 최첨단 방식인 POPH-S-B(2904.6초) 대비 6.3% 감소한 수치이며, POP-S-B(3307.5초) 대비 17.7% 감소한 수치이다.

어려운 인스턴스 성능 (GEOM120b)

가장 어려운 인스턴스인 GEOM120b에 관한 중요한 발견은 다음과 같다:

• 기존 방법들(POPH-S-B 및 POP-S-B)은 한 시간의 시간 제한 내에 GEOM120b를 최적성 입증까지 해결하는 데 실패했다.
• 제안된 **블록 인코딩 (X 및 Xa)**은 약 1000초 내에 GEOM120b를 최적해로 해결하였다 (구체적으로 기본 Xa 구성은 851.4초, 완전히 최적화된 Xa는 1011.6초 소요).
• 이는 이 특정 인스턴스에 대해 기존의 최선인 SAT 기반 접근 방식보다 약 2배의 속도 향상을 보여준다.

상호작용 효과

연구는 인코딩 선택과 솔버 구성 사이의 유의미한 상호작용 효과를 밝혀냈다:

• 증분형 풀이: 블록 구조가 스팬이 감소함에 따라 대체로 안정적으로 유지되기 때문에 블록 인코딩에서 상당한 속도 향상을 제공한다 (예: Xa의 경우 24.4% 개선). 반면, 단일 변수 인코딩(1G, 1L)에서는 새로운 상한에 따라 순서 제약이 재정의되어 학습된 절이 무효화되므로, 이득이 없거나(no benefit) 오히려 성능이 저하된다.
• 대칭성 파괴: 그 효과는 인코딩 유형에 따라 크게 달라진다. 이는 POP-S-B(24.5% 속도 향상)와 1L(13.2% 속도 향상)의 성능을 크게 개선하지만, 2G(11.9% 속도 저하)와 POPH-S-B(11.4% 속도 저하)의 성능은 저하시킨다.
• 블록 너비: 고정 너비와 가변 너비 사이의 선택은 50개의 표준 인스턴스에서 미미한 영향(<1.2% 차이)을 미쳤으며, 이는 솔버의 절 학습이 두 전략 모두에 잘 적응함을 시사한다.

인코딩 크기 vs 효율성

변수와 절의 수가 적을수록 더 빠르게 풀릴 것이라는 직관과는 반대로, Xa 인코딩(가장 압축적인 1G 인코딩보다 7배 많은 변수와 5.5배 많은 절을 생성함)이 가장 빠른 해결 시간을 달성했다. 이는 보조 변수가 단위 전파(unit propagation)를 강화하여 솔버가 함의(implication)를 더 효율적으로 도출할 수 있는 "지름길"을 만들어준다는 원칙을 뒷받침한다.

의의 및 주장

본 논문은 BCP를 위한 SAT 인코딩에 관한 문헌의 공백을 메우는 체계적인 설계 연구를 수행했다고 주장한다. 대칭성 파괴와 증분형 풀이는 GCP를 위해 연구되어 왔으나, BCP 특유의 인코딩과의 적용 및 상호작용에 대해서는 이전에 조사된 바 없다.

주요 기여는 다음과 같다:

1. 해결되지 않았던 문제의 해결: 본 프레임워크는 GEOM120b 벤치마크를 합리적인 시간 내에 최적성을 입증하며 해결한 최초의 프레임워크이다. 이는 이전의 정확한 방법들이 한 시간 내에 완료하지 못한 작업이다.
2. 통합 프레임워크: 6가지 인코딩 방법과 그 구성 가능한 기능들에 대한 포괄적인 비교 연구를 제공하며, 가장 어려운 인스턴스에는 블록 인코딩이 우수하고, 일반적인 경우에는 순서 기반 인코딩(2L, 1G 등)이 구현 복잡도와 성능 사이의 유리한 절충안을 제공함을 확인하였다.
3. 상호작용 통찰: 인코딩 기능들이 독립적으로 작동하지 않음을 강조한다. 특히, 증분형 풀이와 대칭성 파괴는 특정 인코딩 유형에 따라 신중하게 선택되어야 하는데, 이는 이들이 시너지 효과를 내거나 혹은 서로 상충하는 효과를 낼 수 있기 때문이다.

저자들은 블록 인코딩이 가장 도전적인 인스턴스에서 최고의 성능을 제공하지만, BCP 전용 솔버를 발전시키기 위해서는 인코딩 설계 선택에 대한 체계적인 탐색이 필수적이라고 결론짓는다. 향-후 연구로는 이를 대역폭 다중 채색 문제(Bandwidth MultiColoring Problem, BMCP)로 확장하고, 적응형 구성 선택 메커니즘을 개발하는 것이 제안된다.