Реализация функции пола и потолка в Z3 - PullRequest
Новая
       114

Реализация функции пола и потолка в Z3

0 голосов
/ 23 апреля 2020

Я попытался реализовать функцию пола и потолка, как определено в следующей ссылке

https://math.stackexchange.com/questions/3619044/floor-or-ceiling-function-encoding-in-first-order-logic/3619320#3619320

Но контрольный пример запроса Z3 возвращает контрпример.

Функция пола 

_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_n=Int('_n')
_Floor=Function('_Floor',RealSort(),IntSort())
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Floor(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_W<_Y))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_W<_Y))),_Floor(_X)==_Y))
_s.add(Not(_Floor(0.5)==0))

Ожидаемый результат - Unsat

Фактический результат - Сб

Функция потолка 

_X=Real('_X')
_Y=Int('_Y')
_W=Int('_W')
_Ceiling=Function('_Ceiling',RealSort(),IntSort())
..
..
_s.add(_X>=0)
_s.add(_Y>=0)
_s.add(Implies(_Ceiling(_X)==_Y,And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W ==_Y,_Y<_W))))))
_s.add(Implies(And(Or(_Y==_X,_Y<_X),ForAll(_W,Implies(And(_W>=0,_W<_X),And(_W==_Y,_Y<_W)))),_Ceiling(_X)==_Y))
_s.add(Not(_Ceilng(0.5)==1))

Ожидаемый результат - Unsat

Фактический результат - сб

1 Ответ

2 голосов
/ 23 апреля 2020

[Ваша кодировка не загружается в z3, она выдает синтаксическую ошибку даже после устранения '..', так как ваш вызов Implies нуждается в дополнительном аргументе. Но я проигнорирую все это.]

Короткий ответ: вы не можете делать такие вещи в SMT-Solver. Если бы вы могли, то вы можете решить произвольные диофантовы уравнения. Просто приведите его в терминах Реалов, решите его (есть процедура принятия решений для Реалов), а затем добавьте дополнительное ограничение, что результатом является целое число, сказав Floor(solution) = solution. Таким образом, с помощью этого аргумента вы можете видеть, что моделирование таких функций выходит за рамки возможностей решателя SMT.

Подробнее см. В этом ответе: Получение дробной части вещественного в QF_UFNRA

Сказав, что это не означает, что вы не можете закодировать это в Z3. Это просто означает, что это будет более или менее бесполезно. Вот как я бы go об этом: 

from z3 import *

s = Solver()

Floor = Function('Floor',RealSort(),IntSort())

r = Real('R')
f = Int('f')
s.add(ForAll([r, f], Implies(And(f <= r, r < f+1), Floor(r) == f)))

Теперь, если я сделаю это: 

s.add(Not(Floor(0.5) == 0))
print(s.check())

вы получите unsat, что правильно. Если вы сделаете это вместо этого: 

s.add(Not(Floor(0.5) == 1))
print(s.check())

, вы увидите, что z3 просто зацикливается навсегда. Чтобы сделать это полезным, вы бы хотели, чтобы следующее также работало: 

test = Real('test')
s.add(test == 2.4)
result = Int('result')
s.add(Floor(test) == result)
print(s.check())

, но опять же, вы увидите, что z3 просто зацикливается навсегда.

Итак, суть: Да Вы можете смоделировать такие конструкции, и z3 правильно ответит на самые простые запросы. Но с чем-нибудь интересным, это просто l oop навсегда. (По сути, всякий раз, когда вы ожидаете sat и большую часть unsat сценария ios, если только они не могут быть согнуты постоянно, я бы ожидал, что z3 просто l oop.) И есть очень веская причина для что, как я уже говорил: такие теории просто не поддаются решению и выходят далеко за рамки возможностей, которые может решать SMT.

Если вы заинтересованы в моделировании таких функций, лучше всего использовать более традиционный доказатель теорем, как Изабель, Coq, ACL2, HOL, HOL-Light и другие. Они гораздо больше подходят для работы над такими проблемами. А также, прочитайте Получить дробную часть вещественного в QF_UFNRA , так как это входит в некоторые другие детали того, как вы можете go о моделировании таких функций, используя нелинейную вещественную арифметику c.

...