An average case analysis of Monien and Speckenmeyer's mechanical theorem proving algorithm View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

1991

AUTHORS

T. H. Hu , C. Y. Tang , R. C. T. Lee

ABSTRACT

In this paper, we shall give an average case analysis of a mechanical theorem proving algorithm based upon branching techniques for solving the k-satisfiability problem. The branching algorithm is a modified version of Monien and Speckenmeyer's branching algorithm [Monien and Speckenmeyer 1985]. Monien and Speckenmeyer's branching algorithm has a worst case time complexity which is strictly better than 2n [Monien and Speckenmeyer 1985]. Based upon the probability distribution model that given r clauses, each clause is randomly chosen from the set of all k-literal clauses over n variables and each clause is chosen independently with others, we can show that our branching algorithm runs in exponential expected time under the condition that \(\mathop {\lim }\limits_{r,n \to \infty } \frac{t}{n} \to \infty\) and k is a constant. More... »

PAGES

116-126

References to SciGraph publications

  • 1992-03. An average case analysis of a resolution principle algorithm in mechanical theorem proving in ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
  • 1972. Reducibility among Combinatorial Problems in COMPLEXITY OF COMPUTER COMPUTATIONS
  • Book

    TITLE

    ISA'91 Algorithms

    ISBN

    978-3-540-54945-1
    978-3-540-46600-0

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/3-540-54945-5_55

    DOI

    http://dx.doi.org/10.1007/3-540-54945-5_55

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1009229570


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Artificial Intelligence and Image Processing", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "National Tsing Hua University", 
              "id": "https://www.grid.ac/institutes/grid.38348.34", 
              "name": [
                "Institute of Computer Science, National Tsing Hua University, 30043\u00a0Hsinchu, Taiwan, Republic of China"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Hu", 
            "givenName": "T. H.", 
            "id": "sg:person.010634245333.21", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010634245333.21"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "National Tsing Hua University", 
              "id": "https://www.grid.ac/institutes/grid.38348.34", 
              "name": [
                "Institute of Computer Science, National Tsing Hua University, 30043\u00a0Hsinchu, Taiwan, Republic of China"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Tang", 
            "givenName": "C. Y.", 
            "id": "sg:person.01312526135.27", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01312526135.27"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "National Tsing Hua University", 
              "id": "https://www.grid.ac/institutes/grid.38348.34", 
              "name": [
                "National Tsing Hua University, 30043\u00a0Hsinchu, Taiwan"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Lee", 
            "givenName": "R. C. T.", 
            "id": "sg:person.07540250215.50", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07540250215.50"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "https://doi.org/10.1016/0020-0190(83)90127-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001872381"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0166-218x(85)90050-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003058545"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0166-218x(85)90050-2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1003058545"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0166-218x(83)90017-3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007285462"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0166-218x(83)90017-3", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007285462"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4684-2001-2_9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007977430", 
              "https://doi.org/10.1007/978-1-4684-2001-2_9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321250.321253", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009195371"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(86)90051-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013779407"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0190(86)90051-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013779407"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01531030", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1017302452", 
              "https://doi.org/10.1007/bf01531030"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/s0004-3702(83)80007-1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027783001"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321033.321034", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1028819080"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321623.321636", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030098975"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0255(87)90003-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037704413"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0020-0255(87)90003-x", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037704413"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0304-3975(77)90054-8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1050551316"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/321607.321618", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051315256"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/800157.805047", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053230526"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1991", 
        "datePublishedReg": "1991-01-01", 
        "description": "In this paper, we shall give an average case analysis of a mechanical theorem proving algorithm based upon branching techniques for solving the k-satisfiability problem. The branching algorithm is a modified version of Monien and Speckenmeyer's branching algorithm [Monien and Speckenmeyer 1985]. Monien and Speckenmeyer's branching algorithm has a worst case time complexity which is strictly better than 2n [Monien and Speckenmeyer 1985]. Based upon the probability distribution model that given r clauses, each clause is randomly chosen from the set of all k-literal clauses over n variables and each clause is chosen independently with others, we can show that our branching algorithm runs in exponential expected time under the condition that \\(\\mathop {\\lim }\\limits_{r,n \\to \\infty } \\frac{t}{n} \\to \\infty\\) and k is a constant.", 
        "editor": [
          {
            "familyName": "Hsu", 
            "givenName": "Wen-Lian", 
            "type": "Person"
          }, 
          {
            "familyName": "Lee", 
            "givenName": "R. C. T.", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/3-540-54945-5_55", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-540-54945-1", 
            "978-3-540-46600-0"
          ], 
          "name": "ISA'91 Algorithms", 
          "type": "Book"
        }, 
        "name": "An average case analysis of Monien and Speckenmeyer's mechanical theorem proving algorithm", 
        "pagination": "116-126", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/3-540-54945-5_55"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "2bf793ef2d1dcfa9aab7c9469144c6456ba1a40c44c3a40aa6225f4fba103e51"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1009229570"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/3-540-54945-5_55", 
          "https://app.dimensions.ai/details/publication/pub.1009229570"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-15T22:40", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8695_00000015.jsonl", 
        "type": "Chapter", 
        "url": "http://link.springer.com/10.1007/3-540-54945-5_55"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/3-540-54945-5_55'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/3-540-54945-5_55'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-54945-5_55'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-54945-5_55'


     

    This table displays all metadata directly associated to this object as RDF triples.

    129 TRIPLES      23 PREDICATES      41 URIs      20 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/3-540-54945-5_55 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 schema:author Ndfe4907bb1f54cd5aeb0f4b3cca0c3df
    4 schema:citation sg:pub.10.1007/978-1-4684-2001-2_9
    5 sg:pub.10.1007/bf01531030
    6 https://doi.org/10.1016/0020-0190(83)90127-8
    7 https://doi.org/10.1016/0020-0190(86)90051-7
    8 https://doi.org/10.1016/0020-0255(87)90003-x
    9 https://doi.org/10.1016/0166-218x(83)90017-3
    10 https://doi.org/10.1016/0166-218x(85)90050-2
    11 https://doi.org/10.1016/0304-3975(77)90054-8
    12 https://doi.org/10.1016/s0004-3702(83)80007-1
    13 https://doi.org/10.1145/321033.321034
    14 https://doi.org/10.1145/321250.321253
    15 https://doi.org/10.1145/321607.321618
    16 https://doi.org/10.1145/321623.321636
    17 https://doi.org/10.1145/800157.805047
    18 schema:datePublished 1991
    19 schema:datePublishedReg 1991-01-01
    20 schema:description In this paper, we shall give an average case analysis of a mechanical theorem proving algorithm based upon branching techniques for solving the k-satisfiability problem. The branching algorithm is a modified version of Monien and Speckenmeyer's branching algorithm [Monien and Speckenmeyer 1985]. Monien and Speckenmeyer's branching algorithm has a worst case time complexity which is strictly better than 2n [Monien and Speckenmeyer 1985]. Based upon the probability distribution model that given r clauses, each clause is randomly chosen from the set of all k-literal clauses over n variables and each clause is chosen independently with others, we can show that our branching algorithm runs in exponential expected time under the condition that \(\mathop {\lim }\limits_{r,n \to \infty } \frac{t}{n} \to \infty\) and k is a constant.
    21 schema:editor Nf970aa60dd0a468792c6b3c26530977a
    22 schema:genre chapter
    23 schema:inLanguage en
    24 schema:isAccessibleForFree false
    25 schema:isPartOf N225bad08fc7c464e86537e97ccc06484
    26 schema:name An average case analysis of Monien and Speckenmeyer's mechanical theorem proving algorithm
    27 schema:pagination 116-126
    28 schema:productId N5084b7a389da40df9737a84be723c0e5
    29 N805fb8f60bb54b059c34c4b1bf2892fe
    30 Ndefd018e8a6748c5923afd47f2fcf060
    31 schema:publisher N7fa44c3c773942f4a1197ce02f51416a
    32 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009229570
    33 https://doi.org/10.1007/3-540-54945-5_55
    34 schema:sdDatePublished 2019-04-15T22:40
    35 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    36 schema:sdPublisher N81f640550d7043d39828caf5723ec95c
    37 schema:url http://link.springer.com/10.1007/3-540-54945-5_55
    38 sgo:license sg:explorer/license/
    39 sgo:sdDataset chapters
    40 rdf:type schema:Chapter
    41 N225bad08fc7c464e86537e97ccc06484 schema:isbn 978-3-540-46600-0
    42 978-3-540-54945-1
    43 schema:name ISA'91 Algorithms
    44 rdf:type schema:Book
    45 N478c84bb780a453a9e276fc318b4075b rdf:first Nc17904e12d694e08ab24b87d4a0f55fa
    46 rdf:rest rdf:nil
    47 N5084b7a389da40df9737a84be723c0e5 schema:name dimensions_id
    48 schema:value pub.1009229570
    49 rdf:type schema:PropertyValue
    50 N7fa44c3c773942f4a1197ce02f51416a schema:location Berlin, Heidelberg
    51 schema:name Springer Berlin Heidelberg
    52 rdf:type schema:Organisation
    53 N805fb8f60bb54b059c34c4b1bf2892fe schema:name doi
    54 schema:value 10.1007/3-540-54945-5_55
    55 rdf:type schema:PropertyValue
    56 N81f640550d7043d39828caf5723ec95c schema:name Springer Nature - SN SciGraph project
    57 rdf:type schema:Organization
    58 N89770535cd6b4adbb0cefff000d1e5b2 rdf:first sg:person.01312526135.27
    59 rdf:rest N8f1eae9b8534446bb46847ed402ec916
    60 N8f1eae9b8534446bb46847ed402ec916 rdf:first sg:person.07540250215.50
    61 rdf:rest rdf:nil
    62 Nb0f0c9e4f6f049e5b690dbcfc5a4e100 schema:familyName Hsu
    63 schema:givenName Wen-Lian
    64 rdf:type schema:Person
    65 Nc17904e12d694e08ab24b87d4a0f55fa schema:familyName Lee
    66 schema:givenName R. C. T.
    67 rdf:type schema:Person
    68 Ndefd018e8a6748c5923afd47f2fcf060 schema:name readcube_id
    69 schema:value 2bf793ef2d1dcfa9aab7c9469144c6456ba1a40c44c3a40aa6225f4fba103e51
    70 rdf:type schema:PropertyValue
    71 Ndfe4907bb1f54cd5aeb0f4b3cca0c3df rdf:first sg:person.010634245333.21
    72 rdf:rest N89770535cd6b4adbb0cefff000d1e5b2
    73 Nf970aa60dd0a468792c6b3c26530977a rdf:first Nb0f0c9e4f6f049e5b690dbcfc5a4e100
    74 rdf:rest N478c84bb780a453a9e276fc318b4075b
    75 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    76 schema:name Information and Computing Sciences
    77 rdf:type schema:DefinedTerm
    78 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    79 schema:name Artificial Intelligence and Image Processing
    80 rdf:type schema:DefinedTerm
    81 sg:person.010634245333.21 schema:affiliation https://www.grid.ac/institutes/grid.38348.34
    82 schema:familyName Hu
    83 schema:givenName T. H.
    84 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010634245333.21
    85 rdf:type schema:Person
    86 sg:person.01312526135.27 schema:affiliation https://www.grid.ac/institutes/grid.38348.34
    87 schema:familyName Tang
    88 schema:givenName C. Y.
    89 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01312526135.27
    90 rdf:type schema:Person
    91 sg:person.07540250215.50 schema:affiliation https://www.grid.ac/institutes/grid.38348.34
    92 schema:familyName Lee
    93 schema:givenName R. C. T.
    94 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07540250215.50
    95 rdf:type schema:Person
    96 sg:pub.10.1007/978-1-4684-2001-2_9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007977430
    97 https://doi.org/10.1007/978-1-4684-2001-2_9
    98 rdf:type schema:CreativeWork
    99 sg:pub.10.1007/bf01531030 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017302452
    100 https://doi.org/10.1007/bf01531030
    101 rdf:type schema:CreativeWork
    102 https://doi.org/10.1016/0020-0190(83)90127-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001872381
    103 rdf:type schema:CreativeWork
    104 https://doi.org/10.1016/0020-0190(86)90051-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013779407
    105 rdf:type schema:CreativeWork
    106 https://doi.org/10.1016/0020-0255(87)90003-x schema:sameAs https://app.dimensions.ai/details/publication/pub.1037704413
    107 rdf:type schema:CreativeWork
    108 https://doi.org/10.1016/0166-218x(83)90017-3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007285462
    109 rdf:type schema:CreativeWork
    110 https://doi.org/10.1016/0166-218x(85)90050-2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003058545
    111 rdf:type schema:CreativeWork
    112 https://doi.org/10.1016/0304-3975(77)90054-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050551316
    113 rdf:type schema:CreativeWork
    114 https://doi.org/10.1016/s0004-3702(83)80007-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027783001
    115 rdf:type schema:CreativeWork
    116 https://doi.org/10.1145/321033.321034 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028819080
    117 rdf:type schema:CreativeWork
    118 https://doi.org/10.1145/321250.321253 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009195371
    119 rdf:type schema:CreativeWork
    120 https://doi.org/10.1145/321607.321618 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051315256
    121 rdf:type schema:CreativeWork
    122 https://doi.org/10.1145/321623.321636 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030098975
    123 rdf:type schema:CreativeWork
    124 https://doi.org/10.1145/800157.805047 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053230526
    125 rdf:type schema:CreativeWork
    126 https://www.grid.ac/institutes/grid.38348.34 schema:alternateName National Tsing Hua University
    127 schema:name Institute of Computer Science, National Tsing Hua University, 30043 Hsinchu, Taiwan, Republic of China
    128 National Tsing Hua University, 30043 Hsinchu, Taiwan
    129 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...