Literal-Based MCS Extraction
Authors: Carlos Mencía, Alessandro Previti, Joao Marques-Silva
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical results show substantial improvements over the state of the art in MCS extraction and indicate that MCS-based Max SAT approximation is very effective in practice. Experimental results, obtained on representative problem instances, demonstrate that the new MCS extraction algorithm consistently outperforms the approaches that currently represent the state of the art. |
| Researcher Affiliation | Academia | 1CASL, University College Dublin, Ireland 2INESC-ID, IST, ULisboa, Portugal |
| Pseudocode | Yes | Algorithm 1: Literal-Based e Xtractor (LBX) |
| Open Source Code | Yes | LBX1 was implemented in C++ interfacing Minisat 2.2 [E en and S orensson, 2003]. 1Available at http://logos.ucd.ie/wiki/doku.php?id=lbx |
| Open Datasets | Yes | We considered three sets of unsatisfiable instances: The first one, ijcai13-bench, contains 866 instances taken from [Marques-Silva et al., 2013a], both plain and partial formulas. The second one, proposed in [Gr egoire et al., 2014], includes 295 plain instances from the 2011 MUS competition. Finally, as most of these instances were solved swiftly by all the algorithms we propose a new set of hard instances. It contains all the instances from the 2014 Max SAT evaluation2 as well as from other sources3 such that either CMP or LBX took more than 90s to solve, filtering out those where none of these algorithms was able to complete a single call to the SAT solver. [...] 2http://www.maxsat.udl.cat/14/index.html |
| Dataset Splits | No | The paper uses benchmark instances for MCS extraction and Max SAT approximation, but does not specify training, validation, or test dataset splits in the conventional machine learning sense (percentages or counts). |
| Hardware Specification | No | The experiments were run on a Linux cluster (2 GHz, 64bits), with a memory limit of 4 GB. |
| Software Dependencies | Yes | LBX1 was implemented in C++ interfacing Minisat 2.2 [E en and S orensson, 2003]. |
| Experiment Setup | Yes | The time limit was set to 1800 seconds. |