Description: These benchmarks are derived from the problem of
comparing reference and production implementations of cryptographic
algorithms. All but one of these problems, stated as a direct
equivalence between And-Inverter Graphs, can be solved by ABC in a
relatively short amount of time (a few minutes at most), but none of
them can currently be solved within an hour using picosat. This
suggests that they're inherently tractable, but have a structure that
current solvers (or at least one of them!) aren't able to exploit. One
example (aes_id.cnf) has not been proved by any solver in any form,
but at a higher level of abstraction should be a relatively easy
proof.