Combinatorial problems occur quite often in many application areas, e.g. scheduling or cutting stock problems, and may be specified as problems over finite domains, i.e., the variables range over a finite subset of the integers. Our approach taken in the concurrent constraint language Oz is to support an efficiently implementable constraint system for constraints 'x in D'. Using this constraint system, the programmer can add his own functionality by so called virtual constraints (e.g. 'x =< y'). Because the problem of satisfiability of these more complex constraints is NP-complete, most of them are implemented incompletely by using reflecting operators returning the current minimum and maximum of a variable's domain. For these programs serving as the core of finite domain reasoning, the question of verification arises. Verification is complicated by the operators reflecting the current known information about variables. In our approach we translate the computation states into first order formulas by giving virtual constraints their intended semantics (the semantics of the corresponding logic constraint). We prove that for a reduction of computation states Gamma -> Gamma' the corresponding first order formulas are equivalent with respect to the intended model. Our approach, which seems to be very natural in the setting of constraint languages, succeeds in proving virtual constraints to be correct, terminating and complete (in the shown example) with respect to an intended semantics.
Download PDF Show BibTeX
Login to edit