Efficient CNF Simplification Based on Binary Implication Graphs

DOI10.1007/978-3-642-21581-0_17zbMath1330.68269OpenAlexW54305883MaRDI QIDQ3007684

Marijn J. H. Heule, Matti Järvisalo, Armin Biere

Publication date: 17 June 2011

Published in: Theory and Applications of Satisfiability Testing - SAT 2011 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21581-0_17

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)

Related Items

On preprocessing techniques and their impact on propositional model counting, What we can learn from conflicts in propositional satisfiability, Preprocessing for DQBF, Finding kernels or solving SAT, SAT-Inspired Higher-Order Eliminations, An Expressive Model for Instance Decomposition Based Parallel SAT Solvers, Learning from conflicts in propositional satisfiability, The configurable SAT solver challenge (CSSC), Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability, Unnamed Item, Clause vivification by unit propagation in CDCL SAT solvers, Definability for model counting, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, SAT-Inspired Eliminations for Superposition

Uses Software

• MiniSat
• Plingeling
• PrecoSAT
• HeerHugo
• iProver
• CryptoMiniSat
• Lingeling

Cites Work

• Toward leaner binary-clause reasoning in a satisfiability solver
• The propositional formula checker HeerHugo
• Simplifying Binary Propositional Theories into Connected Components Twice as Fast
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Blocked Clause Elimination
• Clause Elimination Procedures for CNF Formulas
• The Transitive Reduction of a Directed Graph
• Depth-First Search and Linear Graph Algorithms
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Unnamed Item