VerifiedPBEncoder/en: Difference between revisions
From International Center for Computational Logic
Tobias Philipp (talk | contribs) No edit summary |
Tobias Philipp (talk | contribs) No edit summary |
||
| Line 12: | Line 12: | ||
It also contains an optimized encoder for at-most-k constraints. | It also contains an optimized encoder for at-most-k constraints. | ||
[[Datei:verifiedpbencoder.zip]] | |||
==Downloads== | |||
* The extracted Haskell code [[Datei:verifiedpbencoder.zip]] | |||
* The Coq code [[Datei:coqsrc.zip]] | |||
Revision as of 20:56, 14 May 2015
VerifiedPBEncoder is a mechanically verified Haskell library that translates pseudo-Boolean (PB) constraints into a formulas in conjunctive normal form.
written by Tobias_Philipp
Pseudo-Boolean (PB) constraints frequently occur in translations from NP-complete problems to the propositional satisfiability problem. However, Aavani et al. have discovered incorrect translations in the state-of-the-art tool minisat+. We therefore propose to develop functional programs that encode complex constraints and proof them afterwards using interactive theorem provers. VerifiedPBEncoder is verified within the Coq proof assistant and Haskell code is extracted by Coq. It also contains an optimized encoder for at-most-k constraints.
Downloads
- The extracted Haskell code Datei:Verifiedpbencoder.zip
- The Coq code Datei:Coqsrc.zip
