Identifying k-Majority Digraphs via SAT Solving

Many voting rules—including single-valued, set-valued, and probabilistic rules—only take into account the majority di-graph. The contribution of this paper is twofold. First, we provide a surprisingly efficient implementation for comput-ing the minimal number of voters that is required to induce a given digraph. This implementation relies on an encoding of the problem as a Boolean satisfiability (SAT) problem which is then solved by a SAT solver. Secondly, we exper-imentally evaluate how many voters are required to induce the majority digraphs of real-world and generated prefer-ence profiles. Our results are based on datasets from the PrefLib library and preferences generated using stochastic models such as impartial culture, impartial anonymous cul-ture, Mallows mixtures, and spatial models. It turns out that all tournaments checked in these experiments can be induced by at most five voters whereas all other digraphs can be induced by at most eight voters. We also confirm a conjecture by Shepardson and Tovey by verifying that all tournaments with less than eight vertices can be induced by three voters