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) ;
...