Порядок добавления ограничений при решении проблемы SMT - PullRequest
Новая
       21

Порядок добавления ограничений при решении проблемы SMT

1 голос
/ 15 апреля 2020

Допустим, у меня довольно простая проблема с SMT - некоторые свободные переменные и некоторые ограничения С на них. У меня также есть дополнительное ограничение EC. Я хочу предпочесть решение, когда встречаются и C, и EC, и переход к C -только решению, если это невозможно.

Как мне в этом случае позвонить check-sat? Интуиция подсказывает мне что-то вроде этого: 

(assert C)
(push)
(assert EC)
(check-sat)
<dance happy dance if it worked, or ...>
(pop)
(check-sat)

Но я подозреваю, что pop сотрет все добывающие решения, а второй check-sat начнется с нуля.

I можно попробовать 

(assert C)
(check-sat)
(push)
(assert EC)
(check-sat)
<dance happy dance if it worked, or ...>
(pop)
(check-sat)

Вопрос в том, могу ли я быть уверен, что последний (check-sat) будет бездействующим, поскольку уже был вызов check-sat с тем же набором ограничений?

1 Ответ

2 голосов
/ 15 апреля 2020

Вы пишете:

Но я подозреваю, что pop уничтожит все добываемые Солвером знания, а второй чек-сат начнется с нуля.

Не обязательно. Изученные предложения, которые зависят только от C, не нужно отбрасывать на pop(), хотя это всегда безопасно. Это может зависеть от решателя.

Вопрос в том, могу ли я быть уверен, что последний (check-sat) будет бездействующим, потому что уже был вызов check-sat с тем же ограничением set?

Я не ожидал бы, что решатель SMT будет помнить, что предыдущий check-sat был удовлетворительным, предыдущая модель или даже предыдущая последовательность решений, которые привели к выводу SAT (после Вы утверждали и проверяли что-то еще). Тем не менее, последний check-sat должен быть намного дешевле, чем первая проверка, потому что выученные предложения не нужно генерировать дважды.

Сосредоточив внимание на чисто SMT-решателях, одним из вариантов будет использование API, а не интерфейс SMT-LIB, так что можно просто сохранить модель SAT после первого check-sat, и нет необходимости в третьем check-sat после pop().

Вероятно, вам нужно закодировать вашу проблему как MaxSMT .

Определение 2.3.4. (Partial Weighted MaxSMT, Partial MaxSMT , Weighted MaxSMT). Частично взвешенная проблема MaxSMT представляет собой пару <φ_h, φ_s>, где φ_h - это набор "жестких" T-предложений, а φ_s - набор положительно-взвешенных "мягких" T- пункты вида <C_i, w_i>, и цель состоит в том, чтобы найти набор максимальных весов T-предложений ψ_s, ψ_s ⊆ φ_s, такой, что φ_h ∪ ψ_s является T-удовлетворяемым [NO06, CFG + 10, ABP + 11b, CGSS13a] .

Частичная проблема MaxSMT - это частичное взвешенное исследование MaxSMT лем, в котором все «мягкие» T-предложения в φ_s имеют унитарный вес.

Взвешенная задача MaxSMT - это проблема Partial Weighted MaxSMT, в которой набор «жестких» T-предложений φ_h равен пусто.

[ источник, с. 40 ]

В этом случае вы бы заявили EC как один или несколько мягких предложений .

Допустим, EC список ограничений ec_1, ..., ec_k, есть два случая:

  • вы хотите, чтобы все ec_1, ..., ec_k были выполнены одновременно; тогда вы бы написали: 

    (assert C)
(assert-soft EC)
(check-sat)
(get-model)

  • вы хотите, чтобы максимально возможное подмножество EC было удовлетворено в то же время; тогда вы бы написали: 

    (assert c)
(assert-soft ec_1)
(assert-soft ...)
(assert-soft ec_k)
(check-sat)
(get-model)

MaxSMT поддерживается такими решателями OMT, как Barcelogi c, OptiMathSAT и Z3 .

...