Reducing the number of used clauses using proof goal in Z3

Question

I am experimenting with optimizing the use of Z3 for proving facts about a first-order theory. Currently, I specify a first-order theory in Python, ground the quantifiers there and send all the clauses along with the negation of the proof goal to Z3. I have the following idea that I hope could optimize the outcome: I only want to send the formulas in the theory to Z3 that are relevant to the proof goal. I will not discuss this concept in detail, but I think the intuition is simple: my theory is a conjunction of formulas, and I only want to send conjuncts that can possibly affect the truth value of the proof goal.

My question is the following: can this lead to an improvement in efficiency, or does Z3 already use a similar method? I would guess not, because I don't think that Z3 always assumes that the last assertion is the proof goal, so it has no way of optimizing this.

Answer 1

Yes, removing irrelevant facts can make a big difference. Suppose that we have a unsatisfiable formula of the form F_1 and F_2 and (not G). Moreover, let us assume that F_1 and (not G) is unsatisfiable, and F_2 is satisfiable. F_2 is what you call irrelevant. If there is a cheap way to remove F_2 before sending the formulat to Z3, it will probable make a big difference.

Z3 has heuristics for "ignoring" irrelevant facts, but they are just heuristics. For our example, the worst case scenario is a F_2 that is really hard for Z3 to satisfy. Z3 is essentially trying to build an interpretation/solution that satisfies the input formula (the formula F_1 an F_2 and (not G) in our working example). A formula is unsatisfiable when Z3 can show it is impossible to build the interpretation. In practice, the formula F_2 is irrelevant for Z3 only if it can quickly show it to be satisfiable, and the interpretation/solution for F_2 does not conflicts F_1 and (not G). If that is not the case, Z3 can waste a lot of resources with F_2.