Bloomfilter-Based Practical Kernelization Algorithms for Minimum Satisfiability

Minimum Satisfiability problem (briefly, given a CNF formula, find an assignment satisfying the minimum number of clauses) has raised much attention recently. In the theoretical point of view, Minimum Satisfiability problem is fixed-parameterized, by transforming into Vertex Cover. However, such kind of transformation would be time-consuming, which takes \(O(m^2\cdot n)\) times to transform into Vertex Cover. We first present a \(O(m^2)\) filtering algorithm to transform MinSAT into Vertex cover with low false positive rate, by utilizing Bloom Filter structure. And then, instead of transformation to Vertex Cover, we present a practical kernelization rule directly on the original formula which takes time of \(O(L\cdot d(F))\) , with a kernel size of \(k^2+k\) .