Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques
Harri Haanpää, Matti Järvisalo, Petteri Kaski, Ilkka Niemelä · Journal on Satisfiability Boolean Modeling and Computation · 2006
A family of satisfiable benchmark instances in conjunctive normal form is introduced. The instances are constructed by transforming a random regular graph into a system of linear equations followed by clausification. Schemes for introducing nonlinear