VPB: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 3: | Zeile 3: | ||
We developed a verified decision procedure for pseudo-Boolean constraints. | We developed a verified decision procedure for pseudo-Boolean constraints. | ||
You can find the verified encoder, a SAT solver that supports proof emission here: [[Datei:VPB.zip]] | You can find the verified encoder, a SAT solver that supports proof emission here: [[Datei:VPB.zip]] | ||
The Coq files can be downloaded from here: [[Datei:SWC.v]] | |||
Aktuelle Version vom 21. Oktober 2016, 22:13 Uhr
A Verified Decision Procedure for Pseudo-Boolean Formulas
We developed a verified decision procedure for pseudo-Boolean constraints. You can find the verified encoder, a SAT solver that supports proof emission here: Datei:VPB.zip The Coq files can be downloaded from here: Datei:SWC.v
