Доказательство теоремы Z3: теорема Пифагора (нелинейная арифметика)

Почему?

Контекст варианта использования, в котором возникает моя проблема

Я определяю 3 случайных элемента треугольника. Microsoft Z3 должен выводить:

  • Удовлетворительны ли ограничения или имеются недопустимые входные значения?
  • Модель для всех остальных элементов треугольника, в которой всем переменным присваиваются конкретные значения.

Чтобы ограничить элементы, мне нужно assert равенства треугольников - я хотел начать с теоремы Пифагора ((h_c² + p² = b²) ^ (h_c² + q² = a²)).

Эта проблема

Я знаю, что Microsoft Z3 имеет лишь ограниченные возможности для решения нелинейных арифметических задач. Но даже некоторые ручные калькуляторы могут решить очень упрощенную версию, например:

(set-option :print-success true)
(set-option :produce-proofs true)
(declare-const a Real)
(declare-const b Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert
    (exists
        ((c Real))
        (=
            (+
                (* a a)
                (* b b)
            )
            (* c c)
        )
    )
)
(check-sat)
(get-model)

Вопрос

  • Есть ли способ заставить Microsoft Z3 решить теорему Пифагора, если заданы два значения?
  • Или: есть ли другое средство доказательства теорем, способное справиться с этим случаем нелинейной арифметики?

Спасибо за вашу помощь по этому поводу - если что-то неясно, пожалуйста, прокомментируйте.


logic constraint-programming z3 smt theorem-proving
person fdj815    schedule 27.02.2013    source источник
comment
дубликат был создан, потому что модератор перенес этот вопрос в StackOverflow, даже если я уже воссоздал его в StackOverflow - я никогда не хотел, чтобы это произошло .   -  person fdj815    schedule 28.02.2013

Ответы (1)


arrow_upward
4
arrow_downward

Z3 имеет новый решатель (nlsat) для нелинейной арифметики. Он более эффективен, чем другие решатели (см. эту статью). Новый решатель готов для задач без кванторов. Однако новый решатель не поддерживает генерацию доказательств. Если мы отключим генерацию доказательств, то Z3 будет использовать nlsat и легко решит проблему. Исходя из вашего вопроса, похоже, вы действительно ищете решения, поэтому отключение генерации доказательств не кажется проблемой.

Более того, Z3 не выдает приближенных решений (как ручные калькуляторы). Он использует точное представление действительных алгебраических чисел. Мы также можем попросить Z3 отобразить результат в десятичном представлении (опция :pp-decimal). Вот ваш онлайн-пример.

В этом примере, когда используется точное представление, Z3 отобразит следующий результат для c.

(root-obj (+ (^ x 2) (- 2)) 1)

Это говорит о том, что c является первым корнем многочлена x^2 - 2. Когда мы используем (set-option :pp-decimal true), он будет отображать

(- 1.4142135623?)

Знак вопроса используется для обозначения усечения результата. Обратите внимание, что результат отрицательный. Тем не менее, это действительно решение проблемы, которую вы написали. Поскольку вы ищете треугольники, вы должны утверждать, что все константы > 0.

Кстати, вам не нужен квантификатор существования. Мы можем просто использовать константу c. Вот пример (также доступен на сайтеrise4fun):

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)

Вот еще один пример, для которого нет решения (также доступен онлайн на сайте ride4fun):

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)

Кстати, вам следует рассмотреть интерфейс Python для Z3. Это намного удобнее для пользователя. В учебнике, на который я ссылаюсь, есть примеры по кинематике. Они также используют нелинейную арифметику для кодирования простых школьных задач по физике.

person Leonardo de Moura    schedule 27.02.2013
comment
Я никогда не хотел говорить, что ручные калькуляторы способны на большее, чем Z3. Я просто хотел показать, что это очень простой вариант использования и что должен быть способ сделать это. - person fdj815; 28.02.2013
comment
Я понимаю. Без проблем. В своем посте я попытался подчеркнуть, что ваш пример не так прост, как вы думаете. Большинство решателей SMT не могут справиться с этой проблемой, поскольку они даже не могут точно представить решение. Z3 без nlsat не может решить эту проблему. Ручной калькулятор также на самом деле не решает задачу, он просто вычисляет приближенное решение. Предположим, мы также утверждаем (assert (= c 1.4142135623)), проблема все еще разрешима? Нет это не так. Однако, если мы используем приближения, мы можем неправильно сказать, что это так. rise4fun.com/Z3/JWYC - person Leonardo de Moura; 28.02.2013
comment
Когда мой сценарий будет готов, он должен поддерживать больше assert, чем просто теорему Пифагора. Я могу обойтись без реального доказательства, но мне очень нужно знать, какие формулы используются. Например: Right triangle: a, b дано, c востребовано - скрипт должен вывести, что для вычисления c использовалась формула (= (+ (* a a) (* b b)) (* c c)). Возможно ли что-то подобное с помощью nlsat? - person fdj815; 28.02.2013
comment
Предположим, у нас есть N утверждений. Когда nlsat возвращает sat, это означает, что ему удалось найти решение, которое делает все эти утверждения верными. Решение содержит значение для c и для всех других констант в задаче. Таким образом, в принципе, он использовал все ограничения, чтобы найти решение для c и любой другой константы в задаче. Если у нас есть такие утверждения, как (or C1 C2), мы можем спросить, верно ли оно, потому что nlsat сделал C1 или C2 истинными. - person Leonardo de Moura; 28.02.2013
comment
Спасибо за вашу помощь в этом вопросе. - Я приму ваш ответ здесь и надеюсь, что будет прекрасное решение для моей проблемы с формулой (которую я перенес в новую тему). - person fdj815; 01.03.2013
comment
Конечно, каждое разумное ограничение ограничивает множество решений. - В новой теме я постарался более точно описать, какие формулы меня интересуют. - person fdj815; 01.03.2013