Mining to Compact CNF Propositional Formulae

TL;DR

This paper introduces Mining4SAT, a novel approach that applies data mining techniques to discover structural patterns in CNF propositional formulas, leading to significant size reductions.

Contribution

It is the first to combine frequent itemset mining with Tseitin's encoding for compacting CNF formulas in propositional satisfiability.

Findings

Significant size reductions in CNF formulas from SAT competition instances

Effective use of data mining techniques in propositional logic

Potential for improved SAT solving efficiency

Abstract

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.