3 ms·
For positive solutions, you are correct--verifying the solution is incredibly easy. For negative solutions (UNSAT), however, this is not the case--UNSAT is in
by Jweb_Guru 4y ago
For positive solutions, you are correct--verifying the solution is incredibly easy. For negative solutions (UNSAT), however, this is not the case--UNSAT is in Co-NP, not NP. Finding an efficiently verifiable representation of the UNSAT proof can be very challenging, which is part of why solvers are given much more time to produce and verify certificates than they are to solve the problem in the first place.
- jhgb 4y agoAhh, I see now what you mean. Thanks, that makes much more sense to me now.
- dwheeler 4y agoRight, unsat is the interesting case where you especially want a proof of the SAT solver. Unsat can be used, in turn, to prove other things. If you want to prove that some condition C is always true in a set of expressions, just ask the SAT solver to solve for "not C". If the answer is UNSAT, then C is always true... if the answer UNSAT is actually correct.