Определение, когда две булевы функции эквивалентны? - PullRequest
Новая
       127

Определение, когда две булевы функции эквивалентны?

1 голос
/ 28 октября 2019

Проблема Учитывая две логические функции f1(a,b) и f2(a,b,c) с логическими значениями a, b и c, я хотел бы знать, существует ли значение c такое, что для любых комбинаций etb f1(a,b)=f2(a,b,c).

Например, если f1(a,b)=a AND b и f2(a,b,c)=a AND b AND c, мы можем увидеть , что f1=f2 при c=1. Однако, если f1(a,b)=a OR b и f2(a,b,c)=a AND b AND c, значение * не сохраняется для f1=f2.

Неудачный подход Я попытался использовать проверку модели с тривиальной моделью, реализованной в nuXmv,ответить на этот вопрос с помощью спецификации CTL, такой как EF ( AG ( (a & b) = (a & b & c))), но это не удается. Очевидно, что он прекрасно работает со спецификацией AG ( c=true -> (a & b = a & b & c)), но требует наличия 2 ^ n спецификаций (при этом n равно разнице в количестве переменных между двумя функциями).

Каков наилучший способ / инструмент/ подход, по вашему мнению, для решения проблемы.

Спасибо за указание в правильном направлении.

1 Ответ

1 голос
/ 28 октября 2019

Если бы я использовал nuXmv для этой задачи, я написал бы следующую модель 

MODULE main
VAR
    a : boolean;
    b : boolean;
    c : boolean;

CTLSPEC ((a & b) = (a & b & c));

, а затем постепенно удалял из пространства состояний все те состояния, для которых свойство подделано. Например, учитывая это: 

nuXmv > reset; read_model -i test.smv ; go ; check_property 
-- specification (a & b) = ((a & b) & c)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a = TRUE
    b = TRUE
    c = FALSE

Я бы тогда написал это (потому что c является единственной наблюдаемой переменной): 

MODULE main
VAR
    a : boolean;
    b : boolean;
    c : boolean;
INVAR
    c != FALSE;

CTLSPEC ((a & b) = (a & b & c));

, которая фактически позволила бы выполнять итеративное уточнениепоиск, чтобы остановить, потому что теперь свойство истинно при всех возможных оценках a и b: 

nuXmv > reset; read_model -i test.smv ; go ; check_property
-- specification (a & b) = ((a & b) & c)  is true

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

Одной из альтернатив является использование SMT с универсальным количественным определением по формуле EUF , включая определения f1 и f2, где единственной свободной переменной является c: 

(define-fun f1 ((a Bool) (b Bool)) Bool
               (and a b)
)
(define-fun f2 ((a Bool) (b Bool) (c Bool)) Bool
               (and a b c)
)
(declare-fun c () Bool)

(assert (forall
            ((a Bool) (b Bool))
            (=
                (f1 a b)
                (f2 a b c)
            )
))

(check-sat)
(get-model)

Это дает вам следующую модель с SMT solver z3: 

~$ z3 test3.smt2 
sat
(model 
  (define-fun c () Bool
    true)
)

Если вы хотите знать все возможные значения c, для которых f1 = f2, тогда ваш лучший выстрелреализовать инкрементный поиск в allsat поверх z3 (см. множество вопросов и ответов здесь по stackoverflow по теме).

...