Armin Biere, Marijn Heule, Matti Järvisalo,
"Efficient CNF Simplification Based on Binary Implication Graphs"
: Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Serie Lecture Notes in Computer Science (LNCS), Vol. 6695, Springer, Seite(n) 201-215, 6-2011
Efficient CNF Simplification Based on Binary Implication Graphs
Sprache des Titels:
Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11)
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.