Constraint Logic Programming

Origin. Jaffar and Lassez introduced CLP scheme (1987). Extends logic programming with constraint solving. Combines Prolog-style reasoning with domain-specific solvers. Foundation for constraint satisfaction and optimization. Systems: CLP(R), CLP(FD), ECLiPSe, SICStus.

Models. Logic programming with constraints. Prolog: unification only. CLP: add domain constraints (arithmetic, finite domains, etc.). Goals include constraints; solver maintains consistency. Combines declarative logic with efficient specialized solvers.

Formalism.

CLP(X) scheme: X: constraint domain (R, Q, FD, etc.)

Syntax: Clauses: H :- B₁, ..., Bₙ, c₁, ..., cₘ where Bᵢ are atoms, cⱼ are constraints.

Constraint domains:

CLP(R): real arithmetic (X > 0, X + Y = Z)
CLP(Q): rational arithmetic
CLP(FD): finite domains (X in 1..10, all_different)
CLP(B): Boolean constraints

Execution: Maintain constraint store. Add constraints, check satisfiability. Backtrack if store becomes unsatisfiable.

Example (CLP(FD)): sudoku(Rows) :- append(Rows, Vs), Vs ins 1..9, maplist(all_distinct, Rows), transpose(Rows, Cols), maplist(all_distinct, Cols), blocks(Rows), label(Vs).

Propagation: Constraints propagate: X in 1..9, X > 5 → X in 6..9. Reduces search space.

Labeling: Enumerate solutions after propagation. Search strategies: first-fail, etc.

Symbols.

Symbol	Unicode	Name	Meaning
:-	—	Rule	If
ins	—	In set	Domain
#=	—	Constraint equals	Arithmetic
#<	—	Constraint less	Inequality
all_different	—	All distinct	Global constraint
label	—	Label	Enumerate

Metatheory. Jaffar and Lassez (POPL 1987) proved the theorem that makes CLP(X) a scheme rather than a family of languages: for a constraint domain that is solution-compact and satisfaction-complete, the logical semantics (the least model over the domain), the fixpoint semantics (the least fixpoint of the immediate-consequence operator) and the operational semantics (successful derivations) all coincide, generalizing the van Emden–Kowalski theorem for pure logic programming. Soundness and completeness of derivations follow, with completeness relative to a fair search rule. Everything else depends on the domain. Linear constraints over the rationals or reals are solvable in polynomial time, whereas satisfiability over finite domains is NP-complete and CLP(B) is exactly SAT. Presburger arithmetic is decidable but Fischer and Rabin (1974) proved a doubly exponential lower bound. Propagation is bounded consistency, not solving: enforcing generalized arc consistency for an arbitrary constraint is NP-hard, though Régin (1994) gave a polynomial filtering algorithm for all_different via bipartite matching.

Applies to. Scheduling. Planning. Configuration. Rostering. Puzzle solving. Optimization. Bioinformatics. Hardware verification.

Limitations. The equivalence of the three semantics is conditional on the constraint domain being solution-compact and satisfaction-complete; a solver that is incomplete, or that computes over floating point rather than the reals, satisfies neither condition, so the declarative reading of a program is no longer guaranteed by the theory. Completeness of the operational semantics also requires a fair search rule, and the depth-first left-to-right strategy that implementations actually use is unfair: a program with solutions can diverge before finding them. Propagation is deliberately incomplete, so search remains necessary and the practical cost is governed by heuristics the semantics says nothing about. CLP(R) implementations delay nonlinear constraints rather than solving them, so a derivation can succeed leaving an unsolved store. Every global constraint needs its own filtering algorithm; there is no general construction.