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/

Zendy Plus

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

Zendy Tools

Zendy Open

Current implementations of pseudo-Boolean (PB) solvers working on native PBconstraints are based on the CDCL architecture which empowers highly efficientmodern SAT solvers. In particular, such PB solvers not only implement a(cutting-planes-based) conflict analysis procedure, but also complementarystrategies for components that are crucial for the efficiency of CDCL, namelybranching heuristics, learned constraint deletion and restarts. However, thesestrategies are mostly reused by PB solvers without considering the particularform of the PB constraints they deal with. In this paper, we present andevaluate different ways of adapting CDCL strategies to take the specificitiesof PB constraints into account while preserving the behavior they have in theclausal setting. We implemented these strategies in two different solvers,namely Sat4j (for which we consider three configurations) and RoundingSat. Ourexperiments show that these dedicated strategies allow to improve, sometimessignificantly, the performance of these solvers, both on decision andoptimization problems.

On Dedicated CDCL Strategies for PB Solvers