English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In this paper we analyze three well-known preprocessors for Max-SAT. The first preprocessor is based on the so-called variable saturation. The second preprocessor is based on the resolution mechanism incorporated in modern branch and bound solvers. The third preprocessor is specific for the Maximum Clique problem and other problems with similar encoding in WCNF such as minimum vertex covering and combinatorial auctions. Our experimental investigation is divided in two parts. In the first part, we study the effect of the preprocessors on several problem instances using different metrics. In the second part, the effect of each preprocessor is analyzed in some of the most relevant Max-SAT local search algorithms of the literature including Gsat, Walksat, Adaptnovelty+, Irots and Saps. Results indicate that some of these algorithms find much better solutions after the preprocessor. Furthermore, some preprocessed instances can be solved to optimality with local search under very specific conditions.

The Impact of Max-SAT Resolution-Based Preprocessors on Local Search Solvers