The Coq mailing list

[Bradford Larsen <brad.larsen AT gmail.com>]

On Wed, Dec 4, 2013 at 7:31 PM, Kristopher Micinski <krismicinski AT gmail.com> wrote:

While [proving the correctness of the Tseitin transformation or other propositional logic transformations in Coq] seems interesting as an academic pursuit, I wonder if it's at all practical.  Are there any SAT solvers which don't also output certificates?

Most SAT solvers expect CNF input, whereas when modeling a problem you usually want a richer language of propositional logic.  A certificate from a SAT solver doesn't help you determine if you've made a mistake in the translation into CNF.

Similar reasoning applies for other simplification passes or translations you might be interested in doing on a rich (i.e., non-CNF) language of propositional logic.

Brad