SAT vs. search for qualitative temporal reasoning

Jinbo Huang*

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    Empirical data from recent work has indicated that SAT-based solvers can outperform native search-based solvers on certain classes of problems in qualitative temporal reasoning, particularly over the Interval Algebra (IA). The present work shows that, for reasoning with IA, SAT strictly dominates search in theoretical power: (1) We present a SAT encoding of IA that simulates the use of tractable subsets in native solvers. (2) We show that the refutation of any inconsistent IA network can always be done by SAT (via our new encoding) as efficiently as by native search. (3) We exhibit a class of IA networks that provably require exponential time to refute by native search, but can be refuted by SAT in polynomial time.

    Original languageEnglish
    Title of host publicationECAI 2012 - 20th European Conference on Artificial Intelligence, 27-31 August 2012, Montpellier, France - Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstration
    PublisherIOS Press BV
    Pages426-431
    Number of pages6
    ISBN (Print)9781614990970
    DOIs
    Publication statusPublished - 2012
    Event20th European Conference on Artificial Intelligence, ECAI 2012 - Montpellier, France
    Duration: 27 Aug 201231 Aug 2012

    Publication series

    NameFrontiers in Artificial Intelligence and Applications
    Volume242
    ISSN (Print)0922-6389
    ISSN (Electronic)1879-8314

    Conference

    Conference20th European Conference on Artificial Intelligence, ECAI 2012
    Country/TerritoryFrance
    CityMontpellier
    Period27/08/1231/08/12

    Fingerprint

    Dive into the research topics of 'SAT vs. search for qualitative temporal reasoning'. Together they form a unique fingerprint.

    Cite this