Vivifying Propositional Clausal Formulae

8 years 4 months ago
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.
Cédric Piette, Youssef Hamadi, Lakhdar Sais
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ECAI
Authors Cédric Piette, Youssef Hamadi, Lakhdar Sais
Comments (0)