SAT Core similar to UNSAT Core

Question

I know that there is the possibility to obtain an UNSAT-Core in Z3. But is it also possible to get something you might call SAT-Core? That means if we have a satisfiable instance then there is also a Model for all variables. A Sat-Core would be a Sub-Model minimum in size with the property that all other variables receive their value through propagation of constraints.

Answer 1

I don't think this is a well-defined concept; think about having two variables a and b, with the constraint a = Not(b), and you assert both a and b. No matter which you pick, the other is determined by constant-propagation; but there's no reason to prefer one over the other.

Of course you can look for an "arbitrary" such set, but that makes it less useful; also minimality, just like in the unset-core case, would be very hard to guarantee in a traditional SAT/SMT solver.

However, there's a related notion of consequences in z3. See https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences for details. The idea is you want to find out what literals are necessarily true in any model. This is an interesting problem, as it shows you under the constraints you put in, what part of the variable space is no longer relevant as it is always forced. These literals are called the backbone literals as well, see https://sat.inesc-id.pt/~mikolas/bb-aicom-preprint.pdf for details.