Non-clausal redundancy properties
type: Item
instance of: scholarly article
title: Non-clausal redundancy properties
DOI: 10.1007/978-3-030-79876-5_15
author: Lee A. Barnett
author: Armin Biere
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437083
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 15
OpenAlex ID: W3179612605
cites work: A New Look at BDDs for Pseudo-Boolean Constraints
cites work: The complexity of the pigeonhole principle
cites work: Binary Decision Diagrams
cites work: Covered clauses are not propagation redundant
cites work: Q5715680
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Generating extended resolution proofs with a BDD-based SAT solver
cites work: DRAT proofs, propagation redundancy, and extended resolution
cites work: Sorting parity encodings by reusing variables
cites work: Bounded model checking using satisfiability solving
cites work: Q4037371
cites work: Theory and Applications of Satisfiability Testing
cites work: Binary decision diagrams for first-order predicate logic.
cites work: Q5219922
cites work: Clause Elimination for SAT and QSAT
cites work: Short proofs without new variables
cites work: Strong extension-free proof systems
cites work: Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
cites work: Generalized resolution for 0--1 linear inequalities
cites work: Size of ordered binary decision diagrams representing threshold functions
cites work: Blocked Clause Elimination
cites work: Inprocessing Rules
cites work: Super-Blocked Clauses
cites work: Computer-aided proof of Erdős discrepancy properties
cites work: On a generalization of extended resolution
cites work: Q5628016
cites work: Q4707784
cites work: The complexity of facets (and some facets of complexity)
cites work: DRAT Proofs for XOR Reasoning
cites work: Q4261069
cites work: Reduction of OBDDs in linear time
cites work: Extended Resolution Proofs for Conjoining BDDs
cites work: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling
cites work: Q5604434
cites work: Hard examples for resolution
cites work: The Complexity of Propositional Proofs
cites work: AVATAR: The Architecture for First-Order Theorem Provers
cites work: A two-phase algorithm for solving a class of hard satisfiability problems
cites work: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
description: scientific article; zbMATH DE number 7437083