SICStus Prolog: FlatZinc Exported Predicates

10.48.2.1 Exported Predicates

The predicates described here operate on a data structure FznState representing a FlatZinc program and consisting of the following members:

A table that maps identifiers of the FlatZinc program to Prolog terms.
A list containing all domain variables of the FlatZinc program, except those with a var_is_introduced annotation.
A list containing all domain variables of the FlatZinc program that may be written on the current output stream.
A goal representing the constraint part of the FlatZinc program.
A goal representing the solve part of the FlatZinc program.
A counter denoting the number of solutions found by the FlatZinc program.

This data structure can be constructed from a FlatZinc program by the predicates fzn_load_stream/2 and fzn_load_file/2 described next, or directly from a MiniZinc program (see MiniZinc).

fzn_load_stream(+FznStream, -FznState)

FznStream is a FlatZinc input stream. FznState is a FlatZinc state that is initialized with respect to FznStream.

Exceptions: Exceptions regarding errors in FznStream (see Zinc Errors).

fzn_load_file(+FznFile, -FznState)

FznFile is a FlatZinc file (extension defaults to .fzn). FznState is a FlatZinc state that is initialized with respect to FznFile. This predicate is just a wrapper around fzn_load_stream/2 handling stream opening and closing.

Exceptions:

Exceptions related to the opening of FznFile for reading.
Exceptions regarding errors in FznFile (see Zinc Errors).

Consider the following FlatZinc program for solving the 4 Queens problem located in library('zinc/examples/queen4.fzn'). (Note that FlatZinc programs are not intended to be written (or read) by humans, but rather to be automatically generated. One method to generate FlatZinc programs is described in MiniZinc.)

% queen4.fzn

int: n = 4;

array[1 .. 4] of var 1 .. 4: q::output_array([ 1 .. 4 ]);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[2] ], 1);

constraint int_ne(q[1], q[2]);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[2] ], -1);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[3] ], 2);

constraint int_ne(q[1], q[3]);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[3] ], -2);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[4] ], 3);

constraint int_ne(q[1], q[4]);

constraint int_lin_ne([ 1, -1 ], [ q[1], q[4] ], -3);

constraint int_lin_ne([ 1, -1 ], [ q[2], q[3] ], 1);

constraint int_ne(q[2], q[3]);

constraint int_lin_ne([ 1, -1 ], [ q[2], q[3] ], -1);

constraint int_lin_ne([ 1, -1 ], [ q[2], q[4] ], 2);

constraint int_ne(q[2], q[4]);

constraint int_lin_ne([ 1, -1 ], [ q[2], q[4] ], -2);

constraint int_lin_ne([ 1, -1 ], [ q[3], q[4] ], 1);

constraint int_ne(q[3], q[4]);

constraint int_lin_ne([ 1, -1 ], [ q[3], q[4] ], -1);

solve satisfy;

A FlatZinc state Queen4State representing the program above can be constructed by typing:

| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State).

The predicates presented next are used to query an already initialized FlatZinc state.

fzn_post(+FznState)

Posts the constraints of the FlatZinc program represented by FznState. May fail if the constraints are inconsistent.

fzn_solve(+FznState)

Runs the solve and output parts of the FlatZinc program represented by FznState to find and display an (optimal) solution. Fails if the constraints of the FlatZinc program are inconsistent. Generates the next solution upon backtracking.

fzn_output(+FznState)

Outputs the values of the variables in FznState that have been annotated with output_var/0 or output_array/1.

Exceptions: An instatiation error if the output variables are not instantiated.

Consider again the FlatZinc program queen4.fzn described above and the following goal at the Prolog top level:

| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State),
     fzn_post(Queen4State),
     fzn_solve(Queen4State).

The first line initializes Queen4State with respect to queen4.fzn. The second and third line posts the constraints of queen4.fzn and runs the solve and output parts of queen4.fzn, respectively. The following is written on the current output stream:

q = array1d(1..4, [2, 4, 1, 3]);
----------

Upon backtracking the solve and output parts of Queen4State are rerun, which means that the following is written on the current output stream:

q = array1d(1..4, [3, 1, 4, 2]);
----------

fzn_identifier(+FznState, +Id, -Value)

FznState is a FlatZinc state initialized with respect to some FlatZinc program and Id is an identifier of the FlatZinc program. Unifies the FlatZinc value of Id with Value according to the following translation scheme:

A bool is translated into a Prolog integer: false is translated into 0 and true is translated into 1.
An int is translated into a Prolog integer.
A float is translated into a Prolog float.
An integer range or an integer set is translated into a library(clpfd) FD set term (see FD Set Operations).
A non-integer set is translated into a sorted Prolog list containing the (translated) elements of the set.
An array is translated into a Prolog list containing the (translated) elements of the array. Ordering is preserved such that the nth element of the array is the nth element of the list.
A var int is translated into a library(clpfd) domain variable (see CLPFD Interface).
A var bool is translated into a library(clpfd) domain variable with the domain 0..1 (see CLPFD Interface).

Exceptions: An existence error if Id is not an identifier of FznState.

fzn_objective(+FznState, -Objective)

FznState is a FlatZinc state initialized with respect to some FlatZinc program. Unifies Objective with a domain variable representing the FlatZinc objective.

Exceptions: An existence error if there is no objective in FznState.

A possible use of fzn_identifier/3 is to post additional library(clpfd) constraints or to apply a Prolog labeling predicate on the FlatZinc variables. For example, given the 4 Queens problem in queen4.fzn described above, the following goal labels the variables to find all solutions:

| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State),
     fzn_post(Queen4State),
     fzn_identifier(Queen4State, q, Q),
     findall(_, (labeling([], Q), fzn_output(Queen4State)), _).

Given this goal, the following is written on the current output stream:

q = array1d(1..4, [2, 4, 1, 3]);
----------
q = array1d(1..4, [3, 1, 4, 2]);
----------

To avoid symmetric solutions where the chess board is rotated 180 degrees, the following goal posts an additional symmetry breaking constraint on the first two queens:

| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State),
     fzn_post(Queen4State),
     fzn_identifier(Queen4State, q, Q),
     Q = [Q1, Q2|_], Q1 #< Q2,
     findall(_, (labeling([], Q), fzn_output(Queen4State)), _).

Given this goal, the following is written on the current output stream:

q = array1d(1..4, [2, 4, 1, 3]);
----------

Note that, now, only the first one of the previous two solutions is displayed.

The following two predicates can be used to run a FlatZinc program in one go. They both take as optional argument a list Options, which can be used to change the default behavior of the execution. This list may contain zero or more of the following:

search(Method) since release 4.3

where Method must be one of the atoms bab and restart. Tells the solver which optimization algorithm to use: branch-and-bound (the default), or to restart the search each time a new solution is found. The corresponding spfz option is -search Method.

solutions(NumberOfSolutions)

where NumberOfSolutions must be an integer greater than zero or the atom all. Describes the number of solutions to search for; the default is 1. The corresponding spfz options are -n N and -a.

output(File)

where File must be the name of a writable file. Causes any output written on the current output stream to be directed to File. The corresponding spfz option is -o File.

ozn_file(File) since release 4.2.3

where File must be the name of an existing file, containing the MiniZinc output commands that solns2out should use. If not given, then solns2out will not be used, and the solutions will be printed unformatted.

statistics(Boolean)

where Boolean must be true or false (default). The corresponding spfz option is -s. If true, the following statistics are written on the current output stream (see the built-in statistics/[0,2] and fd_statistics/[0,2] of library(clpfd) for more detailed information on their meaning):

runtime: Total running time (milliseconds), including parsing the FlatZinc program.
solvetime: Running time (milliseconds) for posting the constraints and performing the search.
solutions: The number of solutions found.
constraints: The number of constraints created.
backtracks: The number of times a contradiction was found by a domain being wiped out, or by a global constraint signalling failure.
prunings: The number of times a domain was pruned.

timeout(Time)

where Time should be an integer greater than zero. Stops the computation if it has not finished before Time milliseconds has elapsed. In any event, the best solution found so far is reported. The corresponding spfz option is -time Time.

fzn_run_stream(+FznStream)

fzn_run_stream(+FznStream, +Options)

FznStream is a FlatZinc input stream and Options is a list of options as described above. Performs the following steps:

Loads the FlatZinc program (fzn_load_stream/2), initializing a FlatZinc state.
Posts the constraints of the FlatZinc program (fzn_post/1).
Runs the solve part of the FlatZinc program (fzn_solve/1).
Outputs the values of the variables that have been annotated with output_var/0 or output_array/1.

The two final steps are repeated until the number of solutions as specified in Options have been found or until no more solutions can be found. At this point, if the whole search space have been explored, then ten consecutive equal signs are output on a separate line.

Exceptions:

A type error if the number of solutions to search for is not greater than zero nor the atom all.
Exceptions regarding errors in FznStream (see Zinc Errors).

fzn_run_file(+FznFile)

fzn_run_file(+FznFile, +Options)

FznFile is a FlatZinc program file (extension defaults to .fzn) and Options is a list of options as described above. This predicate is just a wrapper around fzn_run_stream/[1,2] handling stream opening and closing.

Exceptions:

Exceptions related to the opening of FznFile for reading.
A type error if the number of solutions to search for is not greater than zero nor the atom all.
Exceptions regarding errors in FznFile (see Zinc Errors).

The next predicate can be used to write the constraints of a FlatZinc program to a file, in the format of library(clpfd).

fzn_dump(+FznState, +File)

fzn_dump(+FznState, +Options, +File)

FznState is a FlatZinc state initialized with respect to some FlatZinc program and File is a writable file (extension defaults to .pl). Writes the constraints of FznState to File in the format of library(clpfd).

Options is a list containing zero or more of the following (currently, this is the only available option):

variables(ListOfVarDef): where ListOfVarDef is a list of elements of the form Id=Var where Id is a FlatZinc identifier and Var is a Prolog variable. Means that Var is unified with the value of Id after the FlatZinc program is loaded and that Id=Var is included in a list of arguments to query/1 that is written to File. Default is ListOfVarDef=[vars=Vars], with the meaning that Vars is a list containing all variables of the FlatZinc state, in the order they were introduced.

Exceptions: Exceptions related to the opening of File for writing.

Consider again the FlatZinc program queen4.fzn described above and the following goal at the Prolog top level:

| ?- fzn_load_file(library('zinc/examples/queen4'), Queen4State),
     fzn_dump(Queen4State, [variables([q=Q])], queen4).

The file queen4.pl then contains the following:

queen4.pl

:- use_module(library(clpfd)).

query([q=[A,B,C,D]]) :-
        true,
        domain([A,B,C,D], 1, 4),
        scalar_product([1,-1], [A,B], #\=, -1),
        scalar_product([1,-1], [A,B], #\=, 1),
        scalar_product([1,-1], [A,C], #\=, -2),
        scalar_product([1,-1], [A,C], #\=, 2),
        scalar_product([1,-1], [A,D], #\=, -3),
        scalar_product([1,-1], [A,D], #\=, 3),
        scalar_product([1,-1], [B,C], #\=, -1),
        scalar_product([1,-1], [B,C], #\=, 1),
        scalar_product([1,-1], [B,D], #\=, -2),
        scalar_product([1,-1], [B,D], #\=, 2),
        scalar_product([1,-1], [C,D], #\=, -1),
        scalar_product([1,-1], [C,D], #\=, 1),
        A#\=B,
        A#\=C,
        A#\=D,
        B#\=C,
        B#\=D,
        C#\=D.

Send feedback on this subject.