Clause vivification by unit propagation in CDCL SAT solvers

DOI10.1016/j.artint.2019.103197zbMath1478.68325arXiv1807.11061OpenAlexW2989262635WikidataQ126834322 ScholiaQ126834322MaRDI QIDQ2287199

Mao Luo, Yu Li, Fan Xiao, Felip Manyà, Zhipeng Lü, Chu-Min Li

Publication date: 20 January 2020

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1807.11061

zbMATH Keywords

satisfiabilityconflict-driven clause learningclause vivificationredundant literal

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Automatic generation of dominance breaking nogoods for a class of constraint optimization problems, Boosting branch-and-bound MaxSAT solvers with clause learning, SAT competition 2020, Assessing progress in SAT solvers through the Lens of incremental SAT

Uses Software

• MiniSat
• Chaff
• Plingeling
• PrecoSAT
• Glucose
• CryptoMiniSat
• Treengeling
• COMiniSatPS
• satUZK
• Syrup
• Splatz
• Lingeling
• MapleCOMSPS
• MapleCOMSPS_LRB
• YalSAT
• CaDiCaL
• Maple_LCM_Dist_ChronoBT

Cites Work

• Unnamed Item
• Unnamed Item
• Solving propositional satisfiability problems
• Incremental inprocessing in SAT solving
• Learning Rate Based Branching Heuristic for SAT Solvers
• Inprocessing Rules
• Efficient CNF Simplification Based on Binary Implication Graphs
• GRASP: a search algorithm for propositional satisfiability
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Concurrent Clause Strengthening
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing