On the semantics of optimization predicates in CLP languages

The Constraint Logic Programming systems which have been implemented include various higher-order predicates for optimization. In CLP(FD) systems, optimization predicates such as min(G (X), f (X)), or min-max(G (X), [f1 (X),…., fn(X)]), are implemented by using branch and bound algorithms. In CLP(R) systems, the Simplex algorithm used for satisfiability checks can also be used for linear optimization through the predicate rmin(f(X)) which adds to the constraints on X the ones defining the space where the linear term f(X) is minimized. These optimization constructs do not belong however to the formal CLP scheme of Jaffar and Lassez, and they lack a declarative semantics. In this paper we propose a general definition for optimization predicates, for which one can provide both a logical and a fixpoint semantics based on Kunen-Fitting’s semantics of negation. We show that the branch and bound algorithm can be derived as a specialized version of CSLDNF-resolution procedures, and that the branch and bound algorithm can be lifted to a full first-order setting with constructive negation.