Упрощение уравнений с помощью Python z3 API - PullRequest
Новая
       85

Упрощение уравнений с помощью Python z3 API

0 голосов
/ 23 октября 2019

Я пытаюсь научиться выполнять несколько вещей при работе с выражениями в Python z3 API.

  1. Я хотел бы иметь возможность упростить / уменьшить наборы уравнений, которые содержат промежуточныепеременные. Скажем, у меня есть уравнения (A = B && C) и (C = D || E). В z3 они будут представлены как (Bool('A') == And(Bool('B'), Bool('C')) и (Bool('C') == Or(Bool('D'), Bool('E')). Есть ли какая-либо функция или ряд функций, которые можно использовать для получения упрощенного и сокращенного уравнения (A = B && (D || E))?
  2. Я хотел бы иметь возможность преобразовать выражение z3 в форму суммы продуктов (т.е. Or(minterm1, minterm2,...).
  3. Эффективный способ определения логической эквивалентности двух логических уравнений.
  4. Способ возврата логических уравнений в виде форматированных строк (т. Е. НЕ в форме вложенной функции, используемой для объявления функции. )

Если у кого-либо есть какие-либо идеи по любому из этих пунктов, ваш вклад был бы очень признателен. Кроме того, если понадобятся какие-либо дополнительные разъяснения относительно того, что требуется, пожалуйста, дайте мне знать.

Спасибо,

1 Ответ

1 голос
/ 23 октября 2019

Хорошие вопросы.

  1. Нет, не в общем. Вы можете использовать z3 для упрощения уравнений, но ваше представление о «простом» вряд ли будет соответствовать тому, что он будет считать простым для своих внутренних целей. Люди часто просят эту функцию, но в целом это очень сложная проблема, и не совсем понятно, что подразумевается под простым. Сказав это, у z3 есть понятия Goal и Tactic, и есть даже тактика simplify, которую вы можете использовать. Это упростит формулы, но то, что он ведет себя именно так, как вы хотите, ведет себя глупо.

    Посмотрите этот великий ресурс по тактике, и, возможно, вы можете поиграть, чтобы найти что-то, что работает для вас: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

  2. Тактика упрощения имеет опцию som, я полагаю. Это может помочь. Снова, посмотрите вышеупомянутую ссылку, где у них есть пример: 

    s = Then(With('simplify', arith_lhs=True, som=True),
     'normalize-bounds', 'lia2pb', 'pb2bv', 
     'bit-blast', 'sat').solver()

    Самородок som=True говорит решающему использовать сумму минут. Опять же, ваш пробег может варьироваться в зависимости от точной структуры ваших формул, и z3 может вводить новые имена, которые могут победить цель.

  3. Абсолютно! Это то, что отличает z3. Просто укажите f != g, где f и g - ваши уравнения. Если z3 говорит unsat, то вы знаете, что они эквивалентны для всех назначений переменных. Если это дает вам модель, это является контрпримером к их эквивалентности. (Уловка отрицательного равенства очень распространена при решении SMT: формула является тавтологией именно тогда, когда ее отрицание неудовлетворительно. Таким образом, вы можете утверждать отрицание того, что хотите, и посмотреть, вернется ли оно с unsat.)

    Обратите внимание, что это то, в чем решатели SMT (и SAT) превосходят.

  4. Для любой формулы f, которую вы строите, вы можете выполнить print f, и она напечатаетЭто. Но, как вы, вероятно, уже заметили, он будет , а не выглядеть как логические формулы вашего учебника. У симпатичного принтера есть несколько опций для управления его поведением, но это, вероятно, не совсем то, что вам нужно.

    Однако API предоставляет функции для перехода по AST и извлечения узлов по вашему желанию. Таким образом, вы можете написать свой собственный симпатичный принтер, если хотите. Сделать это не очень сложно, но это не значит, что все просто: есть много случаев, которые нужно рассмотреть, и, по моему опыту, такие принтеры обычно не так легко обмануть;т.е. производить что-то значительно худшее для небольших изменений на входе.

С практической точки зрения, хотя z3 и его высокоуровневые API в Python, C, Java и т. Д. Способны делать все, что вы хотите, это не будетиз коробки кроме № 3. Моя рекомендация будет заключаться в том, чтобы кодировать все остальное самостоятельно, и полагаться на z3 для проверки равенства, в котором он превосходит. Конечно, все зависит от того, что вы пытаетесь сделать. Желаем удачи!

...