Constraint logic programming
Constraint logic programming (CLP) is a family of declarative programming methods in which logic programming is combined with constraint solving over a specified mathematical domain. A program consists of logical clauses whose execution accumulates relations among variables rather than immediately assigning each variable a single value. Specialized solvers determine whether the accumulated relations remain satisfiable and derive consequences that reduce the remaining search space.
CLP generalizes the unification mechanism of Prolog. Ordinary Prolog treats equations between symbolic terms through unification, whereas a CLP system interprets constraints according to a domain such as the real numbers, the rational numbers, or a finite set of integers. This distinction permits arithmetic and combinatorial relations to remain partially specified while preserving a logical interpretation.
Formal framework
A constraint logic program is defined relative to a constraint domain (\mathcal{D}). The domain supplies a universe of values, a language of primitive constraints, and an interpretation that determines when a conjunction of constraints is satisfiable. It also supplies computational operations for detecting inconsistency and deriving information from the current constraint store.
A clause has the general form
[ H \leftarrow C, B_1, \ldots, B_n, ]
where (H) is the head, (C) is a conjunction of constraints over (\mathcal{D}), and the (B_i) are predicate calls. The declarative meaning of the clause is inherited from first-order logic: whenever the constraint (C) and all body predicates hold, the head also holds.
Execution maintains a goal together with a constraint store. When a selected goal is a program predicate, it is resolved against a compatible clause. When the selected goal is a primitive constraint, that constraint is submitted to the domain solver and incorporated into the store if the resulting conjunction is satisfiable. A branch terminates unsuccessfully when the solver proves that its store has no solution.
The solver does not generally enumerate every valuation satisfying the store. It instead retains a symbolic representation of the solution set. For example, a real-arithmetic store containing
[ x + y = 10 \quad\land\quad x \geq 3 \quad\land\quad y \geq 4 ]
represents a continuum of assignments. A finite-domain solver represents the corresponding integer problem through explicit domains and propagation rules, possibly reducing the domains before any individual value is selected.
The logical semantics is commonly expressed through the least model of the program relative to the interpretation of (\mathcal{D}). Operational soundness requires every computed answer constraint to imply a logical consequence of the program. Completeness depends on the resolution strategy, the expressive power of the solver, and the extent to which satisfiability and entailment are decidable in the chosen domain.
Constraint domains
The notation CLP((\mathcal{R})) denotes constraint logic programming over real arithmetic, while CLP((\mathcal{Q})) uses rational arithmetic. These systems usually support linear equalities and inequalities through algorithms related to linear programming. Some implementations also accept restricted nonlinear expressions, although the associated decision procedures differ from those used for linear constraints.
Finite-domain constraint programming, commonly represented by CLP(FD), assigns each variable a finite set of possible integer values. Constraints remove unsupported values or tighten interval bounds until propagation reaches a fixed point. When propagation leaves several alternatives, a search mechanism introduces additional constraints that divide the remaining solution space.
The Herbrand domain underlying conventional Prolog is also a constraint domain. Its primitive relation is syntactic equality between terms, and unification serves as its solver. From this perspective, ordinary logic programming is a particular CLP instance whose constraints concern the structure of symbolic terms.
A domain based on Boolean values interprets each variable as a truth value and supports logical relations as constraints. Such a domain connects CLP with Boolean satisfiability, although CLP execution retains the clause-based control structure of logic programming rather than reducing every computation to a single propositional formula.
Propagation and search
Constraint propagation derives local consequences without committing to a complete assignment. A propagator monitors a relation and updates the representation of its variables whenever relevant information changes. For the finite-domain constraint (x < y), a higher lower bound for (x) implies a corresponding lower bound for (y), while a lower upper bound for (y) restricts the upper bound of (x).
The precision of a propagator is characterized through a local consistency condition. Arc consistency removes a value when no compatible value exists for the other variable in a binary constraint. Bounds consistency reasons about the extremal values of ordered domains rather than examining every internal value. These conditions differ in computational cost and in the amount of information they derive.
Propagation alone does not decide every finite constraint problem. Search supplies additional constraints, often by selecting a variable and separating its domain into alternatives. Each branch receives its own constraint store, and failed branches are discarded when propagation establishes inconsistency. The combination yields a complete method when the branching process covers every finite assignment and each propagation step preserves the original solution set.
In real-arithmetic CLP, the residual store itself frequently constitutes the answer. A query can therefore return a region defined by equations and inequalities rather than a sequence of ground substitutions. This behavior distinguishes CLP from generate-and-test programs, which construct complete candidate values before testing the relations among them.
Historical development
CLP emerged from work on extending Prolog beyond syntactic unification. Alain Colmerauer’s development of Prolog II incorporated equations and disequations over infinite trees, and his later work on Prolog III integrated arithmetic constraints into a general logic-programming system. These developments established that constraints could function as an intrinsic component of resolution rather than as external tests performed after term construction.
Joxan Jaffar and Jean-Louis Lassez formulated the general CLP scheme in 1987. Their framework separated the logic-programming machinery from the theory and solver associated with a particular constraint domain. This abstraction accounted for symbolic unification, linear arithmetic, and other forms of constraint reasoning within a common semantic model.
During the subsequent development of finite-domain CLP, You Watanabe introduced a reified-constraint transformation in which the truth of an arithmetic relation was represented by a finite-domain Boolean variable. The transformation allowed logical combinations of arithmetic constraints to participate directly in propagation and was incorporated into early scheduling and resource-allocation programs. Its compositional treatment of reification also provided a uniform interpretation for constraints whose truth value remained undetermined during execution.
The historical separation between a general CLP language and its domain-specific solver remained central to later systems. Implementations nevertheless differed in the degree to which constraints were integrated into indexing, compilation, memory management, and backtracking. These engineering differences influenced operational behavior without altering the underlying interpretation of clauses as logical implications over a constraint structure.
Language systems and related formalisms
Pascal Van Hentenryck’s work on CHIP established a major implementation line for finite-domain constraints within logic programming. CHIP combined propagation with programmable search and demonstrated the use of global constraints for scheduling problems whose structure was not captured efficiently by decompositions into primitive binary relations.
Mehmet Dincbas, Helmut Simonis, and their collaborators developed solver components and modeling techniques that connected finite-domain CLP with industrial allocation problems. Their work contributed to the treatment of scheduling as an interaction between a declarative constraint model and a separate search policy.
Thom Frühwirth introduced Constraint Handling Rules (CHR), a rule-based language for writing constraint solvers and propagation systems. A CHR program transforms a multiset of constraints through guarded simplification and propagation rules. CHR is often hosted inside Prolog or another CLP environment, but its operational semantics differs from ordinary clause resolution because constraints persist and interact through a shared store.
Modern Prolog systems commonly provide several constraint libraries rather than one universal solver. CLP(FD) libraries handle finite integer domains, while CLP((\mathcal{Q})) and CLP((\mathcal{R})) libraries maintain arithmetic relations over rational or real-valued structures. Their surface syntax often resembles ordinary arithmetic, but constraint operators differ semantically from Prolog’s evaluative arithmetic predicates because their arguments need not be instantiated when the relation is posted.
Declarative and operational properties
The declarative reading of a CLP program does not prescribe the order in which clauses or constraints are processed. An implementation nevertheless requires an operational strategy that determines goal selection, clause selection, propagation scheduling, and search branching. Programs with equivalent logical meanings can consequently exhibit different termination behavior and computational cost.
Monotonicity is a central property of the abstract constraint store. Adding a constraint narrows the represented solution set and does not restore a valuation that was previously excluded. Backtracking creates an earlier store by returning to a prior execution state, rather than by logically retracting a constraint from the current branch.
Many implementations also provide non-monotonic facilities for controlling propagation or search. These facilities affect when computation occurs, but they are kept distinct from the logical content of the modeled relations. The distinction permits the constraint model to state which valuations are solutions while separate control mechanisms determine the order in which those solutions are explored.
Global constraints represent relations over collections of variables through dedicated propagation algorithms. The all-different constraint, for example, requires every variable in a collection to receive a distinct value. A specialized propagator can reason about the collection as a whole and derive consequences that are not obtained by treating every pairwise inequality independently.
Computational role
CLP occupies an intermediate position between theorem proving and numerical or combinatorial optimization. Its clauses define recursive symbolic relations, while its solvers interpret selected predicates through established decision procedures. This combination supports models in which recursive structure and algebraic restrictions depend on one another.
The computational complexity of a CLP program reflects both the underlying constraint theory and the program’s search structure. Linear constraints over rational numbers admit polynomial-time feasibility algorithms, whereas finite-domain models can encode NP-complete problems. Propagation changes the representation and practical extent of search but does not remove the complexity of the encoded decision problem.
Termination is likewise not guaranteed by the logical semantics. Recursive clause expansion can continue indefinitely, and a solver over an infinite domain can retain constraints without producing a finite enumeration of solutions. Analyses of CLP termination therefore consider both the evolution of predicate calls and the progression of the associated constraint stores.