When the result is unsat, it is possible to give some counterexamples? And how to do that?

Feb 13, 2013 at 4:47 PM
When the result is unsat, it is possible to give some counterexamples? And how to do that?
Coordinator
Feb 13, 2013 at 4:58 PM
We say a formula is unsatisfiable when it does not have any model/solution. Similarly, we say a formula is satisfiable when it has a model/solution.
In Z3, to prove that a fomula F is valid (i.e., it is true in any interpretation), we show that its negation is unsatisfiable.
So, a counterexample is a model/solution for the negation of F. Note that, in this case the negation of F is sat.

Models and counterexamples are associated with satisfiable instances.

For unsatisfiable instances, Z3 can produce a proof or extract unsatisfiable cores.