Rule-based specification, analysis and implementation of propagation algorithms for global constaints

• Applicant: Professor Dr. Thom Frühwirth
• Subject Area: Theoretical Computer Science
• Term: from 2006 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 18899577

• Final Report Year: 2011

Final Report Abstract

We have investigated rule-based propagation algorithms for global constraints that can be used to solve constraint satisfaction problems. These included solvers for first-order constraints, the lexicographic order constraint, as well as rules for the preflow-push algorithm necessary for the alldifferent and cardinality constraints. We have proved correctness of the implemented rules. Moreover, since the specification and correct implementation of such propagation algorithms required substantial expertise, we developed algorithms that can correctly generate the rules given the definition of the constraint. The algorithms covered constraints given by their logical definition as well as those described by automata. The automatic generation algorithms were shown to yield solvers that are correct. Furthermore, we provided new means for analyzing CHR programs by investigating similarities with Petri nets, Transaction Logic, and Term Rewriting.

Publications

• A unified semantics for constraint handling rules in transaction logic. In: Baral, C., Brewka, G., Schlipf, J.S. (eds.): Logic Programming and Nonmonotonic Reasoning: 9th International Conf., LPNMR 2007, Tempe, AZ, USA, May 15-17, 2007. Proceedings. Lecture Notes in Computer Science, Vol. 4483. 2007, pp. 201-213.
  Meister, M., Djelloul, K., Robin, J.
  (See online at https://dx.doi.org/10.1007/978-3-540-72200-7_18)
• Concurrency of the preflow-push algorithm in Constraint Handling Rules. In Fages, F., Rossi, F., Soliman, S., eds.: Constraint Solving and Constraint Logic Programming, Annual ERCIM Workshop, CSCLP 2007, Rocquencourt, France, 2007, pp. 161-169.
  Meister, M.
  
• Decomposable theories. Theory and Practice of Logic Programming Vol. 7. 2007, Issue 5, pp. 583-632.
  Djelloul, K.:
  (See online at https://doi.org/10.1017/S1471068406002997)
• A full first-order constraint solver for decomposable theories. In: Intelligent Computer Mathematics: 9th International Conf., AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conf., MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. Lecture Notes in Computer Science, Vol. 5144. 2008, pp.93-108.
  Djelloul, K.:
  (See online at https://dx.doi.org/10.1007/978-3-540-85110-3_9)
• Constructing rule-based solvers for intentionally-defined constraints. In: Constraint Handling Rules - Current Research Topics. Lecture Notes in Computer Science, Vol. 5388. 2008, pp. 70-84.
  Sobhi, I., Abdennadher, S., Betz, H.
  (See online at https://dx.doi.org/10.1007/978-3-540-92243-8_4)
• Semi-automatic generation of CHR solvers for global constraints. In: Principles and Practice of Constraint Programming - 14th International Conference, CP 2008, Sydney, Australia, September 14-18, 2008, Proceedings. Lecture Notes in Computer Science, Vol. 5202. 2008, pp 588-592.
  Raiser, F.
  (See online at https://dx.doi.org/10.1007/978-3-540-85958-1_47)
• Semi-automatic generation of CHR solvers from global constraint automata. Ulmer Informatik Berichte, 2008-03, 18 S., Ulm University
  Raiser, F.
  
• Theory of finite or infinite trees revisited. Theory and Practice of Logic Programming, Vol. 8. 2008, Issue 4, pp. 431-489.
  Djelloul, K., Dao, T.B.H., Fruhwirth, T.
  (See online at https://doi.org/10.1017/S1471068407003171)