Strategic Abstention Based on Preference Extensions: Positive Results and Computer-Generated Impossibilities
Authors: Florian Brandl, Felix Brandt, Christian Geist, Johannes Hofbauer
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | Our contribution is twofold. First, we show that, whenever there are at least five alternatives, every Paretooptimal majoritarian voting rule suffers from the no-show paradox with respect to Fishburn s extension. This is achieved by reducing the statement to a finite yet very large problem, which is encoded as a formula in propositional logic and then shown to be unsatisfiable by a SAT solver. We also provide a human-readable proof which we extracted from a minimal unsatisfiable core of the formula. |
| Researcher Affiliation | Academia | Florian Brandl Felix Brandt Christian Geist Johannes Hofbauer Technische Universit at M unchen 85748 Garching bei M unchen, Germany {brandlfl,brandtf,geist,hofbauej}@in.tum.de |
| Pseudocode | No | The paper describes the encoding of problems for a SAT solver and provides proofs, but it does not include any pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions that a "computer-generated version" of the proof for Theorem 2 is "available from the authors upon request." This does not constitute concrete access to open-source code for the methodology. |
| Open Datasets | No | The paper focuses on theoretical computer-aided proofs using SAT solvers and logical encoding of axioms, rather than empirical studies involving datasets for training models. |
| Dataset Splits | No | The paper is theoretical, focusing on proofs and computer-aided theorem proving. It does not describe experiments with validation datasets or splits. |
| Hardware Specification | No | The paper mentions using a "SAT solver" but provides no specific details about the hardware (e.g., CPU, GPU, memory, cloud instances) used for running the computations. |
| Software Dependencies | Yes | We used PICOMUS, which is part of the PICOSAT distribution [Biere, 2008]. |
| Experiment Setup | No | The paper describes the logical encoding and axioms for the SAT solver but does not provide specific experimental setup details such as hyperparameters, learning rates, or other system-level training settings common in empirical studies. |