Getting 'sat' for large problems

Question

I generate my problems from a template and due to the nature of the problems, I have to rely on quantifiers. Now, the solver can only find instances for really simple (satisfiable) problems. Finding 'unsat' works in many cases. Finding 'sat' rarely works.

The problem is that even simple things like a definition of two disjoint sets have to be expressed with some really nasty formulas:

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8))

(Find the full problem here)

In order to find an instance, Z3 must find an interpretation of the function in_1. All other functions all depend on it.

So far, I have heard the following statements related to my problem:

Every quantifier should have a pattern
Instance finding does not work if there are any infinite models

I could not find any useful information on the web or in the literature on how to achieve or avoid this. So my question remains:

How can I efficiently find instances to satisfiable formulas (with Z3)? How do I achieve this using patterns (if at all)?

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2012-10-23T14:31:47

Z3 4.x uses two main engines for handling quantifiers: EMatching and MBQI (Model Based Quantifier Instantiation). The EMatching engine is only effective for unsatisfiable instances. That is, it will never be able to show that a formula (containing quantifiers) is satisfiable. On the other hand, the MBQI can do that. Actually, it can decide many useful fragments. The Z3 guide (section Quantifiers) describes some of these fragments. That being said, Z3 does not have finite model finder for first-order logic (like Paradox). This is a useful feature, and we may include it in the future. The example in your message, can be solved using Z3. You can try it here.

Regarding Patterns, they are "hints" for the EMatching engine. Since the EMatching engine can't show that a problem is satisfiable, they will not really help. For satisfiable instances, we can add patterns because we don't want the EMatching engine to get in the way of the MBQI engine by generating too many instances; or we want to eagerly prune the search space by asserting simple instances of the quantifier. We may also disable the EMatching engine using the option (set-option :ematching false).

(declare-sort Rel1)
(declare-sort Atom)
(declare-fun disjoint_1 (Rel1 Rel1) Bool)
(declare-fun in_1 (Atom Rel1) Bool)
(declare-const A Rel1)
(declare-const B Rel1)

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8)) 

(check-sat)
(get-model)

Getting 'sat' for large problems

1 Answers