ToySolver.Converter.PB2SAT

Documentation

convert :: Formula -> (CNF, Model -> Model, Model -> Model)

Convert a pseudo boolean formula φ to a equisatisfiable CNF formula ψ together with two functions f and g such that:

• if M ⊨ φ then f(M) ⊨ ψ
• if M ⊨ ψ then g(M) ⊨ φ