CLP(B), CLP(Q/R) & CHR

Uses BDDs; good for circuit verification, puzzles, counting solutions.

29.1 CLP(B) — Boolean constraints

Uses BDDs; good for circuit verification, puzzles, counting solutions.

:- use_module(library(clpb)).

?- sat(X + Y), sat(~X).              % X = 0, Y = 1
?- sat(card([2], [A, B, C])), labeling([A, B, C]).   % exactly two true
?- taut(X + ~X, T).                  % T = 1 (tautology)
?- sat_count(+[1, A, B], N).         % number of models

29.2 CLP(Q) & CLP(R) — linear constraints over rationals/reals

library(clpr) works over floating-point reals; library(simplex) offers LP solving.

:- use_module(library(clpq)).

?- {X + Y = 10, X - Y = 2}.          % X = 6, Y = 4
?- {2*X + Y =< 16, X + 2*Y =< 11, X >= 0, Y >= 0}, maximize(5*X + 4*Y).   % linear programming
?- {Mortgage = Principal * (1 + Rate)}, {Principal = 1000, Rate = 1/20}.

29.3 Constraint Handling Rules (CHR)

A rule-based language embedded in Prolog for writing constraint solvers.

Rule kinds: simplification (<=>), propagation (==>), simpagation (\ ... <=>), with guards (Guard |).

:- use_module(library(chr)).
:- chr_constraint gcd/1.

gcd(0) <=> true.                              % simplification
gcd(N) \ gcd(M) <=> N =< M | L is M mod N, gcd(L).   % simpagation

?- gcd(9), gcd(6).    % leaves gcd(3)

:- chr_constraint leq/2.
reflexivity  @ leq(X, X) <=> true.
antisymmetry @ leq(X, Y), leq(Y, X) <=> X = Y.
idempotence  @ leq(X, Y) \ leq(X, Y) <=> true.
transitivity @ leq(X, Y), leq(Y, Z) ==> leq(X, Z).   % propagation

?- leq(A, B), leq(B, C), leq(C, A).   % A = B, B = C