Producing and verifying extremely large propositional refutations

DOI10.1007/S10472-012-9322-XzbMATH Open1273.68329OpenAlexW60439658MaRDI QIDQ694550FDOQ694550

Authors: Allen Van Gelder 

Publication date: 12 December 2012

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-012-9322-x

Recommendations

• Verifying Refutations with Extended Resolution
• Efficient verified (UN)SAT certificate checking
• Mechanical verification of SAT refutations with extended resolution
• Efficient verified (UN)SAT certificate checking
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

zbMATH Keywords

space complexitypropositional satisfiabilitypseudo-unit propagationresolution refutations

Mathematics Subject Classification ID

Cites Work

• BerkMin: A fast and robust SAT-solver
• Title not available (Why is that?)
• tts: a SAT-solver for small, difficult instances
• Title not available (Why is that?)
• Title not available (Why is that?)
• Simplification by Cooperating Decision Procedures
• Title not available (Why is that?)
• Title not available (Why is that?)
• An observation on time-storage trade off
• Solving SAT and SAT Modulo Theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fast Decision Procedures Based on Congruence Closure
• Toward leaner binary-clause reasoning in a satisfiability solver
• An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• A Generalized Framework for Conflict Analysis
• Deciding Combinations of Theories
• Extended Resolution Proofs for Conjoining BDDs
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic

Cited In (7)

• Simulating strong practical proof systems with extended resolution
• Functional Encryption for Inner Product with Full Function Privacy
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Verifying Refutations with Extended Resolution
• Strong extension-free proof systems
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
• A semantic framework for proof evidence

Uses Software

• tts
• Chaff
• BerkMin
• PicoSAT
• EVC

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)