Parallel SAT simplification on GPU architectures

Muhammad Osama; Anton Wijs

doi:10.1007/978-3-030-17462-0_2

Parallel SAT simplification on GPU architectures

Muhammad Osama, Anton Wijs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

13 Citations (Scopus)

91 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 language	English
Title of host publication	Tools 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
Editors	Lijun Zhang, Tomáš Vojnar
Place of Publication	Cham
Publisher	Springer
Pages	21-40
Number of pages	20
ISBN (Electronic)	978-3-030-17462-0
ISBN (Print)	978-3-030-17461-3
DOIs	https://doi.org/10.1007/978-3-030-17462-0_2
Publication status	Published - 1 Jan 2019
Event	25th 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 2019 → 11 Apr 2019

Publication series

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

Conference

Conference	25th 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
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 11/04/19

Funding

M. Osama—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). A. Wijs—We gratefully acknowledge the support of NVIDIA Corporation with the donation of the GeForce Titan Xp’s used for this research.

Keywords

GPU
Parallel SAT preprocessing
Satisfiability
Subsumption elimination
Variable elimination

Access to Document

10.1007/978-3-030-17462-0_2

publishers versionFinal published version, 2.24 MB

Cite this

Osama, M., & Wijs, A. (2019). Parallel SAT simplification on GPU architectures. In L. Zhang, & T. Vojnar (Eds.), Tools 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 (pp. 21-40). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS). Springer. https://doi.org/10.1007/978-3-030-17462-0_2

Osama, Muhammad ; Wijs, Anton. / Parallel SAT simplification on GPU architectures. Tools 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. editor / Lijun Zhang ; Tomáš Vojnar. Cham : Springer, 2019. pp. 21-40 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{52c102d71ef34a059d2e564b5736593b,

title = "Parallel SAT simplification on GPU architectures",

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.",

keywords = "GPU, Parallel SAT preprocessing, Satisfiability, Subsumption elimination, Variable elimination",

author = "Muhammad Osama and Anton Wijs",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-17462-0_2",

language = "English",

isbn = "978-3-030-17461-3",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "21--40",

editor = "Lijun Zhang and Tom{\'a}{\v s} Vojnar",

booktitle = "Tools 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",

address = "Germany",

note = "25th 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 ; Conference date: 06-04-2019 Through 11-04-2019",

}

Osama, M & Wijs, A 2019, Parallel SAT simplification on GPU architectures. in L Zhang & T Vojnar (eds), Tools 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11427 LNCS, Springer, Cham, pp. 21-40, 25th 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, 6/04/19. https://doi.org/10.1007/978-3-030-17462-0_2

Parallel SAT simplification on GPU architectures. / Osama, Muhammad; Wijs, Anton.
Tools 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. ed. / Lijun Zhang; Tomáš Vojnar. Cham: Springer, 2019. p. 21-40 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Parallel SAT simplification on GPU architectures

AU - Osama, Muhammad

AU - Wijs, Anton

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

KW - GPU

KW - Parallel SAT preprocessing

KW - Satisfiability

KW - Subsumption elimination

KW - Variable elimination

UR - http://www.scopus.com/inward/record.url?scp=85064914062&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17462-0_2

DO - 10.1007/978-3-030-17462-0_2

M3 - Conference contribution

AN - SCOPUS:85064914062

SN - 978-3-030-17461-3

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 21

EP - 40

BT - Tools 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

A2 - Zhang, Lijun

A2 - Vojnar, Tomáš

PB - Springer

CY - Cham

T2 - 25th 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

Y2 - 6 April 2019 through 11 April 2019

ER -

Osama M, Wijs A. Parallel SAT simplification on GPU architectures. In Zhang L, Vojnar T, editors, Tools 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. Cham: Springer. 2019. p. 21-40. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-17462-0_2

Parallel SAT simplification on GPU architectures

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this