VerifiedPBEncoder/en: Difference between revisions
From International Center for Computational Logic
Tobias Philipp (talk | contribs) (Die Seite wurde neu angelegt: „ '''VerifiedPBEncoder is a mechanically verified Haskell library that translates pseudo-Boolean (PB) constraints into a formulas in conjunctive normal form. '…“) |
Tobias Philipp (talk | contribs) No edit summary |
||
| Line 3: | Line 3: | ||
'''VerifiedPBEncoder is a mechanically verified Haskell library that translates pseudo-Boolean (PB) constraints into a formulas in conjunctive normal form. | '''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. | Pseudo-Boolean (PB) constraints frequently occur in translations from NP-complete problems to the propositional satisfiability problem. | ||
Revision as of 16:13, 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.
