Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
Authors: Yunuo Cen, Zhiwei Zhang, Xuanyao Fong
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 4 Experimental Results In this section, we compare our solver Fast Fourier SAT with CLS and other SOTA SAT solvers. We aim to conduct experiments to answer the following research questions: RQ1. Can implementing Fast Fourier SAT on GPU lead to a substantial acceleration in gradient computations compared to prior CPU implementations of CLS? RQ2. Can Fast Fourier SAT outperform SOTA parallel solvers in solving (Max)SAT problems that can be naturally encoded with hybrid Boolean constraints? RQ3. Given industrial-scale problems as (Max)SAT formulas, how does Fast Fourier SAT perform compared to the CDCL solvers that have dominated over the past decades? We implement Fast Fourier SAT in both CPU and GPU frameworks. We use JAX (Bradbury et al. 2018) for the framework and JAXopt (Blondel et al. 2022) for the optimizer. We compare our approach with the following solvers. ... Table 1: The average gradient computation time of different CLS solvers. l m means m cardinality constraints with length l. |
| Researcher Affiliation | Academia | Yunuo Cen1, Zhiwei Zhang2, Xuanyao Fong1* 1National University of Singapore 2Rice University EMAIL, EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: The CLS Framework for Hybrid SAT Solving Input: Boolean formula f with a hybrid constraint set C Output: An discrete assignment x { 1, 1}n ... Algorithm 2: Forward Evaluation with FFT method Input: The current assignment x Parameter: Conjugated Fourier coefficient fc s c C Output: Value Ff ... Algorithm 3: Integrating CLS for Hybrid Max SAT Solving Input: A hybrid constraint set ϕ = ϕhard ϕsoft Output: An discrete assignment x { 1, 1}n |
| Open Source Code | Yes | 2Supplemental materials including code, data, and appendix are available on (https://github.com/seeder-research/Fast Fourier SAT). |
| Open Datasets | Yes | Benchmark 4: SAT Competition (SC) and Max SAT Evaluation (MSEval) 2023 Since CLS is incomplete, we select the instances proven to be satisfiable from SC 23 and all unweighted instances from anytime track in MSEval 23. ... 2Supplemental materials including code, data, and appendix are available on (https://github.com/seeder-research/Fast Fourier SAT). |
| Dataset Splits | No | The paper describes how instances are generated (e.g., 'For each N {50, 100, 150, 200, 250}, we choose l = N/5 and m = 3l to generate 100 instances') and references SAT Competition and Max SAT Evaluation instances, which are typically used as test sets. However, it does not specify explicit train/test/validation dataset splits or cross-validation setups for any experiments. |
| Hardware Specification | Yes | The CPU solvers run on a server with dual AMD Epyc 7773X CPUs and 2 TB of RAM. Each experiment for CPU solvers uses 32 CPU threads, and 128 GB of RAM. The GPU solvers run on a workstation with INTEL i9-12900F CPU, 32 GB of RAM, and NVIDIA RTX 3080 Ti GPU. |
| Software Dependencies | No | We implement Fast Fourier SAT in both CPU and GPU frameworks. We use JAX (Bradbury et al. 2018) for the framework and JAXopt (Blondel et al. 2022) for the optimizer. The paper does not specify version numbers for JAX or JAXopt. While other solvers like Pal SAT, Walk SAT, PRS, CMS, Gpu Share SAT, Para Frost, Lin PB, No SAT-Max SAT, Loandra, and Nu WLS-c are mentioned, their specific version numbers are not provided. |
| Experiment Setup | Yes | Timeout is 300 s unless specifically stated. Each experiment for CPU solvers uses 32 CPU threads... In practice, we use α = 0.1 to adapt the weight as follows... we use Cadical195 and Gluecard4 from Py SAT (Ignatiev, Morgado, and Marques Silva 2018) to enumerate multiple models, which are used to warm-start the CLS component in parallel. |