Verifying the DPLL Algorithm in Dafny
The work
| Authors | Cezar-Constantin Andrici; Ştefan Ciobâcă |
|---|---|
| Editors | |
| Type | misc |
| Year | 2019 |
| Citekey | andrici2019verifying |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|
Identifiers
| arXiv | 1909.01743 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.303.1 |
Access
| Landing page | https://arxiv.org/abs/1909.01743 |
|---|
Related
| Distinct from | bryant2021dual |
|---|---|
| Distinct from | chakraborty2015wordlevel |
| Distinct from | davis2013verified |
| Distinct from | een2011efficient |
| Distinct from | nukala2024translating |
| Superseded by | andrici2020who |
From bibtex.
Abstract
Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness which can be checked independently in the form of a satisfying truth assignment. However, if the instance is unsatisfiable, the certificates could be exponentially large or the SAT solver might not be able to output certificates. The implementation of the SAT solver should then be trusted not to contain bugs. However, the data structures and algorithms implemented by a typical high-performance SAT solver are complex enough to allow for subtle programming errors. To counter this issue, we build a verified SAT solver using the Dafny system. We discuss its implementation in the present article.
A copy is held
pdf, 158.3 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 00:14 UTC |
| Approved by | a person 2026-09-17 17:06 UTC |
Filed under
Cite it as
@misc{andrici2019verifying,
title = {Verifying the DPLL Algorithm in Dafny},
author = {Cezar-Constantin Andrici and Ştefan Ciobâcă},
year = {2019},
journal = {Electronic Proceedings in Theoretical Computer Science},
doi = {10.4204/eptcs.303.1},
}
This record lives at https://refs.drheap.org/andrici2019verifying/ and will keep doing so.