资源On the Resiliency of Unit Propagation to Max-Resolution Andre? Abrame? and Djamal Habet

On the Resiliency of Unit Propagation to Max-Resolution Andre? Abrame? and Djamal Habet

2019-11-18 | |  33 |   1 |   0
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 UPresiliency 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.

上一篇:Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT Jeremias Berg and Paul Saikko and Matti Ja?rvisalo

下一篇:Exploiting the Structure of Unsatisfiable Cores in MaxSAT? Carlos Anso?tegui Frederic Didier Joel Gaba?s

用户评价
全部评价

热门资源

  • Multi-Source Cros...

    Modern NLP applications have enjoyed a great bo...

  • Reference Network...

    Neural Machine Translation (NMT) has achieved n...

  • Soft Contextual D...

    While data augmentation is an important trick t...

  • Style Transformer...

    Disentangling the content and style in the lat...

  • Towards Fine-grai...

    In this paper, we focus on the task of finegra...