TY - GEN
T1 - Efficient CNF Simplification Based on Binary Implication Graphs
AU - Biere, Armin
AU - Heule, Marijn
AU - Järvisalo, Matti
PY - 2011/6
Y1 - 2011/6
N2 - This paper develops techniques for efficiently detecting redundancies
in CNF formulas. We introduce the concept of hidden literals, resulting in the
novel technique of hidden literal elimination. We develop a practical simplification
algorithm that enables “Unhiding” various redundancies in a unified framework.
Based on time stamping literals in the binary implication graph, the algorithm
applies various binary clause based simplifications, including techniques
that, when run repeatedly until fixpoint, can be too costly. Unhiding can also be
applied during search, taking learnt clauses into account. We show that Unhiding
gives performance improvements on real-world SAT competition benchmarks.
AB - This paper develops techniques for efficiently detecting redundancies
in CNF formulas. We introduce the concept of hidden literals, resulting in the
novel technique of hidden literal elimination. We develop a practical simplification
algorithm that enables “Unhiding” various redundancies in a unified framework.
Based on time stamping literals in the binary implication graph, the algorithm
applies various binary clause based simplifications, including techniques
that, when run repeatedly until fixpoint, can be too costly. Unhiding can also be
applied during search, taking learnt clauses into account. We show that Unhiding
gives performance improvements on real-world SAT competition benchmarks.
UR - https://www.scopus.com/pages/publications/79959465742
U2 - 10.1007/978-3-642-21581-0_17
DO - 10.1007/978-3-642-21581-0_17
M3 - Conference proceedings
SN - 9783642215803
VL - 6695
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 201
EP - 215
BT - Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11)
PB - Springer
ER -