397.29 SAT 기반 계획(SAT Planning) 기법

1. 개요

SAT 기반 계획(SAT Planning)은 고전적 AI 계획 문제를 명제 논리의 충족 가능성(Satisfiability) 문제로 변환하여 해결하는 기법이다. 이 접근법은 계획 문제의 초기 상태, 목표 상태, 행동 연산자를 명제 논리 공식(Propositional Logic Formula)으로 인코딩한 후, SAT 솔버(SAT Solver)를 활용하여 충족 가능한 진리 할당(Truth Assignment)을 탐색함으로써 유효한 계획 시퀀스를 도출하는 것이다. Kautz와 Selman이 1992년에 제안한 SATPLAN 시스템은 이 분야의 선구적 연구로서, 계획 문제를 체계적으로 SAT 인스턴스로 변환하는 방법론을 정립하였다 (Kautz & Selman, 1992).

SAT 기반 계획의 핵심적 강점은 현대 SAT 솔버의 비약적인 성능 향상에 기인한다. DPLL(Davis-Putnam-Logemann-Loveland) 알고리즘에서 출발하여 충돌 기반 절 학습(Conflict-Driven Clause Learning, CDCL) 기법, 단위 전파(Unit Propagation), 비연대적 역추적(Non-Chronological Backtracking) 등의 기술이 통합되면서, 수백만 개의 변수를 포함하는 대규모 SAT 인스턴스도 효율적으로 처리할 수 있게 되었다. 이러한 솔버의 발전은 SAT 기반 계획의 실용성을 크게 확장하였다.

2. SAT 기반 계획의 수학적 기초

2.1 계획 문제의 형식적 정의

고전적 계획 문제는 튜플 \mathcal{P} = \langle \mathcal{F}, \mathcal{A}, \mathcal{I}, \mathcal{G} \rangle로 정의된다. 여기서 \mathcal{F}는 유한한 명제 변수(Fluent)의 집합이고, \mathcal{A}는 행동(Action)의 집합이며, \mathcal{I} \subseteq \mathcal{F}는 초기 상태, \mathcal{G} \subseteq \mathcal{F}는 목표 조건이다. 각 행동 a \in \mathcal{A}는 전제 조건(Precondition) \text{Pre}(a) \subseteq \mathcal{F}, 추가 효과(Add Effect) \text{Add}(a) \subseteq \mathcal{F}, 삭제 효과(Delete Effect) \text{Del}(a) \subseteq \mathcal{F}로 구성된다.

길이 T의 계획이 존재하는지를 판별하기 위해, 시간 단계(Time Step) t = 0, 1, \ldots, T에 걸쳐 상태 변수와 행동 변수를 도입한다:

x_{f,t} \in \{0, 1\}, \quad \forall f \in \mathcal{F}, \; t = 0, \ldots, T

y_{a,t} \in \{0, 1\}, \quad \forall a \in \mathcal{A}, \; t = 0, \ldots, T-1

여기서 x_{f,t} = 1은 시간 t에서 명제 f가 참임을, y_{a,t} = 1은 시간 t에서 행동 a가 실행됨을 나타낸다.

2.2 SAT 인코딩의 절 구성

계획 문제를 CNF(Conjunctive Normal Form) 공식으로 변환하기 위해 다음의 절(Clause) 집합을 구성한다.

초기 상태 절(Initial State Clauses):

\bigwedge_{f \in \mathcal{I}} x_{f,0} \quad \wedge \quad \bigwedge_{f \in \mathcal{F} \setminus \mathcal{I}} \neg x_{f,0}

초기 상태에서 참인 명제는 참으로, 그렇지 않은 명제는 거짓으로 설정한다.

목표 상태 절(Goal State Clauses):

\bigwedge_{f \in \mathcal{G}} x_{f,T}

최종 시간 단계 T에서 목표 조건의 모든 명제가 참이어야 한다.

전제 조건 절(Precondition Clauses):

y_{a,t} \rightarrow x_{f,t}, \quad \forall a \in \mathcal{A}, \; f \in \text{Pre}(a), \; t = 0, \ldots, T-1

이는 CNF로 변환하면 \neg y_{a,t} \vee x_{f,t} 형태가 된다. 즉, 행동 a가 시간 t에서 실행되면 그 전제 조건 f가 해당 시간에 참이어야 한다.

효과 절(Effect Clauses):

추가 효과:
y_{a,t} \rightarrow x_{f,t+1}, \quad \forall a \in \mathcal{A}, \; f \in \text{Add}(a), \; t = 0, \ldots, T-1

삭제 효과:
y_{a,t} \rightarrow \neg x_{f,t+1}, \quad \forall a \in \mathcal{A}, \; f \in \text{Del}(a), \; t = 0, \ldots, T-1

프레임 공리(Frame Axioms):

프레임 공리는 명시적으로 변경되지 않는 명제의 지속성을 보장한다. 설명적 프레임 공리(Explanatory Frame Axioms)는 다음과 같이 표현된다:

x_{f,t} \wedge \neg x_{f,t+1} \rightarrow \bigvee_{a \in \mathcal{A}: f \in \text{Del}(a)} y_{a,t}

\neg x_{f,t} \wedge x_{f,t+1} \rightarrow \bigvee_{a \in \mathcal{A}: f \in \text{Add}(a)} y_{a,t}

이 공리는 어떤 명제가 참에서 거짓으로 변하려면 해당 명제를 삭제하는 행동이 반드시 실행되어야 하며, 거짓에서 참으로 변하려면 해당 명제를 추가하는 행동이 반드시 실행되어야 함을 의미한다.

3. 인코딩 기법의 유형

3.1 선형 인코딩(Linear Encoding)

선형 인코딩은 각 시간 단계에서 정확히 하나의 행동만 실행된다고 가정하는 가장 단순한 형태의 인코딩이다. 상호 배제(Mutual Exclusion) 절을 추가하여 이를 보장한다:

\neg y_{a_i,t} \vee \neg y_{a_j,t}, \quad \forall a_i, a_j \in \mathcal{A}, \; a_i \neq a_j, \; t = 0, \ldots, T-1

이 인코딩은 구현이 간단하지만, 병렬 실행 가능한 행동을 허용하지 않으므로 계획 길이가 불필요하게 길어질 수 있다.

3.2 GraphPlan 기반 인코딩

GraphPlan 기반 인코딩은 GraphPlan 알고리즘에서 생성되는 계획 그래프(Planning Graph)의 구조를 활용한다. 계획 그래프의 상호 배제(Mutex) 관계를 절로 변환하여 검색 공간을 줄인다. 이 인코딩에서는 같은 시간 단계에서 상호 배제 관계에 있는 행동 쌍만 동시에 실행할 수 없도록 제한한다:

\neg y_{a_i,t} \vee \neg y_{a_j,t}, \quad \text{if } \text{mutex}(a_i, a_j, t)

두 행동 a_i와 a_j가 상호 배제 관계에 있는 경우는 다음과 같다:

1. 간섭(Interference): 한 행동의 효과가 다른 행동의 전제 조건을 부정하는 경우
2. 경쟁 요구(Competing Needs): 두 행동의 전제 조건이 상호 배제 관계에 있는 경우
3. 불일치 효과(Inconsistent Effects): 한 행동이 추가하는 명제를 다른 행동이 삭제하는 경우

3.3 ∃-단계 의미론(∃-Step Semantics) 인코딩

Rintanen, Heljanko, 그리고 Niemelä가 제안한 ∃-단계 의미론 기반 인코딩은 병렬 행동 실행에 대한 보다 유연한 규칙을 적용한다 (Rintanen et al., 2006). 이 인코딩에서는 동일한 시간 단계에서 여러 행동이 실행될 수 있되, 행동들 사이에 의존 관계가 없어야 한다는 조건을 부과한다. 구체적으로, 두 행동이 동시에 실행 가능한 조건은 다음과 같다:

• 한 행동의 전제 조건이 다른 행동의 추가 또는 삭제 효과에 포함되지 않아야 한다.
• 두 행동의 효과가 서로 모순되지 않아야 한다.

이 의미론을 적용하면 더 짧은 계획 길이(makespan)로 동일한 해를 표현할 수 있어, SAT 인스턴스의 크기를 줄이고 솔버의 효율성을 향상시킬 수 있다.

4. SAT 솔버와의 연동

4.1 CDCL 기반 SAT 솔버의 작동 원리

현대 SAT 솔버는 CDCL(Conflict-Driven Clause Learning) 패러다임에 기반한다. CDCL 솔버의 핵심 구성 요소는 다음과 같다:

1. 결정(Decision): 미결정 변수에 대해 진리값을 할당한다.
2. 부울 제약 전파(Boolean Constraint Propagation, BCP): 단위 절(Unit Clause)에 대해 단위 전파를 수행하여 강제 할당을 도출한다.
3. 충돌 분석(Conflict Analysis): 충돌이 발생하면 함축 그래프(Implication Graph)를 분석하여 충돌의 원인이 되는 절을 학습한다.
4. 비연대적 역추적(Non-Chronological Backtracking): 학습된 절에 기반하여 적절한 결정 수준으로 역추적한다.

MiniSat, Glucose, CaDiCaL, Kissat 등의 고성능 CDCL 솔버는 수백만 개의 변수와 절을 포함하는 대규모 인스턴스를 효율적으로 처리할 수 있다.

4.2 반복적 심화(Iterative Deepening) 전략

SAT 기반 계획에서는 최적 계획 길이 T^*를 사전에 알 수 없으므로, 반복적 심화 전략을 사용한다. T = 0에서 시작하여 계획 길이를 점진적으로 증가시키면서 SAT 인스턴스를 생성하고 해를 탐색한다:

T ← 0
while true:
    φ_T ← Encode(P, T)
    if SAT(φ_T):
        plan ← ExtractPlan(φ_T)
        return plan
    T ← T + 1

이 전략은 최소 길이의 계획(또는 최소 makespan의 계획)을 보장한다. 그러나 충족 불가능한 인스턴스에 대한 UNSAT 증명이 솔버 실행 시간의 상당 부분을 차지할 수 있다는 점에 유의하여야 한다.

5. 최적성과 계산 복잡도

SAT 기반 계획은 계획의 존재 여부와 최적성에 관해 중요한 이론적 보장을 제공한다.

완전성(Completeness): 유한한 상태 공간에서 계획이 존재하면, 충분히 큰 T에 대해 SAT 인코딩이 충족 가능하게 되므로 반드시 계획을 찾을 수 있다. 상태 공간의 크기가 2^{|\mathcal{F}|}이므로, T의 상한은 2^{|\mathcal{F}|}로 설정할 수 있다.

최적성(Optimality): 반복적 심화 전략과 결합하면, SAT 기반 계획은 최소 길이(또는 최소 makespan)의 계획을 도출한다. 이는 계획 길이에 대한 최적성을 보장하지만, 행동 비용이 비균일(Non-Uniform)한 경우의 비용 최적성은 별도의 인코딩 기법이 필요하다.

계산 복잡도: 고전적 계획 문제는 일반적으로 PSPACE-완전(PSPACE-Complete)이며, SAT 문제는 NP-완전(NP-Complete)이다. 고정된 계획 길이 T에 대한 SAT 인코딩은 다항 시간에 생성 가능하므로, T가 상태 공간 크기에 비해 작은 경우 SAT 기반 접근이 효율적일 수 있다. 그러나 최악의 경우 T가 지수적으로 증가할 수 있어 전체 복잡도는 PSPACE 이하로 보장되지 않는다.

6. 인코딩 크기 최적화 기법

SAT 인코딩의 크기는 솔버 성능에 직접적인 영향을 미치므로, 인코딩을 최소화하는 것이 중요하다.

6.1 컴팩트 프레임 공리(Compact Frame Axioms)

전통적인 프레임 공리는 모든 행동 쌍에 대해 절을 생성하므로 O(|\mathcal{A}|^2 \cdot T)개의 절이 필요하다. 컴팩트 프레임 공리는 보조 변수를 도입하여 절의 수를 O(|\mathcal{A}| \cdot T)로 줄인다. 구체적으로, 명제 f를 변경하는 행동 집합에 대해 보조 변수 z_{f,t}를 도입하고:

z_{f,t} \leftrightarrow \bigvee_{a \in \mathcal{A}: f \in \text{Add}(a)} y_{a,t}

이 변환을 통해 프레임 공리의 절 수를 선형으로 감소시킬 수 있다.

6.2 행동 분할(Action Splitting)

대규모 행동 집합을 갖는 계획 문제에서는 행동 변수를 이진 로그 인코딩으로 표현하여 변수의 수를 줄일 수 있다. |\mathcal{A}|개의 행동에 대해 \lceil \log_2 |\mathcal{A}| \rceil개의 이진 변수로 인코딩하면 변수 수가 크게 감소한다. 그러나 이 방법은 절의 구조가 복잡해져 단위 전파의 효율성이 저하될 수 있으므로 주의가 필요하다.

6.3 대칭 제거(Symmetry Breaking)

계획 문제에서 행동의 순서가 중요하지 않은 경우, 동일한 계획의 순열이 다수의 동치 해(Equivalent Solution)를 생성한다. 대칭 제거 절(Symmetry Breaking Clauses)을 추가하여 이러한 중복 해를 제거하면 검색 공간을 줄일 수 있다. 사전 순서(Lexicographic Order) 기반 대칭 제거가 대표적인 기법이다:

y_{a_i,t} \rightarrow \neg y_{a_j,t+1}, \quad \text{if } a_i > a_j \text{ and } \text{independent}(a_i, a_j)

7. 확장 기법

7.1 비용부 계획(Cost-Optimal Planning)의 SAT 인코딩

비균일 행동 비용을 갖는 계획 문제에 대해, 가중 부분 최대 충족 가능성(Weighted Partial MaxSAT) 또는 의사 부울 최적화(Pseudo-Boolean Optimization) 기법을 적용할 수 있다. 행동 a의 비용을 c(a)라 하면, 총 비용 최소화 문제는 다음과 같이 표현된다:

\min \sum_{t=0}^{T-1} \sum_{a \in \mathcal{A}} c(a) \cdot y_{a,t}

이 문제는 의사 부울 제약(Pseudo-Boolean Constraint)으로 인코딩하여 PB 솔버 또는 MaxSAT 솔버로 해결할 수 있다.

7.2 수치 계획(Numeric Planning)의 SAT 확장

수치 변수(Numeric Variable)를 포함하는 계획 문제에 대해서는 SMT(Satisfiability Modulo Theories) 솔버를 활용한 확장이 연구되고 있다. SMT 솔버는 명제 논리에 선형 산술(Linear Arithmetic), 비선형 산술(Nonlinear Arithmetic) 등의 이론을 결합하여 보다 표현력이 풍부한 계획 문제를 다룰 수 있다.

7.3 조건부 효과(Conditional Effects)의 인코딩

조건부 효과를 갖는 행동은 다음과 같이 인코딩할 수 있다. 행동 a가 조건 c하에서 명제 f를 추가하는 효과를 갖는 경우:

(y_{a,t} \wedge x_{c,t}) \rightarrow x_{f,t+1}

이는 CNF로 변환하면 \neg y_{a,t} \vee \neg x_{c,t} \vee x_{f,t+1} 형태가 된다.

8. SATPLAN 시스템의 발전

SATPLAN 시스템은 여러 세대에 걸쳐 발전해 왔으며, 그 주요 버전과 기여는 다음과 같다:

SATPLAN06은 국제 계획 대회(International Planning Competition, IPC)에서 최적 트랙(Optimal Track) 우승을 달성하여, SAT 기반 계획의 실용성과 경쟁력을 입증하였다 (Kautz et al., 2006).

9. 로봇 임무 계획에서의 적용

로봇 임무 계획에서 SAT 기반 계획은 다음과 같은 시나리오에 적용된다:

다중 로봇 작업 할당: 복수의 로봇에 대한 작업 할당 문제를 SAT로 인코딩하면, 각 로봇-작업 쌍에 대한 이진 변수를 도입하고 자원 제약, 시간 제약, 선후 관계 제약을 절로 표현할 수 있다. 이 접근법은 할당 문제의 조합적 구조를 효과적으로 활용한다.

물류 로봇의 임무 시퀀싱: 창고 환경에서 다수의 피킹(Picking) 작업을 수행하는 물류 로봇의 임무 순서를 결정할 때, SAT 기반 계획은 최소 makespan의 임무 시퀀스를 도출할 수 있다. 각 피킹 작업의 전제 조건(로봇 위치, 적재 상태), 효과(물품 이동, 위치 변화), 시간 제약을 체계적으로 인코딩하여 최적 해를 탐색한다.

감시 정찰 임무의 경로 계획: 복수의 감시 지점을 방문하는 임무 계획에서, 각 시간 단계에서 로봇의 위치와 방문 상태를 명제 변수로 표현하고, 이동 가능성 제약과 에너지 제약을 절로 인코딩하여 최적 순회 경로를 도출할 수 있다.

10. SAT 기반 계획의 장단점 분석

장점:

1. 최적성 보장: 반복적 심화 전략과 결합하면 최소 길이의 계획을 보장한다.
2. 완전성: 해가 존재하면 반드시 찾을 수 있다.
3. 솔버 발전의 활용: 현대 SAT 솔버의 비약적 성능 향상을 직접적으로 활용할 수 있다.
4. 선언적 모델링: 계획 문제를 논리 공식으로 선언적으로 표현하므로, 문제의 구조를 명확하게 파악할 수 있다.
5. 병렬 계획의 자연스러운 표현: GraphPlan 기반 인코딩이나 ∃-단계 의미론을 통해 병렬 행동을 자연스럽게 표현할 수 있다.

단점:

1. 인코딩 크기의 폭발: 행동과 명제의 수가 증가하면 CNF 공식의 크기가 급격히 증가한다. 특히 프레임 공리의 절 수가 행동 수의 제곱에 비례하여 증가할 수 있다.
2. 계획 길이 의존성: 반복적 심화 과정에서 충족 불가능한 인스턴스에 대한 UNSAT 증명에 상당한 시간이 소요될 수 있다.
3. 수치적 제약의 제한: 순수 SAT 인코딩은 연속 변수나 수치적 제약을 직접 다루지 못하며, SMT 확장이 필요하다.
4. 확장성의 한계: 로봇 임무 계획에서 상태 공간이 매우 큰 경우, SAT 인코딩의 크기가 실용적 한계를 초과할 수 있다.

11. 참고 문헌

• Kautz, H. & Selman, B. (1992). “Planning as Satisfiability.” Proceedings of the 10th European Conference on Artificial Intelligence (ECAI-92), pp. 359-363.
• Kautz, H., Selman, B., & Hoffmann, J. (2006). “SatPlan: Planning as Satisfiability.” Working Notes of the 5th International Planning Competition (IPC-5).
• Rintanen, J., Heljanko, K., & Niemelä, I. (2006). “Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search.” Artificial Intelligence, 170(12-13), pp. 1031-1080.
• Davis, M., Logemann, G., & Loveland, D. (1962). “A Machine Program for Theorem-Proving.” Communications of the ACM, 5(7), pp. 394-397.
• Ghallab, M., Nau, D., & Traverso, P. (2004). Automated Planning: Theory and Practice. Morgan Kaufmann.

본 절은 SAT 기반 계획(SAT Planning)의 수학적 기초, 인코딩 기법, 최적화 전략, 및 로봇 임무 계획에서의 적용을 다루었다. v1.0