TY - GEN
T1 - On the semantics of optimization predicates in CLP languages
AU - Fages, François
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1993.
PY - 1993/1/1
Y1 - 1993/1/1
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-57529-4_53
DO - 10.1007/3-540-57529-4_53
M3 - Conference contribution
AN - SCOPUS:85029419269
SN - 9783540575290
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 193
EP - 204
BT - Foundations of Software Technology and Theoretical Computer Science - 13th Conference, Proceedings
A2 - Shyamasundar, Rudrapatna K.
PB - Springer Verlag
T2 - 13th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1993
Y2 - 15 December 1993 through 17 December 1993
ER -