Efficient Reasoning about Data Trees via Integer Linear Programming

Abstract : Data trees provide a standard abstraction of XML documents with data values: they are trees whose nodes, in addition to the usual labels, can carry labels from an infinite alphabet (data). Therefore, one is interested in decidable formalisms for reasoning about data trees. While some are known -- such as the two-variable logic -- they tend to be of very high complexity, and most decidability proofs are highly nontrivial. We are therefore interested in reasonable complexity formalisms as well as better techniques for proving decidability. Here we show that many decidable formalisms for data trees are subsumed -- fully or partially -- by the power of tree automata together with set constraints and linear constraints on cardinalities of various sets of data values. All these constraints can be translated into instances of integer linear programming, giving us an \np\ upper bound on the complexity of the reasoning tasks. We prove that this bound, as well as the key encoding technique, remain very robust, and allow the addition of features such as counting of paths and patterns, and even a concise encoding of constraints, without increasing the complexity. The NP bound is tight, as we also show that the satisfiability of a single set constraint is already \np-hard. We then relate our results to several reasoning tasks over XML documents, such as satisfiability of schemas and data dependencies and satisfiability of the two-variable logic. As a final contribution, we describe experimental results based on the implementation of some reasoning tasks using the SMT solver Z3.
Document type :
Journal articles
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-00835833
Contributor : Claire David <>
Submitted on : Wednesday, June 19, 2013 - 6:52:54 PM
Last modification on : Thursday, March 14, 2019 - 9:58:07 AM
Long-term archiving on : Friday, September 20, 2013 - 4:08:19 AM

File

edt-tods.pdf
Files produced by the author(s)

Identifiers

Citation

Claire David, Leonid Libkin, Tony Tan. Efficient Reasoning about Data Trees via Integer Linear Programming. ACM Transactions on Database Systems, Association for Computing Machinery, 2012, 37 (3), pp.19.1-19.28. ⟨10.1145/2338626.2338632⟩. ⟨hal-00835833⟩

Share

Metrics

Record views

558

Files downloads

229