On Continuous Local BDD-Based Search for Hybrid SAT Solving
Authors: Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang3841-3850
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We study the capabilities and limitations of our versatile CLS solver, Grad SAT, by applying it on many benchmark instances. The experimental results indicate that Grad SAT can be a useful addition to the portfolio of existing SAT and Max SAT solvers for solving Boolean satisfiability and optimization problems. |
| Researcher Affiliation | Academia | Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang Rice University, 6100 Main Street, Houston, TX, USA {anastasios, vardi, zhiwei}@rice.edu |
| Pseudocode | Yes | Algorithm 1: Fourier SAT, a CLS-based SAT Solver. ... Algorithm 2: The Probability-Assignment Algorithm ... Algorithm 3: Objective Evaluation (Top-Down) ... Algorithm 4: Objective Evaluation (Bottom-Up) ... Algorithm 5: Efficient Gradient Computation ... Algorithm 6: Grad SAT |
| Open Source Code | Yes | We implement Grad SAT in C++ 9. Available at https://github.com/vardigroup/Grad SAT |
| Open Datasets | Yes | Benchmark 2: Max SAT problems. We gathered 570 instances from the crafted (198 instances) and random track (377 instances) of Max SAT Competition 2016-2019. |
| Dataset Splits | No | No specific details about training, validation, or test dataset splits (e.g., percentages, sample counts, or methodology like cross-validation) were provided for the benchmarks used. |
| Hardware Specification | Yes | Each experiment is run on an exclusive node in a Linux cluster with 16-processor cores at 2.63 GHz and 1 GB of RAM per processor. |
| Software Dependencies | Yes | Thus practical packages for handling BDDs, e.g., CUDD 2 have been developed. Such packages provide sub-function sharing between individual BDDs so that a set of BDDs can be stored compactly. ... 2CUDD: CU Decision Diagram Package Release 3.0.0 |
| Experiment Setup | Yes | Time limit is set to be 100s. ... We set the time limit to 60s. ... We tuned r and T by running Grad SAT on random 3-CNF benchmarks with r {1, 1.5, 2, 2.5, 3} and T {1, 2, 4, 8, 16} and choosing (r, T) that solves most cases. We got r = 2, T = 8. ... The constraint weights are initialized to be the length of the constraint. When a local optimum is reached, we multiply the weights of unsatisfied constraints by r and start from the same point once again. Grad SAT only does random restart when T trials have been made for the same starting point, as shown in Alg. 6. |