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 Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Core-Guided Minimal Correction Set and Core Enumeration
Authors: Nina Narodytska, Nikolaj Bjørner, Maria-Cristina Marinescu, Mooly Sagiv
IJCAI 2018 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, we preform evaluation in a prototype solver FLINT. FLINT is built on top of the PM1 core-guided Max SAT solver [Fu and Malik, 2006]. We compare it with MARCO, the state-of-the-art method that simultaneously extracts MUSes and MCSes. |
| Researcher Affiliation | Collaboration | 1 VMware Research, USA 2 Microsoft Research, USA 3 Barcelona Supercomputing Center, Spain 4 Tel Aviv University, Israel |
| Pseudocode | Yes | Algorithm 1 Enu MMerator, Algorithm 2 Relax, Algorithm 3 Relax Core, Algorithm 4 Strengthen, Algorithm 5 Enu Mus, Algorithm 6 MCSRotation |
| Open Source Code | No | The paper mentions building FLINT on PM1 and using MUSer for comparison, and refers to a website for CIRCUMSCRIPTINO, but does not provide a link or explicit statement about the open-sourcing of their own FLINT implementation. |
| Open Datasets | Yes | We work with a standard set of 295 benchmarks from the MUS track of the 2011 SAT competition [Jarvisalo et al., 2011]. |
| Dataset Splits | No | The paper does not provide specific details on how the dataset was split into training, validation, or test sets, nor does it refer to a standard split for reproducibility. |
| Hardware Specification | Yes | We ran our experiments on Intel(R) Xeon(R) 3.50GHz. |
| Software Dependencies | No | The paper mentions using PM1, MUSer, and a trie data structure but does not specify exact version numbers for these software dependencies, only providing citations to the general tools. |
| Experiment Setup | Yes | We use timeout of 3600 sec in all runs. |