Blocked Clause Elimination
From MaRDI portal
Publication:3557074
DOI10.1007/978-3-642-12002-2_10zbMath1284.03208OpenAlexW1656268799MaRDI QIDQ3557074
Armin Biere, Marijn J. H. Heule, Matti Järvisalo
Publication date: 27 April 2010
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-12002-2_10
Related Items
On preprocessing techniques and their impact on propositional model counting, Solution validation and extraction for QBF preprocessing, Preprocessing for DQBF, Recognition of Nested Gates in CNF Formulas, Exploiting Resolution-Based Representations for MaxSAT Solving, Expressing Symmetry Breaking in DRAT Proofs, A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis, SAT race 2015, Simulating circuit-level simplifications on CNF, Craig interpolation with clausal first-order tableaux, Symmetry in Gardens of Eden, Contradiction separation based dynamic multi-clause synergized automated deduction, An Expressive Model for Instance Decomposition Based Parallel SAT Solvers, Simulating strong practical proof systems with extended resolution, Truth Assignments as Conditional Autarkies, On Freezing and Reactivating Learnt Clauses, Efficient CNF Simplification Based on Binary Implication Graphs, The configurable SAT solver challenge (CSSC), Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability, Multi-threaded ASP solving with clasp, Unnamed Item, Blocked Clause Elimination for QBF, Variable and clause elimination for LTL satisfiability checking, Super-Blocked Clauses, On the Hardness of SAT with Community Structure, Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Non-clausal redundancy properties, Formally verifying the solution to the Boolean Pythagorean triples problem, Set-blocked clause and extended set-blocked clause in first-order logic, Covered clauses are not propagation redundant, A comprehensive framework for saturation theorem proving, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, SAT-Inspired Eliminations for Superposition
