Incoherence with negated existential quantifier

[yblein]

I'm having trouble with existential quantifiers and negation. For instance, given some predicate p, the formula (∃i. p i) ∧ ¬(∃i. p i) is obviously false. However encoding it in SBV says otherwise:

λ> let p = uninterpret "p" :: SInteger -> SBool
λ> let e = exists "i" >>= return . p
λ> sat (liftM2 (&&&) e (bnot <$> e))
Satisfiable. Model:
  i = 0 :: Integer
  i = 1 :: Integer

Note that replacing the existential quantifier with a universal one results in "unsat", as expected. I'm using the default configuration, that is z3 with its default parameters. By looking at the smtlib encoding procuced, I guess that SBV skolemized the existential quantifiers as if they were all at the top level of the formula.

[LeventErkok]

The repeated value of i in the model is a great give-away here. Those two is are actually totally different variables. You can see this if you use the anonymous version of exists:

λ> let p = uninterpret "p" :: SInteger -> SBool
λ> let e = exists_ >>= return . p
λ> sat (liftM2 (&&&) e (bnot <$> e))
Satisfiable. Model:
  s0 = 0 :: Integer
  s1 = 1 :: Integer

So, what you really asked SBV is to find a model for ∃i ∃j. (p i ∧ ¬(p j)), which it did.

What you are trying to say (i.e., (∃i. p i) ∧ ¬(∃i. p i)) is not directly expressible in SBV. Essentially, when you write an SBV program involving quantifiers, they are all grouped at the top: SBV has an implicit assumption that you are always writing in prenex-normal form. Since what you want to write is not in prenex normal form, you first have to do that translation yourself. (SBV does not do prenex-translation, but it does do skolemization.)

If you follow the well-known algorithm (https://en.wikipedia.org/wiki/Prenex_normal_form) to do this step, you end up with: ∃i ∀j. (p i ∧ ¬(p j)) (note the universal thus introduced!), which now you can ask for satisfiability using SBV:

import Data.SBV

p :: SInteger -> SBool
p = uninterpret "p"

g :: Predicate
g = do i <- exists "i"
       j <- forall "j"

       return $ p i &&& bnot (p j)

We get:

λ> sat g
Unsatisfiable

Note that you cannot, in general, ask to prove such quantified predicates in SBV, since the skolemization SBV will perform the translate the problem will produce an equisatisfiable formula, which is not necessarily equivalent. But that's a whole different discussion.

It's rather unfortunate that what you wrote does look like what you wanted to say; but it really means something entirely different. I'm not aware of a simple way to detect and warn the user of such cases. I'd be happy to hear if you had any ideas.

[LeventErkok]

SBV now recognizes and rejects duplicate names; so your first query results in:

*** Exception: SBV: Repeated user given name: "i". Please use unique names.

Of course, there's nothing stopping you from still using non-prenex looking like expressions, yet SBV treating them as such. Unfortunately, that's a much harder thing to recognize and handle. I'm intending to put some text to that effect into the documentation instead. In the mean time, hopefully the above check will alert the user in at least more common cases.

[LeventErkok]

Added some documentation on this issue here: https://github.com/LeventErkok/sbv/commit/b5cf986883f076ef330159d7a7c44950e1dfea6a

I'm closing this ticket as there isn't any actionable item to be done on it. If you have questions/comments, feel free to reopen it.

[LeventErkok]

@ttuegel @yblein

Not sure if this is still relevant to you. But the latest release of SBV has proper support for quantifiers. The old way of dealing with quantifiers is completely removed. The current implementation (I hope!) is much easier to use and much more expressive.

For instance, your very first example is now coded like this:

Prelude Data.SBV> let p = uninterpret "p" :: SInteger -> SBool
Prelude Data.SBV> let e = \(Exists i) -> p i
Prelude Data.SBV> let qAnd a b = quantifiedBool a .&& quantifiedBool b
Prelude Data.SBV> sat (e `qAnd` qNot e)
Unsatisfiable

quantifiedBool is a function that converts a quantified-formula to a regular boolean. The function qAnd we defined allows for lifting the conjunction over quantified booleans.

The new facility can also do skolemization, which I suspect you might be interested in:

Prelude Data.SBV> :set -XDataKinds
Prelude Data.SBV> let q = \(Forall @"x" x) (Exists @"y" y) -> y .== (x+1::SInteger)
Prelude Data.SBV> sat q
Satisfiable
Prelude Data.SBV> sat $ skolemize q
Satisfiable. Model:
  y :: Integer -> Integer
  y x = 1 + x

There are some further examples in https://hackage.haskell.org/package/sbv-10.1/docs/Documentation-SBV-Examples-Misc-FirstOrderLogic.html

Let me know if you give this a try and have any feedback regarding usage/further examples etc.