Premise Set Caching for Enumerating Minimal Correction Subsets
Authors: Alessandro Previti, Carlos Mencía, Matti Järvisalo, Joao Marques-Silva
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The proposed techniques noticeably improves on the performance of state-of-the-art MCS enumeration algorithms in practice. ... We integrated the ideas presented in the preceding sections to the state-of-the-art MCS enumeration algorithm LBX ... The experiments were run under Linux on 2-GHz machines. ... The results are shown in Figures 2 4, with direct comparisons of LBX using PS caching with LBX without caching (Figure 2), ELS with core caching (Figure 3), and CLD (Figure 4), respectively. |
| Researcher Affiliation | Academia | Alessandro Previti HIIT, Department of Computer Science University of Helsinki, Finland alessandro.previti@helsinki.fi Carlos Menc ıa Department of Computer Science University of Oviedo, Spain Matti J arvisalo HIIT, Department of Computer Science University of Helsinki, Finland Joao Marques-Silva LASIGE, Faculty of Science University of Lisbon, Portugal |
| Pseudocode | Yes | Algorithm 1: MCS enumeration (general structure) ... Algorithm 2: LBX ... Algorithm 3: LBX with PS caching |
| Open Source Code | Yes | The implementation is available at https://www.cs. helsinki.fi/group/coreo/lbx-cache/. |
| Open Datasets | Yes | Following Previti et al. (2017), we used as benchmarks 811 instances from (Marques-Silva et al. 2013) originally used for benchmarking algorithms for extracting a single MCS, with the motivation that in terms of the harder task of MCS enumeration, it can be especially beneficial to employ caching on such hard instances. |
| Dataset Splits | No | The paper mentions using 'benchmarks' or 'instances' from other papers but does not explicitly provide specific details on how these were split into training, validation, or test sets for their own experiments. No cross-validation setup or random seed information is provided. |
| Hardware Specification | No | The paper states 'The experiments were run under Linux on 2-GHz machines.' This is not specific enough to identify the CPU model, GPU, or other hardware components. |
| Software Dependencies | Yes | We integrated the ideas presented in the preceding sections to the state-of-the-art MCS enumeration algorithm LBX (Menc ıa, Previti, and Marques-Silva 2015), using Minisat 2.2.0 (E en and S orensson 2004) as the underlying SAT solver. |
| Experiment Setup | Yes | A per-instance memory limit of 8 GB and a per-instance time limit of 1800 seconds was enforced. |