{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T02:50:51Z","timestamp":1781059851933,"version":"3.54.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7-ICT-233599"],"award-info":[{"award-number":["FP7-ICT-233599"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["G049165"],"award-info":[{"award-number":["G049165"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Database Syst."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>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\u2014such as the two-variable logic\u2014they 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.<\/jats:p>\n          <jats:p>Here we show that many decidable formalisms for data trees are subsumed\u2014fully or partially\u2014by 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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/2338626.2338632","type":"journal-article","created":{"date-parts":[[2012,9,11]],"date-time":"2012-09-11T22:21:06Z","timestamp":1347402066000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Efficient reasoning about data trees via integer linear programming"],"prefix":"10.1145","volume":"37","author":[{"given":"Claire","family":"David","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Est, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonid","family":"Libkin","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tony","family":"Tan","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,9,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(03)00032-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/050646895"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346330.1346332"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85238-4_10"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970403"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516515"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Bouyer P. Petit A. and Th\u00e9rien D. 2001. An algebraic characterization of data and timed languages. In CONCUR. Springer 248--261.   Bouyer P. Petit A. and Th\u00e9rien D. 2001. An algebraic characterization of data and timed languages. In CONCUR. Springer 248--261.","DOI":"10.1007\/3-540-44685-0_17"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(02)00223-2"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03793-1_2"},{"key":"e_1_2_1_10_1","volume-title":"Tree Automata: Techniques and Applications","author":"Comon H.","year":"2007","unstructured":"Comon , H. , Dauchet , M. , Gilleron , R. , Jacquemard , F. , L\u00f6ding , C. , Lugiez , D. , Tison , S. , and Tommasi , M . 2007 . Tree Automata: Techniques and Applications . http:\/\/www.grappa.univ-lille3.fr\/tata Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., L\u00f6ding, C., Lugiez, D., Tison, S., and Tommasi, M. 2007. Tree Automata: Techniques and Applications. http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938558"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"de Moura L. M. and Bj\u00f8rner N. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems. 337--340.   de Moura L. M. and Bj\u00f8rner N. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems. 337--340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507246"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567112.567117"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559795.1559827"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1185877.1185882"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2973"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.11"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Kaminski M. and Tan T. 2008. Tree automata over infinite alphabets. In Pillars of Computer Science. Springer 386--423.   Kaminski M. and Tan T. 2008. Tree automata over infinite alphabets. In Pillars of Computer Science. Springer 386--423.","DOI":"10.1007\/978-3-540-78127-1_21"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2009.09.005"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1324185.1324188"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1114244.1114247"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(02)00030-2"},{"key":"e_1_2_1_26_1","volume-title":"Computer Science Logic","author":"Neven F.","unstructured":"Neven , F. 2002. Automata, logic, and XML . In Computer Science Logic . Springer , 2--26. Neven, F. 2002. Automata, logic, and XML. In Computer Science Logic. Springer, 2--26."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00301-2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Pacholski L. and Podelski A. 1997. Set constraints: A pearl in research on constraints. In Principles and Practice of Constraint Programming. 549--562.  Pacholski L. and Podelski A. 1997. Set constraints: A pearl in research on constraints. In Principles and Practice of Constraint Programming. 549--562.","DOI":"10.1007\/BFb0017466"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"e_1_2_1_31_1","unstructured":"Robinson A. and Voronkov A. 2001. Handbook of Automated Reasoning. MIT Press.   Robinson A. and Voronkov A. 2001. Handbook of Automated Reasoning. MIT Press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/974121.974140"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(67)80022-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/375551.375554"},{"key":"e_1_2_1_36_1","volume-title":"Introduction to Graph Theory","author":"West D.","unstructured":"West , D. 2001. Introduction to Graph Theory . Prentice Hall . West, D. 2001. Introduction to Graph Theory. Prentice Hall."}],"container-title":["ACM Transactions on Database Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2338626.2338632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2338626.2338632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:00Z","timestamp":1750236540000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2338626.2338632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2338626.2338632"],"URL":"https:\/\/doi.org\/10.1145\/2338626.2338632","relation":{},"ISSN":["0362-5915","1557-4644"],"issn-type":[{"value":"0362-5915","type":"print"},{"value":"1557-4644","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2011-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-09-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}