Resolution proof compression by splitting (original) (raw)
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 | dbr:Proof_compression dbr:Algorithm dbr:Resolution_(logic) dbc:Proof_theory dbr:Mathematical_logic |
| dbp:wikiPageUsesTemplate | dbt:Reflist |
| dct:subject | dbc:Proof_theory |
| 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 | freebase:Resolution proof compression by splitting wikidata:Resolution proof compression by splitting https://global.dbpedia.org/id/4tipn |
| prov:wasDerivedFrom | wikipedia-en:Resolution_proof_compression_by_splitting?oldid=790774684&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Resolution_proof_compression_by_splitting |
| is dbo:wikiPageWikiLink of | dbr:Proof_compression |
| is foaf:primaryTopic of | wikipedia-en:Resolution_proof_compression_by_splitting |