Clause vivification by unit propagation in CDCL SAT solvers
From MaRDI portal
(Redirected from Publication:2287199)
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 2080337 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- Concurrent clause strengthening
- Efficient CNF simplification based on binary implication graphs
- GRASP: a search algorithm for propositional satisfiability
- Incremental inprocessing in SAT solving
- Inprocessing rules
- Learning rate based branching heuristic for SAT solvers
- Solving propositional satisfiability problems
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
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
- Simplifying CDCL clause database reduction
- Encoding Redundancy for Satisfaction-Driven Clause Learning
- Between SAT and UNSAT: the fundamental difference in CDCL SAT
- SAT competition 2020
Describes a project that uses
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)
