Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017

Armin Biere

Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017

Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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

Original language	English
Title of host publication	Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions
Editors	Tomas Tomáš, Marijn Heule, Matti Järvisalo
Publisher	University of Helsinki
Pages	40-41
Number of pages	2
Volume	B-2017-1
Publication status	Published - 2017

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{83e1e941b9054e16a892ae085fc5d0ce,

title = "Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017",

abstract = "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",

author = "Armin Biere",

year = "2017",

language = "English",

volume = "B-2017-1",

pages = "40--41",

editor = "\{Tomas Tom{\'a}{\v s}, Marijn Heule, Matti J{\"a}rvisalo\}",

booktitle = "Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions",

publisher = "University of Helsinki",

}

Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017. / Biere, Armin.
Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions. ed. / Tomas Tomáš, Marijn Heule, Matti Järvisalo. Vol. B-2017-1 University of Helsinki, 2017. p. 40-41.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017

AU - Biere, Armin

PY - 2017

Y1 - 2017

N2 - 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

AB - 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

M3 - Conference proceedings

VL - B-2017-1

SP - 40

EP - 41

BT - Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions

A2 - Tomas Tomáš, Marijn Heule, Matti Järvisalo, null

PB - University of Helsinki

ER -