Проверка выполнимости формулы первого порядка с использованием Z3

Я пробовал некоторые основные проблемы с выполнимостью формулы FOL, используя Z3. Я не могу понять, почему приведенный ниже фрагмент кода возвращает Unsat. Пожалуйста помоги.

Если возможно, если кто-нибудь пробовал с каким-то примером, для которого FOL с кванторами дает «Sat», а с некоторыми небольшими незначительными изменениями дает «Unsat» в качестве вывода, будет очень полезно.

Существуют ли какие-то простые фрагменты кода формулы FOL для изучения, кроме тех, что представлены на странице руководстваris4fun.

(set-option :smt.mbqi true)
(declare-fun f (Real Real) Bool)
(declare-const a Real)
(declare-const b Real)

(assert (forall ((x Real)) (and (f a x) (> x 6))))
(assert (and (f a b) (> b 6) ))
(check-sat)


z3 first-order-logic satisfiability
person Rituraj Singh Rathore    schedule 10.12.2019    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Ваш ввод unsat из-за этого assert:

(assert (forall ((x Real)) (and (f a x) (> x 6))))

Правая часть - соединение. Таким образом, это говорит о том, что все действительные значения x больше 6, что явно неверно. Фактически, вы можете упростить весь ввод до:

(assert (forall ((x Real)) (> x 6)))
(check-sat)

и это все еще будет unsat по той же самой причине.

Возможно, вы имели в виду что-то вроде этого:

(set-option :smt.mbqi true)
(declare-fun f (Real Real) Bool)
(declare-const a Real)
(declare-const b Real)

(assert (forall ((x Real)) (=> (> x 6) (f a x))))
(assert (and (f a b) (> b 6) ))
(check-sat)
(get-value (f a b))

То есть f a x равно true, если x больше 6? Для этого ввода z3 говорит:

sat
((f (lambda ((x!1 Real) (x!2 Real)) (= x!2 0.0)))
 (a 0.0)
 (b 7.0))

И вы можете видеть, что это действительно удовлетворительная модель, хотя и не особенно интересная.

Надеюсь, это поможет!

person alias    schedule 10.12.2019
comment
Большое спасибо ... Действительно полезно - person Rituraj Singh Rathore; 10.12.2019