1316.42 Madagascar 플래너의 SAT 기반 접근

1. Madagascar의 개요

Madagascar는 Rintanen(2014)이 개발한 SAT 기반 플래너로, SATPLAN의 현대적 발전형이다. 효율적인 CNF 부호화, 증분적 SAT 풀이, 병렬 계획 최적화를 통해 IPC에서 최고 수준의 성능을 보이는 SAT 기반 플래너이다.

2. 핵심 기법

2.1 효율적 부호화

Madagascar는 전통적 SATPLAN의 부호화를 크게 개선하였다:

1. ∃-step 부호화: 각 시간 단계에서 비간섭 액션의 병렬 실행을 허용하면서, 부호화 크기를 최소화하는 정교한 상호 배제 절을 사용한다.
2. 불필요한 변수 제거: 도달 가능성 분석을 통해 각 시간 단계에서 불가능한 액션과 명제를 사전에 제거하여 CNF 크기를 줄인다.
3. 프레임 공리 최적화: 설명적 프레임 공리의 변형을 사용하여 절 수를 줄인다.

2.2 증분적 SAT 풀이

시간 단계 T를 증가시킬 때, 이전 수준의 절과 학습 정보를 재활용하는 증분적 SAT 풀이를 사용한다. 이는 각 반복에서 전체 CNF를 새로 생성하는 것보다 효율적이다.

2.3 병렬 계획 최적화

Madagascar는 최소 makespan(최소 병렬 시간 단계)의 계획을 보장한다. 이는 다중 로봇 시스템에서 임무 수행 시간 최소화에 적합하다.

3. IPC에서의 성능

Madagascar는 IPC의 여러 트랙에서 우수한 성능을 보였다:

특히 병렬 구조가 중요한 도메인(물류, 다중 에이전트 등)에서 휴리스틱 탐색 플래너를 초월하는 성능을 보이기도 한다.

4. 강점과 약점

4.1 강점

1. 최적 병렬 계획: makespan 최적 계획을 보장한다.
2. 해 부재 증명: UNSAT 판정에 의해 특정 길이의 계획이 존재하지 않음을 증명할 수 있다.
3. SAT 솔버 발전의 수혜: CDCL 솔버의 성능 향상에 직접 수혜를 받는다.
4. 병렬 도메인에서의 우수성: 자연스러운 병렬 계획 생성으로 다중 로봇 도메인에 적합하다.

4.2 약점

1. 수치 플루언트 미지원: 순수 명제 부호화에 기반하므로 수치 변수를 직접 처리하지 못한다.
2. 긴 계획에 비효율: 최적 계획의 길이가 긴 도메인에서 부호화 크기가 급증한다.
3. 듀레이티브 액션 미지원: PDDL 2.1의 시간적 기능을 직접 처리하지 못한다.

5. 로봇 도메인에서의 적용 가능성

Madagascar는 다음의 로봇 도메인에서 효과적이다:

• 순수 논리적 플래닝 (수치 제약 없이)
• 다중 로봇의 병렬 태스크 할당
• 최적 makespan이 중요한 임무 계획

PlanSys2에서 Madagascar를 직접 사용하려면 외부 플래너로 설정해야 하며, PDDL 2.1 기능이 필요한 도메인에서는 POPF가 더 적합하다.

6. 참고 문헌

• Rintanen, J. (2012). “Planning as Satisfiability: Heuristics.” Artificial Intelligence, 193, 45–86.
• Rintanen, J. (2014). “Madagascar: Scalable Planning with SAT.” IPC 2014 Planner Abstracts.
• Kautz, H. & Selman, B. (1996). “Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search.” Proceedings of AAAI, 1194–1201.