Wesley H. Holliday, Milan Mosse, Chase Norman, Eric Pacuit, Cynthia Wang
개요
본 논문은 선호 집계에서 다수결 사이클 해결 알고리즘에 대한 연구를 다룬다. 특히, Split Cycle(SC) 방법의 개선판인 Stable Voting과 Simple Stable Voting (SSV)의 관계를 분석한다. 저자들은 SSV가 SC의 개선판이라는 가설을 6개 이하의 대안에 대해서는 증명하고, 7개 이상의 대안에 대해서는 반증하였다. 증명 및 반례 생성에 SAT solving을 활용했다.
시사점, 한계점
•
SSV가 SC의 개선판이라는 가설은 대안의 수에 따라 달라짐을 증명.
•
6개 이하의 대안에 대한 증명은 전통적인 수학적 추론으로, 6개 및 7개 이상의 대안에 대한 증명 및 반례는 SAT solving을 사용하여 얻음.
•
SAT encoding을 활용하여, 승리 마진의 크기 순서에 따라 승자를 결정하는 모든 투표 방식의 특성을 테스트할 수 있는 가능성을 제시.
•
SAT solving 기반의 증명 및 반례 구성은 복잡성이 높은 문제 해결에 효과적임을 보여줌.