About: Resolution proof compression by splitting

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

In mathematical logic, proof compression by splitting is an algorithm that operates as a post-process on resolution proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof". The Splitting algorithm is based on the following observation: Given a proof of unsatisfiability and a variable , it is easy to re-arrange (split) the proof in a proof of and a proof of and the recombination of these two proofs (by an additional resolution step) may result in a proof smaller than the original.

Property Value
dbo:abstract
  • In mathematical logic, proof compression by splitting is an algorithm that operates as a post-process on resolution proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof". The Splitting algorithm is based on the following observation: Given a proof of unsatisfiability and a variable , it is easy to re-arrange (split) the proof in a proof of and a proof of and the recombination of these two proofs (by an additional resolution step) may result in a proof smaller than the original. Note that applying Splitting in a proof using a variable does not invalidates a latter application of the algorithm using a differente variable . Actually, the method proposed by Cotton generates a sequence of proofs , where each proof is the result of applying Splitting to . During the construction of the sequence, if a proof happens to be too large, is set to be the smallest proof in . For achieving a better compression/time ratio, a heuristic for variable selection is desirable. For this purpose, Cotton defines the "additivity" of a resolution step (with antecedents and and resolvent ): Then, for each variable , a score is calculated summing the additivity of all the resolution steps in with pivot together with the number of these resolution steps. Denoting each score calculated this way by , each variable is selected with a probability proportional to its score: To split a proof of unsatisfiability in a proof of and a proof of , Cotton proposes the following: Let denote a literal and denote the resolvent of clauses and where and . Then, define the map on nodes in the resolution dag of : Also, let be the empty clause in . Then, and are obtained by computing and , respectively. (en)
dbo:wikiPageID
  • 35307933 (xsd:integer)
dbo:wikiPageLength
  • 3389 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 790774684 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • In mathematical logic, proof compression by splitting is an algorithm that operates as a post-process on resolution proofs. It was proposed by Scott Cotton in his paper "Two Techniques for Minimizing Resolution Proof". The Splitting algorithm is based on the following observation: Given a proof of unsatisfiability and a variable , it is easy to re-arrange (split) the proof in a proof of and a proof of and the recombination of these two proofs (by an additional resolution step) may result in a proof smaller than the original. (en)
rdfs:label
  • Resolution proof compression by splitting (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License