Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques

Reference:

Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä. Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):27–46, 2006.

Abstract:

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 nonlinearity to the instances are developed, making the instances suitable for benchmarking solvers with equivalence reasoning techniques. An extensive experimental evaluation shows that state-of-the-art solvers scale exponentially in the instance size. Compared with other well-known families of satisfiable benchmark instances, the present instances are among the hardest.

Suggested BibTeX entry:

@article{HJKN:JSAT06,
    author = {Harri Haanp{\"a}{\"a} and Matti J{\"a}rvisalo and Petteri Kaski and Ilkka Niemel{\"a}},
    journal = {Journal on Satisfiability, Boolean Modeling and Computation},
    number = {1-4},
    pages = {27--46},
    title = {Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques},
    volume = {2},
    year = {2006},
}