You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques


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.