Clausal proofs for pseudo-Boolean reasoning
From MaRDI portal
Publication:6535573
DOI10.1007/978-3-030-99524-9_25zbMath1547.68704MaRDI QIDQ6535573
Armin Biere, Marijn J. H. Heule, Randal E. Bryant
Publication date: 23 January 2024
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 (1)
Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The intractability of resolution
- Explicit constructions of linear-sized superconcentrators
- Fourier-Motzkin elimination extension to integer programming problems
- Size of ordered binary decision diagrams representing threshold functions
- Equivalent literal propagation in the DLL procedure
- Mutilated chessboard problem is exponentially hard for resolution
- Bucket elimination: A unifying framework for reasoning
- Generating extended resolution proofs with a BDD-based SAT solver
- Non-clausal redundancy properties
- Efficient certified RAT verification
- Sorting parity encodings by reusing variables
- Inprocessing Rules
- Extending Clause Learning DPLL with Parity Reasoning
- A New Look at BDDs for Pseudo-Boolean Constraints
- Detecting Cardinality Constraints in CNF
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Outline of an algorithm for integer solutions to linear programs
- Extended Resolution Proofs for Conjoining BDDs
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Graph-Based Algorithms for Boolean Function Manipulation
- A Comparison of Sparsity Orderings for Obtaining a Pivotal Sequence in Gaussian Elimination
- The Complexity of Propositional Proofs
- Verifying Refutations with Extended Resolution
- A Machine-Oriented Logic Based on the Resolution Principle
- Sylvester's Identity and Multistep Integer-Preserving Gaussian Elimination
- Extended Resolution Proofs for Symbolic SAT Solving with Quantification
This page was built for publication: Clausal proofs for pseudo-Boolean reasoning
