Clausal proofs for pseudo-Boolean reasoning

DOI10.1007/978-3-030-99524-9_25zbMATH Open1547.68704MaRDI QIDQ6535573FDOQ6535573

Authors Randal E. Bryant, Armin Biere, Marijn J. H. Heule

Publication date 23 January 2024

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)

Recommendations

• In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
• Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
• scientific article; zbMATH DE number 5139161
• scientific article; zbMATH DE number 5139167
• scientific article; zbMATH DE number 5139168

Cites work

• scientific article; zbMATH DE number 1614715 (Why is no real title available?)
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 3483795 (Why is no real title available?)
• scientific article; zbMATH DE number 3487716 (Why is no real title available?)
• A Comparison of Sparsity Orderings for Obtaining a Pivotal Sequence in Gaussian Elimination
• A Machine-Oriented Logic Based on the Resolution Principle
• A New Look at BDDs for Pseudo-Boolean Constraints
• Bucket elimination: A unifying framework for reasoning
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Detecting cardinality constraints in CNF
• Efficient certified RAT verification
• Equivalent literal propagation in the DLL procedure
• Explicit constructions of linear-sized superconcentrators
• Extended Resolution Proofs for Conjoining BDDs
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Extending clause learning DPLL with parity reasoning
• Fourier-Motzkin elimination extension to integer programming problems
• Generating extended resolution proofs with a BDD-based SAT solver
• Graph-Based Algorithms for Boolean Function Manipulation
• Inprocessing rules
• Mutilated chessboard problem is exponentially hard for resolution
• Non-clausal redundancy properties
• Outline of an algorithm for integer solutions to linear programs
• Size of ordered binary decision diagrams representing threshold functions
• Sorting parity encodings by reusing variables
• Sylvester's Identity and Multistep Integer-Preserving Gaussian Elimination
• The Complexity of Propositional Proofs
• The intractability of resolution
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Verifying Refutations with Extended Resolution

Cited in

(1)

• Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms

This page was built for publication: Clausal proofs for pseudo-Boolean reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535573)