3 ms·
Right, 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 pro
by dwheeler 4y ago
Right, 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.