A Verified Implementation of the DPLL Algorithm in Dafny

Cezar-Constantin Andrici and Ștefan Ciobâcă
Additional contact information
Cezar-Constantin Andrici: Max Planck Institute for Security and Privacy, 44799 Bochum, Germany
Ștefan Ciobâcă: Faculty of Computer Science, Alexandru Ioan Cuza University, 700506 Iași, Romania

Mathematics, 2022, vol. 10, issue 13, 1-26

Abstract: 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.

Keywords: DPLL; Dafny; formal verification; auto-active verification; satisfiability solving (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2022
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/10/13/2264/pdf (application/pdf)
https://www.mdpi.com/2227-7390/10/13/2264/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:10:y:2022:i:13:p:2264-:d:850381

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().