Certified SAT solving with GPU accelerated inprocessing
Abstract: Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As one of the main challenges in GPU programming is memory locality, we present new compact data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improve memory locality. Our new parallel variable elimination algorithm is roughly twice as fast as previous work. Moreover, we augment the variable elimination with the first parallel algorithm for functional dependency extraction in an attempt to find more logical gates to eliminate that cannot be found with syntactic approaches. We present a novel algorithm to generate clausal proofs in parallel to validate all simplifications running on the GPU besides the CDCL search, giving high credibility to our solver and its use in critical applications such as model checkers. In experiments, our new solver PARAFROST solves numerous benchmarks faster on the GPU than its sequential counterparts. With functional dependency extraction, inprocessing in PARAFROST was more effective in reducing the solving time. Last but not least, all proofs generated by PARAFROST were successfully verified
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
Formal methods in system design. - 62, 1-3 (2024) , 79-118, ISSN: 1572-8102
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2023
- Creator
- Contributor
- DOI
-
10.1007/s10703-023-00432-z
- URN
-
urn:nbn:de:bsz:25-freidok-2393696
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
14.08.2025, 11:04 AM CEST
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Osama, Muhammad
- Wijs, Anton
- Biere, Armin
- Albert-Ludwigs-Universität Freiburg im Breisgau. Lehrstuhl für Rechnerarchitektur
- Universität
Time of origin
- 2023
Other Objects (12)
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT solving with GPU accelerated inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
G.A.M.E.: GPU-accelerated mixture elucidator
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
GPU accelerated voxel-based machining simulation
Parallel Algorithms for GPU accelerated Probabilistic Inference
SAT solving with message passing
Advanced Methods for SAT Solving
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT solving with GPU accelerated inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
G.A.M.E.: GPU-accelerated mixture elucidator
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
GPU accelerated voxel-based machining simulation
Parallel Algorithms for GPU accelerated Probabilistic Inference
SAT solving with message passing
Advanced Methods for SAT Solving
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT solving with GPU accelerated inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
G.A.M.E.: GPU-accelerated mixture elucidator
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
GPU accelerated voxel-based machining simulation
Parallel Algorithms for GPU accelerated Probabilistic Inference
SAT solving with message passing