부분 결과서지만 확인
Automating Resolution is NP-HardAlbert Atserias, Moritz Müller · 2020Journal of the ACM 67(5), 2020 (논문별 쪽 1–17) · 학회 발표 FOCS 2019 (60th Annual IEEE Symposium on Foundations of Computer Science), 498–509쪽 · arXiv:1904.02991가장 짧은 반박보다 다항식 배만큼만 긴 분해(resolution) 반박을 찾는 문제가 NP-난해임을 보인 논문이다. 곧 P = NP 가 아닌 한 분해 증명을 효율적으로 찾아 주는 알고리즘은 없다. SAT 풀이기가 기대는 증명 체계에서조차 「짧은 증명이 있어도 찾기는 어렵다」는 것을 보여, 증명 탐색과 P 대 NP 의 관계를 다루는 글이 인용한다.
확인:학술지판과 학회판은 Crossref 등록 기록으로, 초록은 Crossref 와 arXiv 초록 페이지로 확인했다.