1316.18 SATPLAN 알고리즘의 원리

1. SATPLAN의 개요

SATPLAN은 Kautz와 Selman(1992, 1996)이 제안한 플래닝 접근법으로, 플래닝 문제를 명제 논리의 충족 가능성(satisfiability, SAT) 문제로 변환하고, SAT 솔버를 사용하여 계획을 추출하는 방식이다. 이 접근은 “플래닝을 탐색이 아닌 추론으로 수행한다“는 패러다임의 전환을 의미하며, 고도로 최적화된 SAT 솔버의 성능을 플래닝에 활용할 수 있다.

2. 기본 원리

SATPLAN의 핵심 원리는 다음의 세 단계로 구성된다:

부호화(Encoding): 플래닝 문제를 시간 단계(time step)별로 명제 논리식(CNF, Conjunctive Normal Form)으로 변환한다.
해결(Solving): SAT 솔버를 사용하여 논리식의 충족 가능 할당(satisfying assignment)을 찾는다.
계획 추출(Plan Extraction): 충족 가능 할당에서 각 시간 단계에 실행되는 액션을 추출한다.

3. 명제 논리 부호화

3.1 변수 정의

시간 단계 $t = 0, 1, \ldots, T$ 에 대해 다음의 명제 변수를 정의한다:

상태 변수 $p_t$ : 명제 $p$ 가 시간 $t$ 에서 참인지 여부
액션 변수 $a_t$ : 액션 $a$ 가 시간 $t$ 에서 실행되는지 여부

3.2 절(Clause) 구성

초기 상태 절: $s_0$ 의 모든 명제를 시간 0에서 참으로 설정
$\bigwedge_{p \in s_0} p_0 \wedge \bigwedge_{p \notin s_0} \neg p_0$

목표 상태 절: 목표 조건의 모든 명제를 시간 $T$ 에서 참으로 설정
$\bigwedge_{g \in \text{goal}} g_T$

전제 조건 절: 액션이 실행되면 전제 조건이 참이어야 한다
$a_t \Rightarrow \bigwedge_{p \in \text{pre}(a)} p_t$

효과 절: 액션이 실행되면 효과가 다음 시간 단계에 반영된다
$a_t \Rightarrow \bigwedge_{p \in \text{eff}^+(a)} p_{t+1}$
$a_t \Rightarrow \bigwedge_{p \in \text{eff}^-(a)} \neg p_{t+1}$

프레임 공리: 명제가 변하지 않으려면 변경하는 액션이 실행되지 않아야 한다
$(p_t \wedge \neg p_{t+1}) \Rightarrow \bigvee_{a: p \in \text{eff}^-(a)} a_t$
$(\neg p_t \wedge p_{t+1}) \Rightarrow \bigvee_{a: p \in \text{eff}^+(a)} a_t$

상호 배제 절: 간섭하는 액션 쌍이 동시에 실행되지 않도록 한다
$\neg a_t \vee \neg a'_t \quad \text{(mutex 액션 쌍에 대해)}$

4. 반복적 심화

SATPLAN은 시간 단계 $T$ 를 1부터 점진적으로 증가시키면서 SAT 문제를 생성하고 풀이한다:

SATPLAN(problem):
    FOR T = 1, 2, 3, ...:
        formula ← ENCODE(problem, T)
        assignment ← SAT_SOLVER(formula)
        IF assignment ≠ UNSATISFIABLE:
            RETURN EXTRACT_PLAN(assignment, T)
    RETURN "No plan exists"

이 반복적 접근에 의해, SATPLAN은 최소 시간 단계(최소 병렬 길이)의 계획을 보장한다.

5. SAT 솔버와의 통합

현대 SAT 솔버(MiniSat, Glucose, CaDiCaL 등)는 DPLL 알고리즘과 CDCL(Conflict-Driven Clause Learning) 기법의 발전으로 수백만 변수를 포함하는 문제를 효율적으로 처리할 수 있다. SATPLAN은 이러한 SAT 솔버의 성능 향상에 직접적으로 수혜를 받는다.

6. SATPLAN의 특성

6.1 장점

최적 병렬 계획: 최소 시간 단계의 계획을 보장한다.
SAT 솔버 발전의 수혜: SAT 솔버의 성능 향상이 플래닝 성능에 직접 반영된다.
해 부재 증명: SAT 문제가 충족 불가능하면 해당 길이의 계획이 존재하지 않음이 증명된다.

6.2 단점

부호화 크기: 시간 단계와 도메인 크기에 비례하여 CNF 공식의 크기가 급증한다.
수치 플루언트 미지원: 순수 명제 논리에 기반하므로 수치 변수를 직접 처리하지 못한다.
긴 계획에 비효율: 최적 계획의 길이가 긴 도메인에서 부호화 크기가 폭발적으로 증가한다.

7. 현대적 발전

Madagascar(Rintanen, 2014) 등의 현대 SAT 기반 플래너는 부호화 효율을 크게 개선하고, 병렬 계획 생성에서 탁월한 성능을 보인다. IPC에서 SAT 기반 플래너가 특정 도메인에서 휴리스틱 탐색 플래너를 초월하는 성능을 보이기도 한다.

8. 참고 문헌

Kautz, H. & Selman, B. (1992). “Planning as Satisfiability.” Proceedings of the 10th European Conference on Artificial Intelligence (ECAI), 359–363.
Kautz, H. & Selman, B. (1996). “Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search.” Proceedings of AAAI, 1194–1201.
Rintanen, J. (2014). “Madagascar: Scalable Planning with SAT.” IPC 2014 Planner Abstracts.
Ghallab, M., Nau, D., & Traverso, P. (2004). Automated Planning: Theory and Practice. Morgan Kaufmann.