Relaxation Search: A Simple Way of Managing Optional Clauses
Authors: Fahiem Bacchus, Jessica Davies, Maria Tsimpoukelli, George Katsirelos
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our empirical results show that the paradigm of relaxation search can achieve state-of-the-art performance, both for solving MAXSAT and for computing MCSes. We implemented the method for finding MCSes on top of MINISAT (E en and S orensson 2003). We compared the performance of our solver on both types of tasks against all algorithms proposed in (Marques-Silva et al. 2013). For the comparison, we experimented with the set of 1343 instances used in (Marques-Silva et al. 2013), which consists of a mix of (Weighted Partial) MAXSAT and SAT instances. |
| Researcher Affiliation | Academia | Fahiem Bacchus, Jessica Davies, Maria Tsimpoukell University of Toronto, Canada [fbacchus jdavies]@cs.toronto.edu maria.tsimpoukelli@gmail.com George Katsirelos MIAT, INRA, Toulouse, France george.katsirelos@toulouse.inra.fr |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states: "We implemented the method for finding MCSes on top of MINISAT (E en and S orensson 2003)." but does not provide any explicit statement or link to their own source code for the methodology described. |
| Open Datasets | Yes | For the comparison, we experimented with the set of 1343 instances used in (Marques-Silva et al. 2013), which consists of a mix of (Weighted Partial) MAXSAT and SAT instances. We implemented the above logic based Benders relaxation search approach for MAXSAT and tested it on all industrial and crafted instances from the 2013 MAXSAT Evaluation. |
| Dataset Splits | No | The paper refers to benchmark instances from prior work and a MAXSAT evaluation but does not specify any train/validation/test data splits or cross-validation setup for its experiments. |
| Hardware Specification | Yes | We ran all experiments on a cluster with 48-core AMD Opteron 6176 nodes at 2.3GHz, with 378GB of RAM under a timeout of 1800 seconds. |
| Software Dependencies | No | The paper mentions implementing on MINISAT (E en and S orensson 2003) and using IBM CPLEX, but it does not provide specific version numbers for these or other software components needed for replication. |
| Experiment Setup | Yes | We ran all experiments on a cluster with 48-core AMD Opteron 6176 nodes at 2.3GHz, with 378GB of RAM under a timeout of 1800 seconds. Relaxation Search ... using the additional restriction that the solver always chooses to branch on a b variable if one remains unassigned. |