Did you know ... Search Documentation:
Pack modeling -- README.md

Modeling pack

MiniZinc-inspired mathematical modeling metapredicates in Prolog.

This pack defines Prolog predicates in the spirit of the MiniZinc modeling language (https://www.minizinc.org/) for shorthand functional notations, subscripted variables with arrays, set comprehension, quantifiers, aggregates, hybrid constraints, combined with

  • the full programming capabilities of Prolog for programming search, tracing and visualizing the search tree, and interfacing with external components;
  • the answer constraint semantics of Prolog for computing non-ground symbolic solutions to constraint satisfaction problems;
  • plus soon coming a MiniZinc parser.

The pack includes libraries shorthand.pl, comprehension.pl, arrays.pl, clp.pl, modeling.pl, drawtree.pl, tracesearch.pl and a benchmark file of examples showing the absence of significant overhead with respect to classical Prolog programs with lists and recursion, see

  • Francois Fages. A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics. In 17th International Symposium on Functional and Logic Programming, FLOPS 2024, volume 14659 of LNCS. Springer-Verlag, 2024. [ preprint https://inria.hal.science/hal-04478132 ]

Install

swipl pack install modeling

or under Prolog

?- pack_install(modeling).

Example of constraint-based model defined on subscripted variables by set comprehension

The N-queens puzzle for placing N queens on a NxN chessboard such that they do not attack each other (i.e. they are not on same column, row or diagonal), which is classically solved by a recursive program on lists, can be modeled in this library using

  • an array Queens with functional notation for subscripted variables Queens[I],
  • bounded quantifier for_all with definition of the variables by list comprehension using in and where conditions,
  • let bindings using shorthand notations for arrays and conditional expressions, as follows:
    :- use_module(library(modeling)).
    
    queens(N, Queens):-
      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).
    
    show(Queens):-
        array(Queens, [N]),
        for_all([I, J] in 1..N,
                let([Q = if(Queens[J] = I, 'Q', '.'),
                     B = if(J = N, '\n', ' ')],
                    format("~w~w",[Q,B]))).
    
    ?- queens(N, Queens), show(Queens).
    Q
    N = 1,
    Queens = array(1) ;
    . . Q .
    Q . . .
    . . . Q
    . Q . .
    N = 4,
    Queens = array(2, 4, 1, 3) ;
    . Q . .
    . . . Q
    Q . . .
    . . Q .
    N = 4,
    Queens = array(3, 1, 4, 2) ;
    Q . . . .
    . . . Q .
    . Q . . .
    . . . . Q
    . . Q . .
    N = 5,
    Queens = array(1, 3, 5, 2, 4) .

Main features

Library shorthand.pl defines

  • a general purpose user-definable shorthand/3 metapredicate to define shorthand functional notations usable with expand/1, expand/2, evaluate/2 predicates,
  • used there to define a conditional expression if(Condition, Expression1, Expression2)
  • suggested to use in expressions for predicates where one argument can be interpreted as a result, or for allowing global variables directly in expressions.

Library comprehension.pl defines

  • for_all/2 bounded quantifier defined by set comprehension for constraining context variables (unlike ISO Prolog forall/2, see below)
  • let/2 metapredicate for binding existential variables to expressions with shorthand functional notation,
  • a general purpose aggregate_for/6 metapredicate to constrain elements defined by comprehension by iteration (not backtracking), with expansion of shorthands in domains and conditions,
  • used in clp.pl to define new global constraints.
?- L=[A, B, C], for_all(X in L, X=1). % constraint posted on all elements
L = [1, 1, 1],
A = B, B = C, C = 1.

?- L=[A, B, C], forall(member(X, L), X=1). % satisfiability test for all elements
L = [A, B, C].

Library arrays.pl provides an implementation of arrays in Prolog

  • with Array[Indices] functional notation defined by shorthand/3.

Library clp.pl is a front-end to libraries clpfd and clpr allowing

  • shorthand notations in domains and constraints,
  • hybrid clpfd-clpr constraints on list and array arguments, plus some new clpfd global constraints,
  • reification of clpfd-clpr constraints with a clpfd Boolean using truth_value/2 predicate or truth_value/1 function in expressions,
  • shorthand functional notations for constraints in which the last argument can be interpreted as a result, e.g. sum/2 function using sum/3 constraint
  • option trace added to labeling/2 predicate to visualize the search tree.

Library tracesearch.pl defines predicates for creating a search tree term, e.g. option trace added to labeling/3.

Library drawtree.pl defines predicates for drawing terms, in particular search trees, in various forms including LaTeX tikz.

Library modeling.pl adds predicates for bool_array/2, int_array/3, float_array/3, satisfy/1, minimize/1.

Reification for clpr and clpfd constraints

Constraints of library(clpr) can be reified (checking variable instanciation rather than constraint entailment) with predicate truth_value/2 predicate 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.

Together with shorthand functional notation for truth_value/2, this can be employed to solve the magic series puzzle by a direct transcription of the mathematical definition of magic series:

i.e. series of integers (X1,...,XN) satisfying for all i in 1..N, Xi = | { Xj = i-1 | j in 1..N} |

magic_series(N, X):-
    array(X, [N]),
    for_all(I in 1..N,
            X[I] #= int_sum(J in 1..N,
                            truth_value(X[J] #= I-1))),
    satisfy(X).

?- magic_series(N, X).
N = 4,
X = array(1, 2, 1, 0) ;
N = 4,
X = array(2, 0, 2, 0) ;
N = 5,
X = array(2, 1, 2, 0, 0) ;
N = 7,
X = array(3, 2, 1, 1, 0, 0, 0) ;
N = 8,
X = array(4, 2, 1, 0, 1, 0, 0, 0) ;
N = 9,
X = array(5, 2, 1, 0, 0, 1, 0, 0, 0) ;
N = 10,
X = array(6, 2, 1, 0, 0, 0, 1, 0, 0, 0) ;
...