Super-Blocked Clauses

DOI10.1007/978-3-319-40229-1_5zbMath1475.68347OpenAlexW2478003478MaRDI QIDQ2817910

Armin Biere, Martina Seidl, Hans Tompits, Benjamin Kiesl

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3044

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Truth Assignments as Conditional Autarkies ⋮ Unnamed Item ⋮ Strong extension-free proof systems ⋮ Non-clausal redundancy properties ⋮ Set-blocked clause and extended set-blocked clause in first-order logic ⋮ Covered clauses are not propagation redundant ⋮ Clause redundancy and preprocessing in maximum satisfiability ⋮ Preprocessing of propagation redundant clauses

Uses Software

• Bloqqer
• Lingeling
• cnf2aig

Cites Work

• Simulating circuit-level simplifications on CNF
• On a generalization of extended resolution
• Blocked Clause Decomposition
• Inprocessing Rules
• Clause Elimination for SAT and QSAT
• Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
• Recognition of Nested Gates in CNF Formulas
• Playing with AVATAR
• Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
• Blocked Clause Elimination
• Verifying Refutations with Extended Resolution
• Soundness of Inprocessing in Clause Sharing SAT Solvers

This page was built for publication: Super-Blocked Clauses