Iterative SAT Solving for Minimum Satisfiability

Minimum Satisfiability (MinSAT) denotes one of the optimization versions of the Boolean Satisfiability (SAT) problem. In some settings MinSAT is preferred to using Maximum Satis-fiability (MaxSAT). Several encodings and dedicated branch and bound algorithms for MinSAT have been recently proposed, and evaluated on small challenging randomly generated instances. Motivated by the observation that current best performing MaxSAT algorithms for structured and industrial instances are based on computing unsatisfiable cores with a SAT solver, this paper proposes novel approaches for MinSAT, that also target these instances. First, the paper proposes an algorithm based on iteratively calling a SAT solver which uses the computed models to relax clauses. Second, the paper proposes group-based MinSAT solving, which is essentially a novel reduction of the MinSAT problem into the Group MaxSAT problem. For a given MinSAT instance, the resulting Group MaxSAT formula is then translated into a standard MaxSAT formula which specifically targets unsatisfiability-based MaxSAT algorithms. Experimental results indicate that, similarly to MaxSAT, the proposed approaches outperform branch and bound algorithms on problem instances obtained from practical applications.