Non-clausal redundancy properties
From MaRDI portal
Publication:2055860
DOI10.1007/978-3-030-79876-5_15OpenAlexW3179612605MaRDI QIDQ2055860
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_15
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computer-aided proof of Erdős discrepancy properties
- The complexity of facets (and some facets of complexity)
- A two-phase algorithm for solving a class of hard satisfiability problems
- Reduction of OBDDs in linear time
- The complexity of the pigeonhole principle
- Generalized resolution for 0--1 linear inequalities
- Size of ordered binary decision diagrams representing threshold functions
- Binary decision diagrams for first-order predicate logic.
- On a generalization of extended resolution
- Generating extended resolution proofs with a BDD-based SAT solver
- Non-clausal redundancy properties
- Covered clauses are not propagation redundant
- DRAT proofs, propagation redundancy, and extended resolution
- Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling
- Strong extension-free proof systems
- Short proofs without new variables
- Sorting parity encodings by reusing variables
- Super-Blocked Clauses
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- DRAT Proofs for XOR Reasoning
- Inprocessing Rules
- AVATAR: The Architecture for First-Order Theorem Provers
- Clause Elimination for SAT and QSAT
- A New Look at BDDs for Pseudo-Boolean Constraints
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Extended Resolution Proofs for Conjoining BDDs
- Blocked Clause Elimination
- Graph-Based Algorithms for Boolean Function Manipulation
- Hard examples for resolution
- Binary Decision Diagrams
- The Complexity of Propositional Proofs
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Bounded model checking using satisfiability solving
This page was built for publication: Non-clausal redundancy properties
