Mining to Compact CNF Propositional Formulae
This work addresses the challenge of compacting CNF formulae for SAT solvers, which is incremental as it applies existing data mining methods to a new domain.
The authors tackled the problem of reducing the size of propositional formulae in conjunctive normal form (CNF) by applying data mining techniques, specifically frequent itemset mining combined with Tseitin's encoding, and achieved interesting reductions in size for many instances from SAT competitions.
In this paper, we propose a first application of data mining techniques to propositional satisfiability. Our proposed Mining4SAT approach aims to discover and to exploit hidden structural knowledge for reducing the size of propositional formulae in conjunctive normal form (CNF). Mining4SAT combines both frequent itemset mining techniques and Tseitin's encoding for a compact representation of CNF formulae. The experiments of our Mining4SAT approach show interesting reductions of the sizes of many application instances taken from the last SAT competitions.