Blocked Clause Elimination

Boolean satisfiability (SAT) and its extensions are becoming a core technology for the analysis of systems. The SAT-based approach divides into three steps: encoding, preprocessing, and search. It is often argued that by encoding arbitrary Boolean formulas in conjunctive normal form (CNF), structural properties of the original problem are not reflected in the CNF. This should result in the fact that CNF-level preprocessing and SAT solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural SAT instance representations such as Boolean circuits. In this work we study the effect of a CNF-level simplification technique called blocked clause elimination (BCE). We show that BCE is surprisingly effective both in theory and in practice on CNFs resulting from a standard CNF encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circui...

• Type: Conference
• Year: 2010
• Where: TACAS
• Authors: Matti Järvisalo, Armin Biere, Marijn Heule
• Keywords: Algorithms, Arbitrary Boolean Formulas, Cnf Encodings, Structural Sat Instance, TACAS 2010