资源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 | |  41 |   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

用户评价
全部评价

热门资源

  • Unsupervised Pivo...

    Unsupervised neural machine translation (NMT) h...

  • Style Transformer...

    Disentangling the content and style in the lat...

  • Transferable Mult...

    Over-dependence on domain ontology and lack of ...

  • On the Word Align...

    Prior researches suggest that neural machine tr...

  • Soft Contextual D...

    While data augmentation is an important trick t...