Я провел несколько экспериментов с тестером z3 smt от Microsoft, работая над своей магистерской диссертацией. В моем случае использования мне нужно проверить выполнимость (без модели) для простых формул, содержащих квантификаторы (логика первого порядка с равенством). Z3 хорошо справляется со всеми моими примерами за пару миллисекунд, кроме этого:
forall x P(f(g(f(x)))) and not P(f(g(h(c))))
Я протестировал формулу на сайте ride4fun.com и на своем компьютере (ubuntu 16.04, 4x 3,4 ГГц) с помощью java-привязки z3. Я убил процесс через 1 час безрезультатно. Я осознаю тот факт, что такие проблемы являются лишь полуразрешимыми. Но почему z3 не подходит для этой конкретной формулы. Я протестировал множество других формул (более мелких и даже более крупных), и z3 преуспел во всех из них. Может быть, кто-нибудь объяснит мне, что делает эту формулу такой сложной для z3? Что происходит внутри z3?
Например: достаточно изменить один функциональный символ, чтобы z3 завершил работу с результатом (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))))
Вы можете попробовать этот пример на http://rise4fun.com/Z3, используя следующий фрагмент кода.
(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)
