Z3 каждый раз дает другой ответ при изменении порядка параметров. Проблема оптимизации - PullRequest
Новая
       133

Z3 каждый раз дает другой ответ при изменении порядка параметров. Проблема оптимизации

2 голосов
/ 18 июня 2020

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

Например,

  1. первый прогон: 
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))

(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

(maximize 
    (bvand 
        (bvor (bvand l3 l4 l1 l2) (bvand l4 l2) (bvand l4 l1 l2) (bvand l2 l3 l4)) 

        (bvor (bvand l4 l2) (bvand l2 l3 l4)) 

        (bvor (bvand l5 l7 l8 l10 l6) (bvand l5 l7 l8 l6) (bvand l5 l7 l8 l9 l6) (bvand l5 l7 l8 l9 l10 l6) (bvand l5 l7 l6) (bvand l5 l7 l9 l10 l6) (bvand l5 l7 l10 l6))
    )
)
(check-sat)
(get-model)

который дает решение: l7, l5, l2, l4, l6, l8. * В данном случае верно 1021 * 6.

второй прогон: 
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))

(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

(maximize 
    (bvand
        (bvor (bvand l2 l3 l4) (bvand l2 l4) (bvand l1 l2 l4) (bvand l2 l3 l4 l1)) 

        (bvor (bvand l2 l3 l4) (bvand l2 l4)) 

        (bvor (bvand l10 l6 l5 l7 l9) (bvand l10 l6 l5 l7) (bvand l10 l6 l5 l7 l8 l9) (bvand l10 l6 l5 l7 l8) (bvand l7 l6 l5) (bvand l7 l8 l9 l6 l5) (bvand l7 l8 l6 l5))
    )
)

(check-sat)
(get-model)

, что дает решение: l7, l9, l5, l2, l4, l6, * В данном случае верны 1034 *, l3.
8.

Для моего проекта мне нужен оптимальный минимизированный набор. Мне нужно, чтобы наименьшее возможное количество переменных было истинным, исходя из условий, описанных ранее. Для обоих этих прогонов правильный и оптимальный ответ должен быть: l2, l4, l5, l6, l7 (5 истинных). По сути, мне нужно минимизировать стоимость и удовлетворить условия внутри условия maximize.

Однако вместо того, чтобы когда-либо давать оптимальное решение с 5 истинными переменными, я получаю 6, 8, 10 истинных значений.
Что-то, что я также пробовал, было (assert (= (bvand ...) #b1) ) вместо (maximize (bvand ...) ), но безрезультатно.

Как я могу получить минимальное, оптимальное количество истинных переменных, которое также удовлетворяет условию и дает то же самое результат каждый раз, даже при переупорядочении?

примечание: я не могу использовать Int или Bool, так как мои программы, вероятно, будут огромными, а int / bool не сможет с этим справиться.

1 Ответ

0 голосов
/ 19 июня 2020

Здесь есть пара проблем. Прежде всего, вы минимизируете сумму, используя bvadd, который выполняет машинную арифметику c. То есть он будет переполняться за размер бит-вектора. (То есть значение всегда либо 0, либо 1.) Чтобы избежать этого, сделайте сложение для большего размера битового вектора: 

(define-fun ext ((x (_ BitVec 1))) (_ BitVec 8)
    ((_ zero_extend 7) x))

(minimize (bvadd (ext l1) (ext l2) (ext l3) (ext l4) (ext l5) (ext l6) (ext l7) (ext l8) (ext l9) (ext l10)))

Здесь я расширил значения до 8- бит перед добавлением: поскольку у вас 10 переменных, 8-битных значений более чем достаточно для представления всего 10. (В этом случае вы также можете обойтись 4-битными; не то чтобы это имело большое значение. Просто убедитесь, что он достаточно широкий, чтобы представить общее количество переменных, которые вы добавляете.)

Но есть здесь вторая проблема. Вы просите z3 сначала минимизировать эту сумму, а затем максимизировать второе выражение. Z3 выполнит оптимизацию lexicographi c, то есть сначала обработает ваше первое ограничение, а затем использует второе. Но ваш первый сделает все переменные 0, чтобы минимизировать сумму. Чтобы избежать этого, убедитесь, что вы поменяли порядок ограничений.

И в качестве последнего комментария: вы явно сказали, что «примечание: я не могу использовать Int или Bool, поскольку мои программы, вероятно, будут огромными и int / bool не сможет с этим справиться ". Я считаю это очень сомнительным. Для такой проблемы Bool будет наиболее очевидным и оптимальным выбором. В частности, оптимизатору будет намного проще работать с логическими значениями, чем с битовыми векторами и целыми числами. Поэтому я бы рекомендовал не отказываться от этой идеи, не поэкспериментировав и не получив некоторых доказательств того, что она не масштабируется.

...