Satisfiability for Knowing How over Linear Plans is NP-complete

문제 진술
본 논문은 "어떻게 하는지 (knowing-how)" 주장을 표현하도록 설계된 모달 논리 $\mathfrak{L}(\mathsf{Kh})$의 만족 가능성 문제 (satisfiability problem) 에 대한 계산 복잡성을 조사한다. 왕 (Wang, 2015, 2018) 이 도입한 이 논리는 모달리티 $\mathsf{Kh}(\varphi, \psi)$를 통해 전제 조건 $\varphi$가 주어졌을 때 에이전트가 목표 $\psi$를 달성할 수 있는 능력을 포착한다. 의미론적으로, 이는 $\varphi$를 만족하는 모든 상태로부터 시작하여 $\psi$를 만족하는 상태로 이끄는 강하게 실행 가능한 (strongly executable) 선형 계획 (즉, 실행 경로에 관계없이 완성이 보장되는 계획) 이 존재할 때 성립한다. 이 논리는 인공지능과 자동 계획에서의 전략 추론을 위한 기초적이지만, 그 정확한 계산 복잡성은 미해결 상태였다. Areces 등 (2023) 의 이전 연구는 $\mathsf{NP}^{\mathsf{NP}}$(다항식 위계의 두 번째 수준인 $\Sigma^P_2$) 를 상한으로 설정하여, 명제 논리에서 유도된 알려진 $\mathsf{NP}$-hardness 와 이 상한 사이의 간극을 남겼다.

방법론
저자들은 $\mathfrak{L}(\mathsf{Kh})$에서 전역 보편 모달리티 (global universal modalities) 가 추가된 모달 논리 S5 의 문법적 변형인 더 간단한 논리 $\mathfrak{L}(\mathsf{A})$로의 직접적인 번역을 개발함으로써 이 복잡성 간극을 해결한다. 핵심 방법론적 혁신은 이전 접근법에서 사용되었던 불만족성 (unsatisfiability) 검사를 피하는 것으로, 이는 더 높은 복잡성 상한을 필요로 했다.

증명은 다음과 같은 기술적 단계를 거쳐 진행된다:

1. 분해: 임의의 $\mathfrak{L}(\mathsf{Kh})$ 공식의 만족 가능성은 "원자 (atoms)"들의 결합의 만족 가능성 검사로 축소된다. 여기서 원자는 $\mathsf{Kh}(\psi, \chi)$ 형태의 양적 원자와 $\neg\mathsf{Kh}(\psi, \chi)$ 형태의 음적 원자로 구성된다.
2. $\mathfrak{L}(\mathsf{A})$로의 번역:
   • 양적 원자: 양적 원자들의 결합은 대응하는 $\mathfrak{L}(\mathsf{A})$ 공식이 만족 가능할 때에만 만족 가능한 것으로 보인다. 이 공식은 각 $\mathsf{Kh}(\psi_i, \chi_i)$에 대해 전제 조건 $\psi_i$가 어디서나 거짓 ($\mathsf{A}\neg\psi_i$) 이거나, 혹은 후제 조건 $\chi_i$가 어딘가에서 참 ($\mathsf{E}\chi_i$) 임을 주장한다.
   • 음적 원자: 음적 원자들의 결합은 존재적 공식 $\mathsf{E}(\psi_j \land \neg\chi_j)$의 만족 가능성으로 축소된다. 이는 각 부정된 "어떻게 하는지" 주장에 대해 전제 조건은 성립하지만 후제 조건은 성립하지 않는 상태가 존재함을 보장한다.
   • 상호작용 처리: 양적 원자와 음적 원자 간의 상호작용을 처리하기 위해 저자들은 인덱스의 분할과 반사적 - 추이적 폐쇄 (reflexive-transitive closure) 관계를 도입한다. 이를 통해 양적 원자에 대한 증명 계획 (witness plans) 과 음적 원자의 요구 사항 사이의 잠재적 모순을 포착하는 복잡한 $\mathfrak{L}(\mathsf{A})$ 공식을 구성할 수 있다.
3. 복잡성 축소: $\mathfrak{L}(\mathsf{A})$(S5 와 동등) 에 대한 만족 가능성 문제가 $\mathsf{NP}$-완전임이 알려져 있으며 (Ladner, 1977), 번역이 만족 가능성을 보존하면서 크기에 있어 다항식적으로 유지되므로, $\mathfrak{L}(\mathsf{Kh})$의 만족 가능성은 $\mathsf{NP}$ 내에 위치한다.

주요 기여 및 결과

• 최적의 복잡성 상한: 주요 결과는 $\mathfrak{L}(\mathsf{Kh})$의 만족 가능성 문제가 $\mathsf{NP}$-완전이라는 것이다. 이는 이전의 $\Sigma^P_2$ 상한을 정교화하여 정확한 복잡성 클래스를 확립한다.
• 다항식 크기 모델 성질: $\mathsf{NP}$ 소속성 증명의 직접적인 결과로서, 논문은 공식이 만족 가능하면 공식 길이에 대해 다항식 크기의 모델 (레이블이 붙은 전이 시스템) 을 가진다고 확립한다. 구체적으로, 상태 공간의 크기는 $O(|\varphi|^3)$으로 제한된다.
• 기술적 단순화: 저자들은 S5 기반 논리로의 직접적인 번역을 제공하여, 이전의 $\mathsf{NP}^{\mathsf{NP}}$ 알고리즘을 특징지었던 불만족성 검사의 필요성을 제거한다.
• 표현력: 논문은 레이블이 붙은 전이 시스템 위에서 $\mathfrak{L}(\mathsf{Kh})$가 $\mathfrak{L}(\mathsf{A})$보다 엄격하게 더 표현력이 있음을 확인함으로써, $\mathsf{NP}$-완전 만족 가능성을 가진 것으로 알려진 논리들의 최전선을 확장한다.

의의 및 주장
본 논문은 "어떻게 하는지" 논리 연구에서 중요한 복잡성 간극을 해소했다고 주장한다. 저자들이 강조한 주목할 만한 관찰은, $\mathsf{Kh}$의 의미론적 정의가 *증명 계획 (witness plans)*의 존재와 강한 실행 가능성 개념에 크게 의존함에도 불구하고, 이러한 구조적 특징들은 만족 가능성 문제 자체에서는 역할을 하지 않는다는 점이다. 이러한 특징들은 $\mathfrak{L}(\mathsf{A})$로의 번역 과정에서 효과적으로 추상화된다.

이 결과는 $\mathfrak{L}(\mathsf{Kh})$의 모델 체킹 문제가 $\mathsf{PSPACE}$-완전임이 알려져 있음 (Demri and Fervari, 2023) 에 따라 만족 가능성은 $\mathsf{NP}$에 속하지만 모델 체킹은 $\mathsf{PSPACE}$-완전이라는 이러한 분기 현상이 "진실로 드문 현상"임을 지적함으로써 대조를 이룬다. 논문은 결론적으로 증명 전략이 효과적인 이론적 절차를 제공하지만, 향후 연구는 자동 추론을 위한 이 절차의 구현과 실용적 적용성 평가, 그리고 다른 "어떻게 하는지" 논리 변형으로의 전략 확장에 초점을 맞춰야 한다고 제안한다.