@inproceedings{HeuleJB:SAT2011, author = {Marijn Heule and Matti J\"arvisalo and Armin Biere}, title = {Efficient {CNF} Simplification based on Binary Implication Graphs}, booktitle = {Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011)}, editor = {Karem Sakallah and Laurent Simon}, series = {Lecture Notes in Computer Science}, volume = {6695}, pages = {201--215}, year = {2011}, } Abstract: 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.