17 ms·
Maybe I'm missing something blindingly obvious, but why is "trusting" a SAT solver necessary in the first place? The solution itself either satisfies the constr
by jhgb 4y ago
Maybe I'm missing something blindingly obvious, but why is "trusting" a SAT solver necessary in the first place? The solution itself either satisfies the constraints or it does not. Are there situations where we can't even tell whether the solution is correct by looking at the problem instance?
- Jweb_Guru 4y agoFor 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.