Vivifying Propositional Clausal Formulae

Abstract. In this paper, we present a new way to preprocess Boolean formulae in Conjunctive Normal Form (CNF). In contrast to most of the current pre-processing techniques, our approach aims at improving the filtering power of the original clauses while producing a small number of additional and relevant clauses. More precisely, an incomplete redundancy check is performed on each original clauses through unit propagation, leading to either a sub-clause or to a new relevant one generated by the clause learning scheme. This preprocessor is empirically compared to the best existing one in terms of size reduction and the ability to improve a state-of-the-art satisfiability solver.

• Type: Conference
• Year: 2008
• Where: ECAI
• Authors: Cédric Piette, Youssef Hamadi, Lakhdar Sais
• Keywords: Artificial Intelligence, Conjunctive Normal Form, Current Pre-processing Techniques, ECAI 2008, Original Clauses