eliminating forall using unsat

Question

We know that, we can prove validity of a theorem by saying :

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
assert ( forall (x,y) . Demorgan(x,y) )

Alternatively we can eliminate the forall quantifier by saying that :

let Demorgan(x, y) = formula1(x,y) iff formula2(x,y)
( assert (not  Demorgan(x,y) ) )

So if it returns unsat, then we can say the above formula is valid.

Now I want to use this idea to eliminate the forall quantifier from the following assertion:

assert ( exists x1,x2,x3 st .( forall y . formula1(x1,y) iff
                                          formula2(x2,y) iff
                                          formula3(x3,y) ) )

So is there any way in Z3(using C++ API or SMT-LIB2.0) that I can assert something like the following :

assert (exists x1,x2,x3 st. ( and ((not ( formula1(x1,y) iff formula2(x2,y) )) == unsat)
                                  ((not ( formula2(x2,y) iff formula3(x3,y) )) == unsat))) 

Answer 1

Yes, when we can prove the validity of a formula by showing its negation to be unsatisfiable. For example, to show that Forall X. F(X) is valid, we just have to show that not (Forall X. F(X)) is unsatisfiable. The formula not (Forall X. F(X)) is equivalent to (Exists X. not F(X)). The formula (Exists X. not F(X)) is equisatisfiable to the formula not F(X) where the bound variable X is replaced by a fresh constant X. By equisatisfiable, I mean that the first one is satisfiable iff the second one is. This step that removes existential quantifiers is usually called skolemization. Note that these last two formulas are not equivalent. For example, consider the interpretation { X -> 2 } that assigns X to 2. The formula Exists X. not (X = 2) still evaluates to true in this interpretation because we can choose X to be 3. On the other hand, the formula not (X = 2) evaluates to false in this interpretation. We usually use the term quantifier elimination procedure for a procedure that given a formula F produces an equivalent quantifier-free formula F'. So, skolemization is not considered a quantifier elimination procedure because the result is not an equivalent formula.

That being said, we don't have to apply the skolemization step by hand. Z3 can do it for us. Here is an example (also available online here).

(declare-sort S)
(declare-fun F (S) Bool)
(declare-fun G (S) Bool)
(define-fun Conjecture () Bool 
    (forall ((x S)) (= (and (F x) (G x)) (not (or (not (F x)) (not (G x)))))))
(assert (not Conjecture))
(check-sat)

Now, let us consider a formula of the form Exists X. Forall Y. F(X, Y). To prove the validity of this formula, we can show the negation not Exists X. Forall Y. F(X, Y) to be unsatisfiable. The negation is equivalent to Forall X. Exists Y. not F(X, Y). Now, if apply skolemization to this formula, we obtain Forall X. not F(X, Y(X)). In this case, the bound variable Y was replaced with Y(X), where Y is a fresh function symbol in the resultant formula. The intuition is that the function Y is the "choice function". For each X, we can choose a different value to satisfy the formula F. Z3 performs all these steps automatically for us. We don't need to apply skolemization by hand. However, in this case, the resultant formula is usually harder to solve because it contains a universal quantifier after the skolemization step.