Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
Authors: Florian Brandl, Felix Brandt, Christian Geist
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we provide a computer-aided proof of a sweeping impossibility using these two conditions for randomized aggregation mechanisms. Our proof is obtained by formulating the claim as a satisfiability problem over predicates from real-valued arithmetic, which is then checked using an SMT (satisfiability modulo theories) solver. |
| Researcher Affiliation | Academia | Florian Brandl, Felix Brandt, Christian Geist Technische Universit at M unchen {brandlfl,brandtf,geist}@in.tum.de |
| Pseudocode | No | The paper describes the SMT encoding and constraints conceptually but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | Footnote 7 mentions that an "MUS... is available as part of an ar Xiv version of this paper [Brandl et al., 2016a]", which refers to the paper itself on arXiv, not a dedicated code repository for the methodology. |
| Open Datasets | No | This paper is theoretical, focusing on formal proofs via SMT solving, and does not use datasets for training. |
| Dataset Splits | No | This paper is theoretical and does not involve empirical validation with dataset splits like training, validation, or testing. |
| Hardware Specification | No | The paper mentions SMT solvers terminating quickly but does not specify any hardware details like GPU/CPU models or memory. |
| Software Dependencies | Yes | For compatibility with different SMT solvers our encoding adheres to the SMT-LIB standard [Barrett et al., 2010]. The SMT solver Math SAT [Cimatti et al., 2013] terminates quickly within less than 3 minutes with the suggested competition settings, whereas z3 [de Moura and Bjørner, 2008] requires some additional configuration. |
| Experiment Setup | Yes | On the domain which starts from the preference profile R from Example 1 and allows sequences of (1, 2, 1, 2)-manipulations, we were able to prove the result within a few minutes of running-time. |