An Exact Inference Scheme for MinSAT

We describe an exact inference-based algorithm for the MinSAT problem. Given a multiset of clauses phi, the algorithm derives as many empty clauses as the maximum number of clauses that can be falsified in phi by applying finitely many times an inference rule, and returns an optimal assignment. We prove the correctness of the algorithm, describe how it can be extended to deal with weighted MinSAT and weighted partial MinSAT instances, analyze the differences between the MaxSAT and MinSAT inference schemes, and define and empirically evaluate the MinSAT Pure Literal Rule.