Clause vivification by unit propagation in CDCL SAT solvers
From MaRDI portal
Publication:2287199
DOI10.1016/J.ARTINT.2019.103197zbMATH Open1478.68325arXiv1807.11061OpenAlexW2989262635WikidataQ126834322 ScholiaQ126834322MaRDI QIDQ2287199FDOQ2287199
Authors: Fan Xiao, Mao Luo, Felip Manya, Zhipeng Lü, Y. Li, Chu-Min Li 
Publication date: 20 January 2020
Published in: Artificial Intelligence (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/1807.11061
Recommendations
Cites Work
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- The complexity of theorem-proving procedures
- Title not available (Why is that?)
- GRASP: a search algorithm for propositional satisfiability
- Inprocessing rules
- Theory and Applications of Satisfiability Testing
- Efficient CNF simplification based on binary implication graphs
- Solving propositional satisfiability problems
- Learning rate based branching heuristic for SAT solvers
- Title not available (Why is that?)
- Incremental inprocessing in SAT solving
- Concurrent clause strengthening
Cited In (10)
- Centrality-based improvements to CDCL heuristics
- On freezing and reactivating learnt clauses
- Automatic generation of dominance breaking nogoods for a class of constraint optimization problems
- Assessing progress in SAT solvers through the Lens of incremental SAT
- Boosting branch-and-bound MaxSAT solvers with clause learning
- Coverage-based clause reduction heuristics for CDCL solvers
- Encoding Redundancy for Satisfaction-Driven Clause Learning
- Simplifying CDCL clause database reduction
- Between SAT and UNSAT: the fundamental difference in CDCL SAT
- SAT competition 2020
Uses Software
This page was built for publication: Clause vivification by unit propagation in CDCL SAT solvers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2287199)
