Как проверить наличие 1000+ переменных, не имеющих повторяющихся значений? - PullRequest
Новая
       6

Как проверить наличие 1000+ переменных, не имеющих повторяющихся значений?

1 голос
/ 16 февраля 2020

Я новичок в Z3 и для программы с открытым исходным кодом я хочу использовать решатель z3 для повышения эффективности.

У меня есть около 1000+ значений 

(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const a4 Int)
...

, что приводит к 

(declare-const x1 Int)
(declare-const x2 Int)
...
(assert (=  (+ a1 a2) x1) // in reality its not "plus" but more sophisticated
(assert (=  (+ a3 a4) x2) // however for simplicity lets keep it at that here.
...

Теперь я хочу убедиться, что все переменные от x1 до x500 + имеют разные значения и что нет дубликатов.

конечно, я мог бы сделать 

(assert (not (= x1 x2)))
(assert (not (= x1 x3)))
(assert (not (= x1 x4)))
...
(assert (not (= x2 x3)))
(assert (not (= x2 x4)))
...
(assert (not (= x718 719)))

и это сработало бы - но есть ли лучшее решение?

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

1 Ответ

2 голосов
/ 17 февраля 2020

Вы можете использовать distinct (см. пример ): 

(assert (distinct x1 ... x500))

AFAIK, обычно это внутреннее расширение в последовательности неравенств, как и в случае, представленном вами в ваш пример.

Обсуждение: Ниже следует чисто теоретическое обсуждение эффективности этого кодирования; z3 довольно эффективный SMT-решатель, поэтому вам, возможно, не понадобится делать что-то более сложное, чем просто запустить инструмент.

Отрицание равенства (например, (not (= x y))) обычно разбивается на пару неравенства: 

x < y \/ x > y

Допустим, x < y и x > y переименованы B1 и B2 соответственно, в SAT-механизм подается следующее предложение: 

B1 \/ B2

Теперь, учитывая вашу проблему, вы получаете сотни этих предложений. Все они связаны друг с другом на уровне Linear Arithmeti c, но не на булевом уровне, на котором работает механизм SAT. Таким образом, механизм SAT может генерировать (значительное) количество противоречивых частичных присвоений истинности, которые обычно нарушают свойство транзитивности оператора <, например, 

 x < y /\ y < z /\ z < x

. Эти конфликты будут обнаружены. решателем теории для LRA во время раннего сокращения вызовов и разрешается на логическом уровне путем изучения предложения конфликта, блокирующего недопустимое назначение.

Что можно попробовать:

  • если ваша проблема допускает такое упрощение (если имена x1 ... x500 могут считаться совершенно произвольными, их можно потом зашифровать ...) , вы можете получить более высокие результаты, навязывая строгий общий порядок по переменным x1 ... x500, например 

    x1 < x2 /\ x2 < x3 /\ ... /\ x499 < x500

  • вы можете попробовать увеличить частоту раннего сокращения вызовов с помощью z3, если это доступна опция (примечание: я не уверен, как часто z3 выполняет такие вызовы)

  • вы можете попробовать mcSAT это может хорошо сочетаться с такого рода ограничениями.

РЕДАКТИРОВАТЬ:

Если набор значений, которые могут быть назначены переменные x_i конечны и несколько ограничены по размеру, вы можете попробовать подсчитать количество переменных x_i с определенным значением, используя нестандартное расширение z3 для определения ограничений мощности, например, 

(assert
    ((_ at-most 1)
     (= x1 0)
     (= x2 0)
     ...
     (= x500 0)
    )
)
...
% repeat for all possible values 
...

Я не уверен относительно влияния этого изменения на производительность. В обычных обстоятельствах это положительно скажется на производительности, поскольку ранее обнаруживаются конфликтующие назначения (см., Например, [1] ). Однако вы имеете дело с довольно большим количеством переменных и большой областью значений-кандидатов для переменных x_i, поэтому сглаживание поиска на логическом уровне может оказаться излишним.

...