Проблемы с использованием Z3 для MAX-SAT

Я заинтересован в MAX-SAT и надеялся, что в Z3 это будет встроено. Есть ли планы сделать это в ближайшее время?

В отсутствие вышесказанного я попытался использовать пример приложения maxsat из командной строки. К сожалению, всякий раз, когда я выполняю exec.sh & quot; filename.z3 & quot ;, я всегда получаю следующий ответ: & quot; проверка того, выполнимы ли жесткие ограничения ... result: 0 & quot ;. Что я делаю неправильно? Уверяю вас, этот ответ, по-видимому, совершенно не зависит от фактического содержимого файла.

Наконец, комментарии в примере maxsat не содержат четкого указания, как помечать ограничения как жесткие или мягкие. Жестким ограничением считается формула, которой предшествует: формула, а мягким ограничением - формула, которой предшествует: допущение. Таким образом, чтобы пометить & quot; (утверждать (& gt; x 0)) & quot; как мягко, куда именно мы помещаем & quot;: предположение & quot ;? (Я прочитал запрос о жестких и мягких ограничениях, но вопрос / ответ, казалось, был скорее в контексте поиска неудовлетворительных ядер, а не «максимально выполнимых ядер» неудовлетворительных формул.)

Ответы на вопрос(1)

Пример MaxSAT в дистрибутиве Z3 демонстрирует, как реализовать два алгоритма MaxSAT с использованием API Z3. В примере все еще используется старый (устаревший) API для установления ограничений, но его можно легко изменить, чтобы использовать новый API решателя. Пример приложения читает файл SMT 1.0. Однако функции MaxSAT можно использовать в формулах, созданных с использованием C API. Сценарий предполагает, что:assumption поля мягкие ограничения и:formula это тяжелый Вот небольшой пример, где(> x 0), (> y 0), (< x y) а также(> x (- y 1)) мягкие ограничения, и(> (+ x y) 0) а также(< (- x y) 100) тяжелые. Пример приложения возвращает3, То есть могут быть выполнены не более трех из мягких ограничений.

(benchmark ex
  :extrafuns ((x Int))
  :extrafuns ((y Int))
  ;; Soft Constraints
  :assumption (> x 0)
  :assumption (> y 0)
  :assumption (< x y)
  :assumption (> x (- y 1))
  :formula 
  (and 
  ;; Hard Constraints
  (> (+ x y) 0)
  (< (- x y) 100)
))

При этом у нас нет планов поддерживать MaxSAT непосредственно в API Z3. В будущих версиях мы можем портировать пример MaxSAT на другие API (.NET, Python и C ++).

Ваш ответ на вопрос