1

问题 给定两个布尔函数f1(a,b)以及f2(a,b,c)a,b 和 c 布尔值，我想知道是否存在 c 的值，这样对于 a et b 的任何组合f1(a,b)=f2(a,b,c)。

例如 iff1(a,b)=a AND b和f2(a,b,c)=a AND b AND c，我们可以看到f1=f2when c=1。但是，如果f1(a,b)=a OR b和f2(a,b,c)=a AND b AND c，则 c 的值不成立f1=f2。

失败的方法 我尝试使用模型检查，在 nuXmv 中实现一个简单的模型，用 CTL 规范回答这个问题，EF ( AG ( (a & b) = (a & b & c)))但它失败了。显然，它适用于规范AG ( c=true -> (a & b = a & b & c))，但它需要有 2^n 规范（其中 n 是两个函数之间的变量数之差）。

您认为解决该问题的最佳方式/工具/方法是什么。

感谢您指出正确的方向。

4

1 回答 1

1

If I were using nuXmv for this task, I would write the following model

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

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

and then incrementally remove from the state space all those states for which the property is falsified. For example, given this:

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

I would then write this (because c is the only watched variable):

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

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

which would actually allow for the iterative-refinement search to stop because now the property is true under all possible evaluations of a and b:

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

Now, this does not appear to be the ideal solution because it requires parsing the output of nuXmv and correspondingly modify the original file. Compared to your approach, that checks all possible assignments of values, this method enumerates only those assignments which make the formula unsatisfiable. Still, there could be exponentially many counter-examples so it is not that much of an improvement.

One alternative is to use SMT with universal quantification over an EUF formula including the definitions of f1 and f2, where the only free variable is 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)

This gives you the following model with the SMT solver z3:

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

If you would like to know all possible values of c for which f1 = f2, then your best shot is to implement an incremental allsat search on top of z3 (see: plenty of Q/A here on stackoverflow on the topic).

于 2019-10-28T11:57:25.877 回答