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. © 2011 Springer-Verlag.
CITATION STYLE
Heule, M. J. H., Järvisalo, M., & Biere, A. (2011). Efficient CNF simplification based on binary implication graphs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6695 LNCS, pp. 201–215). https://doi.org/10.1007/978-3-642-21581-0_17
Mendeley helps you to discover research relevant for your work.