How to efficiently solve combinations of theories in Z3

Question

I am trying to solve a problem that involves propositional satisfiability (with quantifiers), and linear arithmetic.

I have formulated the problem, and Z3 is able to solve it, but it is taking an unreasonably long time.

I have been trying to help Z3 along by specifying tactics, but I haven't made much progress (I have no knowledge of logic theories).

Following is a highly simplified problem that captures the essence of what I am trying to solve. Could anyone give suggestions?

I tried to read up on things like Nelson Oppen method, but there were a lot of unfamiliar notations, and it'll take a long time to learn it.

Also, does Z3 allow users to tweak these configurations? Lastly, how can I use these tactics with z3py?

(declare-datatypes () ((newtype (item1) (item2) (item3))))

(declare-fun f (newtype newtype) Bool)

(declare-fun cost (newtype newtype) Real)

(assert (exists ((x newtype)(y newtype)) (f x y)))

(assert (forall ((x newtype)(y newtype)) (=> (f x y) (> (cost x y) 0))))

(assert (forall ((x newtype) (y newtype)) (<= (cost x y) 5)))

(check-sat)

(get-model)

Answer 1

The sample problem you encoded uses quantification. Z3 uses a particular procedure for deciding satisfiability of a class of quantified formulas, referred to as model-based quantifier instantiation (the mbqi option). It works by extending a candidate model for the quantifier-free portion of your formulas into a model for also the quantifiers. This process may involve a lot of search. You can extract statistics from the search process by running Z3 with the option /st and it will show selected statistics of the search process and give a rough idea of what is happening during search. There is no particular tactic combination that specializes to classes of formulas with arithmetic and quantifiers (there is a class of formulas that use bit-vectors and quantifiers that are handled by a default tactic for such formulas).

I tried to read up on things like Nelson Oppen method, but there were a lot of unfamiliar notations, and it'll take a long time to learn it.

This is going to be a bit tangential to understanding the search issue with quantifiers.

Also, does Z3 allow users to tweak these configurations?

Yes, you can configure Z3 from the command-line. For example, you can disable MBQI using the command line:

z3 tt.smt2 -st smt.auto_config=false smt.mbqi=false

Z3 now returns "unknown" because the weaker quantifier engine that performs selected instantiations is not going to be able to determine that the formula is satisfiable. You can learn the command-line options by following the instructions from "z3 -?"

Lastly, how can I use these tactics with z3py?

You can use tactics from z3py. The file z3.py contains brief information of how to combine tactics. Though, I would expect that the difficulty of your problem class really has to do with the search hardness involved with quantifiers. It is very easy to pose formulas with quantifiers where theorem provers diverge as these classes of formulas are generally highly undecidable.