I‘ve made some experiments with the z3 smt prover from Microsoft, while working on my master thesis. In my use case I need to check satisfiability (no model) for simple formulas containing quantifiers (first order logic with equality). The z3 makes a good job solving all of my examples in a couple of milliseconds, except for this one:
forall x P(f(g(f(x)))) and not P(f(g(h(c))))
I tested the formula on rise4fun.com and on my computer (ubuntu 16.04, 4x 3.4GHz) using the z3 java-binding. I killed the process after 1h with no result. I’m aware of the fact, that such problems are only semidecidable. But why does the z3 fails for this specific formula. I tested a lot of other formulas (smaller ones and even larger ones) and the z3 succeed on all of them. Maybe one could explain to me what makes this formula as difficult for the z3? What happens inside the z3?
E.g.: Changing one function symbol is enough to let the z3 terminating with a result (sat/unsat):
forall x P(f(g(f(x)))) and not P(f(g(f(c))))
forall x P(f(g(f(x)))) and not P(f(g(g(c))))
forall x P(f(g(f(x)))) and not P(f(f(g(c))))
forall x P(f(g(f(x)))) and not P(f(g(i(c))))
// and even
forall x P(f(g(h(x)))) and not P(f(g(f(c))))
You can try those example on http://rise4fun.com/Z3 using the following snippet.
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(declare-fun h (Int) Int)
(declare-fun i (Int) Int)
(declare-fun P (Int) Bool)
(assert (forall ((x Int))
(P (f (g (f x))) )
))
(assert (not
(P (f (g (h c))) )
))
(check-sat)
