Нарушение симметрии для Z3 — в контексте логики UFBV (новая версия)

StackOverflow https://stackoverflow.com/questions/9300754

  •  25-10-2019
  •  | 
  •  

Вопрос

(Это моя вторая попытка получить помощь.Если вопрос/подход не имеет смысла или неясен, просто дайте мне знать.Я также буду рад любой небольшой подсказке или ссылке, которая поможет мне понять поведение Z3 с моими SBA)

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

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

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

Один из моих подходов (я думаю, самый многообещающий) основан на нарушении симметрии отношений относительно.свои домены.Он вводит для каждой области D отношения R и каждого атома a \in D аксиомы, которые обеспечивают порядок в двоичном представлении R^{M} и R^{M[a+1/a]}, где M — это модель по спецификации.Для однородных отношений аксиомы смягчены.

Пусть R \subset AxA — отношение.Мои аксиомы расслабленного нарушения симметрии для R выглядят так:

;; SBA(R, A)_upToDiag
(assert
 (forall ( (ai A) (aj A) )
  (=>
   (bvult ai aj)
   (=>
    (forall ((x A))
     (=>
       (bvult x aj)
       (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
     )
    )
    (=>
     (R ai aj)
     (R (bvadd  ai  (_ bv1 n)) aj)
)))))    

;; SBA(R, A)_diag
(assert
 (forall ( (ai A) )
  (=>
   (forall ((x A))
    (=>
      (bvult x ai)
      (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    )
   )
   (=>
    (R ai ai)
    (R (bvadd  ai  (_ bv1 n)) (bvadd  ai  (_ bv1 n)))
))))

Моя проблема в том, что эффект от использования этих SBA не является стабильным/постоянным.Он отличается от привязки к привязке и спецификации формы от другой.Также на производительность влияет использование всех или только одного из SBA.

В контексте SAT успех так называемого подхода с предикатом нарушения симметрии (SBP) основан на возможности обратного отслеживания решателя SAT, которая (каким-то образом) гарантирует, что, если решатель откажется от обратного пути, он затем сократит пространство поиска, используя: среди прочего, SBP.

  • В чем отличия (если есть) в контексте Z3?
  • Как я могу заставить решение использовать эти аксиомы для сокращения пространства поиска (когда оно возвращается назад)?
  • Поможет ли использование шаблонов (квантификаторов) для моих SBA?

С уважением,

Абубакр Ахраф Эль-Гази

Это было полезно?

Решение

В Z3 3.2 есть два основных механизма для обработки количественных формул:Электронное сопоставление и MBQI (создание квантора на основе модели).Электронное сопоставление эффективно только в случае невыполнимых формул.Z3 не сможет показать, что формула выполнима с использованием этого движка.MBQI дороже, но он может показать, что несколько классов формул (содержащих кванторы) выполнимы.А Руководство по Z3 описывает эти два двигателя (и другие варианты).Чтобы эффективно использовать Z3 для решения нетривиальных задач, очень полезно понимать, как работают эти два движка.

Нарушение симметрии обычно является очень эффективным способом уменьшить пространство поиска.Трудно точно определить, что происходит в вашей проблеме.Я вижу следующие объяснения нестабильного поведения:

  • MBQI испытывает трудности с созданием модели, удовлетворяющей требованиям SBA.Хотя SBA сокращают пространство поиска, если задача выполнима, Z3 попытается построить интерпретацию (модель), которая их удовлетворяет.Итак, в данном случае SBA просто накладные расходы.Это особенно верно, если входную формулу очень легко выполнить, но становится сложно, когда вы добавляете SBA.Вы можете подтвердить эту гипотезу, воспользовавшись опцией MBQI_TRACE=true.Z3 будет отображать такие сообщения, как: [mbqi] failed k!18.Где k![line-number] — идентификатор квантора.Вы можете назначить свои собственные идентификаторы, используя тег :qid.Вот пример:

    (assert (forall ((x T) (y T)) (!(=> (и (подтип xy) (подтип yx)) (= xy)): QID антисимметрия)))))))

Кстати, вы можете отключить модуль MBQI, используя MBQI=false.

В будущих версиях Z3 мы планируем добавить возможность отключения MBQI для некоторых количественных формул.Эта функция может быть полезна для SBA.

  • Другое объяснение состоит в том, что электронное сопоставление создает слишком много экземпляров SBA.Вы можете подтвердить это, используя опцию QI_PROFILE=true.Z3 выгрузит такую ​​информацию, как:

[quantifier_instances] антисимметрия:12 :1:2.00

Первое число — это количество сгенерированных экземпляров.Если это источник проблемы, одним из решений является назначение ограничительных шаблонов для SBA, генерирующих слишком много экземпляров.Например, Z3 будет использовать (R ai aj) как образец для SBA(R, A)_upToDiag.Этот тип шаблона может создавать квадратичное количество экземпляров.Другой эксперимент заключается в отключении электронного сопоставления.Пример, вариант

AUTO_CONFIG=false EMATCHING=false MBQI=true

Вы также можете попробовать отключить распространение релевантности в приведенной выше конфигурации, опция: RELEVANCY=0.

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

Лицензировано под: CC-BY-SA с атрибуция
Не связан с StackOverflow
scroll top