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 Δ by a set of formulas Γ delivers one maximum cardinality subset of Δ from which no formula of Γ can be deduced. Equivalently, multiple contraction can be defined as the extraction of one maximum cardinality subset of Δ 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 Γ and one call to Partial-Max-SAT. On the contrary, in the worst case, a direct approach requires us to compute for each formula γ in Γ all inclusion-maximal subsets of Δ that do not entail γ. 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.