1316.19 플래닝 문제의 명제 논리 부호화

1. 부호화의 목적

플래닝 문제의 명제 논리 부호화(propositional logic encoding)는 PDDL로 정의된 플래닝 문제를 명제 논리의 충족 가능성(SAT) 문제로 변환하는 과정이다. 변환된 SAT 문제의 충족 가능 할당(satisfying assignment)이 원래 플래닝 문제의 유효한 계획에 대응한다(Kautz & Selman, 1992).

2. 명제 변수의 정의

주어진 계획 길이(시간 단계 수) $T$ 에 대해 다음의 명제 변수를 정의한다.

2.1 상태 변수

각 그라운드 술어 인스턴스 $p$ 와 시간 단계 $t \in \{0, 1, \ldots, T\}$ 에 대해:

$p^t \in \{\text{TRUE}, \text{FALSE}\}$

$p^t$ 가 TRUE이면 시간 $t$ 에서 명제 $p$ 가 참임을 의미한다.

2.2 액션 변수

각 그라운드 액션 $a$ 와 시간 단계 $t \in \{0, 1, \ldots, T-1\}$ 에 대해:

$a^t \in \{\text{TRUE}, \text{FALSE}\}$

$a^t$ 가 TRUE이면 시간 $t$ 에서 액션 $a$ 가 실행됨을 의미한다.

3. CNF 절의 구성

3.1 초기 상태 절

;; 초기 상태에서 참인 명제: 긍정 단위 절
p^0                          (∀ p ∈ s₀)

;; 초기 상태에서 거짓인 명제: 부정 단위 절
¬p^0                         (∀ p ∉ s₀)

3.2 목표 상태 절

;; 최종 시간 단계에서 목표 명제가 참
g^T                          (∀ g ∈ goal)

3.3 전제 조건 절

액션이 실행되면 전제 조건이 참이어야 한다:

$a^t \Rightarrow p^t \quad \equiv \quad \neg a^t \vee p^t$

각 액션 $a$ 의 전제 조건 리터럴 $p$ 에 대해 절 $(\neg a^t \vee p^t)$ 를 생성한다.

3.4 효과 절

액션이 실행되면 추가 효과가 다음 시간에 참이 된다:

$a^t \Rightarrow p^{t+1} \quad \equiv \quad \neg a^t \vee p^{t+1}$

삭제 효과:

$a^t \Rightarrow \neg p^{t+1} \quad \equiv \quad \neg a^t \vee \neg p^{t+1}$

3.5 프레임 공리 절

명제가 변하려면 변경하는 액션이 실행되어야 한다:

설명적 프레임 공리(Explanatory Frame Axioms):

참에서 거짓으로 변하려면 삭제하는 액션이 필요:
$(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$

CNF로 변환:
$\neg p^t \vee p^{t+1} \vee a_1^t \vee a_2^t \vee \ldots$

3.6 상호 배제 절

간섭하는 액션 쌍이 동시에 실행되지 않도록 한다:

$\neg a_1^t \vee \neg a_2^t \quad \text{(mutex 액션 쌍에 대해)}$

4. 부호화의 크기

변수 수와 절 수의 근사적 분석:

요소	변수/절 수
상태 변수	$O(\lvert\mathcal{F}\rvert \cdot T)$
액션 변수	$O(\lvert\mathcal{A}\rvert \cdot T)$
초기/목표 절	$O(\lvert\mathcal{F}\rvert + \lvert g\rvert)$
전제 조건 절	$O(\lvert\mathcal{A}\rvert \cdot k_{\text{pre}} \cdot T)$
효과 절	$O(\lvert\mathcal{A}\rvert \cdot k_{\text{eff}} \cdot T)$
프레임 공리	$O(\lvert\mathcal{F}\rvert \cdot T)$
상호 배제 절	$O(\lvert\mathcal{A}\rvert^2 \cdot T)$

$T$ 가 증가하면 부호화 크기가 선형적으로 증가한다.

5. 부호화 효율화 기법

5.1 컴팩트 프레임 공리

설명적 프레임 공리는 전통적 프레임 공리보다 절의 수가 적다. 각 명제에 대해 “변하지 않으려면“이 아닌 “변하려면“을 부호화하므로 효율적이다.

5.2 적용 가능 액션 제한

도달 가능성 분석을 통해 각 시간 단계에서 적용 불가능한 액션을 사전에 제거하여 변수와 절의 수를 줄인다.

5.3 병렬 실행 모델

상호 배제가 아닌 액션은 동일 시간 단계에서 병렬로 실행될 수 있도록 부호화한다. 이는 필요한 시간 단계 수 $T$ 를 줄여 부호화 크기를 감소시킨다.

6. 계획 추출

SAT 솔버가 충족 가능 할당을 반환하면, 각 시간 단계 $t$ 에서 $a^t = \text{TRUE}$ 인 액션을 추출하여 계획을 구성한다:

$\pi = \{a \mid a^t = \text{TRUE}, t = 0, 1, \ldots, T-1\}$

no-op 액션(프레임 유지 액션)은 계획에서 제외한다.

7. 참고 문헌

Kautz, H. & Selman, B. (1992). “Planning as Satisfiability.” Proceedings of ECAI, 359–363.
Kautz, H. & Selman, B. (1996). “Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search.” Proceedings of AAAI, 1194–1201.
Rintanen, J. (2012). “Planning as Satisfiability: Heuristics.” Artificial Intelligence, 193, 45–86.
Ghallab, M., Nau, D., & Traverso, P. (2004). Automated Planning: Theory and Practice. Morgan Kaufmann.