4 ms·
Producing the proofs (especially for UNSAT) is often very time consuming, and verifying them can be subtle (and if an incorrect proof is produced, you still hav
by Jweb_Guru 4y ago
Producing the proofs (especially for UNSAT) is often very time consuming, and verifying them can be subtle (and if an incorrect proof is produced, you still have to deal with that case somehow...). It's not so much that they negate the need for verified SAT solvers as that creating and maintaining a verified SAT solver was considered much too difficult to justify the proof effort required. If the goal can be accomplished with an order of magnitude less effort, that calculus changes somewhat.
- zozbot234 4y agoSAT solving is the subtle and time consuming part. A valid SAT proof certificate can be verified efficiently.
- Jweb_Guru 4y agoI'm referring to producing the certificate as the time-consuming part, not the verification time (I disagree that verification is not subtle, but I suppose that doesn't matter as there are verified verifiers). For example, many SAT solvers no longer attempt to provide "pure" resolution proofs because they are too expensive to produce, which restricts the kinds of techniques you see used in competition. In fact, producing certificates efficiently is an active research area, which wouldn't be the case if certificate production had negligible cost, e.g. see https://lmcs.episciences.org/9357/pdf https://lmcs.episciences.org/9357/pdf.
- xavxav 4y agoSAT comp gives you 5x the solving time to check your proof, which is indicative that checking isn’t so simple (though it is on paper)