Решение проблемы SAT с использованием Z3 без повторения логического выражения

Давайте рассмотрим следующую задачу: f(a, b, c, x, y, z) — это логическая функция, где a, b, c, x, y и z — логические значения, а вывод f — логическое значение. Определение f состоит из ряда операторов и/или/ни. Я хочу найти набор из трех логических значений x0, y0 и z0, таких что:

f(0, 0, 0, x0, y0, z0) = 0 AND
f(0, 0, 1, x0, y0, z0) = 1 AND
f(0, 1, 0, x0, y0, z0) = 1 AND
f(0, 1, 1, x0, y0, z0) = 0 AND
...
f(1, 1, 1, x0, y0, z0) = 1 # A total of 8 constrains. Each of them is from an entry in the truth table.

Наивный подход состоит в том, чтобы определить 3 логические переменные x, y, z и повторно определить функцию f 8 раз. Однако f состоит из сложных логических выражений. Определение его 8 раз может взорвать модель. При этом фактически у меня есть 7 переменных: a, b, c, d, e, f, g. В таблице истинности 128 записей.

Есть ли способ определить что-то вроде переменных-заполнителей a, b, c, которые не являются частью решения? Затем я могу определить f для a, b, c, x, y, z только один раз, а позже каким-то образом присвоить a, b, c булевым константам.

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


sat z3 smt
person Wu Yongzheng    schedule 16.12.2020    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Трудно точно расшифровать, что вы пытаетесь сделать. Но мне кажется, что вы беспокоитесь о том, как легко кодировать это, в отличие от чего-либо еще. Если это так, я бы рекомендовал программировать на языке, который предоставляет API более высокого уровня, чем SMTLib. Вы можете использовать многие интерфейсы, поддерживаемые z3: C, C++, Java и т. д., чтобы упростить задачу программирования.

Например, вот как можно использовать интерфейс Python для кодирования экземпляра вашей проблемы:

from z3 import *

def fOriginal(a, b, c, x, y, z):
    return Or([a, b^c, x, y, z])

x0, y0, z0 = Bools("x0 y0 z0")

def f(a, b, c):
    return fOriginal(a == 1, b == 1, c == 1, x0, y0, z0)

s = Solver()

s.add(f(0, 0, 0) == False)
s.add(f(0, 0, 1) == True)
s.add(f(0, 1, 0) == True)
s.add(f(0, 1, 1) == False)
s.add(f(1, 1, 1) == True)

print(s.check())
print(s.model())

При запуске это печатает:

sat
[y0 = False, z0 = False, x0 = False]

Даю вам задание на x0, y0 и z0, пока вы пытаетесь найти.

Идея состоит в том, чтобы закодировать f как обычную функцию, используя интерфейс z3. Я назвал эту функцию fOriginal в коде Python. Затем мы определяем версию fOriginal, которую я назвал в коде f, которая передает символические значения для последних трех аргументов, но ожидает константы для первых трех.

Затем мы просто добавляем ограничения для каждого из ваших случаев. Я добавил только 5 выше по вашему примеру; Вы можете добавить все 8, конечно.

Я надеюсь, что это поможет вам начать!

person alias    schedule 16.12.2020
comment
Спасибо. Меня беспокоит сложность модели, а не чистый код. Логическое выражение определено 5 (или 8) раз. Вот что меня беспокоит. - person Wu Yongzheng; 17.12.2020
comment
Я не думаю, что сложность модели будет проблемой для такого размера. Если вы используете квантификаторы, решателю определенно будет сложнее решать проблему в любом случае. Я рекомендую попробовать его и иметь дело только со сложностью, если вы ее наблюдаете. - person alias; 17.12.2020
comment
Я пытаюсь построить схему декодера с 7-сегментным дисплеем, используя минимальное количество вентилей NOR. Учитывая булеву функцию от 4 до 7 бит, она в основном ищет эквивалентную схему. Код находится по адресу gist.github.com/wuyongzheng/ab0be78beb3c15d000c32b6c8b773516. С num_gates = 13 он дает unsat через 2 минуты. С большим количеством ворот он работает слишком долго. - person Wu Yongzheng; 19.12.2020

arrow_upward
0
arrow_downward

Мне не ясно, для чего вам нужна модель и какая гибкость вам нужна, но вот идея: если допустимо ограничивать функцию всеми значениями аргументов с помощью одного другого случая, то может работать следующее:

(declare-fun f (Bool Bool Bool Bool) Bool)

(assert (forall ((x Bool) (y Bool) (z Bool) (p Bool)) (!
  (=
    (f x y z p)
    (ite
      (and (not x) y) true (ite         ; 1. case
      (and (not x) (not y) z) true (ite ; 2. case
      (and x (not y) z) true            ; 3. case
      false))))                         ; else-case
  :pattern ((f x y z p)))))

По крайней мере, в этом простом случае модель Z3 фактически игнорировала несущественный 4-й параметр функции f:

(check-sat) ;; SAT --> good
(get-model)  
; NOTE: 4th parameter x!3 is declared, but not used
; (model 
;   (define-fun p () Bool
;     false)
;   (define-fun f ((x!0 Bool) (x!1 Bool) (x!2 Bool) (x!3 Bool)) Bool
;     (or (not (or x!0 (not x!1)))
;         (not (or x!1 (not x!2) (not x!0)))
;         (not (or x!1 x!0 (not x!2)))))
; )
person Malte Schwerhoff    schedule 16.12.2020
comment
Важная часть информации заключается в том, что необходимо использовать квантификатор (и существуют различные кодировки, которые немного отличаются). Проблема в том, что решатель будет вести себя гораздо менее предсказуемо и часто будет занимать гораздо больше времени, чем для некоторого небольшого количества копий f в кодировании без квантификаторов. В некоторых случаях, если нет очевидных упрощений, решатель также выдаст все возможные комбинации значений, которые вы бы перечислили вручную (например, с помощью MBQI). - person Christoph Wintersteiger; 16.12.2020