Parallel SAT simplification on GPU architectures

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    36 Downloads (Pure)

    Abstract

    The growing scale of applications encoded to Boolean Satisfiability (SAT) problems imposes the need for accelerating SAT simplifications or preprocessing. Parallel SAT preprocessing has been an open challenge for many years. Therefore, we propose novel parallel algorithms for variable and subsumption elimination targeting Graphics Processing Units (GPUs). Benchmarks show that the algorithms achieve an acceleration of 66 × over a state-of-the-art SAT simplifier (SatELite). Regarding SAT solving, we have conducted a thorough evaluation, combining both our GPU algorithms and SatELite with MiniSat to solve the simplified problems. In addition, we have studied the impact of the algorithms on the solvability of problems with Lingeling. We conclude that our algorithms have a considerable impact on the solvability of SAT problems.

    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
    EditorsLijun Zhang, Tomáš Vojnar
    Place of PublicationCham
    PublisherSpringer
    Pages21-40
    Number of pages20
    ISBN (Electronic)978-3-030-17462-0
    ISBN (Print)978-3-030-17461-3
    DOIs
    Publication statusPublished - 1 Jan 2019
    Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
    Duration: 6 Apr 201911 Apr 2019

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume11427 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
    CountryCzech Republic
    CityPrague
    Period6/04/1911/04/19

    Keywords

    • GPU
    • Parallel SAT preprocessing
    • Satisfiability
    • Subsumption elimination
    • Variable elimination

    Fingerprint Dive into the research topics of 'Parallel SAT simplification on GPU architectures'. Together they form a unique fingerprint.

    Cite this