Parallel optimization for satisfiability problem solving.
Saved in:
| Title: | Parallel optimization for satisfiability problem solving. |
|---|---|
| Authors: | LI, Ji1, ZHOU, Lei2, GONG, Chunye3,4, MA, Di3, SHEN, Yulin5, ZHANG, Xiang3 zhangxiang08@nudt.edu.cn |
| Source: | Computer Engineering & Science / Jisuanji Gongcheng yu Kexue. May2026, Vol. 48 Issue 5, p793-802. 10p. |
| Subjects: | Satisfiability (Computer science), Parallel programming, Constraint satisfaction, Software verification, Verification of computer systems |
| Abstract: | The satisfiability problem (SAT) solver is widely applied in fields such as hardware and software verification, information security, and computational biology. Current optimizations of SAT solvers primarily focus on reducing the solution space of formulas and simplifying the entire solving formula. However, reducing the solution space faces challenges such as slow space reduction and insufficient parallel granularity, while formula simplification exhibits poor performance when combined with existing parallel strategies for solving small-scale problems. This paper introduces kissat++, developed based on kissat, the fastest serial SAT solver to date. Specifically, we propose a fine-grained parallel algorithm for unit propagation using observation list-based dynamic blocking techniques and introduce guided paths to achieve coarse-grained parallel optimization during the search space partitioning process. To further enhance space partitioning efficiency, factors such as decision levels are considered when constructing guided paths to select key variables early, thereby reducing the search space on each process. Experimental results on the Tianhe supercomputer demonstrate that kissat++ achieves more than a 2x speedup compared to the original kissat. Additionally, it solves 49 more instances within the time limit on the SAT benchmark set and ranks ninth among the 16 solvers submitted to the parallel track of the 2023 competition. [ABSTRACT FROM AUTHOR] |
| Copyright of Computer Engineering & Science / Jisuanji Gongcheng yu Kexue is the property of Computer Engineering & Science and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 194237693 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Parallel optimization for satisfiability problem solving. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22LI%2C+Ji%22">LI, Ji</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22ZHOU%2C+Lei%22">ZHOU, Lei</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22GONG%2C+Chunye%22">GONG, Chunye</searchLink><relatesTo>3,4</relatesTo><br /><searchLink fieldCode="AR" term="%22MA%2C+Di%22">MA, Di</searchLink><relatesTo>3</relatesTo><br /><searchLink fieldCode="AR" term="%22SHEN%2C+Yulin%22">SHEN, Yulin</searchLink><relatesTo>5</relatesTo><br /><searchLink fieldCode="AR" term="%22ZHANG%2C+Xiang%22">ZHANG, Xiang</searchLink><relatesTo>3</relatesTo><i> zhangxiang08@nudt.edu.cn</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Computer+Engineering+%26+Science+%2F+Jisuanji+Gongcheng+yu+Kexue%22">Computer Engineering & Science / Jisuanji Gongcheng yu Kexue</searchLink>. May2026, Vol. 48 Issue 5, p793-802. 10p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Satisfiability+%28Computer+science%29%22">Satisfiability (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Parallel+programming%22">Parallel programming</searchLink><br /><searchLink fieldCode="DE" term="%22Constraint+satisfaction%22">Constraint satisfaction</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Verification+of+computer+systems%22">Verification of computer systems</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: The satisfiability problem (SAT) solver is widely applied in fields such as hardware and software verification, information security, and computational biology. Current optimizations of SAT solvers primarily focus on reducing the solution space of formulas and simplifying the entire solving formula. However, reducing the solution space faces challenges such as slow space reduction and insufficient parallel granularity, while formula simplification exhibits poor performance when combined with existing parallel strategies for solving small-scale problems. This paper introduces kissat++, developed based on kissat, the fastest serial SAT solver to date. Specifically, we propose a fine-grained parallel algorithm for unit propagation using observation list-based dynamic blocking techniques and introduce guided paths to achieve coarse-grained parallel optimization during the search space partitioning process. To further enhance space partitioning efficiency, factors such as decision levels are considered when constructing guided paths to select key variables early, thereby reducing the search space on each process. Experimental results on the Tianhe supercomputer demonstrate that kissat++ achieves more than a 2x speedup compared to the original kissat. Additionally, it solves 49 more instances within the time limit on the SAT benchmark set and ranks ninth among the 16 solvers submitted to the parallel track of the 2023 competition. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Computer Engineering & Science / Jisuanji Gongcheng yu Kexue is the property of Computer Engineering & Science and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=194237693 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.3969/j.issn.1007-130X.2026.05.004 Languages: – Code: chi Text: Chinese PhysicalDescription: Pagination: PageCount: 10 StartPage: 793 Subjects: – SubjectFull: Satisfiability (Computer science) Type: general – SubjectFull: Parallel programming Type: general – SubjectFull: Constraint satisfaction Type: general – SubjectFull: Software verification Type: general – SubjectFull: Verification of computer systems Type: general Titles: – TitleFull: Parallel optimization for satisfiability problem solving. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: LI, Ji – PersonEntity: Name: NameFull: ZHOU, Lei – PersonEntity: Name: NameFull: GONG, Chunye – PersonEntity: Name: NameFull: MA, Di – PersonEntity: Name: NameFull: SHEN, Yulin – PersonEntity: Name: NameFull: ZHANG, Xiang IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 05 Text: May2026 Type: published Y: 2026 Identifiers: – Type: issn-print Value: 1007130X Numbering: – Type: volume Value: 48 – Type: issue Value: 5 Titles: – TitleFull: Computer Engineering & Science / Jisuanji Gongcheng yu Kexue Type: main |
| ResultId | 1 |
