Iterating over unsat cores

Question

I use (get-unsat-core) in Z3 to extract an unsat-core of an unsatisfiable set of constraints. However, some constraints may have more than one unsat core. In such cases, is there any way to iterate over unsat-cores?

Answer 1

Yes, but it isn't totally straight-forward. The MARCO algorithm by Mark Liffiton and collaborators and variants are good bets for extracting multiple cores. The Z3 distribution comes with a Python example of a simplified MARCO algorithm. There are other variants described on http://theory.stanford.edu/~nikolaj/mod.html#/sec-cores-correction-sets-satisfying-assignments