Large Neighbourhood Search for Anytime MaxSAT Solving
Authors: Randy Hickey, Fahiem Bacchus
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | All of our experiments were run on 2.7GHz Intel cores with 300 second CPU time and 16GB memory limits.3 The benchmarks we used for the first two experiments were the 253 weighted and 262 unweighted instances from the Incomplete Tracks of the 2020 Max SAT Evaluation [Bacchus et al., 2020a] (we used the 2020 benchmarks instead of 2021 because there are more total instances in the 2020 benchmarks). In order to avoid overfitting, we did all tuning of our neighbourhood selection policy on the instances from the 2018 and 2019 Max SAT Evaluations before settling on the policy described in Section 3.1. We implemented our LNS algorithm as described in Section 3 using Max HS [Bacchus, 2020] as the complete solver C Max Slv. To measure how effective our approach was at finding good solutions, we used the same scoring system as used in the Max SAT evaluations. |
| Researcher Affiliation | Academia | Randy Hickey and Fahiem Bacchus University of Toronto rhickey@cs.toronto.edu, fbacchus@cs.toronto.edu |
| Pseudocode | Yes | Algorithm 1 Generic LNS algorithm for Max SAT" and "Algorithm 2 Neighbourhood selection policy" |
| Open Source Code | Yes | Source code can be found at https://github.com/rgh000/Max SAT LNS. |
| Open Datasets | Yes | The benchmarks we used for the first two experiments were the 253 weighted and 262 unweighted instances from the Incomplete Tracks of the 2020 Max SAT Evaluation [Bacchus et al., 2020a] (we used the 2020 benchmarks instead of 2021 because there are more total instances in the 2020 benchmarks). For the last set of experiments, we used the union of all weighted and unweighted instances from the 2020 and 2021 Max SAT evaluations. |
| Dataset Splits | No | The paper does not specify traditional training/validation/test dataset splits. It mentions grouping solutions into 'buckets' based on quality for analysis, but this is not a data split for model training. |
| Hardware Specification | Yes | All of our experiments were run on 2.7GHz Intel cores with 300 second CPU time and 16GB memory limits. |
| Software Dependencies | Yes | We implemented our LNS algorithm as described in Section 3 using Max HS [Bacchus, 2020] as the complete solver C Max Slv. We chose TT-Open-WBO [Nadel, 2021], one of the best incomplete solvers in recent Max SAT evaluations, as the representative state-of-the-art anytime solver to compare LNS rate of improvement with. [...] For the last set of experiments, we try to improve the performance of three of the best performing anytime Max SAT solvers from the 2020 and 2021 Max SAT evaluations: TTOpen-WBO, Loandra [Berg et al., 2021], and satlike [Lei et al., 2021]. |
| Experiment Setup | Yes | All of our experiments were run on 2.7GHz Intel cores with 300 second CPU time and 16GB memory limits. [...] We decided to start with a small neighbourhood (a large fixed set) because small neighbourhoods will usually be easier to solve with C Max Slv. Notice that once δ gets to 0.1 and we encounter ten consecutive rounds with no new best solution, δ will be set to 0 and the entire problem will be solved by C Max Slv optimally. [...] We start with a fixed set α of size about 80% of the total number of variables in the problem, i.e., with δ = 0.8. After ten consecutive rounds of LNS where no new best solution is found, we reduce α s size by reducing δ by 0.1. |