An Efficient MaxSAT-DDD Approach for Train Rescheduling via Precedence Propagation and Hybrid AMO Encodings

기술 요약: 열차 재스케줄링을 위한 효율적인 MaxSAT-DDD 접근 방식

문제 정의
본 논문은 정해진 경로를 가진 열차 재스케줄링 문제(TRP)를 다룬다. 이 문제의 목표는 열차 경로 선점, 자원 용량 제약 조건을 준수하면서 방해된 시간표를 복구하고 지연 목적 함수를 최소화하는 것이다. 본 모델은 열차의 경로가 고정되어 있다고 가정하며, 이는 탐색 공간을 단순화하지만 대규모 경로 변경이 필요한 대형 장애 상황보다는 경미한 지연 복구 시나리오에 국한된다는 한계가 있다. 모델은 다음을 포함한다:

• 선점 제약 조건(Precedence Constraints): 열차 경로를 따른 작업 순서를 보장함.
• 자원 안전성(Resource Safety): 열차가 동일한 자원(구간, 선로, 또는 역)을 동시에 점유하는 것을 방지하는 이산 제약 조건(disjunctive constraints).
• 지연 목적 함수(Delay Objectives): 세 가지 비용 함수가 평가된다: 단계적(Stepwise, 특정 임계값 초과 시 페널티), 반올림(Rounded, 180분 단위 페널티), 그리고 연속적(Continuous, 선형 지연 비용).

저자들은 전체 시간 이산화를 통한 계산 불가능성을 피하기 위해 **동적 이산화 발견(Dynamic Discretization Discovery, DDD)**을 활용한다. 대신, DDD는 제한된 시간 인덱스 모델을 해결하고, 타당성과 최적성을 입증하는 데 필요한 시점만을 반복적으로 정밀하게 조정한다.

방법론
핵심 기여는 두 가지 특정 개선 사항을 정밀화 루프(refinement loop)에 통합한 강화된 MaxSAT-DDD 인코딩이다.

1. 자원 충돌을 위한 하이브리드 AMO (At-Most-One) 인코딩:

   • 자원 충돌은 시간 의존적 점유 클리크(clique)로 모델링된다.
   • 저자들은 표준 쌍별 배제(pairwise exclusions, $\Theta(n^2)$ 개의 절 생성)를 대신하여 하이브리드 접근 방식을 채택했다. 작은 클리크($n < 6$)의 경우 쌍별 절을 유지하고, 큰 클리크의 경우 Sinz의 순차 카운터(sequential-counter) 인코딩을 사용하여 절의 개수를 선형 복잡도($O(n)$)로 줄였다.
   • 이 인코딩은 특정 시점에 열차가 자원을 점유하는지 여부를 정의하는 "래더 리터럴(ladder literals)"에 지시 변수(indicator variables)를 연결한다.

2. 열차 경로 선점 전파(Train-Path Precedence Propagation):

   • 첫 번째 DDD 반복 이전에, 솔버는 각 열차 경로의 작업에 대한 유효 최단 시간($t^{eff}$)을 계산하기 위해 순방향 패스(forward pass)를 수행한다.
   • 이 전파 과정은 이전 작업의 종료 시간과 주행 시간을 더한 값보다 시작 시간이 커야 함을 강제함으로써 초기 하한 래더(lower-bound ladders)를 조여준다.
   • 이 전처리 단계는 전체 경로 길이에 대해 선형이며, 모든 가능한 스케줄을 보존하면서 탐색 공간을 조기에 가지치기한다.

솔버 아키케처
제안된 솔버인 MaxSAT-Default는 이 두 가지 개선 사항을 결합한다. 이는 다음을 교대로 수행하는 DDD 루프 내에서 작동한다:

1. 제한된 가중치 부분 MaxSAT 인instance 해결 (타당성을 위한 hard clauses, 지연 비용을 위한 soft clauses).
2. 위반 사항 확인을 위한 솔루션 디코딩.
3. 위반이나 목적 함수 불일치가 발견될 경우 시간 간격을 정밀화하고 새로운 경로/자원/비용 절(clause) 추가.
   본 연구는 이를 기준으로 삼아 Baseline MaxSAT 인코딩, 증분 및 비증분 SAT 백엔드(RC2, Glucose 4.2), 그리고 Big-M MILP, Time-Indexed (TI) MILP, 제약 프로그래밍(CP) 공식을 사용하는 상용 솔버(Gurobi, CPLEX)와 비교한다.

주요 기여

• 인코딩 효율성: 대규모 자원 클리크에 대한 순차 카운터 AMO 인코딩의 통합은 CNF 크기를 크게 줄이고 쌍별 인코딩에 비해 단위 전파(unit propagation) 속도를 향상시킨다.
• 탐색 공간 가지치기: 선점 전파는 초기 경계를 조여 DDD 반복 횟수와 솔버의 백트래킹을 줄이며, 특히 연속 지연 목적 함수에서 효과적이다.
• 실증적 평가: 세 가지 지연 목적 함수에 대해 72개의 인스턴스를 대상으로 한 포괄적인 평가를 수행하였으며, 네 가지 MaxSAT 변형을 최신 MILP 및 CP 베이스라인과 비교하였다.

실험 결과
실험은 노르웨이 베르겐 노선(Bergen Line)에서 파생된 벤치마크를 통해 수행되었으며, 25~30대의 열차와 다양한 수준의 자원 집계(원래, 선로, 역)를 특징으로 한다.

• 단계적 목적 함수(Stepwise Objectives): MaxSAT-Default는 72개 인스턴스를 모두 해결했으며 평균 실행 시간은 23 ms로, Gurobi의 Big-M MILP와 해결된 인스턴스 수는 동일했으나 평균적으로 약 16배 더 빨랐다.
• 반올림 목적 함수(Rounded Objectives): MaxSAT-Default는 해결된 인스턴스 수를 변경하지 않으면서 평균 실행 시간을 794 ms(베이스라인)에서 479 ms로 단축했다. 어려운 연속 트랙 인스턴스에 대한 절제 연구(ablation study) 결과, 공통 해결 집합에 대해 최대 79.6%의 실행 시간 감소를 보였다.
• 연속적 목적 함수(Continuous Objectives): 연속 지연에 대해서는 Big-M MILP(Gurobi)가 여전히 가장 강력한 베이스라인이었으나, MaxSAT-Default는 베이스라인 MaxSAT 인코딩보다 개선된 성능을 보였으며(59개 대비 60개 해결), 실행 시간도 단축되었다.
• 어려운 인스턴스: 밀도가 높고 집계된 인스턴스(예: trackA8, stationA8)에서 MaxSAT-Default는 베이스라인을 지속적으로 능가했으며, 종종 타임아웃이 발생하거나 메모리를 소진하는 TI-MILP 및 CP 접근 방식보다 우수한 성능을 보였다.

의의 및 주장
본 논문은 제안된 MaxSAT-DDD 접근 방식이 이산 지연 목적 함수(단계적 및 반올림)에 매우 효과적이며, 베이스라인 MaxSAT보다 상당한 속도 향상을 제공하고 상용 MILP 솔버와 경쟁력 있는 성능을 보인다고 주장한다. 저자들은 고정 경로 가정이 범위 제한적이라는 점을 언급하며, 본 연구가 이 분야의 정밀 방법론(exact methods)을 위한 필수적인 토대를 제공한다고 밝힌다.

연구는 연속 지연 목적 함수의 경우 Big-M MILP가 여전히 우위에 있으며, MaxSAT 방식은 하한(lower bound)을 강화하기보다는 어려운 하위 집합에 대한 탐색을 가속화하는 데 가장 가치가 있다고 겸허히 결론짓는다. 제안된 인코딩의 주요 가치는 자원 집계를 효율적으로 처리하고 DDD 정밀화 루프의 계산 오버헤드를 줄이는 능력에 있다. 향후 과제로 모델을 확장하여 경로 변경(rerouting)을 처리하고 연속 비용에 대한 하한을 강화하는 것이 식별되었다.