1316.20 SAT 솔버를 이용한 계획 추출

1. SAT 솔버의 역할

SATPLAN에서 SAT 솔버는 플래닝 문제를 부호화한 CNF(Conjunctive Normal Form) 공식의 충족 가능성을 판정하고, 충족 가능한 경우 충족 할당(satisfying assignment)을 반환하는 핵심 엔진이다. 반환된 할당에서 각 시간 단계의 실행 액션을 추출함으로써 계획이 완성된다.

2. 현대 SAT 솔버의 핵심 기법

2.1 DPLL 알고리즘

Davis-Putnam-Logemann-Loveland(DPLL) 알고리즘은 SAT 솔버의 기본 골격이다:

DPLL(formula, assignment):
    formula ← UNIT_PROPAGATION(formula, assignment)
    IF formula contains empty clause: RETURN UNSATISFIABLE
    IF formula is empty: RETURN assignment

    variable ← SELECT_VARIABLE(formula)
    IF DPLL(formula ∧ variable, assignment ∪ {variable}): RETURN result
    IF DPLL(formula ∧ ¬variable, assignment ∪ {¬variable}): RETURN result
    RETURN UNSATISFIABLE

2.2 CDCL(Conflict-Driven Clause Learning)

현대 SAT 솔버의 핵심 기법으로, 탐색 중 발견된 충돌(conflict)을 분석하여 새로운 학습 절(learned clause)을 추가하고, 비연대기적 역추적(non-chronological backtracking)을 수행한다. 이 기법은 SAT 솔버의 성능을 수 배에서 수십 배까지 향상시킨다.

2.3 주요 SAT 솔버

3. 충족 할당에서 계획 추출

SAT 솔버가 반환한 충족 할당(model)에서 계획을 추출하는 과정:

EXTRACT_PLAN(assignment, T):
    plan ← []
    FOR t = 0 TO T-1:
        actions_at_t ← []
        FOR EACH ground action a:
            IF assignment[a^t] = TRUE:
                actions_at_t.append(a)
        ;; no-op 액션 제외
        plan.append(filter_noops(actions_at_t))
    RETURN plan

각 시간 단계에서 TRUE로 할당된 액션 변수가 해당 시간에 실행되는 액션이다. no-op(무행동) 액션은 프레임 유지를 위한 것이므로 실제 계획에서 제외한다.

4. 병렬 계획과 순차 계획

SAT 기반 부호화에서 각 시간 단계에 여러 액션이 동시에 TRUE일 수 있다(상호 배제 절에 의해 비간섭 액션만). 이에 따라 추출되는 계획은 병렬 계획(parallel plan)이다:

시간 0: {move(r1, wp1, wp2), move(r2, wp3, wp4)}
시간 1: {pick(r1, box1, wp2), pick(r2, box2, wp4)}
시간 2: {move(r1, wp2, wp5), move(r2, wp4, wp5)}

순차 계획이 필요하면 병렬 계획을 선형화(linearization)한다. 동일 시간 단계의 비간섭 액션은 임의의 순서로 배치할 수 있다.

5. 반복적 탐색과 최적성

SATPLAN은 시간 단계 T를 1부터 점진적으로 증가시키며 SAT 문제를 풀이한다:

FOR T = 1, 2, 3, ...:
    formula ← ENCODE(problem, T)
    result ← SAT_SOLVER(formula)
    IF result = SATISFIABLE:
        RETURN EXTRACT_PLAN(result.model, T)
    ;; T에서 UNSATISFIABLE이면 T+1로 시도

처음 충족 가능해지는 T가 최소 병렬 길이이므로, SATPLAN은 최소 makespan 계획을 보장한다.

6. 증분적 SAT 풀이

시간 단계를 증가시킬 때마다 전체 CNF를 새로 생성하는 대신, 이전 수준의 절을 유지하면서 새로운 수준의 절만 추가하는 증분적(incremental) 접근이 가능하다. 이는 솔버의 학습 절을 재활용하여 효율성을 향상시킨다.

7. 계획 추출의 검증

추출된 계획의 유효성을 독립적으로 검증하기 위해, 상태 시뮬레이션을 수행한다:

VERIFY_PLAN(plan, s0, goal):
    s ← s0
    FOR EACH action_set in plan:
        FOR EACH action a in action_set:
            IF s ⊭ pre(a): RETURN INVALID
            s ← γ(s, a)
    IF s ⊨ goal: RETURN VALID
    RETURN INVALID

SAT 기반 부호화가 정확하면 검증은 항상 성공하지만, 구현 오류 검출을 위해 검증 단계를 포함하는 것이 권장된다.

8. 참고 문헌

• Kautz, H. & Selman, B. (1996). “Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search.” Proceedings of AAAI, 1194–1201.
• Eén, N. & Sörensson, N. (2003). “An Extensible SAT-solver.” SAT 2003, LNCS 2919, 502–518.
• 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.