# Clause Vivification by Unit Propagation in CDCL SAT Solvers

arXiv: https://arxiv.org/abs/1807.11061 · HTML: https://mlsanity.com/paper/1807.11061/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Jul 2018.

## Built on by (most cited first, 6 of 6)

- [Autonomous Code Evolution Meets NP-Completeness](https://mlsanity.com/paper/2509.07367/) (2025)
- [Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers](https://mlsanity.com/paper/2401.10589/) (2024)
- [Branching Strategy Selection Approach Based on Vivification Ratio](https://mlsanity.com/paper/2112.06917/) (2021)
- [A novel framework for systematic propositional formula simplification based on existential graphs](https://mlsanity.com/paper/2405.17072/) (2024)
- [Integer Linear Programming Preprocessing for Maximum Satisfiability](https://mlsanity.com/paper/2506.06216/) (2025)
- [Learning Lookahead Lemmas for Neural Network Verification](https://mlsanity.com/paper/2607.29051/) (2026)

## Abstract (arXiv)

Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt clauses. To overcome this drawback, we propose a clause vivification approach that eliminates redundant literals by applying unit propagation. The proposed clause vivification is activated before the SAT solver triggers some selected restarts, and only affects a subset of original and learnt clauses, which are considered to be more relevant according to metrics like the literal block distance (LBD). Moreover, we conducted an empirical investigation with instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a remarkable number of additional instances are solved when the proposed approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS_LRB). More importantly, the empirical investigation includes an in-depth analysis of the effectiveness of clause vivification. It is worth mentioning that one of the SAT solvers described here was ranked first in the main track of SAT Competition 2017 thanks to the incorporation of the proposed clause vivification. That solver was further improved in this paper and won the bronze medal in the main track of SAT Competition 2018.