SAT 기반 플래닝 기법 (SAT-Based Planning Techniques)

1. 개요

SAT 기반 플래닝은 계획 문제를 명제 논리 만족 가능성(Boolean Satisfiability, SAT) 문제로 변환하여, 고성능 SAT 솔버를 활용하여 계획을 탐색하는 기법이다. Kautz와 Selman(1992)이 SATPLAN에서 도입하였다.

2. 원리

2.1 계획을 SAT로 변환

길이 k의 계획이 존재하는지를 판정하기 위해, k 시간 단계에 걸친 명제 논리식을 생성한다.

\Phi_k = \text{Init}(s_0) \wedge \text{Goal}(G, k) \wedge \bigwedge_{t=0}^{k-1} \text{Transition}(t)

• \text{Init}(s_0): 초기 상태를 인코딩하는 절(clause)
• \text{Goal}(G, k): 시각 k에서의 목표 조건
• \text{Transition}(t): 시각 t에서 t+1로의 전이를 인코딩

반복적 심화

k = 0, 1, 2, \ldots로 점진적으로 증가시키며, 만족 가능한 최소 k를 찾는다. 이에 의해 최단(최적) 계획이 보장된다.

SAT 인코딩의 유형

장점과 한계

참고 문헌

• Kautz, H., & Selman, B. (1992). “Planning as Satisfiability.” ECAI 1992.
• Ghallab, M., Nau, D., & Traverso, P. (2016). Automated Planning and Acting. Cambridge University Press.