Exploiting the Structure of Unsatisfiable Cores in MaxSAT
Authors: Carlos Ansotegui, Frederic Didier, Joel Gabas
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results on industrial instances show that the proposed approach outperforms both complete and incomplete stateof-the-art Max SAT solvers at the last international Max SAT Evaluation in terms of robustness and total number of solved instances. |
| Researcher Affiliation | Collaboration | Carlos Ans otegui DIEI, Univ. of Lleida, Spain carlos@diei.udl.es Frederic Didier Google Paris, France fdid@google.com Joel Gab as DIEI, Univ. of Lleida, Spain jgabas@diei.udl.es |
| Pseudocode | Yes | Algorithm 1: WPM3 |
| Open Source Code | No | The paper mentions 'or-tools package [Google, 2009]' which is a third-party tool, but does not provide a specific link or explicit statement that the source code for the methodology described in this paper is publicly available. |
| Open Datasets | Yes | We have evaluated our approach on the industrial instances from the Max SAT Evaluation 2014 (MSE14) [Argelich et al., 2006 2014]. |
| Dataset Splits | No | The paper refers to the 'instance set of MSE14' but does not provide specific details on training, validation, or test dataset splits (e.g., percentages, sample counts, or predefined split citations) needed for reproduction. |
| Hardware Specification | Yes | We run our experiments on a cluster featured with 2.6GHz processors and a memory limit of 3.5 GB. |
| Software Dependencies | Yes | All the variations on WPM3 are implemented on top of the glucose SAT solver (version 3.0) [Audemard and Simon, 2009]. |
| Experiment Setup | Yes | Table 1 shows our first experiment, where we evaluate the impact of each improvement on WPM3 (with a timeout of 1800 seconds). |