Solver Predicates

The solver interface for both Q and R consists of the following predicates, which are exported from module(linear).

{+Constraint}

Constraint is a term accepted by the the grammar below. The corresponding constraint is added to the current constraint store and checked for satisfiability. Use the module prefix to distinguish the solvers if both clp(Q) and clp(R) were loaded 

          | ?- clpr:{Ar+Br=10}, Ar=Br, clpq:{Aq+Bq=10}, Aq=Bq.
          
          Aq = 5,
          Ar = 5.0,
          Bq = 5,
          Br = 5.0

Although clp(Q) and clp(R) are independent modules, you are asking for trouble if you (accidently) share variables between them: 

          | ?- clpr:{A+B=10}, clpq:{A=B}.
          ! Type error in argument 2 of clpq:=/2
          ! a rational number expected, but 5.0 found
          ! goal:  _118=5.0

This is because both solvers eventually compute values for the variables and Reals are incompatible with Rationals.

Here is the constraint grammar:

Constraint ::= C
| C , C { conjunction }

C ::= Expr =:= Expr { equation }
| Expr = Expr { equation }
| Expr < Expr { strict inequation }
| Expr > Expr { strict inequation }
| Expr =< Expr { nonstrict inequation }
| Expr >= Expr { nonstrict inequation }
| Expr =\= Expr { disequation }

Expr ::= variable { Prolog variable }
| number { floating point or integer }
| + Expr { unary plus }
| - Expr { unary minus }
| Expr + Expr { addition }
| Expr - Expr { subtraction }
| Expr * Expr { multiplication }
| Expr / Expr { division }
| abs(Expr) { absolute value }
| sin(Expr) { trigonometric sine }
| cos(Expr) { trigonometric cosine }
| tan(Expr) { trigonometric tangent }
| pow(Expr,Expr) { raise to the power }
| exp(Expr,Expr) { raise to the power }
| min(Expr,Expr) { minimum of the two arguments }
| max(Expr,Expr) { maximum of the two arguments }
| #(Const) { symbolic numerical constants }

Conjunctive constraints {C,C} have been made part of the syntax to control the granularity of constraint submission, which will be exploited by future versions of this software. Symbolic numerical constants are provided for compatibility only; see Monash Examples.

entailed(+Constraint)

Succeeds iff the linear Constraint is entailed by the current constraint store. This predicate does not change the state of the constraint store. 

          clp(q) ?- {A =< 4}, entailed(A=\=5).
          
          {A=<4}
          
          clp(q) ?- {A =< 4}, entailed(A=\=3).
          
          no

inf(+Expr, -Inf)
inf(+Expr, -Inf, +Vector, -Vertex)

Computes the infimum of the linear expression Expr and unifies it with Inf. If given, Vector should be a list of variables relevant to Expr, and Vertex will be unified a list of the same length as Vector containing the values for Vector, such that the infimum is produced when assigned. Failure indicates unboundedness.

sup(+Expr, -Sup)
sup(+Expr, -Sup, +Vector, -Vertex)

Computes the supremum of the linear expression Expr and unifies it with Sup. If given, Vector should be a list of variables relevant to Expr, and Vertex will be unified a list of the same length as Vector containing the values for Vector, such that the supremum is produced when assigned. Failure indicates unboundedness. 

          clp(q) ?- { 2*X+Y =< 16, X+2*Y =< 11,
                      X+3*Y =< 15, Z = 30*X+50*Y
                    }, sup(Z, Sup, [X,Y], Vertex).
          
          Sup = 310,
          Vertex = [7,2],
          {Z=30*X+50*Y},
          {X+1/2*Y=<8},
          {X+3*Y=<15},
          {X+2*Y=<11}

minimize(+Expr)

Computes the infimum of the linear expression Expr and equates it with the expression, i.e. as if defined as: 

          minimize(Expr) :- inf(Expr, Expr).

maximize(+Expr)

Computes the supremum of the linear expression Expr and equates it with the expression. 

          clp(q) ?- { 2*X+Y =< 16, X+2*Y =< 11,
                      X+3*Y =< 15, Z = 30*X+50*Y
                    }, maximize(Z).
          
          X = 7,
          Y = 2,
          Z = 310

bb_inf(+Ints, +Expr, -Inf)

Computes the infimum of the linear expression Expr under the additional constraint that all of variables in the list Ints assume integral values at the infimum. This allows for the solution of mixed integer linear optimization problems; see MIP. 

          clp(q) ?- {X >= Y+Z, Y > 1, Z > 1}, bb_inf([Y,Z],X,Inf).
          
          Inf = 4,
          {Y>1},
          {Z>1},
          {X-Y-Z>=0}

bb_inf(+Ints, +Expr, -Inf, -Vertex, +Eps)

Computes the infimum of the linear expression Expr under the additional constraint that all of variables in the list Ints assume integral values at the infimum. Eps is a positive number between 0 and 0.5 that specifies how close a number X must be to the next integer to be considered integral: abs(round(X)-X) < Eps. The predicate bb_inf/3 uses Eps = 0.001. With clp(Q), Eps = 0 makes sense. Vertex is a list of the same length as Ints and contains the (integral) values for Ints, such that the infimum is produced when assigned. Note that this will only generate one particular solution, which is different from the situation with minimize/1, where the general solution is exhibited.

bb_inf/5 works properly for non-strict inequalities only! Disequations (=\=) and higher dimensional strict inequalities (>,<) are beyond its scope. Strict bounds on the decision variables are honored however: 

          clp(q) ?- {X >= Y+Z, Y > 1, Z > 1}, bb_inf([Y,Z],X,Inf,Vertex,0).
          
          Inf = 4,
          Vertex = [2,2],
          {Y>1},
          {Z>1},
          {X-Y-Z>=0}

The limitation(s) can be addressed by:


ordering(+Spec)

Provides a means to control one aspect of the presentation of the answer constraints; see Variable Ordering.

dump(+Target, -NewVars, -CodedAnswer)

Reflects the constraints on the target variables into a term, where Target and NewVars are lists of variables of equal length and CodedAnswer is the term representation of the projection of constraints onto the target variables where the target variables are replaced by the corresponding variables from NewVars (see Turning Answers into Terms). 

          clp(q) ?- {A+B =< 10, A>=4}, 
                    dump([A,B],Vs,Cs), 
                    dump([B],Bp,Cb).
          
          Cb = [_A=<6],
          Bp = [_A],
          Cs = [_B>=4,_C+_B=<10],
          Vs = [_C,_B],
          {A>=4},
          {A+B=<10}
The current version of dump/3 is incomplete with respect to nonlinear constraints. It only reports nonlinear constraints that are connected to the target variables. The following example has no solution. From the top-level's report we have a chance to deduce this fact, but dump/3 currently has no means to collect global constraints ... 
          q(X) :-
                  {X>=10},
                  {sin(Z)>3}.
          
          clp(r) ?- q(X), dump([X],V,C).
          
          C = [_A>=10.0],
          V = [_A],
          clpr:{3.0-sin(_B)<0.0},
          {X>=10.0}

projecting_assert/1(:Clause)

If you use the database, the clauses you assert might have constraints associated with their variables. Use this predicate instead of assert/1 in order to ensure that only the relevant and projected constraints get stored in the database. It will transform the clause into one with plain variables and extra body goals that set up the relevant constraint when called.