A Verified Implementation of the DPLL Algorithm in Dafny
We present a DPLL SAT solver, which we call TrueSAT, developed in the verification-enabled programming language Dafny. We have fully verified the functional correctness of our solver by constructing machine-checked proofs of its soundness, completeness, and termination. We present a benchmark of the...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-06-01
|
| Series: | Mathematics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2227-7390/10/13/2264 |
| _version_ | 1827625947167195136 |
|---|---|
| author | Cezar-Constantin Andrici Ștefan Ciobâcă |
| author_facet | Cezar-Constantin Andrici Ștefan Ciobâcă |
| author_sort | Cezar-Constantin Andrici |
| collection | DOAJ |
| description | We present a DPLL SAT solver, which we call TrueSAT, developed in the verification-enabled programming language Dafny. We have fully verified the functional correctness of our solver by constructing machine-checked proofs of its soundness, completeness, and termination. We present a benchmark of the execution time of TrueSAT and we show that it is competitive against an equivalent DPLL solver implemented in C++, although it is still slower than state-of-the-art CDCL solvers. Our solver serves as a significant case study of a machine-verified software system. The benchmark also shows that auto-active verification is a promising approach to increasing trust in SAT solvers, because it combines execution speed with a high degree of trustworthiness. |
| first_indexed | 2024-03-09T12:45:50Z |
| format | Article |
| id | doaj.art-6923e3f10b7b46c6b259db9a8776be6e |
| institution | Directory Open Access Journal |
| issn | 2227-7390 |
| language | English |
| last_indexed | 2024-03-09T12:45:50Z |
| publishDate | 2022-06-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Mathematics |
| spelling | doaj.art-6923e3f10b7b46c6b259db9a8776be6e2023-11-30T22:11:48ZengMDPI AGMathematics2227-73902022-06-011013226410.3390/math10132264A Verified Implementation of the DPLL Algorithm in DafnyCezar-Constantin Andrici0Ștefan Ciobâcă1Max Planck Institute for Security and Privacy, 44799 Bochum, GermanyFaculty of Computer Science, Alexandru Ioan Cuza University, 700506 Iași, RomaniaWe present a DPLL SAT solver, which we call TrueSAT, developed in the verification-enabled programming language Dafny. We have fully verified the functional correctness of our solver by constructing machine-checked proofs of its soundness, completeness, and termination. We present a benchmark of the execution time of TrueSAT and we show that it is competitive against an equivalent DPLL solver implemented in C++, although it is still slower than state-of-the-art CDCL solvers. Our solver serves as a significant case study of a machine-verified software system. The benchmark also shows that auto-active verification is a promising approach to increasing trust in SAT solvers, because it combines execution speed with a high degree of trustworthiness.https://www.mdpi.com/2227-7390/10/13/2264DPLLDafnyformal verificationauto-active verificationsatisfiability solving |
| spellingShingle | Cezar-Constantin Andrici Ștefan Ciobâcă A Verified Implementation of the DPLL Algorithm in Dafny Mathematics DPLL Dafny formal verification auto-active verification satisfiability solving |
| title | A Verified Implementation of the DPLL Algorithm in Dafny |
| title_full | A Verified Implementation of the DPLL Algorithm in Dafny |
| title_fullStr | A Verified Implementation of the DPLL Algorithm in Dafny |
| title_full_unstemmed | A Verified Implementation of the DPLL Algorithm in Dafny |
| title_short | A Verified Implementation of the DPLL Algorithm in Dafny |
| title_sort | verified implementation of the dpll algorithm in dafny |
| topic | DPLL Dafny formal verification auto-active verification satisfiability solving |
| url | https://www.mdpi.com/2227-7390/10/13/2264 |
| work_keys_str_mv | AT cezarconstantinandrici averifiedimplementationofthedpllalgorithmindafny AT stefanciobaca averifiedimplementationofthedpllalgorithmindafny AT cezarconstantinandrici verifiedimplementationofthedpllalgorithmindafny AT stefanciobaca verifiedimplementationofthedpllalgorithmindafny |