Combination of decomposability and propagation for solving first-order constraints in decomposable theories

ABSTRACT

Over the last decade, first-order constraints have been efficiently used in the constraint programming world to model many kinds of complex problems such as: scheduling, resource allocation, computer graphics and bio-informatics. Recently, a new property called "decomposability" has been introduce and many first-order theories have been proved to be decomposable: finite or infinite trees, rational and real numbers, linear dense order, ... etc. A decision procedure in the form of 5 rewriting rules has also been developed but this later can only decide if a formula without free variables is true or not in any decomposable theory T. Unfortunately, this decision procedure is not enough when we want to find the values of the free variables of any first-order constraint ϕ so that ϕ is true in any decomposable theory T. These kind of problems are generally known as first-order constraint satisfaction problems. We present in this paper not only a decision procedure but a full first-order constraint solver for any decomposable theory T. Our solver is given in the form of six rewriting rules which transform any first-order constraint (which can possibly contain free variables) into an equivalent solved formula which is either the formula true, or the formula false or a formula having at least one free variable and written in a very simple and explicit solved form. We also show the efficiency of our solver by solving complex first-order constraints containing a huge number of imbricated quantifiers and negations. This is the first full first-order constraint solver over any decomposable theory.

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: Khalil Djelloul, Decomposable theories, Theory and Practice of Logic Programming, v.7 n.5, p.583-632, September 2007 [doi>10.1017/S1471068406002997]
• 4: Djelloul K., Dao T., Fruehwirth T. Theory of finite or infinite trees revisited. Theory and practice of logic programming (TPLP). Cambridge journals. 2007 (to appear).
• 5: Thom Fruewirth , Slim Abdennadher, Essentials of Constraint Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 6: Maher M. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In proc of LICS 88 Annual Symposium on Logic in Computer Science, pages: 348--357. 1988.
• 7: 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]
• 8: 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

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

General Terms:
Algorithms, Design, Theory

Keywords:
complete theory, first-order constraint satisfaction problems, first-order constraint solvers, first-order constraints, rewriting rules