Producing and verifying extremely large propositional refutations
type: Item
instance of: scholarly article
title: Producing and verifying extremely large propositional refutations
zbMATH Open document ID: 1273.68329
published in: Annals of Mathematics and Artificial Intelligence
publication date: 2012-12-12T00:00:00Z
review text: Most high-performance satisfiability solvers and special-theory decision procedures are unable to provide a proof of unsatisfiability. Since bugs have been discovered in many such programs long after being put into service, an uncheckable decision poses a significant problem if important economic or safety decisions are to be based upon it. The thesis of the paper is that decision procedures can and should be designed to be able to output an easily verifiable certificate (i.e., proof), then that certificate can be verified without addressing the issue of whether the program is bug-free. The standard proposed is that the language of certificates should be recognizable in deterministic log-space. Intuitively, an algorithm to recognize a log-space language may re-read the input as often as desired, but can only write into working storage consisting of a fixed number of registers, each able to store \(O(\log L)\) bits, for inputs of length \(L\). An explicit resolution proof is one of the suitable certificates. A detailed specification for an explicit resolution derivation is called the \%RES format. The author of the paper has developed a verifier for the \%RES format (named checker 3) that is able to handle proofs with lengths in the thousands of gigabytes on certain available computer servers. But the leading solvers develop a conflict graph as the basis for deriving new clauses and use much more compact formats for derivations. This paper provides the in-depth comparison of various formats. One of these compact formats, called \%RUP (reverse unit propagation), states the derived clauses but does not provide any information about how each was derived. This language has little hope for log-space recognition. However, \%RUP is useful as an intermediate format that can be post-processed into the \%RES format for final checking by an independent checker. The question of whether \%RUP proofs can viably be post-processed into an explicit resolution format is discussed in d…
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6115332
zbMATH Keywords: propositional satisfiability
zbMATH Keywords: resolution refutations
zbMATH Keywords: space complexity
zbMATH Keywords: pseudo-unit propagation
author: Allen Van Gelder
reviewed by: Nail Zamov
describes a project that uses: BerkMin
describes a project that uses: tts
describes a project that uses: Chaff
describes a project that uses: EVC
describes a project that uses: PicoSAT
MaRDI profile type: Publication
full work available at URL: s10472-012-9322-x
OpenAlex ID: W60439658
cites work: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
cites work: A Generalized Framework for Conflict Analysis
cites work: Q2723410
cites work: Q5715680
cites work: Q3604000
cites work: An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
cites work: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
cites work: Q4485829
cites work: An observation on time-storage trade off
cites work: BerkMin: A fast and robust SAT-solver
cites work: Q4227581
cites work: Q4488342
cites work: Q4139711
cites work: Simplification by Cooperating Decision Procedures
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Solving SAT and SAT Modulo Theories
cites work: Deciding Combinations of Theories
cites work: Extended Resolution Proofs for Conjoining BDDs
cites work: Q3392273
cites work: Q3604004
cites work: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
cites work: Toward leaner binary-clause reasoning in a satisfiability solver
cites work: Q4553255
DOI: 10.1007/S10472-012-9322-X
description: scientific article; zbMATH DE number 6115332