Producing and verifying extremely large propositional refutations
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1614688 (Why is no real title available?)
- scientific article; zbMATH DE number 5595151 (Why is no real title available?)
- scientific article; zbMATH DE number 5510691 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1254648 (Why is no real title available?)
- scientific article; zbMATH DE number 1461245 (Why is no real title available?)
- scientific article; zbMATH DE number 1470716 (Why is no real title available?)
- scientific article; zbMATH DE number 1798182 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- A Generalized Framework for Conflict Analysis
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- An improved separation of regular resolution from pool resolution and clause learning
- An observation on time-storage trade off
- BerkMin: A fast and robust SAT-solver
- Deciding Combinations of Theories
- Extended Resolution Proofs for Conjoining BDDs
- Fast Decision Procedures Based on Congruence Closure
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Simplification by Cooperating Decision Procedures
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Toward leaner binary-clause reasoning in a satisfiability solver
- tts: a SAT-solver for small, difficult instances
Cited in
(15)- Functional encryption for inner product with full function privacy
- Compositional propositional proofs
- A flexible proof format for SAT solver-elaborator communication
- Efficient verified (UN)SAT certificate checking
- Mechanical verification of SAT refutations with extended resolution
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Verifying Refutations with Extended Resolution
- Simulating strong practical proof systems with extended resolution
- Strong extension-free proof systems
- Efficient verified (UN)SAT certificate checking
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Proofs and Certificates for Max-SAT
- A semantic framework for proof evidence
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for publication: Producing and verifying extremely large propositional refutations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q694550)
