pith. sign in

arxiv: 2604.19851 · v1 · submitted 2026-04-21 · 💻 cs.GT · cs.AI

Is Four Enough? Automated Reasoning Approaches and Dual Bounds for Condorcet Dimensions of Elections

Itai Zilberstein , Ratip Emin Berker , George Li , Ruben Martins This is my paper

Pith reviewed 2026-05-10 00:56 UTC · model grok-4.3

classification 💻 cs.GT cs.AI
keywords Condorcet dimensionCondorcet winning setmixed-integer linear programmingautomated reasoningsocial choice theoryvoting theorylinear programming dualitycommittee selection
0
0 comments X

The pith

Computational searches on elections find no case needing a Condorcet winning set larger than size 3, and a dual simplification yields a conjecture implying size 4 always works.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies the Condorcet dimension of elections, the smallest committee size k that guarantees a Condorcet winning set exists no matter how voters rank the candidates. Prior results establish that k equals 1 or 2 is not always sufficient while k equals 5 is always sufficient, leaving a gap at 3 and 4. The authors encode the search for counterexample elections as a mixed-integer linear program, add symmetry breaking and subsampling to handle larger electorates, and run extensive experiments. These searches produce no election requiring k greater than 3. The authors then simplify the dual of the linear-programming relaxation and state a conjecture whose validity would prove that k equals 4 is always sufficient.

Core claim

Despite exhaustive MILP searches over moderate-sized elections that incorporate symmetry breaking, subsampling, and constraint generation, no instance is found in which a Condorcet winning set of size larger than three is required. Motivated by this observation, the dual of the LP relaxation is simplified to produce a conjecture that, if true, directly implies every election admits a Condorcet winning set of size at most four.

What carries the argument

The mixed-integer linear program that searches for elections whose minimal Condorcet winning set exceeds a conjectured size, together with the simplification of its dual linear program that supports the new upper-bound conjecture.

If this is right

  • If the conjecture holds, the known upper bound on Condorcet dimension drops from five to four.
  • No moderate-sized election requires a Condorcet winning set of size four or five.
  • The MILP encoding together with duality supplies a reusable automated framework for tightening existence bounds in ranked voting.
  • The same search-and-dual pipeline can be applied to other committee-selection problems in social choice.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the conjecture is correct, many practical voting rules could safely restrict attention to committees of size at most four without sacrificing the Condorcet property.
  • The dual-simplification technique may transfer to other combinatorial existence questions in social choice where linear-programming relaxations are available.
  • Further computational searches on larger instances or analytic proof of the conjecture would strengthen the case that the current upper bound of five is loose.
  • The absence of size-four or size-five examples suggests that worst-case Condorcet dimension may be determined by a small number of structural patterns rather than arbitrary voter profiles.

Load-bearing premise

The moderate-sized elections examined after symmetry breaking and subsampling, together with the particular dual simplification chosen, are representative of all possible elections and do not omit constraints that would force a larger committee.

What would settle it

An explicit election in which no set of three candidates forms a Condorcet winning set would falsify the empirical claim; a counterexample showing that the simplified dual does not imply the existence of a size-four set would falsify the conjectured upper bound.

Figures

Figures reproduced from arXiv: 2604.19851 by George Li, Itai Zilberstein, Ratip Emin Berker, Ruben Martins.

Figure 1
Figure 1. Figure 1: Example election consisting of voters 𝑣1, 𝑣2 and 𝑣3 and candidates A, B, and C. The committee {A, B} is a CWS. The sets {A}, {B}, and {C} are all not CWS. 3 OPTIMIZATION FORMULATION We are interested in finding the smallest committee size 𝑘 that guar￾antees the existence of a CWS. Given candidates 𝑚 and committee size 𝑘, we formulate this as an optimization problem maximizing the worst-case margin of defea… view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of the infinite cycle concept used in [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
read the original abstract

In an election where $n$ voters rank $m$ candidates, a Condorcet winning set is a committee of $k$ candidates such that for any outside candidate, a majority of voters prefer some committee member. Condorcet's paradox shows that some elections admit no Condorcet winning sets with a single candidate (i.e., $k=1$), and the same can be shown for $k=2$. On the other hand, recent work proves that a set of size $k=5$ exists for every election. This leaves an important theoretical gap between the best known lower bound $(k\geq 3)$ and upper bound $(k \leq 5)$ for the number of candidates needed to guarantee existence. We aim to close the gap between the existence guarantees and impossibility results for Condorcet winning sets. We explore an automated reasoning approach to tighten these bounds. We design a mixed-integer linear program (MILP) to search for elections that would serve as counter-examples to conjectured bounds. We employ a number of optimizations, such as symmetry breaking, subsampling, and constraint generation, to enhance the search and model effectively infinite electorates. Furthermore, we analyze the dual of the linear programming relaxation as a path towards obtaining a new upper bound. Despite extensive search on moderate-sized elections, we fail to find any election requiring a committee larger than size 3. Motivated by our experimental results in this direction, we simplify the dual linear program and formulate a conjecture which, if true, implies that a winning set of size 4 always exists. Our automated reasoning results provide strong empirical evidence that the Condorcet dimension of any election may be smaller than currently known upper bounds, at least for small instances. We offer a general-purpose framework for searching elections in ranked voting and a new, concrete analytical path via duality toward proving that smaller committees suffice.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that by using MILP to search for elections with high Condorcet dimension, no examples requiring committee size larger than 3 are found in moderate-sized instances. Motivated by this, they simplify the dual LP and conjecture that this implies every election has a Condorcet winning set of size 4, improving on the known upper bound of 5.

Significance. If the conjecture is true, it would provide a new upper bound of 4 for the Condorcet dimension, significantly narrowing the gap between lower and upper bounds in the theory of Condorcet winning sets. The automated reasoning approach and dual analysis represent valuable methodological contributions to computational social choice.

major comments (2)
  1. The simplification of the dual linear program is presented as motivated by experimental results, but the manuscript does not demonstrate that this simplification holds for arbitrary elections without introducing additional constraints or losing tightness, which is critical for the claimed implication that a winning set of size 4 always exists.
  2. The MILP search employs symmetry breaking and subsampling, but it is not shown that these techniques preserve the possibility of finding all potential counterexamples with Condorcet dimension 4 or higher; if certain profiles are systematically excluded, the failure to find counterexamples does not adequately support the conjecture.
minor comments (2)
  1. The abstract mentions 'strong empirical evidence' but given the limitations of the search, this phrasing could be tempered to 'preliminary empirical evidence'.
  2. Ensure all variables in the MILP are clearly defined with their domains in the main text.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed feedback and the positive assessment of the significance of our work. We address the major comments point by point below and propose revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: The simplification of the dual linear program is presented as motivated by experimental results, but the manuscript does not demonstrate that this simplification holds for arbitrary elections without introducing additional constraints or losing tightness, which is critical for the claimed implication that a winning set of size 4 always exists.

    Authors: The manuscript presents the simplification as the basis for a conjecture rather than a proven result for arbitrary elections. We explicitly state that the conjecture, if true, implies the bound of 4. We do not claim to have demonstrated the simplification holds universally; instead, the experiments motivate the conjecture. To clarify this distinction and address the concern about tightness, we will revise the relevant section to emphasize the conjectural nature and outline conditions under which the simplification would be valid. revision: yes

  2. Referee: The MILP search employs symmetry breaking and subsampling, but it is not shown that these techniques preserve the possibility of finding all potential counterexamples with Condorcet dimension 4 or higher; if certain profiles are systematically excluded, the failure to find counterexamples does not adequately support the conjecture.

    Authors: Symmetry breaking is applied to reduce isomorphic duplicates without excluding any distinct election profiles up to relabeling, which is appropriate since Condorcet dimension is invariant under candidate and voter permutations. For subsampling, it is used to approximate infinite electorates with finite but representative voter sets; we will add an explanation in the revision showing that any potential counterexample with dimension >=4 would manifest in the sampled instances we considered, as the MILP constraints capture the necessary majority conditions. We agree that more explicit justification is warranted and will include it. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical search and dual simplification remain independent

full rationale

The paper performs an MILP search over elections (with symmetry breaking and subsampling) to hunt for counterexamples requiring Condorcet dimension >3, reports none found, and separately simplifies the dual LP to state a conjecture whose truth would imply dimension ≤4. Neither step reduces to the other by construction: the search outputs are not fed as fitted parameters into the dual, the conjecture is not a renaming of the search results, and no self-citation or uniqueness theorem from the authors is invoked to close the argument. The derivation chain is therefore self-contained; the conjecture is an independent analytic claim motivated by but not logically equivalent to the experimental outcomes.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the correctness of the MILP encoding of Condorcet winning sets and on the validity of the dual simplification; no free parameters are fitted to data and no new entities are postulated.

axioms (2)
  • domain assumption The mixed-integer linear program correctly encodes the existence of a Condorcet winning set of size k for a given election profile.
    Invoked when the authors design the MILP to search for counter-examples to conjectured bounds.
  • domain assumption The simplified dual linear program is a valid relaxation whose feasibility implies the existence of a size-4 winning set in the original problem.
    Central to the conjecture; stated after the experimental results.

pith-pipeline@v0.9.0 · 5658 in / 1532 out tokens · 45380 ms · 2026-05-10T00:56:44.378873+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [1]

    2nd edition, 1963

    Kenneth Joseph Arrow. 2nd edition, 1963. 1st edition 1951.Social choice and individual values. New Haven: Cowles Foundation

    work page 1963

  2. [2]

    Ratip Emin Berker, Emanuel Tewolde, Vincent Conitzer, Mingyu Guo, Marijn Heule, and Lirong Xia. 2026. On the Edge of Core (Non-) Emptiness: An Auto- mated Reasoning Approach to Approval-Based Multi-Winner Voting. InConfer- ence on Artificial Intelligence (AAAI)

    work page 2026

  3. [3]

    Florian Brandl, Felix Brandt, Manuel Eberl, and Christian Geist. 2018. Proving the incompatibility of efficiency and strategyproofness via SMT solving.Journal of the ACM (JACM)65, 2 (2018), 1–28

    work page 2018

  4. [4]

    Florian Brandl, Felix Brandt, Christian Geist, and Johannes Hofbauer. 2019. Strate- gic abstention based on preference extensions: Positive results and computer- generated impossibilities.Journal of Artificial Intelligence Research66 (2019), 1031–1056

    work page 2019

  5. [5]

    Florian Brandl, Felix Brandt, Dominik Peters, and Christian Stricker. 2021. Dis- tribution rules under dichotomous preferences: two out of three ain’t bad. In Proceedings of the 22nd ACM Conference on Economics and Computation. 158–179

    work page 2021

  6. [6]

    Felix Brandt and Christian Geist. 2016. Finding strategyproof social choice functions via SAT solving.Journal of Artificial Intelligence Research55 (2016), 565–602

    work page 2016

  7. [7]

    Felix Brandt, Christian Geist, and Dominik Peters. 2017. Optimal bounds for the no-show paradox via SAT solving.Mathematical Social Sciences90 (2017), 18–27

    work page 2017

  8. [8]

    Moses Charikar, Alexandra Lassota, Prasanna Ramakrishnan, Adrian Vetta, and Kangning Wang. 2025. Six Candidates Suffice to Win a Voter Majority. InPro- ceedings of the 57th Annual ACM Symposium on Theory of Computing(Prague, Czechia)(STOC ’25). Association for Computing Machinery, New York, NY, USA, 1590–1601. https://doi.org/10.1145/3717823.3718235

    work page doi:10.1145/3717823.3718235 2025

  9. [9]

    Edith Elkind, Jérôme Lang, and Abdallah Saffidine. 2015. Condorcet winning sets. Soc. Choice Welfare44, 3 (March 2015), 493–517

    work page 2015

  10. [10]

    Christian Geist. 2016. Finding Preference Profiles of Condorcet Dimension 𝑘 via SAT. arXiv:1402.4303 [cs.MA] https://arxiv.org/abs/1402.4303

    work page arXiv 2016

  11. [11]

    Christian Geist and Ulrich Endriss. 2011. Automated search for impossibility theorems in social choice theory: Ranking sets of objects.Journal of Artificial Intelligence Research40 (2011), 143–174

    work page 2011

  12. [12]

    Christian Geist and Dominik Peters. 2017. Computer-aided methods for social choice theory.Trends in Computational Social Choice(2017), 249–267

    work page 2017

  13. [13]

    Allan Gibbard. 1973. Manipulation of voting schemes: a general result.Econo- metrica: Journal of the Econometric Society(1973), 587–601

    work page 1973

  14. [14]

    Gurobi Optimization, LLC. 2026. Gurobi Optimizer Reference Manual. https: //www.gurobi.com

    work page 2026

  15. [15]

    Timo Mennle and Sven Seuken. 2016. The Pareto frontier for random mechanisms. InProceedings of the 2016 ACM Conference on Economics and Computation. 769– 769

    work page 2016

  16. [16]

    Thanh Nguyen, Haoyu Song, and Young-San Lin. 2025. A few good choices. arXiv:2506.22133 [cs.GT] https://arxiv.org/abs/2506.22133

    work page arXiv 2025

  17. [17]

    Mark Allen Satterthwaite. 1975. Strategy-proofness and Arrow’s conditions: Existence and correspondence theorems for voting procedures and social welfare functions.Journal of Economic Theory10, 2 (1975), 187–217

    work page 1975

  18. [18]

    2008.A computer-aided proof to Gibbard– Satterthwaite theorem

    Pingzhong Tang and Fangzhen Lin. 2008.A computer-aided proof to Gibbard– Satterthwaite theorem. Technical Report. Technical report, Department of Com- puter Science, Hong Kong University of Science and Technology

    work page 2008

  19. [19]

    Pingzhong Tang and Fangzhen Lin. 2009. Computer-aided proofs of Arrow’s and other impossibility theorems.Artificial Intelligence173, 11 (2009), 1041–1053

    work page 2009