본 논문은 주어진 도메인에서 일차 논리 문장의 가중치 모델 합을 계산하는 WFOMC(Weighted First-Order Model Counting) 문제를 다룬다. 특히, 증거(evidence)를 기반으로 WFOMC를 조건부로 계산하는 것은 도메인 크기에 대해 다항 시간 내에 불가능하다는 것이 밝혀졌다. 본 연구는 가이프만 그래프(Gaifman graph)가 제한된 트리의 너비(treewidth)를 갖는 경우, 이진 증거(binary evidence)를 조건으로 하는 WFOMC 문제를 다룬다. 저자들은 $\text{FO}^2$ 및 $\text{C}^2$와 같은 2변수 단편에 대해 도메인 크기에서 다항 시간 내에 WFOMC를 계산하는 알고리즘을 제시한다. 또한, 제한된 트리의 너비와 차수를 갖는 그래프에서 안정적인 좌석 배치 문제를 해결하여 알고리즘의 유용성을 입증했다. 마지막으로, 기존 모델 계산 솔버와 비교한 실험을 통해 알고리즘의 확장성을 보여주었다.
