본 논문은 불가능한(unsatisfiable) 논리식의 불가능성의 근본 원인을 이해하는 데 중요한 최소 불가능 부분집합(MUS: Minimal Unsatisfiable Subset)을 효율적으로 찾는 새로운 프레임워크 MUS-ASP를 제안한다. MUS는 불가능한 상태를 유지하는 최소한의 절(clause) 집합이다. 기존 연구는 주어진 시간 제한 내에 가능한 많은 MUS를 열거하거나, 주어진 불가능한 논리식에 대한 MUS의 총 개수를 세는 두 가지 방향에 초점을 맞추고 있다. MUS-ASP는 Answer Set Programming(ASP)을 기반으로 하며, ASP의 지식 표현 능력을 활용하여 MUS 열거 문제를 해결한다. 실험 결과, MUS-ASP는 특히 하이브리드 솔버와 통합되었을 때 MUS 열거 및 계산 작업에서 효율성을 보이는 것으로 나타났다.
