Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Finding Strategyproof Social Choice Functions via SAT Solving
Authors: Felix Brandt, Christian Geist
JAIR 2016 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | A promising direction in computational social choice is to address research problems using computer-aided proving techniques. In particular with SAT solvers, this approach has been shown to be viable not only for proving classic impossibility theorems such as Arrow s Theorem but also for finding new impossibilities in the context of preference extensions. In this paper, we demonstrate that these computer-aided techniques can also be applied to improve our understanding of strategyproof irresolute social choice functions. ... Our contribution is two-fold: We present an efficient encoding for translating such problems to SAT and leverage this encoding to prove new results about strategyproofness with respect to Kelly s and Fishburn s preference extensions. |
| Researcher Affiliation | Academia | Felix Brandt EMAIL Technical University of Munich (TUM) Munich, Germany Christian Geist EMAIL Technical University of Munich (TUM) Munich, Germany |
| Pseudocode | Yes | Algorithm 1: P E-tournament-strategyproofness (optimized)... Algorithm 2: A search algorithm to find a cardinality-minimal SCF f (i.e., with minimal value for avg(f)) that satisfies a given set of axioms. ... Appendix B. Pseudo-Code for Encoding We present (as an illustrative example) the simple pseudo-code of Algorithm 3 to generate the CNF form of Axiom 1 |
| Open Source Code | No | The paper discusses using SAT solvers and tools like 'nauty' and 'Pico MUS' for computer-aided proving. However, it does not explicitly state that the authors' own implementation or source code for the methodology described in the paper is openly available, nor does it provide any repository links or supplementary material for their code. |
| Open Datasets | No | The paper focuses on theoretical research in social choice theory using SAT solvers to prove impossibility theorems. It deals with abstract mathematical structures like tournaments and preference relations, rather than empirical datasets. Therefore, there are no publicly available or open datasets used in the context of experimental evaluation. |
| Dataset Splits | No | The paper presents theoretical research using SAT solving to prove theorems in social choice theory. It does not involve empirical experiments with datasets that would require training, test, or validation splits. |
| Hardware Specification | No | The paper mentions 'running time for m = 6, for example, was reduced from almost five hours to three minutes' and 'for m = 7 ... encoding and solving the problem takes almost 24 hours', which indicates computational effort. However, it does not provide any specific details about the hardware used, such as CPU or GPU models, memory, or cloud resources. |
| Software Dependencies | No | The paper mentions using a 'SAT solver', and specifically names 'Pico MUS (part of Pico SAT, Biere, 2008)' and 'nauty (Mc Kay & Piperno, 2013)'. However, it only provides publication years for these tools, not specific version numbers for the software used in their implementation, which is required for reproducibility. |
| Experiment Setup | No | The paper describes a methodological approach involving SAT solving and encoding for theoretical proofs. While it discusses 'optimization techniques' and 'heuristics' (e.g., 'randomly sampling sets of tournaments') for improving the SAT solving process, these are part of the methodology itself rather than specific experimental setup details or hyperparameters for an empirical evaluation. |