Computing desk
< June 24	<< May \| June \| Jul >>	Current desk >

Welcome to the Wikipedia Computing Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

June 25

SAT Solver's non-existence certificate

So apparently a SAT Solver can return a certificate to prove its conclusion that there are no solutions. I don't know what the certificate for this would look like. Can someone point me to some information on non-existence certificates? Thank you. RJFJR (talk) 22:04, 25 June 2022 (UTC)[reply]

I don't know what I'm looking at here but I see the words Certified UNSAT ... 3 different UNSAT certificate types ... Certified UNSAT solver output example, is this any help? Card Zero (talk) 22:52, 25 June 2022 (UTC)[reply]

As defined in that document it is basically the same as the proof of unsatisfiability. Not as snappy as a certificate of satisfiability (being the satisfying assignment), but still, checking a proof is much easier than finding one. --Lambiam 08:15, 26 June 2022 (UTC)[reply]

Thank you. I think I understand the idea now. RJFJR (talk) 18:36, 26 June 2022 (UTC)[reply]

UNSAT is in co-NP so there is (as far as we know) no succinct certificate for it. The best you can hope for is a formally verified prover, which means that after you run it and it says "unsatisfiable", you can trust the result. That takes (like a SAT solver) potentially exponential time, but only a reasonable amount of space. There is something about a formally verified UNSAT prover and SAT solver here, but I haven't looked into it. 2601:648:8202:350:0:0:0:FD2B (talk) 05:23, 2 July 2022 (UTC)[reply]