=Paper=
{{Paper
|id=Vol-1648/paper4
|storemode=property
|title=Multiple-Origin-Multiple-Destination Path Finding with Minimal Arc Usage:
Complexity and Models
|pdfUrl=https://ceur-ws.org/Vol-1648/paper4.pdf
|volume=Vol-1648
|authors=Roman Bartak,Neng-Fa Zhou,Agostino Dovier
|dblpUrl=https://dblp.org/rec/conf/ijcai/BartakZD16
}}
==Multiple-Origin-Multiple-Destination Path Finding with Minimal Arc Usage:
Complexity and Models==
https://ceur-ws.org/Vol-1648/paper4.pdf
Multiple-Origin-Multiple-Destination Path Finding with Minimal Arc Usage:
Complexity and Models
Roman Barták Neng-Fa Zhou Agostino Dovier
Charles University in Prague CUNY Brooklyn College Università degli Studi di Udine
Prague, Czech Republic New York, U.S.A. Udine, Italy
Abstract The MOMD problem is also related to the road-
building/maintenance problem, which designs/maintains a
The multiple-origin-multiple-destination (MOMD) transportation network that satisfies connection requirements
problem is a simplified version of the logistics plan- with the minimum cost. There exist techniques for spe-
ning problem in which packages are required to be cial versions of the problem, for example, the multiple-
transported from their origins to their destinations origin-single-destination [10] (or the single-origin-multiple-
by multiple trucks with a minimum total cost. This destination, or the Steiner tree problem [3]), but we are un-
paper proves the NP-hardness of the problem, and aware of any studies of the general MOMD problem.
gives two SAT-based models for solving the prob- In this paper, we will formally define the multiple-origin-
lem optimally. It also gives experimental results multiple-destination problem and we will show that its deci-
that compare these two SAT models and ASP and sion variant is NP-complete. We will then propose an exact
CP models. method to solve the problem by modeling it as a SAT prob-
lem. In particular, we will present two models of the problem,
one based on flow constraints and the other based on reach-
Introduction ability constraints. The optimization variant of the problem
Given a weighted directed graph G = (V, E), where V is is then solved using the dichotomic branch-and-bound algo-
a set of vertices, and E is a set of arcs each of which has rithm. The paper is concluded by experimental comparison of
an associated weight, and a set of origin-destination pairs, the models using the Picat system [8].
the multiple-origin-multiple-destination (MOMD) problem
amounts to finding a subgraph G0 of the minimum total Problem Formulation and Complexity
weight that connects each origin-destination pair with a path. The multiple-origin-multiple-destination (MOMD) path find-
The resulting subgraph G0 is guaranteed to be cycle-free if the ing problem is formulated as follows. Assume a directed arc-
weights are all non-negative. The Floyd-Warshall algorithm weighted graph G = (V, E, w), where V is a set of ver-
[2] for finding shortest paths is not applicable to the MOMD tices, E is a set of directed arcs, and w : E → N is a
problem since it finds a shortest path for each of the pairs sep- mapping of arcs to non-negative weights. Let P be a set of
arately, and does not guarantee the minimality of the overall packages, such that each package p ∈ P is defined as a pair
cost since it does not take into account shared arcs. Tech- (orig(p), dest(p)), where orig(p) ∈ V is p’s original loca-
niques for solving closely-related cooperative path-finding tion and dest(p) ∈ V is p’s destination location. The task is
(CPF) problems [9] (also known as multi-agent path-finding to select a subset A ⊆ E of arcs such that for each package
problems) cannot be applied to MOMD due to a significance p there exists a directed path in the graph G0 = (V, A) from
difference in problem constraints. While the CPF problem re- orig(p)
P to dest(p) and the sum of weights of arcs in A (that
quires that two agents do not share the same link at the same is a∈A w(a)) is minimal.
time and usually the objective is minimizing makespan, the As mentioned in the Introduction, there exists a straight-
MOMD problem actually supports sharing the links as the forward method to solve the MOMD problem non-optimally.
objective is minimizing the total weight of used links. First, find the shortest path for each package, for example
The MOMD problem is a simplified version of the logics using an all-pairs-shortest-path algorithm such as the Floyd-
planning problem from the International Planning Competi- Warshall algorithm [2]. Let sp(p) be the set of arcs used by
tion 2014 [4], in which we can assume there are unlimited the shortest path for package p. Then define A as ∪p∈P sp(p).
number of trucks each with unlimited capacity for transport- Obviously, this method has a polynomial time complex-
ing a set of packages from their origins to their destinations. ity (the Floyd-Warshall algorithm has the time complexity
The optimal solution to the MOMD problem provides a lower O(|V |3 ) and there are even faster methods, for example, if the
bound for the original logistics problem and hence it can be graph is sparse or the number of packages is small then the
used for a better heuristic than the minimum-path heuristic Dijkstra’s algorithm is a better option). However, this method
used for the Transport problem. does no guarantee optimality as we will show in the section
with experimental results. In this paper we focus on solving (a) (b) (c)
the MOMD problem optimally; we are not aware about any
known method for the problem.
Let us first show that the MOMD problem is an NP-hard
problem. We will assume the decision variant of the prob-
lem, where the task is for any given number k to verify that z
P
a set A ⊆ E of arcs exists such that a∈A w(a) ≤ k and s x y x y x
for each package p there exists a directed path in the graph
G0 = (V, A) from orig(p) to dest(p). It is obvious that the s
decision variant of the MOMD problem belongs to the NP s
complexity class, because, given the set A, it is easy to verify
in polynomial time that A is indeed a solution to the MOMD
problem by finding a path for each package in the reduced Figure 1: Cycles in the solution to a MOMD problem.
graph G0 = (V, A).
The MOMD problem resembles the well known minimum
Steiner tree problem [3], which is one of Karp’s original 21 set T̂ of directed arcs such that there is a directed path in
NP-complete problems. We will use the following general T̂
P from s to each P vertex d ∈ S \ {s}. Moreover, it holds
version of the minimum Steiner tree problem. We are given a∈T̂ ŵ(a) = a∈T w(a) = k. Hence any Steiner tree T
an edge-weighted graph G = (V, E, w) and a subset S ⊆ V with cost k defines a solution T̂ of the MOMD with cost k.
of required vertices. A Steiner tree is a tree in G that spans Let us assume now that we have a set A ⊆ Ê of arcs with
all vertices of S. There are two variants of the problem: in the the total cost k such that A is a solution to the above MOMD
optimization problem, the task is to find a minimum-weight problem containing only the vertices reachable from s (arcs
Steiner tree; in the decision problem, we are given a value k leading to vertices that are not reachable from s can be re-
and the task is to decide if a Steiner tree of total weight at most moved from A while still having a solution of the MOMD
k exists. We shall show now that the Steiner tree problem can problem). Assume that A contains a directed cycle. If this cy-
be converted to the MOMD problem, which proves that the cle contains the vertex s (the vertex selected as the origin dur-
decision variant of the MOMD problem is an NP-complete ing the transformation) then there is also some arc (x, s) ∈ A
problem. in the cycle (see Figure 1(a)). We can remove the arc (x, s)
Theorem 1. The Steiner tree problem is reducible to the and the set A \ {(x, s)} is a solution to the MOMD problem
multiple-origin-multiple-destination problem in polynomial with a smaller cost (every vertex y ∈ S \ {s} is still reach-
time. able from s). If the cycle does not contain the vertex s then
the cycle contains a vertex y that is reachable from s with-
Proof. Let the Steiner tree problem be defined using the undi- out using any arc from the cycle (such vertex must exists as
rected edge-weighted graph G = (V, E, w) and the subset the cycle is reachable from s and s is not part of the cycle),
S ⊆ V of required vertices. For each non-directed edge see Figure 1(b). Let (x, y) ∈ A be the arc from the cycle
{a, b} ∈ E we introduce two directed arcs (a, b) and (b, a) going to y. Then we can remove (x, y) from A and all ver-
both with the same weight as the original undirected edge, tices in A (including y) still remain reachable from s so the
ŵ((a, b)) = ŵ((b, a)) = w({a, b}). So we define the set Ê set A \ {(x, y)} is a solution to the MOMD with a smaller
of arcs and mapping ŵ to weights as follows: cost. Assume now that A contains an undirected cycle (that
is not a directed cycle). It means that there is some vertex y
Ê = {(a, b) | {a, b} ∈ E}, ŵ((x, y)) = w({x, y}). such that there are arcs (x, y) ∈ A and (z, y) ∈ A in the cy-
cle. According to our assumption about A, both x and z are
Let s ∈ S be any vertex. Then we define the set P of packages reachable from s. Without loss of generality let z be reachable
as follows: from s by a path non-containing x. Then we can remove arc
P = {(s, d) | d ∈ S \ {s}}. (x, y) and all vertices in S including y will still be reachable
In other words, all packages are originated at some vertex from s.
s and their destinations are the other vertices from S (the We just showed that if there exists a solution A with the
case when S contains a single vertex is trivial). The MOMD cost k of the MOMD problem then it is possible to get a so-
problem then consists of the graph Ĝ = (V, Ê, ŵ) and the lution A0 with the cost at most k such that this solution does
set P of packages. Notice that we actually define a single- not contain any cycle (directed or undirected) and all vertices
origin-multiple-destinations problems, which is a special case used by arcs in A are reachable from s.
of MOMD. Obviously this MOMD problem is generated in Now, let us define the set of arcs T = {{a, b} | (a, b) ∈
the polynomial time from the Steiner tree problem. A0 }. As all the vertices from arcs in A0 are reachable and
Now, we shall show that any Steiner tree of the cost at there is no cycle in A0 then T must be a tree. Moreover
most k corresponds to a solution of the MOMD problem |T | = |A0 | because there is no pair of arcs (x, y)
Pand (y, x) in
with the cost at most k and vice versa. Assume that T is a A (they would form a directed cycle). Hence a∈T w(a) =
0
P
Steiner tree in G covering S. Then we can orient all edges in a∈A0 ŵ(a) ≤ k. Finally, because A is a solution of the
T in the direction away from s (start with the direct neigh- MOMD obtained from the original Steiner tree problem, all
bors of s and continue away from s). This way we get a vertices from S are included in some arc from A0 and hence
they are part of tree T . Therefore T is a solution to the origi- ∀a ∈ OutArcs(dest(p)) : Used [a, p] = 0
nal Steiner tree problem.
Flow [orig(p), p] = 1
In summary, the problem of finding a Steiner tree of cost
at most k can be solved by converting the undirected graph G Flow [dest(p), p] = 1
and the set S of vertices to a directed graph Ĝ and the set P X
∀x ∈ V \ {orig(p)} : Used [a, p] = Flow [x , p]
of packages, finding a solution of the corresponding MOMD
a∈InArcs(x )
problem with the cost at most k, and converting the solution
to the Steiner tree.
X
∀x ∈ V \ {dest(p)} : Used [a, p] = Flow [x , p]
Theorem 2. The decision variant of the multiple-origin- a∈OutArcs(x )
multiple-destination problem is an NP-complete problem. We use Boolean decision variables Used [a] to describe
whether or not a given arc a ∈ E is used by any package.
Proof. The problem of finding a solution of cost at most k of
This is modeled using the following constraint:
the MOMD problem belongs to NP. The NP-complete prob-
lem of finding a Steiner tree of cost at most k can be reduced max Used [a, p] = Used [a]
to the problem of finding a solution of cost at most k of the p∈P
MOMD problem. Hence, the decision variant of the MOMD The objective is then expressed using the constraint:
problem is NP-complete. X
Obj = Used [a] × w (a) (1)
SAT Models a∈E
We describe two constraint models for the MOMD problem where Obj is a variable describing the total cost of solution.
that can be used to find a solution with cost restricted by lower Notice that the size of the model depends on the number
and upper bounds. These models will then be used to find an of packages, vertices, and arcs so for sparse graphs the model
optimal solution using the dichotomic branch-and-bound al- is smaller than for dense graphs. More precisely, the number
gorithm. We will describe the constraint model using arith- of decision variables is nq + eq + e, where n = |V |, e =
metic constraints over Boolean variables and this model is |E|, q = |P | and all the decision variables are Boolean.
then translated to a SAT formula.
The Reachability Model
The Flow Model
The Flow model finds a path for each package explicitly. As
The MOMD problem requires that for each package there ex- some packages might share parts of their paths, it might be
ists a path from the package’s origin to the package’s desti- beneficial to find a path between vertices just once and then
nation. The Flow model describes a path separately for each for each package ensuring that a path exists. This idea is be-
package, accumulates all the arcs used by the packages, and hind our Reachability model that decides for any pair of ver-
restricts the total cost. tices if a path exists between them (using the selected arcs
Let G = (V, E, w) be a directed arc-weighted graph and P only). We will assume the same input G and P as described
be a set of packages. For each package p ∈ P and for each arc above.
a ∈ E we introduce a Boolean decision variable Used [a, p] We propose a model where for each pair of vertices the
that indicates whether or not arc a is used to transport pack- model describes whether or not a path exists between these
age p. For each package p ∈ P and for each vertex x ∈ V vertices. The model basically mimics the Floyd-Warshall
a Boolean variable Flow [x , p] indicates whether or not the algorithm [2]. Again, we use Boolean decision variables
transport of package p goes through the vertex x. Used [a] to indicate whether or not a given arc a ∈ E is se-
Let InArcs(x ) be the set of incoming arcs to x and lected in the solution. Assume that the vertices are indexed
OutArcs(x ) be the set of outgoing arcs from x. Formally, (totally ordered) by numbers from the set {1, 2, . . . , |V |}
(when using “the node x” we will mean its index). The
InArcs(x ) = {(y, x ) | (y, x ) ∈ E }, Boolean decision variables Reach[x , y, z ] describe whether
OutArcs(x ) = {(x , y) | (x , y) ∈ E } or not there exists a path from x to y using only vertices i
such that i ≤ z. In particular Reach[x, y, 0] says that an arc
To model a transport path for a package we specify the flow
from x to y exists and is used in the solution or x = y. The
preservation constraints. These constraints describe that each
variables are connected using the following constraints:
package must leave its origin and must arrive at its destina-
tion, and if the package goes through some vertex then it must
1 if x = y,
enter the vertex and leave it (both exactly once). In the case
∀x, y ∈ V : Reach[x, y, 0] = 0 if (x, y) ∈
/ E,
of origin, the package only leaves it and, similarly, in the case
Used [a] if a = (x, y) ∈ E.
of destination, the package only enters it. Formally, for each
package p ∈ P we introduce the following flow preserva-
tion constraints (recall that domains of all the variables are ∀x, y, z ∈ V :
Boolean, that is, {0, 1}):
Reach[x, y, z] = max(Reach[x, y, z − 1],
∀a ∈ InArcs(orig(p)) : Used [a, p] = 0 Reach[x, z, z − 1] × Reach[z, y, z − 1])
Now, for each package p we require that a path from constraints used in the models are translated to SAT:
orig(p) to dest(p) exists: max({X1 , X2 , . . . , Xn } = Y :
Y = 1 ⇒ X1 ∨ X2 ∨ · · · ∨ Xn
∀p ∈ P : Reach[orig(p), dest(p), |V |] = 1 Y = 0 ⇒ ¬X1 ∧ ¬X2 ∧ · · · ∧ ¬Xn
sum({X1 , X2 , . . . , Xn } = Y :
The objective function is expressed using the constraint (1) Y = 1 ⇒ exactly one({X1 , X2 , . . . , Xn })
as in the Flow model. Now, the number of Boolean decision Y = 0 ⇒ ¬X1 ∧ ¬X2 ∧ · · · ∧ ¬Xn
variables is (n + 1)n2 + e. Notice that the number does not exactly one({X1 , X2 , . . . , Xn }) ⇔
depend on the number of packages. at most one({X1 , X2 , . . . , Xn })∧
at least one({X1 , X2 , . . . , Xn })
Optimization Procedure The at most one constraint Σi Xi ≤ 1 is encoded into CNF
The constraint models specified in the previous section de- by using Chen’s algorithm [1], which splits the sequence of
scribe the decision variant of the MOMD problem – the value Boolean variables into two subsequences, and encodes the
k from the problem specification can be used as the upper sum Σni Xi as the Cartesian product of the two subsequences.
bound for the objective variable Obj using the constraint The objective constraint is broken down to primitive con-
Obj ≤ k. To solve the minimization problem, we use the straints, which are encoded as adders and multipliers.
dichotomic version of the branch-and-bound algorithm [5],
where the lower and upper bounds are moving closer to each ASP Model
other by splitting the interval between them into halves until We have encoded the MOMD problem in Answer Set Pro-
the bounds become equal. Let Bound− be the known lower gramming (ASP). As usual in ASP the coding is very con-
bound of the objective function and Bound+ be the known cise and, basically, based on a generate & test programming
upper bound of the objective function. Then the dichotomic scheme. Assume the input graph is encoded by a predicate
branch-and-bound algorithm works as follows. It finds a mid- road/3 where road(a, b, w) denotes that the arc (a, b) has
dle value Bound between Bound− and Bound+ and tries to cost w. Each origin/destination (o/d) pair is imposed by a bi-
find a solution better or equal to Bound. If no solution exists nary predicate trip. We can define the predicate node by
then the lower bound is increased to Bound + 1. If a solution projection. Then, using a choice rule we can either select an
is found then the upper bound is decreased to Bound. This edge or not. Reachability is computed on the subgraph of the
process is repeated until Bound− = Bound+ . The pseu- selected nodes, and a constraint is added to force the connec-
docode is shown in Algorithm 1. tivity between all o/d pairs. Finally, the cost optimization is
imposed.
node(A) :- road(A,_,_).
repeat node(B) :- road(_,B,_).
Bound ← round((Bound+ + Bound− )/2)
Sol ← Solve(Cons ∪ {Obj ≤ Bound} {selected(A,B,C)} :- road(A,B,C).
if Sol=fail then
Bound− ← Bound + 1 reach(A,A) :- node(A).
else reach(A,B) :- selected(A,C,_), reach(C,B).
Bound+ ← Bound
:- trip(Origin,Destination),
end
not reach(Origin,Destination).
until Bound− = Bound+ ; cost(Cost) :- Cost = #sum{C,A,B : selected(A,B,C)}.
Algorithm 1: A dichotomic version of branch-and- #minimize {C:cost(C)}.
bound. Minimum path for each o/d pair in the complete graph can be
modeled with few lines of code in order to compute bounds
We calculated the initial bounds as follows. The lower that can be used in the successive search. The obtained code
bound is the maximum from the costs of shortest paths for however suffers from huge grounding and the running time is
all the packages. Obviously, no better solution exists as for (slightly) better than the one of the above code only in few
each package we need to go from its origin to its destination. instances.
The upper bound is the cost of the straightforward solution
– the shortest (cost optimal) path is found for each package MiniZinc Model
and the solution is defined as all the arcs in the union of these We have also tested a similar, highly non-deterministic, en-
shortest paths. coding in MiniZinc [6]. Basically, for each o/d pair (assume
there are p of them) we introduce an array path[i] where
Translation to SAT i = 1, . . . , p aimed at storing the path using selected edges.
These arrays have length n (number of nodes). path[i, j] is
The proposed models are translated to SAT formulas. We use the j-th node found in the path that leads the i-th origin to the
the Picat SAT compiler, which employs hybrid encodings for i-th destination. When the destination d is reached, all succes-
constraints [11]. The following summarizes how the Boolean sive values of the vector are d. No other “loops” are possible.
We found also convenient to use an auxiliary successor MHz DDR3 RAM. For this comparison we used the instances
predicate that allows to restrict the domain of the next ele- of the Transport domain from the optimal track of the Inter-
ment of the path. national Planning Competition 2014 [4]. Table 1 gives char-
% domain for the successor (for the path p) acteristics, including the lower bound, the upper bound, and
constraint the optimal solution, of each of the instances.
forall (i in 1..nodes, p in 1..pairs, Table 1 also shows the runtimes (in seconds) for both SAT
j in 1..nodes where i != trip[p,2]) models to find and proof optimal solutions. The Flow model
(graph[i,j]=0 -> successor[p,i] != j); is clearly faster on all the benchmark instances. This is prob-
ably due to the fact that the Flow model uses fewer decision
% the target has no successor (self-loop) variables than the Reachability model for the instances.
constraint
forall (p in 1..pairs) We also developed models in ASP and MiniZinc for the
(successor[p,trip[p,2]]=trip[p,2]); problem, both of which use reachability constraints. The
clingo solver [7] with the default setting found optimal so-
% Every path starts from the source lutions for 19 of the 20 instances, 12 of which were found
constraint within 1 minute each, but took considerably more time than
forall (p in 1..pairs) our models on the solved instances, and failed to solve in-
(path[p, 1] = trip[p, 1]); stance p17 within 24 hours. Although both ASP model and
our SAT models use SAT, our models are significantly more
% the target is eventually reached efficient than ASP because of the compact and efficient en-
constraint
codings used for the constraints.
forall (p in 1..pairs)
(path[p,nodes]=trip[p,2]); We also compared our models with a model implemented
in MiniZinc [6], which uses constraints to prevent cycles.
% Check/Force that the path is feasible This model, when run by Gecode, solved 10 of the 20 in-
% (use successor) stances, 7 of which were solved within 1 minute each, but
constraint failed to solve 10 of the instances under the time limit of 24
forall (p in 1..pairs, i in 2..nodes) hours per instance. This comparison once again demonstrates
(path[p, i] = successor[p, path[p,i-1]]); the effectiveness of the SAT models for the problem.
% No self-loops during search
constraint Conclusions
forall (p in 1..pairs, i in 1..nodes - 1)
(path[p,i+1] = path[p,i] -> The paper proposes a path finding problem called multiple-
path[p,i] = trip[p,2]); origin-multiple-destination (MOMD) problem, where the ob-
jective is minimizing the total cost of used arcs. This prob-
% Connection between selected and path
lem is motivated by transportation and network problems
constraint
forall (p in 1..pairs, i in 2..nodes) where the variation between paths should be minimized. We
(path[p, i] > 0 -> showed that this problem is NP-complete, and proposed two
selected[path[p, i - 1], path[p, i]]); SAT-based models to solve the problem optimally. The model
based on flow-preserving constraints seems computationally
% Cost more efficient than the model based on reachability con-
constraint straints. The initial experiments also showed that the SAT
cost = sum (i in 1..nodes, j in 1..nodes)( model is more efficient than the CP and ASP models.
selected[i, j] * graph[i, j] There are several open problems to be resolved. First, it
);
would be interesting to compare both SAT models using prob-
The running times are very unsatisfactory. We experimen- lems with different numbers of packages, in particular be-
tally found the best results with this program designed search cause the number of decision variables in the Flow model
heuristics depends on the number of packages while the number of vari-
solve::int_search([path[p, i]| p in 1..pairs, ables in the Reachability model is independent of the number
i in 1..nodes], of packages. Second, it would be interesting to study better
first_fail, indomain_min, complete) lower bounds for the objective function, in particular in rela-
minimize cost; tion to the original motivation of computing better heuristic
estimates for the Transport problem. Third, it would be inter-
Experimental Evaluation esting to compare efficiency of the SAT solvers with state-of-
We have implemented the SAT models in Picat [8], which the-art MIP solvers, in particular for the Flow model that uses
employs Lingeling as the SAT solver. In Picat, it is also pos- linear constraints.
sible to use CP and MIP solvers for the same models, but
the SAT solver overwhelmingly outperforms the CP and MIP Acknowledgments.
solvers for these models. We used Picat 1.9b1 running with Roman Barták is supported by the Czech Science Foundation
MacOS X 10.11.4 on 1.7GHz Intel Core I7 with 8GB 1600 under the project P103-15-19877S.
Table 1: Problem instances and solution times (proof of optimality).
Problem characteristics Runtime in seconds
instance #vertices #arcs #packs lb ub opt Flow model Reach model
p01 5 12 3 58 122 122 0.096 0.183
p02 10 34 4 90 189 162 0.395 0.669
p03 12 40 5 122 235 234 0.568 1.402
p04 15 44 5 86 197 197 0.599 1.913
p05 18 70 6 130 408 284 6.868 6.980
p06 20 62 6 134 408 355 1.330 5.013
p07 10 24 3 307 367 352 0.285 0.554
p08 20 62 4 339 391 362 0.697 2.271
p09 24 84 5 316 440 384 1.366 5.913
p10 30 94 5 334 510 507 2.093 7.101
p11 36 144 6 294 539 529 21.283 30.676
p12 40 138 6 376 603 558 5.634 18.663
p13 15 40 4 263 499 491 0.673 2.642
p14 30 98 4 288 376 376 3.796 7.252
p15 36 124 5 278 693 646 4.159 17.145
p16 45 148 5 310 841 688 4.159 18.554
p17 54 204 6 318 1153 832 31.884 47.948
p18 60 222 6 356 902 890 15.922 46.539
p19 60 222 7 373 966 911 22.287 56.813
p20 60 222 7 373 966 911 22.212 46.377
References [11] Zhou N.-F., Kjellerstrand H.: The Picat-SAT Com-
[1] Chen J.: A new SAT encoding of the at-most-one con- piler. Practical Aspects of Declarative Languages, LNCS
straint. Proc. of the 9th Int. Workshop of Constraint Mod- 9585, pp. 48–62 , 2016.
eling and Reformulation, 2010.
[2] Floyd R. W.: Algorithm 97: Shortest Path. Communica-
tions of the ACM 5 (6): 345, 1962.
[3] Garey M. R.; Johnson D. S.: Computers and Intractabil-
ity: A Guide to the Theory of NP-Completeness, W. H.
Freeman, 1979.
[4] International Planing Competions web site,
http://ipc.icaps-conference.org/, Accessed March
24, 2016.
[5] Land A. H. and Doig A. G.: An automatic method of
solving discrete programming problems. Econometrica
28(3): 497–520, 1960.
[6] MiniZinc web site, http://www.minizinc.org, Accessed
April 22, 2016.
[7] Potassco, the Potsdam Answer Set Solving Collection
web site, http://potassco.sourceforge.net, Accessed April
22, 2016.
[8] Picat web site, http://picat-lang.org/, Accessed March
24, 2016.
[9] Surynek P.: Compact Representations of Cooperative
Path-Finding as SAT Based on Matchings in Bipartite
Graphs, Proceedings of the 26th International Confer-
ence on Tools with Artificial Intelligence (ICTAI 2014),
IEEE, pp. 875–882, 2014.
[10] Thomas R. S. D. and Wells J. M.: Multiple-Origin
Single-Destination Transit Routing. Interfaces 10(2):41–
43, 1980.