Understanding the power of Max-SAT resolution through UP-resilience

摘要

A typical Branch and Bound algorithm for Max-SAT computes the lower bound by estimating the number of disjoint Inconsistent Subsets (IS) of the formula. The IS detection is ensured by Simulated Unit Propagation (SUP). Then, the inference rule for Max-SAT, Max-SAT resolution, is applied to ensure that the detected IS is counted only once. Learning Max-SAT resolution transformations can be detrimental to the algorithm performance, so they are usually selectively learned if they match certain patterns. In this paper, we study the impact of the transformations by Max-SAT resolution on the SUP mechanism, indispensable for IS detection. We introduce the notion of UP-resilience of a transformation which quantifies this impact and provides, from a theoretical point of view, an explanation to the empirical efficiency of the learning schemes developed in the last ten years. We also focus on recently introduced patterns called Unit Clause Subsets (UCSs). We characterize the transformations of certain UCSs using UP-resilience and we explain how our result can help extend the current patterns. Finally, we present empirical observations that support the relevance of the UP-resilience property and further consolidate our theoretical results.