Core-Guided Minimal Correction Set and Core Enumeration
Authors: Nina Narodytska, Nikolaj Bjørner, Maria-Cristina Marinescu, Mooly Sagiv
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | 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. |