Maximum Satisfiability Using Cores and Correction Sets
Authors: Nikolaj Bjorner, Nina Narodytska
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | 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 efficient 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 nbjorner@microsoft.com Nina Narodytska Carnegie Mellon University Pittsburgh, USA ninan@cs.cmu.edu |
| 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. |