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].
On Consensus Extraction
Authors: éric Grégoire, Sébastien Konieczny, Jean Marie Lagniez
IJCAI 2016 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this work, we define consensus operators as functions that deliver parts of the set-theoretical union of the information sources (in propositional logic) to be reconciled, such that no source is logically contradicted. We also investigate different notions of maximality related to these consensuses. From a computational point of view, we propose a generic problem transformation that leads to a method that proves experimentally efficient very often, even for large conflicting sources to be reconciled. |
| Researcher Affiliation | Academia | Eric Gr egoire, S ebastien Konieczny, Jean-Marie Lagniez CRIL Univ. Artois & CNRS F-62300 Lens France EMAIL |
| Pseudocode | Yes | Algorithm Transform1 illustrates the construction of the soft and hard clauses of the instance of the Weighted Partial Max SAT problem. |
| Open Source Code | Yes | Our software, as well as the data and results of these experimentations are available at www.cril.fr/ consensus. |
| Open Datasets | Yes | The profiles S were based on the 291 different unsatisfiable (mostly real-world) instances from the 2011 MUS competition www.satcompetition.org/2011 |
| Dataset Splits | Yes | Each instance was randomly split into n 2 [3, 5, 7, 10] samesize (modulo n) Φi to yield all the S. |
| Hardware Specification | Yes | All experimentations have been conducted on Intel Xeon E52643 (3.30GHz) processors with 8Gb RAM on Linux Cent OS. |
| Software Dependencies | No | We made used of Max HS, the Weighted Partial Max SAT solver from www.maxhs.org. We have implemented all the other algorithms in C++ on top of Glucose (www.labri.fr/ perso/lsimon/glucose). The paper mentions software names but does not provide specific version numbers for reproducibility. |
| Experiment Setup | Yes | Time-out was set to 900 seconds per consensus extraction. When preferences that rank-order clauses were considered, 5 levels of preference were used: clauses were assigned randomly inside these levels so that each level contains a same number of clauses. When n 5 sources had to be rank-ordered, each source was assigned to one of the 5 levels, randomly. For n < 5 sources, we used n levels of preference between sources. |