Detect Unsatisfiable Model in a Satisfiable Problem

[mfazelnia]

I'm looking to identify any unsatisfiable cases in a set of statements. I understand Z3 can identify unsatisfiability and unsatisfiable subsets as long as the problem is unsatisfiable. Can Z3 also pinpoint unsatisfiable assignments within a satisfiable problem?

For instance, consider the following statements:

1. If A > B, then C = 0
2. If A > B, then D = 0
3. C != 0
   Here, a conflict arises if A > B, while the whole problem is satisfiable when A <= B. I want to avoid checking every possible combination manually, or adding negated statement to the model. Can Z3 help identify such conflicting cases? Ideally, is it possible for it to generate the (minimal) unsatisfiable subset?

[mfazelnia]

Any suggestions how to directly find an unsatisfiable model in a satisfiable problem with Z3?

[mfazelnia]

Thanks, I don't actually need every unsatisfiable assignment; even one is fine. Is there a way to ensure I can find such an assignment if it exists? I'm afraid dumping the learned clauses might miss the unsatisfiable assignment.

[ThomasHaas]

I'm afraid dumping the learned clauses might miss the unsatisfiable assignment.

I'm not sure I understand. Every single clause gives you an unsatisfiable assignment, namely the assignment that falsifies this clause, so you can freely pick. Are you looking for a specific assignment?

[mfazelnia]

Could you provide more details? For instance, can you show how I can apply that to the example I shared above? Specifically, I'm interested in the cases where A > B, making the entire set unsatisfiable.

[ThomasHaas]

Your example consists of the clauses

1) not (A > B) or C = 0
2) not (A > B) or D = 0
3) not (C = 0)  // C != 0

The following partial assignments (on the boolean level) lead to unsatisfiable formulas:
From 1) you get (A > B) and not (C = 0), from 2) you get (A > B) and not (D = 0) and from 3) you get C = 0 (all obtained by just negating the clauses).
Each of these three is trivially unsatisfiable. You could actually do "resolution" on these partial assignments and obtain
from 1) + 3) that "A > B" on its own is unsatisfiable (this one is not trival unlike the others).

The question is why you want to find "(A > B)" as opposed to, say, "C = 0"? Both are "unsatisfiable" partial assignments but it seems that you have a (personal) preference of which one you actually care about. You need to know what you are looking for because even if the solver could generate these unsatisfiable partial assignments, he would probably give you the (undesired) answer C = 0 before finding something like A > B.
Are some of the conditions maybe considered "configurables/options" and you want to find invalid configurations? I've seen something like this in the context of software product lines.

[mfazelnia]

Actually I need the "undesired" answer, which is C = 0. I want the model to inform me if there could be a potential contradiction among the given clauses. In other words, I am seeking to find invalid configurations, such as A > B, which could potentially cause a contradiction in the set of clauses.