Решатель Z3 возвращает unsat, когда формула должна быть удовлетворительной

У меня есть «простая» формула, которую решатель Z3 (интерфейс Python) не может обработать. Он работает довольно долго (30 минут), а затем возвращается неизвестным, хотя я могу найти удовлетворительное задание вручную менее чем за минуту. Это формула:

[Or(<uc 1.0> == 0, <uc 1.0> == 1),
 Or(<uc 1.1> == 0, <uc 1.1> == 1),
 Or(<uc 1.2> == 0, <uc 1.2> == 1),
 <uc 1.0> + <uc 1.1> + <uc 1.2> == 1,
 Or(<uc 0.0> == 0, <uc 0.0> == 1),
 Or(<uc 0.1> == 0, <uc 0.1> == 1),
 Or(<uc 0.2> == 0, <uc 0.2> == 1),
 <uc 0.0> + <uc 0.1> + <uc 0.2> == 1,
 Or(<uc 2.0> == 0, <uc 2.0> == 1),
 Or(<uc 2.1> == 0, <uc 2.1> == 1),
 Or(<uc 2.2> == 0, <uc 2.2> == 1),
 <uc 2.0> + <uc 2.1> + <uc 2.2> == 1,
 ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000,
                           ForAll(a,
                                  Or(a > 1000,
                                     Or(a < -1000,
                                        And(And(And(True,
                                        a ==
                                        <uc 0.0>*b +
                                        <uc 0.1>*c +
                                        <uc 0.2>*a),
                                        b ==
                                        <uc 1.0>*b +
                                        <uc 1.1>*c +
                                        <uc 1.2>*a),
                                        c ==
                                        <uc 2.0>*b +
                                        <uc 2.1>*c +
                                        <uc 2.2>*a))))))))))]

Это может показаться немного пугающим, но позвольте мне рассказать вам об этом. ‹Uc i.j> - целые переменные. Сначала я указываю, что они должны быть либо 0, либо 1, а затем ввожу ограничение, согласно которому ровно один из них должен быть равен 1, а остальные должны быть равны 0 (используя сумму).

Во второй части вы можете игнорировать все ИЛИ, которые в основном просто ограничивают мое пространство поиска для каждой переменной до [-1000, 1000]. Затем у меня есть большинство внутренних ограничений, которые должны означать: ‹uc 0.2> = 1‹ uc 1.0> = 1 ‹uc 2.1> = 1 и все остальные = 0. Вот и все. Я почти уверен, что решатель должен решить эту проблему, но не повезло. Я могу изменить ограничение суммы на что-то вроде Or (‹uc 1.0>,‹ uc 1.1>, ‹uc 1.2>), что, как ни странно, решает мою проблему в этом случае (решатель возвращает правильное назначение в секундах), но в целом , это, очевидно, не эквивалентно тому, что я хочу иметь.

Вопросы:

  • Есть ли что-то вроде бита, который я мог бы использовать вместо целых чисел?
  • Какой-нибудь рекомендуемый способ выразить тот факт, что ровно один аргумент равен 1?
  • Другой способ сделать это разрешимым без изменения второй части формулы.

Большое тебе спасибо!

// Редактировать: поигравшись с несколькими вариантами, я «решил» это, поместив побочные условия после условия ForAll (просто поменяв местами две строки кода). Это не должно иметь никакого значения, но теперь он находит правильное задание за 0,5 секунды - что? Я также пробовал пример с 4 переменными (a, b, c, d) вместо (a, b, c), но опять же он работает часами ... Любая помощь? Также не сработало изменение суммы с длиной И / ИЛИ.


python z3 z3py sat-solvers
person user667804    schedule 15.05.2015    source источник
comment
Попробуйте заменить * на + (функция, конечно же, должна быть обратимой), и вы увидите чудесное улучшение скорости.   -  person phant0m    schedule 17.05.2015
comment
как я могу? Я имею в виду, что мне нужен a * b, чтобы в зависимости от того, 0 или 1, я выбираю b. Использование + изменило бы результат, верно?   -  person user667804    schedule 17.05.2015
comment
Конечно, будет. Просто у z3 вроде бы проблемы с умножением в некоторых случаях. Когда вы пробуете функцию с эквивалентной или аналогичной сложной структурой, которая использует + вместо *, таких проблем не возникает. Кажется, что как только вы начинаете связывать несколько уравнений, содержащих int *, z3 застревает. OTOH, я только что заметил, что у вас * для выбора выбора ... Этого можно избежать, но * в самой функции - нет;)   -  person phant0m    schedule 17.05.2015

Ответы (2)


arrow_upward
1
arrow_downward

Я пробовал ваш пример, используя логические значения вместо целых чисел для переменных 0-1. Однако это не слишком хорошо помогает. В настоящее время механизмы создания экземпляров квантора могут быть улучшены для обработки таких экземпляров.

person Nikolaj Bjorner    schedule 19.05.2015

arrow_upward
1
arrow_downward

поэтому я не мог избавиться от умножений без реструктуризации всего подхода, поэтому вместо этого я переместил блок со всеми условиями (uc = 1 или uc = 1 и sum = 1) ниже блока forAll. В большинстве случаев это срабатывало, но было еще несколько тестов, где он работал часами безрезультатно. Что в итоге дало мне возможность, так это сгруппировать операторы forAll вместе вместо того, чтобы разделять их. Так что вместо:

ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000...

Я бы получил что-то вроде этого

ForAll(c,
   ForAll(b,
        Or(c > 1000,
           Or(c < -1000,
              Or(b > 1000,
                 Or(b < -1000...

Это, наконец, решило проблему, и теперь решатель смог справиться со всеми тестовыми примерами. Я немного разочарован тем, что потребовалось столько попыток и ошибок, чтобы все исправить, но, по крайней мере, теперь я могу решать свои формулы. Спасибо!

person user667804    schedule 19.05.2015
comment
Я согласен, это определенно указывает на несколько мест, где Z3 мог бы добиться большего. Спасибо за пример. - person Nikolaj Bjorner; 20.05.2015