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].
Strategic Abstention based on Preference Extensions: Positive Results and Computer-Generated Impossibilities
Authors: Florian Brandl, Felix Brandt, Christian Geist, Johannes Hofbauer
JAIR 2019 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | The first result is obtained using computer-aided theorem proving techniques. In particular, we reduce 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 for this result, which we extracted from a minimal unsatisfiable core of the SAT formula. |
| Researcher Affiliation | Academia | Florian Brandl EMAIL Stanford University Palo Alto, USA Felix Brandt EMAIL Christian Geist EMAIL Johannes Hofbauer EMAIL Technical University of Munich Munich, Germany |
| Pseudocode | No | The paper describes a methodology involving computer-aided theorem proving and SAT solving by encoding problems into propositional logic formulas. It does not present any pseudocode or algorithm blocks in the traditional sense of a structured procedure. |
| Open Source Code | No | The paper states: "We used Pico MUS, which is part of the Pico SAT distribution (Biere, 2008)." This refers to a third-party SAT solver tool that the authors utilized, not source code for their own methodology or implementation that they are releasing. |
| Open Datasets | No | The paper deals with theoretical concepts such as "preference profile," "majority relations," and "alternatives." While it mentions reducing problems to "finite instances" for SAT solving, these are not empirical datasets for which public access information would typically be provided. No traditional datasets or their access details are mentioned. |
| Dataset Splits | No | The paper does not utilize empirical datasets with train/test/validation splits. Its methodology involves theoretical analysis and computer-aided theorem proving using SAT solvers, not machine learning or data-driven experiments that require dataset partitioning. |
| Hardware Specification | No | The paper mentions using a "SAT solver" for "computer-aided theorem proving techniques" but does not specify any details about the hardware (e.g., CPU, GPU models, memory) used to run these computations. |
| Software Dependencies | Yes | We used Pico MUS, which is part of the Pico SAT distribution (Biere, 2008). |
| Experiment Setup | No | The paper describes a theoretical approach aided by SAT solving, detailing the encoding of logical formulas and the use of SAT solvers. However, it does not include details typical of an empirical experimental setup, such as hyperparameters, training configurations, or system-level settings for models. |