Maximum Satisfiability Using Core-Guided MaxSAT Resolution
Authors: Nina Narodytska, Fahiem Bacchus
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this section, we preform an experimental evaluation of our proposed algorithm. We run our experiments on a cluster of AMD Opteron@2.2 GHz machines restricted to 2.5Gb or RAM and 1800 sec. of CPU time. We used all industrial instances from the 2013 Evaluation of Max-SAT Solvers competition. We compare our solver with those state-of-the-art weighted partial MAXSAT solvers that performed best on these instances during the latest evaluation (Argelich et al. 2013): wpm1 1 (Ans otegui, Bonet, and Levy 2013), wpm2 (Ans otegui, Bonet, and Levy 2013), wpm1 (Janota 2013) and msunc (Morgado, Heras, and Marques-Silva 2012). All solvers were provided in the binary or source code by the authors.2 We replaced the base SAT solver, minisat (Een and Sorensson 2003), in wpm1 by glucose (Audemard, Lagniez, and Simon 2013) to improve its performance. |
| Researcher Affiliation | Academia | Nina Narodytska University of Toronto and UNSW Toronto, Canada and Sydney, Australia ninan@cs.toronto.edu Fahiem Bacchus University of Toronto Toronto, Canada fbacchus@cs.toronto.edu |
| Pseudocode | Yes | Algorithm 1 PMRes Input: φ = {C1, . . . , Cm} Output: (I, cost(φ)), where I is an optimal assignment 1 i = 0, φ0 = φ 2 while true do 3 (issat, κi, I) = Solve SAT(φi { i j=1( , 1)}) 4 if issat return (I, i) 5 (φ , B) = Reify Core(φi, κi) 6 φ+ = φ {( b Bb)} 7 φi+1 = Apply Max Res(φ+, B) 8 i = i + 1 |
| Open Source Code | No | We implemented our algorithm using the wpm1 implementation by Mikola Janota as our base. Our solver is called eva. (No explicit statement or link for *their* code's open-source availability.) |
| Open Datasets | Yes | We used all industrial instances from the 2013 Evaluation of Max-SAT Solvers competition. We compare our solver with those state-of-the-art weighted partial MAXSAT solvers that performed best on these instances during the latest evaluation (Argelich et al. 2013): wpm1 1 (Ans otegui, Bonet, and Levy 2013), wpm2 (Ans otegui, Bonet, and Levy 2013), wpm1 (Janota 2013) and msunc (Morgado, Heras, and Marques-Silva 2012). All solvers were provided in the binary or source code by the authors.2 |
| Dataset Splits | No | The paper uses "industrial instances from the 2013 Evaluation of Max-SAT Solvers competition" but does not explicitly describe any specific training, validation, or test dataset splits (e.g., percentages, sample counts, or predefined split methods) used for their experiments. |
| Hardware Specification | Yes | We run our experiments on a cluster of AMD Opteron@2.2 GHz machines restricted to 2.5Gb or RAM and 1800 sec. of CPU time. |
| Software Dependencies | No | We replaced the base SAT solver, minisat (Een and Sorensson 2003), in wpm1 by glucose (Audemard, Lagniez, and Simon 2013) to improve its performance... We use glucose as the SAT solver and preprocess hard clauses using standard subsumption technique before we start the search. (Software names like minisat, glucose, and wpm1 are mentioned, but specific version numbers are not provided.) |
| Experiment Setup | No | We use glucose as the SAT solver and preprocess hard clauses using standard subsumption technique before we start the search. (This is a general setup detail, but no specific hyperparameters or detailed training configurations are provided.) |