Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
On Continuous Local BDD-Based Search for Hybrid SAT Solving
Authors: Anastasios Kyrillidis, Moshe Vardi, Zhiwei Zhang3841-3850
AAAI 2021 | Venue PDF | 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 EMAIL |
| 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. |