Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

기술 요약: 유휴 시간 균형을 고려한 B2B 회의 스케줄링을 위한 컴팩트 SAT 및 MaxSAT 인코딩

문제 정의

본 논문은 요청된 쌍방향 회의를 특정 시간대와 장소에 할당해야 하는 조합 최적화 문제인 기업 간(B2B) 회의 스케줄링을 다룹니다. 스케줄링은 다음의 제약 조건을 충족해야 합니다:

• 참가자 중복 불가: 참가자는 두 개의 회의에 동시에 참석할 수 없습니다.
• 장소 용량: 임의의 시간대에 진행되는 회의 수는 가용 장소의 수($K$)를 초 exceed할 수 없습니다.
• 가용성 및 제한 사항: 회의는 요청된 세션, 고정된 슬롯 또는 금지된 슬롯 내에서 발생해야 합니다.
• 선행 관계: 방향성 아크 $(i, j)$는 회의 $i$가 반드시 회의 $j$보다 먼저 발생해야 함을 강제합니다.

본 연구에서 제안하는 목적 함수는 기존의 정식화(주로 "브레이크 그룹"을 최소화하거나 브레이크 횟수의 불균형을 제한함)와 다릅니다. 대신, 본 연구는 최소 두 번 이상의 회의가 배정된 참가자들 사이의 내부 유휴 슬롯 총합의 범위($\Delta I$)를 최소화합니다. 내부 유휴 슬롯은 참가자의 첫 번째 배정된 회의와 마지막 배정된 회의 사이에 존재하는 비어 있는 시간을 의미합니다. 이 지표는 짧은 중단과 긴 대기를 구분함으로써, 균형 잡힌 학술 커리큘럼 문제(BACP)와 유사한 균형 잡힌 부하 분배를 목표로 합니다. 또한 보완적인 지표로서 총 유휴 시간($I_\Sigma$)도 보고됩니다.

방법론

저자들은 기존에 발표된 정식화들에 대해 세 가지 주요 모델링 개선 사항을 통합한 컴팩트한 SAT(불리언 만족 가능성) 및 MaxSAT 인코딩을 제안합니다.

1. 솔루션 보존 도메인 필터링 (전처리):
   CNF를 생성하기 전에, 저자들은 지원되지 않는 할당을 제거하는 전처리 알고리즘(Algorithm 1)을 적용합니다. 여기에는 다음이 통합됩니다:

   • 엔드포인트 경계 필터: 경로를 따라 선행 관계를 전파(직접 아크 또는 추이적 폐쇄 사용).
   • 참가자별 매칭: 특정 참가자에 대해 충돌 없는 스케줄의 일부가 될 수 없는 할당을 제거.
   • 포화 슬롯 전파: 용량이 이미 강제된 할당에 의해 완전히 사용된 슬롯을 제거.
   • 주장: 이 과정은 모든 실행 가능한 스케줄을 보존하면서 도메인 크기를 줄여, 변수와 절(clause)의 수를 줄입니다.

2. 희소 공유 접미사 선행 관계 인코딩 (SPARSESUFFIX):
   선행 관계를 쌍별 절(pairwise clauses)을 사용하여 인코딩하는 대신(이는 도메인 크기에 대해 이차적으로 증가할 수 있음), 저자들은 희소 인코딩을 도입합니다.

   • 이는 제약 조건이 활성화되는 선행 도메인의 고유한 "컷 포인트(cut points)"만을 구체화합니다.
   • 서로 다른 관계 간에 동일한 컷에 대해 보조 변수를 재사용합니다.
   • 이 접근 방식은 쌍별 절과 동등함이 증명되었으나, 특히 도메인 감소와 결합될 때 절의 수를 크게 줄여줍니다.

3. 범위 기반 유휴 시간 목적 함수:
   본 논문은 내부 유휴 슬롯의 범위($\Delta I$)를 최소화하는 정밀한 인코딩을 도입합니다.

   • 각 참가자의 첫 번째 및 마지막 점유 슬롯을 도출합니다.
   • 관련 있는 모든 참가자 간의 최대 및 최소 유휴 횟수 차이를 계산하기 위해 선형 개수의 보조 변수를 사용합니다.

본 연구는 ORG-MAXSAT 정식화(기존 모델의 변형) 및 상용 솔버(Gurobi, CPLEX, CP Optimizer)를 대상으로 위 구성 요소들을 평가합니다. 평가는 126개의 공식 벤치마크 인스턴스와 다양한 선행 밀도를 가진 100개의 파생된 "스트레스(Stress)" 인스턴스를 대상으로 수행되었습니다.

주요 기여

논문은 세 가지 구체적인 기여를 식별합니다:

1. 전처리 절차: CNF 생성 전에 지원되지 않는 할당을 제거하는 필터 통합. 명제 1은 이것이 실행 가능성을 보존함을 증명하며, 실험 결과 할당 변수를 24.1%, 절을 16.2% 감소시킴을 보여줍니다.
2. 희소 공유 접미사 표현: 필요한 선행 도메인 컷 포인트만을 구체화하는 정밀한 인코딩(SPARSESUFFIX). 명제 3은 이것이 쌍별 절과 동등함을 증명합니다. 연구 결과, 도메인 감소가 변수 수를 낮추는 한편, 접미사 공유가 독립적으로 절의 수를 낮춘다는 것을 입증했습니다.
3. B2B 특화 목적 함수: 내부 대기 시간의 불균형을 측정하는 범위 기반 유휴 시간 목적 함수로, 선형 개수의 보조 변수로 인코딩되었습니다.

실험 결과

실험은 7,200초의 시간 제한을 가진 4코어 머신에서 수행되었습니다. 주요 결과는 다음과 같습니다:

• 공식 크기 및 메모리: 적응된 ORG-MAXSAT 베이스라인과 비교하여, 제안된 컴팩트 인코딩은 중앙값 절 개수를 40.3% 감소시켰고 중앙값 피크 메모리 사용량을 55.9% 감소시켰습니다.
• 도메인 감소 영향: 도메인 필터링만으로 할당 변수를 24.1%, 절을 16.2% 감소시켰으며, 이는 공식 크기 감소에서 가장 큰 비중을 차지했습니다.
• 선행 관계 인코딩: SPARSESUFFIX 인코딩은 공식 선행 인스턴스에서 중앙값 절 개수를 0.5%~1.0% 감소시켰으며, 추이적 폐쇄와 결합된 최고 밀도의 파생 인스턴스에서는 최대 **5.5%**까지 감소시켰습니다.
• 솔버 성능:
  • 제안된 세 가지 SAT/MaxSAT 방법(Incremental SAT, Non-Incremental SAT, UWrMaxSAT) 모두 126개의 공식 인스턴스를 모두 해결했습니다.
  • Gurobi(모든 인스턴스를 해결한 유일한 상용 솔버)와 비교했을 때, 제안된 SAT/MaxSAT 방법들은 더 낮은 중앙값 총 소요 시간을 달려냈습니다.
  • Incremental SAT가 완전한 방법들 중 가장 낮은 중앙값 시간(0.227초)을 기록했습니다.
  • CP Optimizer는 가장 낮은 중앙값 시간(0.110초)을 기록했으나, 11개의 인스턴스를 시간 제한 내에 해결하지 못했습니다.

의의 및 주장

본 논문은 제안된 컴팩트 인코딩이 B2B 회의 스케줄링을 위한 기존 불리언 정식화에 비해 상당한 효율성 향상을 제공한다고 주장합니다. 도메인 필터링을 선행 관계 표현으로부터 분리함으로써, 저자들은 도메인 감소가 공식 크기를 줄이는 주요 동력인 반면, 희소 공유 접미사 인코딩은 관계 집합과 독립적으로 추가적인 절 감소를 제공한다는 것을 입양합니다.

본 연구는 새로운 유휴 시간 범위 목적 함수가 짧은 중단과 긴 대기를 구분함으로써 기존의 "브레이크 그룹" 지표보다 더 미세한 스케줄 품질 측정을 제공한다고 단언합니다. 또한, 결과는 현대적인 SAT 및 MaxSAT 솔버가 이러한 컴팩트한 인코딩을 갖추었을 때, 특정 문제 클래스에 대해 주요 MIP 및 CP 솔버보다 중앙값 해결 시간 면에서 더 뛰어난 성능을 보일 수 있으며, 일부 상용 솔버가 타임아웃된 모든 벤치마크 인스턴스를 해결할 수 있음을 나타냅니다.

저자들은 현재 연구가 단일 실행 타이밍에 집중하고 있음을 언급하며, 향후 연구에서 반복적인 타이밍 실행 및 렉시코그래픽 목적 함수( $\Delta I$를 우선적으로 최소화한 후 $I_\Sigma$를 최소화)를 탐구할 수 있을 것이라고 언급하며 겸허한 태도를 유지했습니다.