고전 계획(Classical Planning) 분야의 팩터드 태스크(Factored Task System, FTS) 표현을 SAT(Boolean Satisfiability) 풀이 문제로 변환·인코딩하는 방법론을 체계적으로 비교한 연구가 arXiv에 공개됐다(논문 번호 2605.30563). FTS는 SAS+를 확장한 고전 계획 표현 형식으로, 제한적 형태의 논리합 전제조건·조건부 효과·비결정론적 선택을 지원해 기존 STRIPS나 SAS+보다 더 간결하게 작업을 표현할 수 있다. 그러나 기존 FTS 계획 솔루션은 휴리스틱 탐색 방식에 한정돼 있었으며, SAT 기반 접근은 시도되지 않았다.
연구팀은 FTS를 SAT로 인코딩하는 여러 방식을 제안하고, 팩터드 전이 관계를 명제 논리로 변환하는 전략별 성능 차이를 실험으로 분석했다. 또한 다양한 수준에서 병렬성을 활용하는 방법과, 일반적인 태스크 변환이 SAT 기반 계획기 성능에 미치는 영향도 함께 연구했다. 어떤 인코딩 방식이 성능을 높이고 어떤 방식이 오히려 저하시키는지를 구체적으로 규명한 점이 핵심 기여다.
이 연구의 학문적 의의는 AI 계획 이론과 SAT 풀이 기술을 연결하는 다리 역할에 있다. SAT 솔버는 수십 년간 형식 검증·하드웨어 설계·소프트웨어 모델 체킹 분야에서 비약적으로 발전했으며, 이 성과를 AI 계획에 이식하려는 시도는 계획기의 완전성 보장과 확장성 개선에 기여할 수 있다. FTS가 표현할 수 있는 비결정론적 환경이나 조건부 효과는 실제 로봇 작업 계획이나 물류 최적화 문제에서 자주 등장하는 구조이므로, 이번 연구의 결과는 이론적 틀을 넘어 실응용 연구의 기반이 될 수 있다.
국내 AI 계획·형식 검증 분야 연구자에게 이 논문은 기존 FTS 계획기에 SAT 기반 추론 엔진을 접목하는 출발점으로 활용 가능하다. 산업 자동화나 로봇 제어처럼 복잡한 조건부 행동 계획이 필요한 분야의 개발팀에도 SAT 기반 계획기의 적용 가능성과 인코딩 선택 기준을 파악하는 데 도움이 된다. 병렬 처리를 통한 SAT 풀이 가속화 연구가 함께 진행된 만큼, 대규모 계획 문제에 대한 실용적 접근 경로도 모색할 수 있다.
