Efficient satisfiability solver
dc.contributor.advisor | Ting Zhang | |
dc.contributor.advisor | Wensheng Zhang | |
dc.contributor.author | Jiang, Chuan | |
dc.contributor.department | Computer Science | |
dc.date | 2018-08-11T11:01:42.000 | |
dc.date.accessioned | 2020-06-30T02:52:44Z | |
dc.date.available | 2020-06-30T02:52:44Z | |
dc.date.copyright | Wed Jan 01 00:00:00 UTC 2014 | |
dc.date.embargo | 2001-01-01 | |
dc.date.issued | 2014-01-01 | |
dc.description.abstract | <p>The past few decades saw great improvements in the performance of satisfiability (SAT) solvers. In this thesis, we discuss the state-of-the-art techniques used in building an efficient SAT solver. Modern SAT solvers are mainly constituted by the following components: decision heuristics, Boolean constraint propagation, conflict analysis, restart, clause deletion and preprocessing. Various algorithms and implementations in each component will be discussed and analyzed. Then we propose a new backtracking strategy, partial backtracking, which can be easily implemented in SAT solvers. It is essentially an extension of the backtracking strategy used in most SAT solvers. With partial backtracking, the solver consecutively amends the variable assignments instead of discarding them completely so that it does not backtrack as many levels as the classic strategy does after analyzing a conflict. We implemented this strategy in our solver Nigma and the experiments show that the solver benefits from this adjustment.</p> | |
dc.format.mimetype | application/pdf | |
dc.identifier | archive/lib.dr.iastate.edu/etd/13869/ | |
dc.identifier.articleid | 4876 | |
dc.identifier.contextkey | 5777583 | |
dc.identifier.doi | https://doi.org/10.31274/etd-180810-2105 | |
dc.identifier.s3bucket | isulib-bepress-aws-west | |
dc.identifier.submissionpath | etd/13869 | |
dc.identifier.uri | https://dr.lib.iastate.edu/handle/20.500.12876/28056 | |
dc.language.iso | en | |
dc.source.bitstream | archive/lib.dr.iastate.edu/etd/13869/Jiang_iastate_0097M_14035.pdf|||Fri Jan 14 20:02:50 UTC 2022 | |
dc.subject.disciplines | Computer Sciences | |
dc.subject.keywords | backtracking | |
dc.subject.keywords | conflict-driven clause learning | |
dc.subject.keywords | satisfiability | |
dc.title | Efficient satisfiability solver | |
dc.type | article | |
dc.type.genre | thesis | |
dspace.entity.type | Publication | |
relation.isOrgUnitOfPublication | f7be4eb9-d1d0-4081-859b-b15cee251456 | |
thesis.degree.level | thesis | |
thesis.degree.name | Master of Science |
File
Original bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- Jiang_iastate_0097M_14035.pdf
- Size:
- 299.55 KB
- Format:
- Adobe Portable Document Format
- Description: