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

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

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)

Cites Work

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

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)