Efficient CNF simplification based on binary implication graphs

DOI10.1007/978-3-642-21581-0_17MaRDI QIDQ3007684zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Clause elimination procedures for CNF formulas
• Theory and Applications of Satisfiability Testing
• Simulating circuit-level simplifications on CNF
• Conditional lower bounds for failed literals and related techniques
• Clause elimination for SAT and QSAT

Cites work

• scientific article; zbMATH DE number 2080337 (Why is no real title available?)
• Blocked clause elimination
• Clause elimination procedures for CNF formulas
• Depth-First Search and Linear Graph Algorithms
• Simplifying binary propositional theories into connected components twice as fast
• The Transitive Reduction of a Directed Graph
• The propositional formula checker HeerHugo
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Toward leaner binary-clause reasoning in a satisfiability solver
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Cited in

(22)

• Local redundancy in SAT: generalizations of blocked clauses
• SAT-Inspired Higher-Order Eliminations
• On preprocessing techniques and their impact on propositional model counting
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Finding kernels or solving SAT
• Learning from conflicts in propositional satisfiability
• Theory and Applications of Satisfiability Testing
• What we can learn from conflicts in propositional satisfiability
• Optimal implementation of watched literals and more general techniques
• An expressive model for instance decomposition based parallel SAT solvers
• Sometimes hoarding is harder than cleaning: NP-hardness of maximum blocked-clause addition
• Simplifying binary propositional theories into connected components twice as fast
• Conditional lower bounds for failed literals and related techniques
• Clause elimination procedures for CNF formulas
• Definability for model counting
• Simulating circuit-level simplifications on CNF
• Preprocessing for DQBF
• Clause vivification by unit propagation in CDCL SAT solvers
• The configurable SAT solver challenge (CSSC)
• Efficient Generation of Small Interpolants in CNF
• Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability
• SAT-Inspired Eliminations for Superposition

Describes a project that uses

Uses Software

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

This page was built for publication: Efficient CNF simplification based on binary implication graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3007684)