clp2zinc is a front-end to compile CLP specifications of search strategies into Zinc models. Zinc is a well-established language to describe CSP: MiniZinc should be installed to run the generated models. Moreover, dynamic search strategies (with indexicals) should be run with a patched solver.
clp2zinc command-line usage
clp2zinc is a command-line tool. The basic usage is
, which compiles the ClpZinc model clp2zinc file.plzfile.plz and generates the MiniZinc model file.mzn. clp2zinc recognizes a few options:
-g: this option traces the execution of the main goal on standard error. That is useful for debugging and seeing what happens.
This option does not affect the output file, which will still be generated identically. E.g., .clp2zinc -gfile.plz
-t: this option asks clp2zinc to produce an and-or tree instead of a MiniZinc model.
By default, the tree will be written in .inc in the tikz-qtree format. To include it in a TeX document:
\documentclass{article}
\usepackage{tikz,tikz-qtree}
\begin{document}
\begin{tikzpicture}
\input{file.inc}
\end{tikzpicture}
\end{document}
-o output file name: this option specifies the name for the generated file. E.g., orclp2zinc -o output.mznfile.plz
.clp2zinc -o tree.inc -tfile.plz
-I path: this option adds a search path for include items, see the include Items-O prefix: this option adds a prefix to the search paths for include items, see the include ItemsSeveral files can be compiled together: e.g.
, the result is identical as if the files were concatenated in a single file in the same order.
If the output file name is not specified with the clp2zinc file1.plz file2.plz...-o option, then the base name file1 is used, with the proper .mzn or .inc suffix.
Either use our build: choco-3.1.1-clpzinc.jar, or recompile it yourself:
choco3-choco-3.1.1/, run the following command: patch -s -p0 < choco-3.1.1-clpzinc.patch,choco3-choco-3.1.1/, run the following command: mvn package -DskipTests,.jar file is in choco3-choco-3.1.1/choco-parser/target/choco-parser-3.1.1-jar-with-dependencies.jar.
To solve a .mzn model:
mzn2fzn -I choco3-choco-3.1.1/choco-parser/src/chocofzn/globals/ file.mzn,java -jar choco-3.1.1-clpzinc.jar file.fzn | solns2out file.ozn.Either use our build: jacop-4.0.0-clpzinc.jar, or recompile it yourself:
git clone https://github.com/radsz/jacop.git,jacop/, run the following command: patch -s -p0 < jacop-4.0.0-clpzinc.patch,jacop/, run the following command: mvn install -DskipTests,.jar file is in jacop/target/jacop-4.0.0.jar.
To solve a .mzn model:
mzn2fzn -I jacop/src/main/minizinc/org/jacop/minizinc/mznlib/ file.mzn,java -cp jacop-4.0.0.jar org.jacop.fz.Fz2jacop file.fzn | solns2out file.ozn.Recompile it yourself:
svn checkout https://svn.gecode.org/svn/gecode/tags/release-4.2.1,release-4.2.1/, run the following command: patch -s -p0 < gecode-4.2.1-clpzinc.patch,gecode-4.2.1/, run the following command: ./configure && make,release-4.2.1/tools/flatzinc/fzn-gecode.
To solve a .mzn model:
mzn2fzn -I release-4.2.1/gecode/flatzinc/mznlib/ file.mzn,release-4.2.1/tools/flatzinc/fzn-gecode file.fzn | solns2out file.ozn.Install it with the patch:
sicstus4.2.3/ (typically in /usr/local/), run the following command: patch -s -p0 < sicstus-4.2.3-clpzinc.patch,
To solve a .mzn model:
sicstus,use_module(library(zinc)).mzn_run_file('file.plz').Recompile it yourself:
svn checkout http://or-tools.googlecode.com/svn/trunk/ or-tools,or-tools/, run the following command: patch -s -p0 < or-tools-clpzinc.patch,or-tools/, run the following command: make third_party bin/fz,or-tools/bin/fz.
To solve a .mzn model:
mzn2fzn -I or-tools/src/flatzinc/mznlib/ file.mzn,or-tools/bin/fz file.fzn | solns2out file.ozn.
ClpZinc extends the Zinc programming language by allowing the
item to be replaced by a CLP goal solve
.
There can be at most one goal item in a ClpZinc model, as there can be only one
:- goal.solve item in a Zinc model.
A ClpZinc goal is either:
A,B)
or the disjunction of two goals (A;B).Terms are either:
X, Y, Max, ...),p(t1,...,tn),(f1:t1,...,fn:tn) (or, alternatively, {f1:t1,...,fn:tn})
.field
(or, alternatively, record:field)forall (scope) (constraint) and exists (scope) (constraint)
where
f1, ..., and fn are field names (any valid identifiers)
t1, ..., and tn are terms.
Model variables are a special case of compound terms, either atomic (a, b, ...)
or array accessors (x[I,J]).
Lists are denoted [X1,...,Xn] ([] for the empty list)
and partial lists are denoted [X1,...,Xn | T].
Zinc arrays have been unified with Prolog-like lists to ease their
enumeration in search strategies.
CLP lists are mapped to Zinc arrays in code generation.
Zinc two-dimensional arrays have been unified with lists of lists.
Basic constraints are:
true: always true.false: always false (Prolog fail goal is therefore denoted false in ClpZinc). = Y: states that X equals Y. X and Y can be terms, numbers or model variables, and they can be mixed:
(A, B) = (C, D) is equivalent to A = C, B = D.The following constraints are only defined when X and Y are numbers (or arithmetic expressions, or model variables, but not terms).
!= Y: states that X and Y are different. <= Y: states that X is less than or equal to Y. > Y: states that X is strictly greater than Y. >= Y: states that X is greater than or equal to Y. < Y: states that X is strictly less than Y.The following pseudo-constraints are only tests, they do not change the current store.
== Y: tests whether X and Y are identical (if they contain model variables, they should refer to the same variable). \= Y: equivalent to \+ X == Y, i.e., the negation of the previous test.
Goals without pending constraints can be negated with the
negation-by-failure \+.
Note that MiniZinc pending constraints never fail at compile time when
they are not fully instantiated, therefore their negation will never succeed.
A comprehensive list of constraints is given in the MiniZinc specification. Every unknown predicate is assumed to be a constraint and is passed to MiniZinc, therefore all the constraints can be accessed, even solver-specific constraints.
CLP predicates can be defined with clauses:
a ClpZinc clause is an item of the form
where t1 and tn are terms
and goal is a ClpZinc goal. The goal part can be omitted:
p(t1,...,tn) :- goal.
is a shorthand for
p(t1,...,tn).
.
p(t1,...,tn) :- true.
include
Every
item is evaluated by ClpZinc by expanding it with the contents of the file include "file.plz";file
.
.plzinclude items that include files with any other suffix than
(typically, .plz.mzn) are left to MiniZinc.
Files are searched in the current directory and in the list of include directories,
in their order of appearance.
This list contains all the directories listed in the CLP2ZINCPATH environment variable if it exists (separated by
),
and ends with the :lib/ sub-directory in the directory where
the clp2zinc executable is located.
Search paths can be added on the top of this list with the
option.
-I path
Moreover, for every directory in this list, prefixes can be added with the
. By default, only the -O prefix
prefix is tried (the directory itself), but sub-directories can be added as prefix, for example to look in a sub-directory specific to a particular solver.
.
In CLP(X + H), arithmetic differs from Prolog.
Indeed, in accordance with the theory of CLP
and unlike most Prolog systems,
arithmetic is supposed to be contained in X and is distinguished from H terms,
e.g.,
is undistinguishable from 1 + 1
and is not a H term.
In ClpZinc,
the different forms of unification, equality, and evaluation predicates
that are encountered in Prolog systems (2=, #=, is, ...)
are thus all unified in a unique notion of equality, which is accessible either
explicitly with the predicate =, or implicitly when predicate arguments in either X of H are unified.
+ J: addition. - J: subtraction.- I: opposite. * J: multiplication. div J: division (either integer division if I and J are integers, floating-point division otherwise). rem J: modulo. / Y: floating-point division.log(B, X): logarithm of X in base B.ceil(X): smallest integer greater than X.floor(X): largest integer smaller than X.min(A, B): minimum between two values.max(A, B): maximum between two values.min([X1,...,Xn]): minimum of a list (distinguished from the indexical of the same name, if min is applied to a model integer variable rather than a list).max([X1,...,Xn]): maximum of a list (distinguished from the indexical of the same name, if max is applied to a model integer variable rather than a list).A comprehensive list of arithmetic operators is given in the MiniZinc specification. Every unknown term is treated as an Herbrand term and is printed as is in the MiniZinc generated model, therefore every MiniZinc function symbol can be used.
Arithmetic expressions are also extended for accessing
the indexicals of the model variables. For instance,
the goal M = min(X) assumes that X
is a model variable and unifies M with the
currently known lower-bound of X.
The available indexicals are:
min(X): returns the current lower-bound in the domain of X.max(X): returns the current upper-bound in the domain of X.card(X): returns the number of elements in the domain of X.dom_nth(X,N): returns the Nth element in the domain of X.
Some search strategies require to iterate a search tree several times with some kind of memory passed from one branch to another.
That is typically the case for optimization methods like branch-and-bound where the best score reached up to now is remembered
from one iteration to another of the underlying search strategy,
or for shaving, where one step of propagation is performed and undone in
order to select the best one.
In languages like Prolog, such methods are implemented with the help of some kind of global state, most commonly
stored within the fact database (with assert and retract).
The two additional annotations can be used in ClpZinc to handle global state.
store("global", [X1,...,Xn]): stores the current values of the sequence of variables [X1,...,Xn] into the global state identified as global.retrieve("global", [X1,...,Xn]): assigns the values previously remembered into the global state identified as global into the sequence of variables [X1,...,Xn].The search annotations of MiniZinc are accessible in goals in order to allow the composition of user-defined strategies with built-in ones. MiniZinc search annotations (except indexicals and accesses to global states) cannot appear under an unsolved choice-point.
int_search([X1,...,Xn], variable selector, value selector, search method):
defines a search step choosing between the variables X1,...,Xn according to
the variable selector (either input_order, first_fail, most_constrained, etc.)
using the value selector (either indomain_min, indomain_max, indomain_split, etc.).
Search method can be either complete or lds(N) when solvers support this annotation.
The three following pseudo-search annotations can appear at most once in the goal.
satisfy (default): tells the solver to look for any solution.minimize(N): tells the solver to find a solution that minimizes the value of the objective N.maximize(N): tells the solver to find a solution that maximizes the value of the objective N.The standard library is in the lib/ directory. It contains the following ClpZinc files:
dichotomic searchsearch strategy, bissecting over the domain of a variable.
interval splittingpartial search strategy.
limited discrepancy searchsearch strategy transformer, by meta-interpretation.
branch & boundoptimization procedure, for minimization or maximization.