On the Resiliency of Unit Propagation to Max-Resolution

Abstract

At each node of the search tree, Branch and Bound solvers for Max-SAT compute the lower bound (LB) by estimating the number of disjoint inconsistent subsets (IS) of the formula. IS are detected thanks to unit propagation (UP) then transformed by max-resolution to ensure that they are counted only once. However, it has been observed experimentally that the max-resolution transformations impact the capability of UP to detect further IS. Consequently, few transformations are learned and the LB computation is redundant. In this paper, we study the effect of the transformations on the UP mechanism. We introduce the notion of UP-resiliency of a transformation, which quantifies its impact on UP. It provides, from a theoretical point of view, an explanation to the empirical efficiency of the learning scheme developed in the last ten years. The experimental results we present give evidences of UP-resiliency relevance and insights on the behavior of the learning mechanism.