Multiple Contraction Through Partial-Max-SAT

An original encoding of multiple contraction in Boolean logic through Partial-Max-SAT is proposed. Multiple contraction of a set of clauses Delta by a set of formulas Gamma delivers one maximum cardinality subset of Delta from which no formula of G can be deduced. Equivalently, multiple contraction can be defined as the extraction of one maximum cardinality subset of Delta that is satisfiable together with a given set of formulas. Noticeably, the encoding schema allows multiple contraction to be computed through a number of calls to a SAT solver that is bound by the number of formulas in Gamma and one call to Partial-Max-SAT. On the contrary, in the worst case, a direct approach requires us to compute for each formula gamma in Gamma all inclusion-maximal subsets of Delta that do not entail gamma. Extensive experimental results show that the encoding allows multiple contraction to be computed in a way that is practically viable in many cases and outperforms the direct approach.