Certified SAT solving with GPU accelerated inprocessing

Muhammad Osama (Corresponding author), Anton Wijs, Armin Biere

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

1 Citaat (Scopus)

Samenvatting

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.

Originele taal-2Engels
TijdschriftFormal Methods in System Design
VolumeXX
Nummer van het tijdschriftX
DOI's
StatusGeaccepteerd/In druk - 2023

Bibliografische nota

Funding Information:
This work is part of the GEARS project with project number TOP2.16.044, which is (partly) financed by the Netherlands Organisation for Scientific Research (NWO). In addition, this work made use of the Dutch national e-infrastructure with the support of the SURF Cooperative using Grant No. EINF-1688. The third author was supported by the LIT AI Lab funded by the Upper State of Austria.We would like to thank the anonymous reviewers for their valuable feedback to improve an earlier version of this manuscript.

Vingerafdruk

Duik in de onderzoeksthema's van 'Certified SAT solving with GPU accelerated inprocessing'. Samen vormen ze een unieke vingerafdruk.

Citeer dit