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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SATsolvers often contain redundant literals. This may have a negative impact onperformance because redundant literals may deteriorate both the effectivenessof Boolean constraint propagation and the quality of subsequent learnt clauses.To overcome this drawback, we propose a clause vivification approach thateliminates redundant literals by applying unit propagation. The proposed clausevivification is activated before the SAT solver triggers some selectedrestarts, and only affects a subset of original and learnt clauses, which areconsidered to be more relevant according to metrics like the literal blockdistance (LBD). Moreover, we conducted an empirical investigation withinstances coming from the hard combinatorial and application categories ofrecent SAT competitions. The results show that a remarkable number ofadditional instances are solved when the proposed approach is incorporated intofive of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS,MapleCOMSPS and MapleCOMSPS_LRB). More importantly, the empirical investigationincludes an in-depth analysis of the effectiveness of clause vivification. Itis worth mentioning that one of the SAT solvers described here was ranked firstin the main track of SAT Competition 2017 thanks to the incorporation of theproposed clause vivification. That solver was further improved in this paperand won the bronze medal in the main track of SAT Competition 2018.

Clause Vivification by Unit Propagation in CDCL SAT Solvers