Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Maximum Satisfiability Using Cores and Correction Sets
Authors: Nikolaj Bjorner, Nina Narodytska
IJCAI 2015 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We theoretically show that correction sets and cores have complementary strengths and empirically demonstrate that their combination leads to an ef๏ฌcient MAXSAT solver that outperforms state-of-the-art WPMS solvers on the 2014 Evaluation on industrial instances. |
| Researcher Affiliation | Collaboration | Nikolaj Bjorner Microsoft Research Redmond, USA EMAIL Nina Narodytska Carnegie Mellon University Pittsburgh, USA EMAIL |
| Pseudocode | Yes | Algorithm 1 shows the pseudocode. |
| Open Source Code | No | The paper does not provide concrete access to source code for the methodology described. It states: "PRIMALDUALMAXSAT (PD) and PRIMALDUALMIN (PDm) are implemented inside Mini SAT [Een and Sorensson, 2003]", which refers to a third-party solver used, but not their own code release. |
| Open Datasets | Yes | We used all industrial instances from the 2014 Evaluation of Max-SAT Solvers competition. |
| Dataset Splits | No | The paper uses industrial instances from a competition, which typically defines splits, but the paper itself does not explicitly state the training, validation, or test dataset splits used for its own experiments in terms of percentages, counts, or specific predefined split names. |
| Hardware Specification | Yes | We ran our experiments on a cluster of AMD Opteron@2.1 GHz machines restricted to 3.5Gb or RAM and 3600 seconds of CPU time. |
| Software Dependencies | No | The paper states: "PRIMALDUALMAXSAT (PD) and PRIMALDUALMIN (PDm) are implemented inside Mini SAT [Een and Sorensson, 2003]". While Mini SAT is named, a specific version number for Mini SAT itself or any other software dependency is not provided. |
| Experiment Setup | Yes | We observed that some candidate correction sets were expensive to check. We, therefore, apply a timeout of three seconds when checking ฯi. The timeout was gradually decreased as search proceeded. |