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