Каков наиболее эффективный способ кодирования псевдобулевых ограничений в z3?

Question

Я думаю, что есть два различных соответствующих случаев здесь:

Случай 1:

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

(ITE (boolean_expr) 1 0)

Я тогда установить общий булево используя только сумму и большее, чем

(> (+ b1 b2 b3 ...) 0)

Случай 2 (это не может быть действительно псевдобулева):

у меня есть два набора логических переменных:

set1 = n_1, n_2 ....

set2 = m_1, m_2 ....

Я хотел бы добавить ограничение: количество переменных, заданной истину в set1 равно к числу, установленному в true в set2.

Как и выше, я в настоящее время делаю это с помощью целых чисел вместо Булевых и установки каждых из них с Внутриушными формами:

n_1 = (ITE (boolean_expr) 1 0)

, а затем говоря, что:

n_1 + n_2 + .... = m_1 + m_2 ......

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

Спасибо.

Answer 1

В настоящее время вы можете использовать целые числа для кодирования ограничений PB. Вы должны связаны переменные, чтобы быть в интервале 0, 1. Например:

(set-logic QF_LIA) 
(declare-const n1 Int) 
(declare-const n2 Int) 
(assert (<= 0 n1)) 
(assert (<= n1 1)) 
(assert (<= 0 n2)) 
(assert (<= n2 1)) 
(assert (>= (+ n1 n2) 1)) 
(check-sat) 

Если установить логику в QF_LIA, то Z3 будет пытаться автоматически перекодировать эти ограничения с помощью битового векторы. В подробном выводе вы увидите, что Z3 вызывает тактику pb2bv, которая делает переписывание для вас

z3 ty.smt2 /v:10 
(simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(propagate-values :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(ctx-simplify :num-steps 17) 
(ctx-simplify :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(solve_eqs :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(elim-uncnstr-vars :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(simplifier :num-exprs 10 :num-asts 173 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(pb2bv :num-exprs 4 :num-asts 180 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(simplifier :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(propagate-values :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(solve_eqs :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(max-bv-sharing :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(bit-blaster :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(aig :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77) 
(ast-table :capacity 640 :size 178) 
(sat-status 
    :inconsistent false 
    :vars   2 
    :elim-vars  0 
    :lits   2 
    :assigned  0 
    :binary-clauses 1 
    :ternary-clauses 0 
    :clauses   0 
    :del-clause  0 
    :avg-clause-size 2.00 
    :memory   0.77)