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 |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 5: | Line 5: | ||
''written by [[Tobias_Philipp]]'' | ''written by [[Tobias_Philipp]]'' | ||
===Abstract=== | |||
Pseudo-Boolean (PB) constraints frequently occur in translations from NP-complete problems to the propositional satisfiability problem. | Pseudo-Boolean (PB) constraints frequently occur in translations from NP-complete problems to the propositional satisfiability problem. | ||
| Line 12: | Line 14: | ||
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]] | |||
Latest revision as of 20:57, 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
Abstract
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
