Использование SMT-LIB для подсчета количества модулей по формуле - PullRequest
Новая
       13

Использование SMT-LIB для подсчета количества модулей по формуле

0 голосов
/ 07 января 2019

Я не уверен, что это возможно при использовании SMT-LIB, если это невозможно, существует ли альтернативный решатель, способный это сделать?

Рассмотрим уравнения

  • a < 10 и a > 5
  • b < 5 и b > 0
  • b < c < a
  • с a, b и c целыми числами

Значения для a и b, где существует максимальное количество моделей, которые удовлетворяют уравнениям при a=9 и b=1.

Поддерживает ли SMT-LIB следующее: Для каждого значения a и b подсчитывайте количество моделей, которые удовлетворяют формулам, и задайте значения для a и b, которые максимизируют количество.

Ответы [ 2 ]

0 голосов
/ 08 января 2019

Давайте сломаем ваши цели:

  • Вы хотите перечислить все возможные способы, которыми a и b (... и более) можно присвоить
  • Для каждой комбинации вы хотите посчитать количество подходящих моделей

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

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

Однако также возможно, что ваше реальное приложение не так сложно на практике, и поэтому оно может быть обработано SMT Solver .

Общая идея может состоять в том, чтобы использовать SMT Solver API и действовать следующим образом:

  • assert вся формула
  • повторять до завершения комбинации значений:
    • push точка возврата
    • assert одна конкретная комбинация значений, например, a = 8 and b = 2
    • повторить навсегда:
      • check для решения
      • если UNSAT, выйти из самой внутренней петли
      • если SAT, увеличить счетчик моделей для данной комбинации значений a и b
      • принять значение модели любой другой переменной, например, c = 5 and d = 6
      • assert новое ограничение, запрашивающее, чтобы хотя бы одна из «других» переменных изменила свое значение, например, c != 5 or d != 6
    • pop точка возврата

В качестве альтернативы, вы можете перечислить возможные назначения по a и b не явно, а явно. Идея была бы следующей:

  • assert вся формула
  • повторить навсегда:
    • check для решения
    • если UNSAT, выходной цикл
    • если SAT, взять комбинацию значений ваших управляющих переменных из модели (например, a = 8 and b = 2), проверить на внутренней карте, встречались ли вы раньше с этой комбинацией, если не установить счетчик на 1, в противном случае увеличить счетчик на 1.
    • принять значение модели любой другой переменной, например, c = 5 and d = 6
    • assert новое ограничение, запрашивающее новое решение, например, a != 8 or b != 2 or c != 5 or d != 6

В случае, если вы сомневаетесь, какой SMT Solver выбрать, я бы посоветовал вам начать решение вашей задачи с pysmt , что позволяет один на выбор из нескольких двигателей SMT с легкостью.

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

0 голосов
/ 08 января 2019

Я не думаю, что вы можете сделать это в целом; то есть, когда вы можете иметь произвольные ограничения на произвольные теории. Вы задаете мета-вопрос: «Максимизировать количество моделей» - это не вопрос самой проблемы, а вопрос о моделях проблемы; что-то, с чем SMTLib не может справиться.

Сказав это, однако, я думаю, что должно быть возможно закодировать это для определенных проблем. В приведенном вами примере пространство модели максимизируется, когда a - b является наибольшим; так что вы можете просто написать: 

(set-option :produce-models true)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (< 5 a 10))
(assert (< 0 b  5))
(assert (< b c  a))

(maximize (- a b))
(check-sat)
(get-value (a b))

На что отвечает z3: 

sat
((a 9)
 (b 1))

по желанию. Или вы можете использовать привязки Python: 

from z3 import *

a, b, c = Ints('a b c')
o = Optimize()
o.add(And(5 < a, a < 10, 0 < b, b < 5, b < c, c < a))
o.maximize(a - b)

if o.check() == sat:
    m = o.model()
    print "a = %s, b = %s" % (m[a], m[b])
else:
    print "unsatisfiable or unknown"

который печатает: 

a = 9, b = 1

Существуют также привязки для C / C ++ / Java / Scala / Haskell и т. Д., Которые позволяют вам делать более или менее то же самое с этими хостами.

Но решающим моментом здесь является то, что нам пришлось вручную придумать цель, чтобы максимизация a - b разрешила бы проблему здесь. Этот шаг требует вмешательства человека, так как он относится к вашей текущей проблеме. (Представьте, что вы работаете с теорией поплавков или произвольными типами данных; придумать такую ​​меру может быть невозможно.) Я не думаю, что эту часть можно волшебным образом автоматизировать с помощью традиционного решения SMT. (Если Патрик не придумает умную кодировку, он довольно умный в этом смысле!)

...