Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting

README.md for the code used in the paper Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting by Wesley H. Holliday, Chase Norman, Eric Pacuit, and Saam Zahedian.

Notebooks

The three main notebooks that contain the proofs of Propositions A.12 and B.3:

1. Majoritarian.ipynb: This notebook contains the proof of Proposition A.12 using a SAT solver.

2. Pairwise.ipynb: This notebook contains the proof of Proposition B.3. using a SAT solver.

3. UniquelyRanked.ipynb: This notebook contains verifications that the profiles used in the proof of Proposition 2.13 are uniquely weighted and uniquely ranked.

The following notebooks contain the code to reproduce generation of the canonical (weighted) tournaments and finding a minimal set of (weighted) tournaments needed for the impossibility theorems:

1. CanonicalObjects.ipynb: This notebook shows how to generate the canonical weak tournaments and canonical weighted tournaments.

2. MinSetTournaments.ipynb: This notebook shows how to find minimal sets of graphs needed to provied Propositions A.12 and B.3.

Other Files/Directories

1. graphs_for_impossibilities/all_gs_mus_dict_majoritarian.pkl: A minimal set of weighted tournaments needed to prove Proposition A.12.

2. graphs_for_impossibilities/wts_for_impossibility.pkl: A minimal set of weighted tournaments needed to prove Proposition B.3.

3. graphs_for_impossibilities/all_gs_mus_dict_pairwise.pkl: Another weighted tournaments needed to prove Proposition B.3.

4. mus_cnfs/ar_bg_output.cnf: MUS generated by PicoMUS to prove Proposition A.12

5. mus_cnfs/qr_bg_output.cnf: MUS generated by PicoMUS to prove Proposition B.3

6. tourns/tourns_{nc}.pkl: For $nc\in {2, 3, 4, 5, 6}$, tourns/tourns_{nc}.pkl is a pickle file containing all the canonical tournaments for $nc$ candidates.

7. weak_tourns/weak_tourns_{nc}.pkl: For $nc\in {2, 3, 4, 5, 6}$, weak_tourns/weak_tourns_{nc}.pkl is a pickle file containing all the canonical weak tournaments for $nc$ candidates.

8. weighted_tourns/weighted_tourns_{nc}.pkl: For $nc\in {2, 3, 4}$, weighted_tourns/weighted_tourns_{nc}.pkl is a pickle file containing all the canonical weighted tournaments for $nc$ candidates with weights from the set ${2, 4, 6, 8, 10, 12}$.

9. A verification of the SAT encoding using the Lean interactive theorem prover is available at https://github.com/chasenorman/verified-encodings-social-choice.

Requirements

All the code is written in Python 3. The notebooks use the following libraries:

• Preferential Voting Tools
• The notebooks and the pref_voting library is built around a full SciPy stack: MatPlotLib, Numpy, Pandas, numba, networkx, and tabulate
• tqdm.notebook
• PySAT