combination of decomposability and propagation for solving first-order constraints in decomposable theories
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 &phiv; so that &phiv; 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.
first-order constraints rewriting rules first-order constraint solvers complete theory