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 (20)

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

This page was built for publication: Clause Elimination Procedures for CNF Formulas