Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT
Authors: Jeremias Berg, Paul Saikko, Matti Järvisalo
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our empirical results on standard crafted and industrial weighted partial Max SAT Evaluation benchmarks show overall improvements over the original Max HS algorithm both with and without SAT-based preprocessing. |
| Researcher Affiliation | Academia | Jeremias Berg and Paul Saikko and Matti J arvisalo HIIT & Department of Computer Science, University of Helsinki, Finland |
| Pseudocode | Yes | Algorithm 1: The Max HS algorithm; Algorithm 2: LCNF-Max HS, lifting of Max HS to LCNFs |
| Open Source Code | No | The paper mentions extending their 'own prototype re-implementation' but does not provide a link or explicitly state that their code for the LCNF-Max HS is publicly available or open-source. |
| Open Datasets | Yes | We used all 624 instances from the weighted partial crafted (214) and industrial (410) categories of Max SAT Evaluation 2014 (http://www.maxsat.udl.cat/14/). |
| Dataset Splits | No | The paper refers to 'instances' from the Max SAT Evaluation 2014 benchmark, which are complete problems to be solved. It does not describe training, validation, or test dataset splits for its own experimental setup in the conventional machine learning sense. |
| Hardware Specification | Yes | The experiments were run on a cluster of 2.53-GHz Intel Xeon quad core machines with 32-GB memory and Ubuntu Linux 12.04. |
| Software Dependencies | Yes | Mini SAT 2.2.0 [E en and S orensson, 2003] is used as the underlying SAT solver and IBM CPLEX 12.6.0 [Cpl, 2015] is used to solve the minimum-cost hitting set IPs. As the SAT preprocessor, we used Coprocessor 2.0 [Manthey, 2012] |
| Experiment Setup | Yes | Refining Algorithm 1, this re-implementation includes the SAT solver tweaks and disjoint phase of [Davies and Bacchus, 2011], the non-optimal hitting set computations of [Davies and Bacchus, 2013b], as well as the core minimization and eq-seeding techniques of [Davies and Bacchus, 2013a]. A timeout of 1 h was enforced for solving each benchmark instance. |