TY - GEN
T1 - SAT vs. search for qualitative temporal reasoning
AU - Huang, Jinbo
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84878776729&partnerID=8YFLogxK
U2 - 10.3233/978-1-61499-098-7-426
DO - 10.3233/978-1-61499-098-7-426
M3 - Conference contribution
AN - SCOPUS:84878776729
SN - 9781614990970
T3 - Frontiers in Artificial Intelligence and Applications
SP - 426
EP - 431
BT - ECAI 2012 - 20th European Conference on Artificial Intelligence, 27-31 August 2012, Montpellier, France - Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstration
PB - IOS Press BV
T2 - 20th European Conference on Artificial Intelligence, ECAI 2012
Y2 - 27 August 2012 through 31 August 2012
ER -