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

Conflict-driven clause learning (CDCL) is a remarkably successful paradigmfor solving the satisfiability problem of propositional logic. Instead of asimple depth-first backtracking approach, this kind of solver learns the reasonbehind occurring conflicts in the form of additional clauses. However, despitethe enormous success of CDCL solvers, there is still only a limitedunderstanding of what influences the performance of these solvers in what way.  Considering different measures, this paper demonstrates, quite surprisingly,that clause learning (without being able to get rid of some clauses) can notonly help the solver but can oftentimes deteriorate the solution processdramatically. By conducting extensive empirical analysis, we furthermore findthat the runtime distributions of CDCL solvers are multimodal. Thismultimodality can be seen as a reason for the deterioration phenomenondescribed above. Simultaneously, it also gives an indication of why clauselearning in combination with clause deletion is virtually the de facto standardof SAT solving, in spite of this phenomenon. As a final contribution, we showthat Weibull mixture distributions can accurately describe the multimodaldistributions. Thus, adding new clauses to a base instance has an inherenteffect of making runtimes long-tailed. This insight provides an explanation asto why the technique of forgetting clauses is useful in CDCL solvers apart fromthe optimization of unit propagation speed.

Too much information: why CDCL solvers need to forget learned clauses