Clause Elimination Procedures for CNF Formulas

DOI10.1007/978-3-642-16242-8_26zbMath1306.68144OpenAlexW1564470442MaRDI QIDQ4933317

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

Publication date: 12 October 2010

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-16242-8_26

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

On preprocessing techniques and their impact on propositional model counting, Solution validation and extraction for QBF preprocessing, What we can learn from conflicts in propositional satisfiability, Preprocessing for DQBF, Mining definitions in Kissat with Kittens, Learning from conflicts in propositional satisfiability, Projection and scope-determined circumscription, Truth Assignments as Conditional Autarkies, Efficient CNF Simplification Based on Binary Implication Graphs, Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Blocked Clause Elimination for QBF, Definability for model counting, Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers, Set-blocked clause and extended set-blocked clause in first-order logic, Covered clauses are not propagation redundant, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Vampire getting noisy: Will random bits help conquer chaos? (system description), SAT-Inspired Eliminations for Superposition, Hash-based preprocessing and inprocessing techniques in SAT solvers

Uses Software

• NiVER