Clause elimination procedures for CNF formulas

DOI10.1007/978-3-642-16242-8_26MaRDI QIDQ4933317zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Clause elimination for SAT and QSAT
• Efficient CNF simplification based on binary implication graphs
• Theory and Applications of Satisfiability Testing
• Simulating circuit-level simplifications on CNF
• Blocked clause elimination

Cited in

(31)

• Equivalent literal propagation in the DLL procedure
• Covered clauses are not propagation redundant
• Vampire getting noisy: Will random bits help conquer chaos? (system description)
• Hash-based preprocessing and inprocessing techniques in SAT solvers
• Definability for model counting
• Set-blocked clause and extended set-blocked clause in first-order logic
• On preprocessing techniques and their impact on propositional model counting
• Solution validation and extraction for QBF preprocessing
• A unifying principle for clause elimination in first-order logic
• What we can learn from conflicts in propositional satisfiability
• Synthesis of domain specific CNF encoders for bit-vector solvers
• Clause elimination for SAT and QSAT
• Efficient CNF simplification based on binary implication graphs
• Truth assignments as conditional autarkies
• Preprocessing for DQBF
• Simulating circuit-level simplifications on CNF
• Eliminating Redundant Clauses in SAT Instances
• Learning from conflicts in propositional satisfiability
• Projection and scope-determined circumscription
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability
• scientific article; zbMATH DE number 7267155 (Why is no real title available?)
• Blocked clause elimination for QBF
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• SAT-Inspired Eliminations for Superposition
• Mining definitions in Kissat with Kittens
• On Incremental Pre-processing for SMT
• Certified SAT solving with GPU accelerated inprocessing
• The complexity of pure literal elimination

Describes a project that uses

Uses Software

• NiVER

This page was built for publication: Clause elimination procedures for CNF formulas

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