VerifiedPBEncoder
Aus International Center for Computational Logic
VerifiedPBEncoder is a mechanically verified Haskell library that translates pseudo-Boolean (PB) constraints into a formulas in conjunctive normal form.
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.
