Armin Biere,
"Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017"
, in Tomas Toma?s?, Marijn Heule, Matti Järvisalo: Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions, Vol. B-2017-1, University of Helsinki, Seite(n) 40-41, 2017
Original Titel:
Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017
Sprache des Titels:
Englisch
Original Buchtitel:
Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions
Original Kurzfassung:
In this benchmark description we describe our three set of benchmarks submitted to the SAT Competition 2016. The ?rst contains bounded model checking problems from the deep bound track of the hardware model checking competition. The second crafted set of benchmarks has the sole purpose to show that the standard watch list implementation has a quadratic corner case. As third set of benchmarks we submitted factoring problems of products of medium sized primes, which seem to be hard for standard SAT solvers, but become trivial if the solution is reencoded back into the CNF by ?ipping literals appropriately
Forschungs-