4

Even for simplest arithmetic SMT problems the existential quantifier is required to declare symbolic variables. And ∀ quantifier can be turned into ∃ by inverting the constraint. So, I can use both of them in QF_* logics and it works.

I take it, "quantifier free" means something else for such SMT logics, but what exactly?

arrowd
  • 33,231
  • 8
  • 79
  • 110

2 Answers2

4

The claim is that

∀ quantifier can be turned into ∃ by inverting the constraint

AFAIK, the following two relations hold:

 ∀x.φ(x) <=> ¬∃x.¬φ(x)
¬∀x.φ(x) <=>  ∃x.¬φ(x)

Since a quantifier-free SMT formula φ(x) is equisatisfiable to its existential closure ∃x.φ(x), we can use the quantifier-free fragment of an SMT Theory to express a (simple) negated occurrence of universal quantification, and [AFAIK] also a (simple) positive occurrence of universal quantification over trivial formulas (e.g. if [∃x.]φ(x) is unsat then ∀x.¬φ(x)¹).

¹: assuming φ(x) is quantifier-free; As @Levent Erkok points out in his answer, this approach is inconclusive when both φ(x) and ¬φ(x) are satisfiable

However, we cannot, for example, find a model for the following quantified formula using the quantifier-free fragment of SMT:

[∃y.]((∀x.y <= f(x)) and (∃z.y = f(z)))

For the records, this is an encoding of the OMT problem min(y), y=f(x) as a quantified SMT formula. [related paper]

A term t is quantifier-free iff t syntactically contains no quantifiers. A quantifier-free formula φ is equisatisfiable with its existential closure

(∃x1. (∃x2 . . .(∃xn.φ ). . .))

where x1, x2, . . . , xn is any enumeration of free(φ), the free variables in φ.

The set of free variables of a term t, free(t), is defined inductively as:

  • free(x) = {x} if x is a variable,
  • free((f t1 t2 . . . tk)) = \cup_{i∈[1,k]} free(ti) for function applications,
  • free(∀x.φ) = free(φ) \ {x}, and
  • free(∃x.φ) = free(φ) \ {x}.

[source]

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
  • You say `φ(x)` is equisatisfiable to `∃x.φ(x)`, but it isn't equivalent, right? I'm still puzzled what's semantic difference between them. I seem to understand that `∃x.φ(x)` means "there exists such x that φ(x) is true`, but what `φ(x)` means without quantifier prefix? – arrowd Feb 21 '19 at 11:55
  • @arrowd Equisatisfiability is definitely more easy to handle than equivalence. Making such claim without listing a number of restrictions like, e.g. that `x` must belong to `free(φ(x))`, sounds a bit like an abuse of notation and terminology. Since I am not confident enough with this, I would like to avoid making any definitive claim other than the existential quantification over `x` wrt. `φ(x)` is implicit in the definition of the satisfiability problem itself. – Patrick Trentin Feb 21 '19 at 13:01
3

Patrick gave an excellent answer, but here're a few more thoughts. (I'd have put this up as a comment, but StackOverflow thinks it's too long for that!)

  • Notice that you cannot always play the "negate and check the opposite" trick. This only works because if the negation of a property is unsatisfiable, then the property must be true for all inputs. But it doesn't go the other way around: A property can be satisfiable, and its negation can be satisfiable as well. Simple example: x < 10. This is obviously satisfiable, and so is its negation x >= 10. So, you cannot always get rid of quantifiers by playing this trick. It only works if you want to prove something: Then you can negate it and see if that negation is unsatisfiable. If you're concerned about finding a model to a formula, the method doesn't apply.

  • You can always skolemize a formula and eliminate all the existential quantifiers by replacing them with uninterpreted functions. What you then end up with is an equisatisfiable formula that has all prefix universals. Clearly, this is not quantifier free, but this is a very common trick that most tools do for you automatically.

  • Where all this hurts is alternating quantifiers. Regardless of skolemization, if you have alternating quantifiers than your problem is already too difficult to deal with. The wikipedia page on quantifier elimination is rather terse, but it gives a very good introduction: https://en.wikipedia.org/wiki/Quantifier_elimination Bottom line: Not every theory admits quantifier elimination, and even those that do might require exponential algorithms to get rid of them; causing performance issues.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Great job in pointing out that reversing a certain property is only useful in the case of an *unsat* result and provides no evidence whatsoever in the case of a *sat* result. – Patrick Trentin Feb 20 '19 at 16:00
  • You said `If you're concerned about finding a model to a formula, the method doesn't apply`. If I'm finding a model, I shouldn't have any `∀` in my problem formulation anyway, no? I can't came up with an example of using `∀` outside of proofs. – arrowd Feb 21 '19 at 11:52
  • @arrowd isn't the *"optimization"* use-case in my answer one such example? – Patrick Trentin Feb 21 '19 at 12:11
  • @PatrickTrentin Aha, you're right. Follow-up question - can we reformulate your example problem as `[∃y, z.]((∀x.y <= f(x)) and (y = f(z)))`? – arrowd Feb 21 '19 at 12:18
  • Last time I read the book from [Dirk Van Dalen](https://www.springer.com/it/book/9781447145578) was a long time ago, but since `(∀x.y <= f(x))` is *free for `z`*, [i don't see any problem with that](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1410d244a43ab2b837b62490e1e70c184f99778). – Patrick Trentin Feb 21 '19 at 12:27