generalizing-sat

This is repo contains code accompanying the Appendix of the paper "An approach to generalizing some impossibility theorems in social choice" by Wesley H. Holliday, Eric Pacuit, and Saam Zahedian.

1. In Canonical Tournaments, we construct the canonical tournament objects used in our later analysis. The outputs of this notebook are produced in /tourns, /weak_tourns, and /weighted_weak_tourns.

2. In SAT Solving for C1 Methods, we use a SAT solver to prove that anonymity, neutrality, binary quasi-resoluteness, binary $\gamma$, and $\alpha$-resoluteness are inconsistent.

3. In SAT Solving for Pairwise Methods, we use a SAT solver to prove that anonymity, neutrality, quasi-resoluteness, and binary $\gamma$ are inconsistent.