CODEWITHSUNDEEP
model-checkingsatctlnuxmv
f1f2
f1f2

Reputation: 23

Determining when two boolean functions are equivalent?

Problem Given two boolean functions f1(a,b) and f2(a,b,c) with a,b and c booleans, I'd like to know if there exists a value of c such that for any combinations of a et b f1(a,b)=f2(a,b,c).

For example if f1(a,b)=a AND b and f2(a,b,c)=a AND b AND c, we can see that f1=f2 when c=1. However, if f1(a,b)=a OR b and f2(a,b,c)=a AND b AND c, no value of c holds for f1=f2.

Failed approach I tried to use model checking, with a trivial model implemented in nuXmv, to answer this question with a CTL specification such as EF ( AG ( (a & b) = (a & b & c))) but it fails. Obviously, it works fine with the specification AG ( c=true -> (a & b = a & b & c)) but it requires to have 2^n specifications (with n being the difference between the number of variables between the two functions).

What is the best way/tool/approach in your opinion to tackle the issue.

Thanks for pointing to the right direction.

Upvotes: 1

Views: 787

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

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).

Upvotes: 1

Related Questions