SAT solving with GPU accelerated inprocessing
Abstract: Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver ParaFROST solves many benchmarks faster on the GPU than its sequential counterparts
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
ISBN: 978-3-030-72016-2
ISSN: 1611-3349
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2023
- Creator
- DOI
-
10.1007/978-3-030-72016-2_8
- URN
-
urn:nbn:de:bsz:25-freidok-2393777
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
25.03.2025, 1:44 PM CET
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Osama, Muhammad
- Wijs, Anton
- Biere, Armin
- Universität
Time of origin
- 2023
Other Objects (12)
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra
Parallel Algorithms for GPU accelerated Probabilistic Inference
Advanced Methods for SAT Solving
SAT solving with message passing
Design and Development of a GPU-Accelerated Micromagnetic Simulator
GPU‐accelerated simulation of a non‐local conservation law
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra
Parallel Algorithms for GPU accelerated Probabilistic Inference
Advanced Methods for SAT Solving
SAT solving with message passing
Design and Development of a GPU-Accelerated Micromagnetic Simulator
GPU‐accelerated simulation of a non‐local conservation law
Certified SAT solving with GPU accelerated inprocessing
SAT Solving with GPU Accelerated Inprocessing
SAT Solving mit GPU Unterstützung
SAT-Solving mit GPU-Unterstützung
GPU-accelerated adjoint algorithmic differentiation
GPU Accelerated Visualization for Neurostimulation Therapy
Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra
Parallel Algorithms for GPU accelerated Probabilistic Inference
Advanced Methods for SAT Solving
SAT solving with message passing
Design and Development of a GPU-Accelerated Micromagnetic Simulator