Voting with ties: Strong impossibilities via SAT solving

Voting rules allow groups of agents to aggregate their preferences in order to reach joint decisions. The Gibbard-Satterthwaite theorem, a seminal result in social choice theory, implies that, when agents have strict preferences, all anonymous, Pareto-optimal, and single-valued voting rules can be strategically manipulated. In this paper, we consider multi-agent voting when there can be ties in the preferences as well as in the outcomes. These assumptions are extremely natural-especially when there are large numbers of alternatives-and enable us to prove much stronger results than in the overly restrictive setting of strict preferences. In particular, we show that (i) all anonymous Pareto-optimal rules where ties are broken according to the preferences of a chairman or by means of even-chance lotteries are manipuiable, and that (ii) all pairwise Pareto-optimal rules are manipuiable, no matter how ties are broken. These results are proved by reducing the statements to finite-yet very large-problems, which are encoded as formulas in prepositional logic and then shown to be unsatisfiable by a SAT solver. We also extracted human-readable proofs from minimal unsatisfiable cores of the formulas in question, which were in turn verified by an interactive higher-order theorem prover.