HW experiment - report

[JoD]

In attachment a hardware verification experiment for IDP. The problem consists of proving that two functions (val_b3_bus and i_val_b3_bus) with the same definition will never be different, regardless of the instantiations of their defining components.

Regular IDP

The proof is exponential in the domains of clock, inval_b1 and inval_b2. This is because the solver needs to assign a two-valued structure to the above predicates before CP can derive that the two functions must be equal.

IDP with standard Congruence Closure (CC) in MinisatID

The proof is only exponential in the size of clock. Given a two-valued interpretation to the clock predicate, chains of equalities of constants can be derived. CC can infer from these equalities of constants that the two functions must be equal. So the domains of inval_b1 and inval_b2 can be arbitrarily large (ofcourse, grounding must still be possible, but CP strongly helps in this regard).

IDP with CC reasoning on equivalences and definitions

Were the two functions defined by an inductive definition, subformula sharing could have derived that they shared the same definitional bodies. Hence, it could be possible for a CC algorithm taking equivalences and rules into account, to derive that both functions are in fact equivalent, implying they must be equal. The exact interpretation of the clock predicate would as a result no longer matter, so this approach is only polynomial in proof size.

IDP with lifted CC reasoning

Ofcourse, this one wouldn't even need grounding :P

[Joachim Jansen]

Is the tested CC branch for MinisatID open for testing by other users?

[Koen De Cock]

It is. It does require some changes to IDP. Both MinisatID/IDP branches are called congruence_closure. CC can be switched on with the option:

stdoptions.congruenceclosure=true

There is still a segfault which occurs with another version of the hw-problem, but this version works fine. I'll try to solve it as soon as possible.