Challenging Certificates from Model Checking

The Hardware Model Checking Competition 2024 introduced certificates to the bit-level track of the competition in the form of witness circuits.Checking the correctness of a witness circuit entails solving a set of five SAT formulas. If all of them are unsatisfiable the witness circuit is valid, and the safety of the original model is proven. This benchmark set containts 20 of the most challenging certification tasks from the competition. The benchmark set is contained in cnf.tar.zst. Run make to regenerate it. Note that this runs a model checker portfolio and is therefore non-deterministic. To produce more/different CNFs adjust the list in make_cnf.sh