Super-Blocked Clauses
From MaRDI portal
Publication:2817910
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
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
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