Докажите, что функция сюръективна, используя Z3 - PullRequest
Новая
       89

Докажите, что функция сюръективна, используя Z3

2 голосов
/ 28 мая 2020
• 1000 так что это скорее вычислительный вопрос. * 
N = BitVec('N', 32)
M = BitVec('M', 32)
solve(N != M, f(N) == f(M))

Однако это занимает довольно много времени (> 10 минут, но выключите его после), и это вполне разумно, поскольку пространство поиска в значительной степени 64-битное, и функция может быть довольно сложной для рассмотрения, поскольку она смешивает много умножения с двоичной арифметикой c, поэтому я подумал, можно ли вместо этого доказать это сюръекцией, возможно, быстрее.

Действительно ли это быстрее или есть даже способ решить эту проблему эффективно еще может быть другой вопрос, однако я застрял в размышлениях, как доказать это сюрпризом. то есть попросить Z3 найти M такое, что f(N) != M forall N.

Это где-нибудь отличается от доказательства приемистости?

Как мне указать это в привязках Z3 python?

Можно ли вообще удалить экзистенциальные квалификаторы из сюръективного утверждения?

Есть ли более эффективные способы доказать, что функция биективна? Поскольку для чего-то вроде этого поиск методом перебора может быть более эффективным, так как требуемой памяти не должно быть много для 32-битных векторов, но этот подход определенно не будет работать на 64-битном вводе / выводе.

1 Ответ

1 голос
/ 28 мая 2020

Вы бы записали сюръективность следующим образом: 

N = BitVec('N', 32)
M = BitVec('M', 32)
s = Solver()
s.add(ForAll([N], f(N) != M))

r = s.check()
if r == sat:
    print(s.model())
else:
    print(r)

К сожалению, добавление кванторов к битовым векторам делает logi c неразрешимым в целом, и z3 просто сдается примерно через 10 секунд на моей машине : 

unknown

В общем, добавление квантификаторов только сделает проблему очень сложной для z3 (или любого другого решателя SMT в этом отношении). Ваша исходная кодировка: 

solve(N!=M, f(N) == f(M))

, вероятно, лучший способ кодировать эту проблему. Фактически, если вы измените диапазон с 10 на что-то меньшее (я пробовал до 3), z3 сравнительно быстро ответит unsat. Но очевидно, что время решателя будет go экспоненциально по мере увеличения количества итераций в вашей функции f.

Решатель SMT, вероятно, не лучший инструмент для доказательства такого свойства. Конечно, вы можете express таких ограничений, но в лучшем случае вы получите unknown в качестве ответа, а в худшем - oop навсегда. Правильная программа доказательства теорем (например, Isabelle, HOL, Coq, ACL2 и др. c.) Предоставит гораздо лучшую (за счет меньшей автоматизации) платформу для выполнения этих доказательств.

...