From exponential to almost linear decomposability of finite or infinite trees

ABSTRACT

First-order constraints are first-order formulas built on a set of function and relation symbols using the following logical symbols: =, true, false, ¬, ∧, ∨, →, ↔, ∀, ∃, (,). Over the last decade, first-order constraints have been efficiently used in the artificial intelligence world to model many kinds of complex problems such as: scheduling, resource allocation, configuration, temporal and spatial reasoning, computer graphics, bio-informatics. While theory of finite or infinite trees T has played a fundamental role for both modeling and solving these problems, the complexity of solving first-order constraints with nested quantifiers and negations in T has been proved to be inherently huge (a tower of powers of two). However, a new property called decomposability has been recently introduced and used as a black-box to build many efficient first-order constraint solvers over T. We show in this paper that the algorithm which is used in this black-box (i.e. the algorithm which performs decomposability) has an exponential time and space complexity. We then present a much more efficient algorithm in the form of four rewriting rules which can perform the same decomposability in an almost-linear time and space complexity.

REFERENCES

• 1: Krzysztof Apt, Principles of Constraint Programming, Cambridge University Press, New York, NY, 2003
• 2: Alain Colmerauer , Thi-Bich-Hanh Dao, Expressiveness of Full First-Order Constraints in the Algebra of Finite or Infinite Trees, Constraints, v.8 n.3, p.283-302, July 2003 [doi>10.1023/A:1025675127871]
• 3: Alain Colmerauer, An introduction to Prolog III, Communications of the ACM, v.33 n.7, p.69-90, July 1990 [doi>10.1145/79204.79210]
• 4: Colmerauer, A. Equations and inequations on finite and infinite trees. Proceeding of the International conference on the fifth generation of computer systems, pp. 8599. 1984.
• 5: Colmerauer, A., Kanoui, H. and Van-caneghem, M. Prolog, Theoretical Basis and Current Developments. TSI 2(4): 271311. 1983.
• 6: Colmerauer, A. Prolog and infinite trees. In K. L. Clark and S-A. Tarnlund, editors, Logic Programming. Academic Press. pp. 231251. 1982.
• 7: Khalil Djelloul , Thi-bich-hanh Dao , Thom FrÜhwirth, Theory of finite or infinite trees revisited, Theory and Practice of Logic Programming, v.8 n.4, p.431-489, July 2008 [doi>10.1017/S1471068407003171]
• 8: Khalil Djelloul, Decomposable theories, Theory and Practice of Logic Programming, v.7 n.5, p.583-632, September 2007 [doi>10.1017/S1471068406002997]
• 9: Khalil Djelloul, Combination of decomposability and propagation for solving first-order constraints in decomposable theories, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil [doi>10.1145/1363686.1364099]
• 10: Khalil Djelloul , Thi-Bich-Hanh Dao , Thom Fruehwirth, Toward a first-order extension of Prolog's unification using CHR: a CHR first-order constraint solver over finite or infinite trees, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea [doi>10.1145/1244002.1244016]
• 11: Duck, J., Stuckey, J., Garcya de la Banda., and C. Holzbaur. The refined operational semantics of Constraint Handling Rules. In proc ICLP'04 International Conference on Logic Programming, volume 3132 of LNCS, pages 90104. Springer, 2004.
• 12: Gregory J. Duck , Peter J. Stuckey , Maria Garcia de la Banda , Christian Holzbaur, Extending arbitrary solvers with constraint handling rules, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.79-90, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888260]
• 13: Fruehwirth, T. Theory and Practice of Constraint Handling Rules. Special Issue on Constraint Logic Programming. Journal of Logic Programming. 37(13): 95--138. 1998.
• 14: Thom Fruewirth , Slim Abdennadher, Essentials of Constraint Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 15: Maher M. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In proc of LICS'88 IEEE Symposium on Logic in Computer Science. pp. 348--357. 1988.
• 16: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 17: A decision procedure for term algebras with queues, ACM Transactions on Computational Logic (TOCL), v.2 n.2, p.155-181, April 2001 [doi>10.1145/371316.371494]
• 18: J. Michael Spivey, A Categorial Approch to the Theory of Lists, Proceedings of the International Conference on Mathematics of Program Construction, 375th Anniversary of the Groningen University, p.399-408, June 26-30, 1989
• 19: Tom Schrijvers , Thom Frühwirth, Optimal union-find in Constraint Handling Rules, Theory and Practice of Logic Programming, v.6 n.1-2, p.213-224, January 2006 [doi>10.1017/S1471068405002541]
• 20: Robert E. Tarjan , Jan van Leeuwen, Worst-case Analysis of Set Union Algorithms, Journal of the ACM (JACM), v.31 n.2, p.245-281, April 1984 [doi>10.1145/62.2160]
• 21: Sergei G. Vorobyov, An Improved Lower Bound for the Elementary Theories of Trees, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.275-287, August 03, 1996

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

General Terms:
Theory

Keywords:
first-order logic, rewriting rules, solving first order constraints, theory of trees