Tailoring Local Search for Partial MaxSAT
Authors: Shaowei Cai, Chuan Luo, John Thornton, Kaile Su
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results on PMS benchmarks from Max SAT Evaluation 2013 show that Dist significantly outperforms state-of-the-art PMS algorithms, including both local search algorithms and complete ones, on random and crafted benchmarks. For the industrial benchmark, Dist dramatically outperforms previous local search algorithms and is comparable with complete algorithms. Experimental Evaluation We empirically evaluate Dist on all Partial Max SAT benchmarks in Max SAT Evaluation 2013, including three categories namely random, crafted and industrial. |
| Researcher Affiliation | Academia | Shaowei Cai1,2 , Chuan Luo3, John Thornton4, Kaile Su4 1State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China 2Queensland Research Laboratory, NICTA, Brisbane, Australia 3Key Laboratory of High Confidence Software Technologies, Peking University, Beijing, China 4Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia |
| Pseudocode | Yes | Algorithm 1: Dist Input: Partial Max SAT instance F, max Steps α := randomly generated truth assignment; 1 cost := + ; 2 for step := 1 to max Steps do 3 if falsified hard clauses & cost(α) < cost then 4 α := α; cost := cost(α); |
| Open Source Code | No | Dist is implemented in C++ and complied by g++ with the O2 option, and will be distributed online. |
| Open Datasets | Yes | We empirically evaluate Dist on all Partial Max SAT benchmarks in Max SAT Evaluation 2013, including three categories namely random, crafted and industrial. |
| Dataset Splits | No | The paper mentions using Partial Max SAT benchmarks from Max SAT Evaluation 2013 but does not explicitly state specific training, validation, or test dataset splits (e.g., percentages or sample counts). The evaluation is done on pre-defined benchmark sets. |
| Hardware Specification | Yes | All experiments are carried out on a workstation under Ubuntu Linux operation system, using an Intel(R) Core(TM) i7-2640M 2.8 GHz CPU and 8 GB RAM. |
| Software Dependencies | No | The paper states that Dist is implemented in C++ and compiled by g++ with the O2 option, but it does not provide specific version numbers for C++ compiler (g++) or any other software libraries. |
| Experiment Setup | Yes | The sp parameter for the weighting scheme is set to 0.0012.2 (Footnote 2: except that 0.0001 for industrial instances with more than 2500 variables). |