Проблема производительности с неудовлетворительными моделями

Question

Я использую Z3 для создания ограниченной модели-проверки. Я сталкиваюсь со странной проблемой производительности при попытке выполнить тест на полноту. Тест на полноту должен убедиться, что во всех состояниях каждый путь содержит каждое состояние не более одного раза. Если есть еще пути, которые удовлетворяют этому свойству, Z3 быстро с ответом, однако в случае, когда все пути были рассмотрены, Z3 кажется экспоненциально медленным.

Я сократил свой тестовый пример до следующего:

; Set the problem size (length of path)
(define-fun sz () Int 5)

; Used to define valid states
(define-fun limit ((s Int)) Bool
  (and (>= s 0)
       (<= s sz)))

; Constructs a path of a given length
(define-fun path-of-len ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int))
          (=> (and (>= i 0)
                   (< i len))
          (limit (select path i)))))

; Asserts that a given path only contains unique states
(define-fun loop-free ((path (Array Int Int)) (len Int)) Bool
  (forall ((i Int) (j Int))
          (=> (and (>= i 0)
                   (>= j 0)
                   (< i len)
                   (< j len)
                   (not (= i j)))
              (not (= (select path i) (select path j))))))

; Construct a unique path of a given length
(define-fun path ((path (Array Int Int)) (len Int)) Bool
  (and (path-of-len path len)
       (loop-free path len)))

; Declare a concrete path
(declare-const tpath (Array Int Int))

; Assert that the path is loop free
(assert (path tpath (+ sz 2)))

(check-sat)

На моем компьютере это приводит к следующему времени работы (в зависимости от длины пути):

• 3: 0,057 с
• 4: 0,561 с
• 5: 42.602 с
• 6:> 15 м (прервано)

Если я переключусь с Int на битовые векторы размера 64, производительность станет немного лучше, но все равно будет выглядеть экспоненциально:

• 3: 0,035 с
• 4: 0,053 с
• 5: 0,061 с
• 6: 0,106 с
• 7: 0,467 с
• 8: 1,809
• 9: 2 м 49.074 с

Как ни странно, для длины 10 это займет всего 2м34,197 с. Если я переключусь на битовые векторы меньшего размера, производительность будет немного лучше, но все равно будет экспоненциальной.

Итак, мой вопрос: это ожидать? Есть ли лучший способ сформулировать это ограничение без петель?

Answer 1

Ваша формула, по сути, кодирует проблему «голубиного отверстия».У вас есть sz+1 отверстия (значения 0, 1,…, sz) и sz+2 голуби (ячейки массива (select tpath 0),…, (select tpath (+ sz 1))).Ваш первый квантификатор утверждает, что каждый голубь должен быть помещен в одно из отверстий.Во-вторых, утверждается, что два разных голубя не должны находиться в одной и той же лунке.

Для решения проблемы «лунная дыра» не существует доказательства разрешения по полиномиальному размеру.Таким образом, ожидается экспоненциальный рост времени выполнения.Обратите внимание, что любой SAT-решатель, основанный на разрешении, DPLL или CDCL, будет плохо работать при решении проблемы с голубями.

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

Кстати, вы используете квантификаторы для кодирования параметрических задач.Это элегантное решение, но это не самый эффективный подход для Z3.В целом, для Z3 лучше утверждать, что проблема «расширенного» квантора свободна.Однако для проблемы, описанной в вашем вопросе, это не будет иметь большого значения, поскольку вы все равно будете испытывать экспоненциальный рост.

Answer 2

Точно так же, как сказал Леонардо, поскольку проблема с голубями имеет экспоненциальный характер, производительность в конечном итоге ухудшится.Единственное, что вы, вероятно, могли бы сделать, это отложить время, когда производительность ухудшается.Поскольку вы пробовали битовый вектор, мои предложения - попытаться преобразовать проблему в проблему без кванторов, как это предложил Леонардо, учитывая, что размер задачи заранее задан, и попробовать использовать некоторые тактики.