The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

It actually is practical, since answers of UNSAT do not always come with 
certificates, and are exponential in size, generally. A certified DPLL 
implementation does not also need to remember all of the resolutions it's 
made to produce a certificate. In testing different SMT solvers' bitvector 
reasoning capabilities, I found that CVC3 could "prove" my theorem regardless 
of the bit-width instantiation I went with (the others I tried choked after 8 
bits or something). When I asked for the certificate however, the tool just 
crashed. Not a lot of confidence there.

I think the versat team showed that on the satlib benchmark suite, their tool 
has competitive performance as picosat with additional certification checking.
-Ian
----- Original Message -----
From: "Kristopher Micinski" 
<krismicinski AT gmail.com>
To: "Bradford Larsen" 
<brad.larsen AT gmail.com>
Cc: "coq club" 
<coq-club AT inria.fr>
Sent: Wednesday, December 4, 2013 7:31:09 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Formalization of SAT solver-related problems?


While this 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? 


Kris 





On Wed, Dec 4, 2013 at 4:53 PM, Bradford Larsen < 
brad.larsen AT gmail.com
 > wrote: 



Is there any work proving the correctness of the Tseitin transformation or 
other propositional logic transformations in Coq? 


More generally, I'm interested in seeing what existing work has been done on 
formalizing the algorithms used in SAT/SMT solvers. 


Thanks, 
Brad Larsen