1/*
    2  modeling.pl
    3  
    4  @author Francois Fages
    5  @email Francois.Fages@inria.fr
    6  @institute Inria, France
    7  @license LGPL-2
    8
    9  @version 1.1.4
   10
   11  Mathematical modeling with constraints on subscripted variables.
   12*/
   13
   14:- module(
   15	  modeling,
   16	  [
   17	   int_array/2,
   18	   int_array/3,
   19	   bool_array/2,
   20	   float_array/2,
   21	   float_array/3,
   22	   satisfy/1,
   23	   satisfy/2,
   24	   satisfy_attvars/1,
   25	   satisfy_attvars/2,
   26	   minimize/2,
   27	   minimize/3,
   28	   maximize/2,
   29	   maximize/3
   30	  ]
   31	 ).

Mathematical modeling with constraints on subscripted variables.

author
- Francois Fages
version
- 1.1.4

This module provides a constraint-based mathematical modeling language in the spirit of MiniZinc in Prolog (A MiniZinc parser is planned to be added to this library in a next release).

The pack includes 5 modules with the following dependencies quantifiers.pl --> arrays.pl --> clp.pl --> modeling.pl --> examplesFLOPS2024.pl

library(examplesFLOPS2024) contains the examples and benchmark presented in the article:

  • F. Fages. A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics. 17th International Symposium on Functional and Logic Programming, FLOPS 2024. May 15, 2024 - May 17, 2024, Kumamoto, Japan. LNCS, Springer-Verlag.

library(quantifiers) defines bounded quantifiers with "in" domain and "where" conditions, let bindings, and a multifile user-defined predicate for defining shorthand/3 functional notations in expressions, e.g. conditional expressions with if/3 term.

library(arrays) defines multidimensional arrays for constraints on subscripted variables and the Array[Indices] shorthand/3 notation.

library(clp) is a frontend to library(clpr) and library(clpfd) to define hybrid constraints and allow shorthand notations such as Array[Indices] in constraints and domains.

Below is the example of a goal that can be written in this library to solve the 4-queens placement problem and pretty-print the chessboard, using subscripted variables (arrays) instead of lists, bounded quantifiers instead of recursion and functional notations in let bindings and constraints.

?- N=4, int_array(Queens, [N], 1..N),
  
  for_all([I in 1..N-1, D in 1..N-I],
    (Queens[I] #\= Queens[I+D],
     Queens[I] #\= Queens[I+D]+D,
     Queens[I] #\= Queens[I+D]-D)),
  
  satisfy(Queens),
  
  for_all([I, J] in 1..N,
    let([QJ = Queens[J],
         Q = if(QJ = I, 'Q', '.'),
         B = if(J = N, '\n', ' ')],
        format("~w~w",[Q,B]))).
. . Q .
Q . . .
. . . Q
. Q . .
N = 4,
Queens = array(2, 4, 1, 3) ;
. Q . .
. . . Q
Q . . .
. . Q .
N = 4,
Queens = array(3, 1, 4, 2) ;
false.

Below is an example of hybrid reified clpr clpfd constraint defined in library(clp).

?- array(A, [3]), truth_value({A[1] < 3.14}, B).
A = array(_A, _, _),
when((nonvar(_A);nonvar(B)), clp:clpr_reify(_A<3.14, _A>=3.14, B)).

?- array(A, [3]), truth_value({A[1] < 3.14}, B), {A[1]=2.7}.
A = array(2.7, _, _),
B = 1.

*/

  102%:- catch(reexport(library(clp)), _, (throw(error(pack_clp_is_not_installed)), fail)).
  103:- reexport(library(clp)).  104
  105:- op(990, xfx, where).  106:- op(100, yf, []).
 bool_array(?Array, ?Dimensions)
Array is a array of Boolean values (0 or 1) or Boolean variables of dimensions Dimensions.
  113bool_array(Array, Dimensions):-
  114    int_array(Array, Dimensions, 0..1).
 int_array(?Array, ?Dimensions)
Array is an array of integer numbers or variables of dimensions Dimensions.
  121int_array(Array, Dimensions):-
  122    int_array(Array, Dimensions, _Domain).
 int_array(?Array, ?Dimensions, +Domain)
Array is an array of integer numbers or variables in Domain of dimensions Dimensions.
  129int_array(Array, Dimensions, Domain):-
  130    array(Array, Dimensions),
  131    array_list(Array, List),
  132    (
  133     ground(Domain)
  134    ->
  135     List ins Domain
  136    ;
  137     List ins inf..sup
  138     % for_all([Cell in List],
  139     % 	     exists([Mi, Ma], (fd_inf(Cell, Mi), Min #=< Mi, fd_sup(Cell, Ma), Ma #=< Max))),
  140     % fd_sup(Min, Inf),
  141     % fd_inf(Max, Sup),
  142     % Domain = Inf .. Sup
  143    ).
 float_array(?Array, ?Dimensions)
Array is an array of real numbers or variables of dimensions Dimensions.
  150float_array(Array, Dimensions):-
  151    array(Array, Dimensions).
 float_array(?Array, ?Dimensions, +Range)
Array is an array of real numbers or variables in Range Min..Max of dimensions Dimensions. If not given the Range variables are returned with constraints, or fails if they are unbounded.
  159float_array(Array, Dimensions, Min..Max):-
  160    array(Array, Dimensions),
  161    array_list(Array, List),
  162    for_all([Cell in List], {Min=< Cell, Cell =< Max}).
  163
  164
  165				% ENUMERATION PREDICATES
 satisfy(+Term)
enumerate all solutions of the variables contained or related to Term, with smallest-domain first-fail and-choice heuristics ff.
  172satisfy(Term):-
  173    satisfy(Term, [ff]).
 satisfy(+Term, +Options)
same as satisfy/1 with the Options from library(clpfd) predicate labeling/2.
  180satisfy(Term, Options) :-
  181    term_variables(Term, Vars),
  182    labeling(Options, Vars).
 satisfy_attvars(+Term)
same as satisfy/1 but enumerating the values of the variables in term and in their attributes.
  189satisfy_attvars(Term):-
  190    satisfy_attvars(Term, [ff]).
 satisfy_attvars(+Term, +Options)
same as satisfy/2 but enumerating also the values of the variables contained in the attributes of the variables in Term.
  197satisfy_attvars(Term, Options) :-
  198    term_attvars(Term, Vars),
  199    labeling(Options, Vars).
 minimize(+Expr, +Term)
enumerate all solutions of the variables contained in Term in increasing order of Expr.
  207minimize(Expr, Term):-
  208    term_attvars(Term, Vars),
  209    labeling([min(Expr), ff], Vars).
 minimize(+Expr, +Term, +Options)
same as minimize/2 using extra library(clpfd) labeling/2 options
  215minimize(Expr, Term, Options):-
  216    term_attvars(Term, Vars),
  217    labeling([min(Expr) | Options], Vars).
 maximize(+Expr, +Term)
enumerate all solutions of the variables contained in Term in decreasing order of Expr.
  224maximize(Expr, Term):-
  225    term_attvars(Term, Vars),
  226    labeling([max(Expr), ff], Vars).
 maximize(+Expr, +Term, +Options)
same as maximize/2 using extra library(clpfd) labeling/2 options
  232maximize(Expr, Term, Options):-
  233    term_attvars(Term, Vars),
  234    labeling([max(Expr) | Options], Vars)